prod is needed for some automatically generated constructions. So, it is important it is loaded in the environment as early as possible. |
||
---|---|---|
.. | ||
decl.lean | ||
default.lean | ||
thms.lean |
prod is needed for some automatically generated constructions. So, it is important it is loaded in the environment as early as possible. |
||
---|---|---|
.. | ||
decl.lean | ||
default.lean | ||
thms.lean |