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

chore: use bracketed do in quotations

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-28 11:20:11 -07:00
parent 6ddec22763
commit 783fd1c160
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Elab/Do.lean
View file

@ -260,7 +260,7 @@ private partial def expandLiftMethodAux : Syntax → StateT (Array Syntax) Macro
else if k == `Lean.Parser.Term.liftMethod then withFreshMacroScope $ do
let term := args.get! 1;
term ← expandLiftMethodAux term;
auxDo ← `(do let a ← $term; $(Syntax.missing));
auxDo ← `(do { let a ← $term; $(Syntax.missing) });
let auxDoElems := (getDoElems auxDo).pop;
modify $ fun s => s ++ auxDoElems;
`(a)
@ -321,15 +321,15 @@ private partial def expandDoElems : Bool → Array Syntax → Nat → MacroM Syn
rest ← mkRest ();
newBody ←
if optElse.isNone then do
`(do let x ← $discr; (match x with | $pat => $rest))
`(do { let x ← $discr; (match x with | $pat => $rest) })
else
let elseBody := optElse.getArg 1;
`(do let x ← $discr; (match x with | $pat => $rest | _ => $elseBody));
`(do { let x ← $discr; (match x with | $pat => $rest | _ => $elseBody) });
addPrefix newBody
else if i < doElems.size - 1 && doElem.getKind == `Lean.Parser.Term.doExpr then do
-- def doExpr := parser! termParser
let term := doElem.getArg 0;
auxDo ← `(do let x ← $term; $(Syntax.missing));
auxDo ← `(do { let x ← $term; $(Syntax.missing) });
let doElemNew := (getDoElems auxDo).get! 0;
let doElems := doElems.set! i doElemNew;
expandDoElems true doElems (i+2)