Reservoir

WinstonHartnett/lean-club

None Description

GitHub Link Documentation

Pick a version!

TODO: should show a time axes that allows the users to view, filter and click copy the lakefile config.

README

Lean

Be sure Nat_ as the type and not Nat

It seems unnecessary to use a package manager like lake, but it was the only way I could get the imports to work properly. The package name is "Arithmetic" so there is the Arithmetic.lean file in the base directory and then all other files should go in the "Arithmetic" folder and be imported with import Arithmetic.. The command lake build builds the package.