How to check definitional equality?

Stream: new members

[Thomas Brooks]

Is there an simple way in Lean to check if two expressions are definitionally equal? I'm trying to check my understanding of what is definitionally equal in Lean and am not sure how to do this (I'm probably overlooking something very simple).

[Riccardo Brasca]

You can just check if example foo = bar := rfl works

[Thomas Brooks]

What am I doing wrong when I try something trivial like example (Prop = Prop) := rfl I get several errors:

exercises.lean:4:8
don't know how to synthesize placeholder
context:
⊢ Sort ?
exercises.lean:4:9
invalid binder, identifier expected
exercises.lean:4:9
command expected

[Mario Carneiro]

use triple backtick for multiline code blocks

[Riccardo Brasca]

First of all I forgot the : in my example, sorry.

[Mario Carneiro]

you are missing a colon: example: (Prop = Prop) := rfl

[Riccardo Brasca]

Then refl is a tactic, you should use rfl (without the e).

[Thomas Brooks]

Okay thank you, that has fixed it! Oddly, I am using triple-backticking in my message but it still displays incorrectly.

[Mario Carneiro]

the triple backtick has to be on its own line (both the beginning and the end one)

[Riccardo Brasca]

And pay attention that you are proving equality of types, that is something a little odd (even if in this case it works). If you want to try something mathematically meaningful you can prove 1+1=2.

[Thomas Brooks]

Yes, I was trying the most trivial statement I could think of since I was getting errors on more meaningful propositions too (due to these mistakes). @Mario Carneiro Even on separate lines for both, it doesn't seem to display properly. (By the way, I find your Type Theory of Lean paper very helpful.)

[Mario Carneiro]

there is a space before the first triple-backtick

[Thomas Brooks]

Oops. Not my day for noticing trivial errors. Thanks