Evidences

Stream: new members

[Artem Storozhuk]

Let's consider two following theorems:

def theorem1 : 2 + 3 = 5 := rfl
def theorem2 : 2 + 3 = 5 := by decide

so both rfl and by decide can generate evidences for us in this context

At the same:

def theorem3 : 5 < 18 := by decide

will work, but using rfl here will not. If rfl has a bit more limitation, can't I use by decide all the time, since it is more powerful? Or rfl has some use cases when by decide is not relevant?

I also encountered by simp evidence generation. Where can I read more about those different notions?
Thanks!

[Kenny Lau]

rfl proves a = a, or more precisely, [expr 1] = [expr 2] where both expressions can be definitionally reduced to the same form