mgrabovs/lean3-community

Lean is at the same time a modern interactive theorem prover/proof assistant for higher-order intuitionistic logic and a dependently typed purely functional programming language.


This is a companion discussion topic for the original entry at https://copr.fedorainfracloud.org/coprs/mgrabovs/lean3-community/