4 ms·
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 the
by Someody42 5y ago
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
- foooobar 5y agoSome constructivists may also take offense with proof irrelevance (and the resulting loss of normalization [1] or its incompatibility with HoTT), which you can only really avoid by avoiding Prop. [1] https://arxiv.org/abs/1911.08174 https://arxiv.org/abs/1911.08174
- xvilka 5y agoThere is also a problem of HoTT and equality reflection incompatibility[1]. [1] https://www2.mathematik.tu-darmstadt.de/~streicher/barc_corr.pdf https://www2.mathematik.tu-darmstadt.de/~streicher/barc_corr...