Jon Eugster
|
6970f10e30
|
Merge pull request #116 from leanprover-community/eugster/level-error-msg
fix: show error on duplicated level number
|
3 years ago |
Jon
|
6e046d72b6
|
show error on duplicated level number
|
3 years ago |
Alexander Bentkamp
|
5c919fb983
|
Add NewHiddenTactic command
Fixes #109
|
3 years ago |
|
Jon Eugster
|
6371f77379
|
satisfy unused variable linter
|
3 years ago |
|
Jon Eugster
|
73b80e714d
|
improve welcome page
|
3 years ago |
|
Jon Eugster
|
b6ea453084
|
add Template server-side
|
3 years ago |
|
Alexander Bentkamp
|
df8fa2933b
|
record used inventory
|
3 years ago |
|
Jon Eugster
|
047d75e74d
|
add function to retrieve tactic docstring
|
3 years ago |
|
Jon Eugster
|
3bf5c5e5e8
|
rename and tidy up
|
3 years ago |
|
Jon Eugster
|
fbf0f55968
|
reorganisational draft
|
3 years ago |
|
Jon Eugster
|
60876b4a77
|
move Doc class
|
3 years ago |
|
Jon Eugster
|
d753d1d873
|
docstrings
|
3 years ago |
|
Jon Eugster
|
1b0e4a6a81
|
make command optional
|
3 years ago |
|
Jon Eugster
|
13233710e9
|
modified inventory doc requirement
|
3 years ago |
|
Jon Eugster
|
ebcc1df171
|
add syntax for attr in statements; add new key to computed inventory items.
|
3 years ago |
|
Jon Eugster
|
8246ae6eac
|
change folder structure
|
3 years ago |
|
Alexander Bentkamp
|
732754c9fc
|
rework build process
|
4 years ago |
|
Alexander Bentkamp
|
d6bd2c98da
|
split off test game
still need to adapt the call to the lean binary to provide two arguments
|
4 years ago |