phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

update doc #171

Browse Source
This commit is contained in:
Jon Eugster
2023-12-15 00:04:54 +01:00
parent 5f52e23f29
commit c4f4dbdc6b
1 changed files with 6 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
doc/create_game.md
+5
View File
@@ -129,6 +129,9 @@ NewLemma Nat.zero_mul
NewDefinition Pow
```
**Important:** All commands in this section 6a) expect the `Name` they take as input
to be **fully qualified**. For example `NewLemma Nat.zero_mul` and not `NewLemma zero_mul`.
#### Doc entries
You'll see a warning about a missing Lemma documentation. You can fix it by adding doc-entries like the following somewhere above it.
@@ -182,6 +185,8 @@ The statement is the exercise of the level. the basics work the same as they wou
You can give your exercise a name: `Statement my_first_exercise (n : Nat) ...`. If you do so, it will be added to the inventory and be available in future levels.
You can but a `Statement` inside namespaces like you would with `theorem`.
#### Doc String / Exercise statement
Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. It supports Latex.