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

cleanup

Browse Source
This commit is contained in:
Jon Eugster
2024-06-18 16:00:42 +02:00
parent 67090f53fa
commit 5310e69d98
1 changed files with 7 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/GameServer/Commands.lean
+7 -8
View File
@@ -352,11 +352,10 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
collectUsedInventory proof collectUsedInventory proof
| _ => throwError "expected `:=`" | _ => throwError "expected `:=`"
-- extract the `tacticSeq` from `val` in order to add `let_intros` in front. -- modify the proof to start with `let_intros` and any specified preamble sequence.
-- TODO: don't understand meta-programming enough to avoid having `let_intros` let modifiedVal ← match val with
-- duplicated three times below… | `(Parser.Command.declVal| := by $proof) =>
let tacticStx : TSyntax `Lean.Parser.Tactic.tacticSeq := match val with `(Parser.Command.declVal| := by {let_intros; $(⟨preambleSeq⟩); $(⟨proof⟩)})
| `(Parser.Command.declVal| := by $proof) => proof
| _ => panic "expected `:= by`" | _ => panic "expected `:= by`"
-- Add theorem to context. -- Add theorem to context.
@@ -372,17 +371,17 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
-- in that case. -- in that case.
logWarningAt name (m!"Environment already contains {fullName}! Only the existing " ++ logWarningAt name (m!"Environment already contains {fullName}! Only the existing " ++
m!"statement will be available in later levels:\n\n{origType}") m!"statement will be available in later levels:\n\n{origType}")
let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨preambleSeq⟩); $(⟨tacticStx⟩)}) let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $modifiedVal)
elabCommand thmStatement elabCommand thmStatement
-- Check that statement has a docs entry. -- Check that statement has a docs entry.
checkInventoryDoc .Theorem name (name := fullName) (template := docContent) checkInventoryDoc .Theorem name (name := fullName) (template := docContent)
else else
let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig := by {let_intros; $(⟨preambleSeq⟩); $(⟨tacticStx⟩)}) let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig $modifiedVal)
elabCommand thmStatement elabCommand thmStatement
-- Check that statement has a docs entry. -- Check that statement has a docs entry.
checkInventoryDoc .Theorem name (name := fullName) (template := docContent) checkInventoryDoc .Theorem name (name := fullName) (template := docContent)
| none => | none =>
let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨preambleSeq⟩); $(⟨tacticStx⟩)}) let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $modifiedVal)
elabCommand thmStatement elabCommand thmStatement
let msgs := (← get).messages let msgs := (← get).messages