max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: update macros for extra info field

Browse source
This commit is contained in:
Gabriel Ebner 2021-10-25 13:11:07 +02:00 • committed by Sebastian Ullrich
parent 6efb459d5b
commit b74db2d902
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Binders.lean
View file

@ -55,7 +55,7 @@ partial def quoteAutoTactic : Syntax → TermElabM Syntax
else
let quotedArg ← quoteAutoTactic arg
quotedArgs ← `(Array.push $quotedArgs $quotedArg)
`(Syntax.node $(quote k) $quotedArgs)
`(Syntax.node SourceInfo.none $(quote k) $quotedArgs)
| Syntax.atom info val => `(mkAtom $(quote val))
| Syntax.missing => throwError "invalid auto tactic, tactic is missing"

2
src/Lean/Elab/Quotation.lean
View file

@ -145,7 +145,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
else do
let arg ← quoteSyntax arg
args := args.push arg
`(Syntax.node $(quote k) $(args.build))
`(Syntax.node SourceInfo.none $(quote k) $(args.build))
| Syntax.atom _ val =>
`(Syntax.atom info $(quote val))
| Syntax.missing => throwUnsupportedSyntax