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

chore: use (doElem| ...) quotation instead of auxDo idiom

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-08 13:54:49 -07:00
parent a31595bda5
commit 9ec583e808
1 changed files with 3 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -209,8 +209,7 @@ hasExitPointPred (fun c => !isTerminalAction c) c
def mkAuxDeclFor {m} [Monad m] [MonadQuotation m] (e : Syntax) (mkCont : Syntax → m Code) : m Code := withFreshMacroScope do
y ← `(y);
let yName := y.getId;
auxDo ← `(do let y ← $e:term);
let doElem := (getDoSeqElems (getDoSeq auxDo)).head!;
doElem ← `(doElem| let y ← $e:term);
-- Add elaboration hint for producing sane error message
y ← `(ensureExpectedType! "type mismatch, result value" $y);
k ← mkCont y;
@ -960,9 +959,8 @@ private partial def expandLiftMethodAux : Syntax → StateT (List Syntax) MacroM
else if k == `Lean.Parser.Term.liftMethod then withFreshMacroScope $ do
let term := args.get! 1;
term ← expandLiftMethodAux term;
auxDo ← `(do let a ← $term:term);
let auxDoElems := getDoSeqElems (getDoSeq auxDo);
modify fun s => s ++ auxDoElems;
auxDoElem ← `(doElem| let a ← $term:term);
modify fun s => s ++ [auxDoElem];
`(a)
else do
args ← args.mapM expandLiftMethodAux;