3 ms·
Yup! Lean is based on a variant of the Calculus of Constructions, which is in turn based on strong connections between (intuitionistic) natural deduction and ty
by rck 2y ago
Yup! Lean is based on a variant of the Calculus of Constructions, which is in turn based on strong connections between (intuitionistic) natural deduction and type theory. The connection is incredibly beautiful:
https://en.wikipedia.org/wiki/Calculus_of_constructions https://en.wikipedia.org/wiki/Calculus_of_constructions
- hoping1 2y agoAh heck, I should have added a section on PTSs, maybe I still will or maybe that will be standalone later. It really is gorgeous stuff!!