Someody42·il y a 5 ans·discussYou 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
Someody42·il y a 5 ans·discussIn 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.- we don't only want to port the theorem. We want to port them to a human-readable proof that can be easily maintained