Viewing profile — Someody42

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 w…

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 red…