Y
HN Search
Hacker News Search
new
|
comments
|
top
|
jobs
Someody42
searching PlanetScale…
1.
▲
2.
▲
3.
▲
4.
▲
5.
▲
6.
▲
3 ms
·
1.
▲
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
2.
▲
by
Someody42
5y ago
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. - we don't onl