search

dselsam / binport

A tool for building Lean4 .olean files from Lean3 export data
Apache License 2.0
10 stars 1 forks source link

Well-founded rfl-proofs even less likely to work in MetaM #20

Open dselsam opened 3 years ago

dselsam commented 3 years ago

See discussion on zulip: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathport.3Awhnf-power/near/231172023

Mario suggested backporting well-founded non-rfl proofs to lean3.