issues
search
leanprover-community
/
lean4-metaprogramming-book
https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
204
stars
47
forks
source link
Two minor lakefile tweaks
#108
Closed
Julian
closed
1 year ago
Julian
commented
1 year ago
Remove
isLeanOnly
which is deprecated in newer Lean and will emit a warning
Use
python3
not
python
as the executable we look for, as the latter is / should be a Py2 interpreter
isLeanOnlywhich is deprecated in newer Lean and will emit a warningpython3notpythonas the executable we look for, as the latter is / should be a Py2 interpreter