Commit 2022-09-30 18:23 fdd0ff17

View on Github →

feat: Extend rfl tactic to use refl attribute. (#436) This extends the rfl tactic in Lean 4 to use refl attribute.

Estimated changes

added def Foo.le
added theorem Foo.le_refl
added structure Foo
added def iseqv_refl