Thorsten Altenkirch (Sep 27 2020 at 14:10):
I gave a talk with live proofs in our fp lunch meeting last Friday using lean for the first time:
Sorry for the low level of automatisation but this is the style I am also using in my lecture. The main story is that you don't need to assume EM as an axiom but there is also some discussion about lean...
Pedro Minicz (Sep 27 2020 at 17:47):
Very interesting! This remembers me of the "stable propositions" exercise at the end of the negation chapter of Programming Language Foundations in Agda. Coincidentally, I have redone the exercise in Lean around a week ago (you can see it here).
Junyan Xu (Sep 28 2020 at 05:12):
Coincidentally I also did some similar exercises regarding stable propositions (which corresponds to regular elements in Heyting algebras): https://gist.github.com/alreadydone/7474d5000c912194d794d06192e84f1e#file-choice_and_excluded_middle-lean-L557
Basically I formalized https://en.wikipedia.org/wiki/Heyting_algebra#The_De_Morgan_laws_in_a_Heyting_algebra in Lean.
Last updated: May 12 2021 at 05:19 UTC