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

set_option tactic.hygienic false

Browse Source 
Fixes #28
This commit is contained in:
Alexander Bentkamp
2023-01-26 12:17:26 +01:00
parent f82c310557
commit fdbd962742
1 changed files with 3 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/leanserver/GameServer/FileWorker.lean
+3 -1
View File
@@ -104,7 +104,9 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
let done := Syntax.node (.synthetic cmdParserState.pos cmdParserState.pos) ``Lean.Parser.Tactic.done #[] let done := Syntax.node (.synthetic cmdParserState.pos cmdParserState.pos) ``Lean.Parser.Tactic.done #[]
let tacticStx := (#[skip] ++ tacticStx.getArgs ++ #[done]).map (⟨.⟩) let tacticStx := (#[skip] ++ tacticStx.getArgs ++ #[done]).map (⟨.⟩)
let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*) let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*)
let cmdStx ← `(command| theorem my_theorem $(level.goal) := by {$(⟨tacticStx⟩)} ) let cmdStx ← `(command|
set_option tactic.hygienic false in
theorem my_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
Elab.Command.elabCommandTopLevel cmdStx) Elab.Command.elabCommandTopLevel cmdStx)
cmdCtx cmdStateRef cmdCtx cmdStateRef
let postNew := (← tacticCacheNew.get).post let postNew := (← tacticCacheNew.get).post