pull/68/head
Jon Eugster 3 years ago
parent e93e480f27
commit c2b298e650

@ -326,6 +326,11 @@ Arguments:
-/ -/
elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
-- Check that the statement name is a lemma in the doc
match statementName with
| some name => checkInventoryDoc .Lemma name.getId
| none => pure Unit.unit
let lvlIdx ← getCurLevelIdx let lvlIdx ← getCurLevelIdx
let defaultDeclName : Name := (← getCurGame).name ++ (← getCurWorld).name ++ let defaultDeclName : Name := (← getCurGame).name ++ (← getCurWorld).name ++
("level" ++ toString lvlIdx : String) ("level" ++ toString lvlIdx : String)

Loading…
Cancel
Save