You can absolutely do constructive things in Lean, as long as you use neither the built-in "quot" type nor the three other axioms described in the docs, and then you get a system with all the desired properties I think
In theory yes, but there are two main things that makes it harder : - some technical details have changed. They don't affect the axiomatic aspects of Lean, but they force us to redefine some things in a cleaner way. -…
You can absolutely do constructive things in Lean, as long as you use neither the built-in "quot" type nor the three other axioms described in the docs, and then you get a system with all the desired properties I think
In theory yes, but there are two main things that makes it harder : - some technical details have changed. They don't affect the axiomatic aspects of Lean, but they force us to redefine some things in a cleaner way. -…