chore: update stage0

2020-02-01 00:13:29 -08:00 · 2020-02-01 00:13:29 -08:00 · f8b9ea898a
commit f8b9ea898a
parent b332d5e74d
19 changed files with 14859 additions and 9403 deletions
--- a/stage0/src/Init/Control/Id.lean
+++ b/stage0/src/Init/Control/Id.lean
@ -20,6 +20,9 @@ f x
@[inline] def Id.map {α β : Type u} (f : α → β) (x : Id α) : Id β :=
 f x

+instance Id.hasBind : HasBind Id :=
+{ bind := @Id.bind }
+
 instance Id.monad : Monad Id :=
 { pure := @Id.pure, bind := @Id.bind, map := @Id.map }

--- a/stage0/src/Init/Lean/Elab/Command.lean
+++ b/stage0/src/Init/Lean/Elab/Command.lean
@ -192,6 +192,8 @@ adaptReader (fun (ctx : Context) => { macroStack := { before := beforeStx, after
 instance : MonadMacroAdapter CommandElabM :=
 { getEnv                 := getEnv,
  getCurrMacroScope      := getCurrMacroScope,
+  getNextMacroScope      := do s ← get; pure s.nextMacroScope,
+  setNextMacroScope      := fun next => modify $ fun s => { nextMacroScope := next, .. s },
  throwError             := @throwError,
  throwUnsupportedSyntax := @throwUnsupportedSyntax}

--- a/stage0/src/Init/Lean/Elab/DoNotation.lean
+++ b/stage0/src/Init/Lean/Elab/DoNotation.lean
@ -5,18 +5,18 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Lean.Elab.Term
+import Init.Lean.Elab.TermBinders
 import Init.Lean.Elab.Quotation

 namespace Lean
 namespace Elab
 namespace Term

-private def mkIdMonadFor (ref : Syntax) (type : Expr) : TermElabM (Expr × Expr) := do
+private def mkIdBindFor (ref : Syntax) (type : Expr) : TermElabM (Expr × Expr) := do
 u ← getLevel ref type;
-let id      := (Lean.mkConst `Id [u]);
-let idType  := Lean.mkApp (Lean.mkConst `Id [u]) type;
-let idMonad := Lean.mkConst `Id.monad [u];
-pure (idType, idMonad)
+let id        := Lean.mkConst `Id [u];
+let idBindVal := Lean.mkConst `Id.hasBind [u];
+pure (id, idBindVal)

 private def extractMonad (ref : Syntax) (expectedType? : Option Expr) : TermElabM (Expr × Expr) := do
 match expectedType? with
@ -28,11 +28,11 @@ match expectedType? with
  | Expr.app m _ _ =>
    catch
      (do
-        monadInst ← mkAppM ref `Monad #[m];
-        monad     ← synthesizeInst ref monadInst;
-        pure (m, monad))
-      (fun ex => mkIdMonadFor ref type)
-  | _ => mkIdMonadFor ref type
+        bindInstType ← mkAppM ref `HasBind #[m];
+        bindInstVal  ← synthesizeInst ref bindInstType;
+        pure (m, bindInstVal))
+      (fun ex => mkIdBindFor ref type)
+  | _ => mkIdBindFor ref type

 private def getDoElems (stx : Syntax) : Array Syntax :=
 --parser! "do " >> (bracketedDoSeq <|> doSeq)
@ -43,13 +43,43 @@ if arg.getKind == `Lean.Parser.Term.bracketedDoSeq then
 else
  arg.getArgs

-/- Expand `doLet`, `doPat`, and nonterminal `doExpr` -/
-private partial def expandDoElems : Array Syntax → Nat → TermElabM (Option Syntax)
-| doElems, i =>
+private partial def hasLiftMethod : Syntax → Bool
+| Syntax.node k args =>
+  if k == `Lean.Parser.Term.do then false
+  else if k == `Lean.Parser.Term.liftMethod then true
+  else args.any hasLiftMethod
+| _ => false
+
+private partial def expandLiftMethodAux : Syntax → StateT (Array Syntax) TermElabM Syntax
+| stx@(Syntax.node k args) =>
+  if k == `Lean.Parser.Term.do then pure stx
+  else if k == `Lean.Parser.Term.liftMethod then withFreshMacroScope $ do
+    let term := args.get! 1;
+    term ← expandLiftMethodAux term;
+    auxDo ← `(do a ← $term; $(Syntax.missing));
+    let auxDoElems := (getDoElems auxDo).pop;
+    modify $ fun s => s ++ auxDoElems;
+    `(a)
+  else do
+    args ← args.mapM expandLiftMethodAux;
+    pure $ Syntax.node k args
+| stx => pure stx
+
+private def expandLiftMethod (stx : Syntax) : TermElabM (Option (Array Syntax)) :=
+if hasLiftMethod stx then do
+  (stx, doElems) ← (expandLiftMethodAux stx).run #[];
+  let doElems := doElems.push stx;
+  pure doElems
+else
+  pure none
+
+/- Expand `doLet`, `doPat`, nonterminal `doExpr`s, and `liftMethod` -/
+private partial def expandDoElems : Bool → Array Syntax → Nat → TermElabM (Option Syntax)
+| modified, doElems, i =>
  let mkRest : Unit → TermElabM Syntax := fun _ => do {
    let restElems := doElems.extract (i+2) doElems.size;
    if restElems.size == 1 then
-      pure (restElems.get! 0)
+      pure $ (restElems.get! 0).getArg 0
    else
      `(do { $restElems* })
  };
@ -57,54 +87,148 @@ private partial def expandDoElems : Array Syntax → Nat → TermElabM (Option S
    if i == 0 then
      pure rest
    else
-      let newElems := doElems.extract 0 (i-1);
+      let newElems := doElems.extract 0 i;
      let newElems := newElems.push $ Syntax.node `Lean.Parser.Term.doExpr #[rest];
      `(do { $newElems* })
  };
-  if h : i < doElems.size then
+  if h : i < doElems.size then do
    let doElem := doElems.get ⟨i, h⟩;
-    if doElem.getKind == `Lean.Parser.Term.doLet then do
-      let letDecl := doElem.getArg 1;
-      rest ← mkRest ();
-      newBody ← `(let $letDecl:letDecl; $rest);
-      addPrefix newBody
-    else if doElem.getKind == `Lean.Parser.Term.doPat then withFreshMacroScope $ do
-      -- (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
-      let pat      := doElem.getArg 0;
-      let discr    := doElem.getArg 2;
-      let optElse  := doElem.getArg 3;
-      rest ← mkRest ();
-      newBody ←
-        if optElse.isNone then do
-          `(do x ← $discr; match x with | $pat => $rest)
-        else
-          let elseBody := optElse.getArg 1;
-          `(do x ← $discr; match x with | $pat => $rest | _ => $elseBody);
-      addPrefix newBody
-    else if i < doElems.size - 2 && doElem.getKind == `Lean.Parser.Term.doExpr then do
-      -- def doExpr := parser! termParser
-      let term := doElem.getArg 0;
-      auxDo ← `(do x ← $term; $(Syntax.missing));
-      let doElemNew := (getDoElems auxDo).get! 0;
-      let doElems := doElems.set! i doElemNew;
-      expandDoElems doElems (i+2)
-    else
-      expandDoElems doElems (i+2)
+    doElemsNew? ← expandLiftMethod doElem;
+    match doElemsNew? with
+    | some doElemsNew => do
+      let post    := doElems.extract (i+1) doElems.size;
+      let pre     := doElems.extract 0 i;
+      let doElems := pre ++ doElemsNew ++ post;
+      tmp ← `(do { $doElems* });
+      expandDoElems true doElems i
+    | none =>
+      if doElem.getKind == `Lean.Parser.Term.doLet then do
+        let letDecl := doElem.getArg 1;
+        rest ← mkRest ();
+        newBody ← `(let $letDecl:letDecl; $rest);
+        addPrefix newBody
+      else if doElem.getKind == `Lean.Parser.Term.doPat then withFreshMacroScope $ do
+        -- (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
+        let pat      := doElem.getArg 0;
+        let discr    := doElem.getArg 2;
+        let optElse  := doElem.getArg 3;
+        rest ← mkRest ();
+        newBody ←
+          if optElse.isNone then do
+            `(do x ← $discr; match x with | $pat => $rest)
+          else
+            let elseBody := optElse.getArg 1;
+            `(do 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 x ← $term; $(Syntax.missing));
+        let doElemNew := (getDoElems auxDo).get! 0;
+        let doElems := doElems.set! i doElemNew;
+        expandDoElems true doElems (i+2)
+      else
+        expandDoElems modified doElems (i+2)
+  else if modified then
+    `(do { $doElems* })
  else
    pure none

+private def ensureDoElemType (ref : Syntax) (expectedMonad : Expr) (expectedType : Expr) (val : Expr) : TermElabM Expr := do
+-- TODO: try MonadLift
+ensureHasType ref expectedType val
+
+structure ProcessedDoElem :=
+(action : Expr)
+(var    : Expr)
+
+instance ProcessedDoElem.inhabited : Inhabited ProcessedDoElem := ⟨⟨arbitrary _, arbitrary _⟩⟩
+
+private def extractTypeFormerAppArg (ref : Syntax) (type : Expr) : TermElabM Expr := do
+type ← withReducible $ whnf ref type;
+match type with
+| Expr.app _ a _ => pure a
+| _              => throwError ref ("type former application expected" ++ indentExpr type)
+
+/-
+HasBind.bind : ∀ {m : Type u_1 → Type u_2} [self : HasBind m] {α β : Type u_1}, m α → (α → m β) → m β
+-/
+private def mkBind (ref : Syntax) (m bindInstVal : Expr) (elems : Array ProcessedDoElem) (body : Expr) : TermElabM Expr :=
+if elems.isEmpty then
+  pure body
+else do
+  let x := elems.back.var; -- any variable would work since they must be in the same universe
+  xType ← inferType ref x;
+  u_1 ← getLevel ref xType;
+  u_1 ← decLevel ref u_1;
+  bodyType ← inferType ref body;
+  u_2 ← getLevel ref bodyType;
+  u_2 ← decLevel ref u_2;
+  let bindAndInst := mkApp2 (Lean.mkConst `HasBind.bind [u_1, u_2]) m bindInstVal;
+  elems.foldrM
+    (fun elem body => do
+      -- dbgTrace (">>> " ++ toString body);
+      let var    := elem.var;
+      let action := elem.action;
+      α  ← inferType ref var;
+      mβ ← inferType ref body;
+      β  ← extractTypeFormerAppArg ref mβ;
+      f  ← mkLambda ref #[var] body;
+      -- dbgTrace (">>> f: " ++ toString f);
+      let body := mkAppN bindAndInst #[α, β, action, f];
+      pure body)
+    body
+
+private partial def processDoElemsAux (doElems : Array Syntax) (m bindInstVal : Expr) (expectedType : Expr) : Nat → Array ProcessedDoElem → TermElabM Expr
+| i, elems =>
+  let doElem := doElems.get! i;
+  let k      := doElem.getKind;
+  let ref    := doElem;
+  if k == `Lean.Parser.Term.doId then do
+    when (i == doElems.size - 1) $
+      throwError ref "the last statement in a 'do' block must be an expression";
+    -- try (ident >> optType >> leftArrow) >> termParser
+    let id        := doElem.getIdAt 0;
+    let typeStx   := expandOptType ref (doElem.getArg 1);
+    let actionStx := doElem.getArg 3;
+    type ← elabType typeStx;
+    let actionExpectedType := mkApp m type;
+    action ← elabTerm actionStx actionExpectedType;
+    action ← ensureDoElemType actionStx m actionExpectedType action;
+    withLocalDecl ref id type $ fun x =>
+      processDoElemsAux (i+1) (elems.push { action := action, var := x })
+  else if doElem.getKind == `Lean.Parser.Term.doExpr then do
+    when (i != doElems.size - 1) $
+      throwError ref ("unexpected 'do' expression element" ++ Format.line ++ doElem);
+    let bodyStx := doElem.getArg 0;
+    body ← elabTerm bodyStx expectedType;
+    body ← ensureDoElemType ref m expectedType body;
+    mkBind ref m bindInstVal elems body
+  else
+    throwError ref ("unexpected 'do' expression element" ++ Format.line ++ doElem)
+
+private def processDoElems (doElems : Array Syntax) (m bindInstVal : Expr) (expectedType : Expr) : TermElabM Expr :=
+processDoElemsAux doElems m bindInstVal expectedType 0 #[]
+
@[builtinTermElab «do»] def elabDo : TermElab :=
 fun stx expectedType? => do
  let ref := stx;
  tryPostponeIfNoneOrMVar expectedType?;
  let doElems := getDoElems stx;
-  stxNew? ← expandDoElems doElems 0;
+  stxNew? ← expandDoElems false doElems 0;
  match stxNew? with
  | some stxNew => withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
  | none => do
+    trace `Elab.do ref $ fun _ => stx;
    let doElems := doElems.getSepElems;
-    (m, monad) ← extractMonad ref expectedType?;
-    throwError stx ("WIP " ++ toString doElems ++ Format.line ++ monad)
+    (m, bindInstVal) ← extractMonad ref expectedType?;
+    result ← processDoElems doElems m bindInstVal expectedType?.get!;
+    -- dbgTrace ("result: " ++ toString result);
+    pure result
+
+@[init] private def regTraceClasses : IO Unit := do
+registerTraceClass `Elab.do;
+pure ()

 end Term
 end Elab
--- a/stage0/src/Init/Lean/Elab/Tactic/Basic.lean
+++ b/stage0/src/Init/Lean/Elab/Tactic/Basic.lean
@ -177,6 +177,8 @@ adaptReader (fun (ctx : Context) => { macroStack := { before := beforeStx, after
 instance : MonadMacroAdapter TacticM :=
 { getEnv                 := getEnv,
  getCurrMacroScope      := getCurrMacroScope,
+  getNextMacroScope      := do s ← get; pure s.nextMacroScope,
+  setNextMacroScope      := fun next => modify $ fun s => { nextMacroScope := next, .. s },
  throwError             := @throwError,
  throwUnsupportedSyntax := @throwUnsupportedSyntax }

--- a/stage0/src/Init/Lean/Elab/Term.lean
+++ b/stage0/src/Init/Lean/Elab/Term.lean
@ -470,6 +470,8 @@ private def elabTermUsing (s : State) (stx : Syntax) (expectedType? : Option Exp
 instance : MonadMacroAdapter TermElabM :=
 { getEnv                 := getEnv,
  getCurrMacroScope      := getCurrMacroScope,
+  getNextMacroScope      := do s ← get; pure s.nextMacroScope,
+  setNextMacroScope      := fun next => modify $ fun s => { nextMacroScope := next, .. s },
  throwError             := @throwError,
  throwUnsupportedSyntax := @throwUnsupportedSyntax}

--- a/stage0/src/Init/Lean/Elab/TermBinders.lean
+++ b/stage0/src/Init/Lean/Elab/TermBinders.lean
@ -253,6 +253,17 @@ fun stx expectedType? => do
    e ← elabTerm body none;
    mkLambda stx xs e

+def withLocalDecl {α} (ref : Syntax) (n : Name) (type : Expr) (k : Expr → TermElabM α) : TermElabM α := do
+fvarId ← mkFreshFVarId;
+ctx ← read;
+let lctx       := ctx.lctx.mkLocalDecl fvarId n type;
+let localInsts := ctx.localInstances;
+let fvar       := mkFVar fvarId;
+c? ← isClass ref type;
+match c? with
+| some c => adaptReader (fun (ctx : Context) => { lctx := lctx, localInstances := localInsts.push { className := c, fvar := fvar }, .. ctx }) $ k fvar
+| none   => adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $ k fvar
+
 def withLetDecl {α} (ref : Syntax) (n : Name) (type : Expr) (val : Expr) (k : Expr → TermElabM α) : TermElabM α := do
 fvarId ← mkFreshFVarId;
 ctx ← read;
--- a/stage0/src/Init/Lean/Elab/Util.lean
+++ b/stage0/src/Init/Lean/Elab/Util.lean
@ -226,16 +226,19 @@ fun stx =>
 class MonadMacroAdapter (m : Type → Type) :=
 (getEnv {}                            : m Environment)
 (getCurrMacroScope {}                 : m MacroScope)
+(getNextMacroScope {}                 : m MacroScope)
+(setNextMacroScope {}                 : MacroScope → m Unit)
 (throwError {} {α : Type}             : Syntax → MessageData → m α)
 (throwUnsupportedSyntax {} {α : Type} : m α)

@[inline] def adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] (x : Macro) (stx : Syntax) : m Syntax := do
 scp  ← MonadMacroAdapter.getCurrMacroScope;
 env  ← MonadMacroAdapter.getEnv;
-match x stx { currMacroScope := scp, mainModule := env.mainModule } with
-| Except.error Macro.Exception.unsupportedSyntax => MonadMacroAdapter.throwUnsupportedSyntax
-| Except.error (Macro.Exception.error msg)       => MonadMacroAdapter.throwError stx msg
-| Except.ok stx                                  => pure stx
+next ← MonadMacroAdapter.getNextMacroScope;
+match x stx { currMacroScope := scp, mainModule := env.mainModule } next with
+| EStateM.Result.error Macro.Exception.unsupportedSyntax _ => MonadMacroAdapter.throwUnsupportedSyntax
+| EStateM.Result.error (Macro.Exception.error msg) _       => MonadMacroAdapter.throwError stx msg
+| EStateM.Result.ok stx nextMacroScope                     => do MonadMacroAdapter.setNextMacroScope nextMacroScope; pure stx

@[init] private def regTraceClasses : IO Unit := do
 registerTraceClass `Elab;
--- a/stage0/src/Init/LeanInit.lean
+++ b/stage0/src/Init/LeanInit.lean
@ -9,7 +9,7 @@ import Init.Data.Array.Basic
 import Init.Data.UInt
 import Init.Data.Hashable
 import Init.Control.Reader
-import Init.Control.Except
+import Init.Control.EState

 namespace Lean
 /-
@ -371,7 +371,7 @@ inductive Exception

 end Macro

-abbrev MacroM := ReaderT Macro.Context (ExceptT Macro.Exception Id)
+abbrev MacroM := ReaderT Macro.Context (EStateM Macro.Exception MacroScope)

 def Macro.addMacroScope (n : Name) : MacroM Name := do
 ctx ← read;
@ -380,10 +380,14 @@ pure $ Lean.addMacroScope ctx.mainModule n ctx.currMacroScope
 def Macro.throwUnsupported {α} : MacroM α :=
 throw Macro.Exception.unsupportedSyntax

+@[inline] protected def Macro.withFreshMacroScope {α} (x : MacroM α) : MacroM α := do
+fresh ← modifyGet (fun s => (s, s+1));
+adaptReader (fun (ctx : Macro.Context) => { currMacroScope := fresh, .. ctx }) x
+
 instance MacroM.monadQuotation : MonadQuotation MacroM :=
 { getCurrMacroScope   := fun ctx => pure ctx.currMacroScope,
  getMainModule       := fun ctx => pure ctx.mainModule,
-  withFreshMacroScope := fun _ x => x }
+  withFreshMacroScope := @Macro.withFreshMacroScope }

 abbrev Macro := Syntax → MacroM Syntax

--- a/stage0/stdlib/Init/Control/Id.c
+++ b/stage0/stdlib/Init/Control/Id.c
@ -20,7 +20,6 @@ lean_object* l_Id_monad___closed__6;
 lean_object* l_Id_monad___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Id_monad___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Id_run(lean_object*);
-lean_object* l_Id_monad___closed__9;
 lean_object* l_Id_monad;
 lean_object* l_Id_monad___closed__8;
 lean_object* l_Id_monad___closed__3;
@ -36,8 +35,10 @@ lean_object* l_Id_monad___closed__2;
 lean_object* l_Id_pure(lean_object*);
 lean_object* l_Id_monad___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Id_monad___closed__5;
+lean_object* l_Id_hasBind;
 lean_object* l_Id_MonadRun;
 lean_object* l_Id_MonadRun___closed__1;
+lean_object* l_Id_hasBind___closed__1;
 lean_object* l_Id_run___rarg(lean_object*);
 lean_object* l_Id_monad___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Id_pure___rarg(lean_object* x_1) {
@ -96,6 +97,22 @@ x_3 = lean_alloc_closure((void*)(l_Id_map___rarg), 2, 0);
 return x_3;
 }
 }
+lean_object* _init_l_Id_hasBind___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Id_bind), 2, 0);
+return x_1;
+}
+}
+lean_object* _init_l_Id_hasBind() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Id_hasBind___closed__1;
+return x_1;
+}
+}
 lean_object* l_Id_monad___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
@ -191,17 +208,9 @@ return x_6;
 lean_object* _init_l_Id_monad___closed__8() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Id_bind), 2, 0);
-return x_1;
-}
-}
-lean_object* _init_l_Id_monad___closed__9() {
-_start:
-{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Id_monad___closed__7;
-x_2 = l_Id_monad___closed__8;
+x_2 = l_Id_hasBind___closed__1;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@ -212,7 +221,7 @@ lean_object* _init_l_Id_monad() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Id_monad___closed__9;
+x_1 = l_Id_monad___closed__8;
 return x_1;
 }
 }
@ -285,6 +294,10 @@ _G_initialized = true;
 res = initialize_Init_Control_Lift(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l_Id_hasBind___closed__1 = _init_l_Id_hasBind___closed__1();
+lean_mark_persistent(l_Id_hasBind___closed__1);
+l_Id_hasBind = _init_l_Id_hasBind();
+lean_mark_persistent(l_Id_hasBind);
 l_Id_monad___closed__1 = _init_l_Id_monad___closed__1();
 lean_mark_persistent(l_Id_monad___closed__1);
 l_Id_monad___closed__2 = _init_l_Id_monad___closed__2();
@ -301,8 +314,6 @@ l_Id_monad___closed__7 = _init_l_Id_monad___closed__7();
 lean_mark_persistent(l_Id_monad___closed__7);
 l_Id_monad___closed__8 = _init_l_Id_monad___closed__8();
 lean_mark_persistent(l_Id_monad___closed__8);
-l_Id_monad___closed__9 = _init_l_Id_monad___closed__9();
-lean_mark_persistent(l_Id_monad___closed__9);
 l_Id_monad = _init_l_Id_monad();
 lean_mark_persistent(l_Id_monad);
 l_Id_MonadRun___closed__1 = _init_l_Id_MonadRun___closed__1();
--- a/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
+++ b/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
--- a/stage0/stdlib/Init/Lean/Elab/Command.c
+++ b/stage0/stdlib/Init/Lean/Elab/Command.c
--- a/stage0/stdlib/Init/Lean/Elab/DoNotation.c
+++ b/stage0/stdlib/Init/Lean/Elab/DoNotation.c
--- a/stage0/stdlib/Init/Lean/Elab/Syntax.c
+++ b/stage0/stdlib/Init/Lean/Elab/Syntax.c
--- a/stage0/stdlib/Init/Lean/Elab/SynthesizeSyntheticMVars.c
+++ b/stage0/stdlib/Init/Lean/Elab/SynthesizeSyntheticMVars.c
@ -31,7 +31,6 @@ lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SynthesizeSy
 lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_7__synthesizeSyntheticMVarsStep___spec__2___closed__7;
 lean_object* l_Lean_mkMVar(lean_object*);
 lean_object* l_Lean_Elab_Term_liftTacticElabM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_7__synthesizeSyntheticMVarsStep___closed__4;
 lean_object* l_List_append___rarg(lean_object*, lean_object*);
@ -51,7 +50,6 @@ lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_7__synthesizeSy
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_ensureHasType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_7__synthesizeSyntheticMVarsStep___spec__2___closed__8;
-lean_object* l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1(lean_object*);
 lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_3__synthesizePendingInstMVar(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__1;
 lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -77,6 +75,7 @@ lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SynthesizeSy
 lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_7__synthesizeSyntheticMVarsStep___spec__2___closed__3;
 lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_5__checkWithDefault(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_11__synthesizeSyntheticMVarsAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_ReaderT_lift___at_Lean_Elab_Term_Lean_Elab_MonadMacroAdapter___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_getMVarDecl___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_8__synthesizeUsingDefault(lean_object*, lean_object*);
 lean_object* l_List_lengthAux___main___rarg(lean_object*, lean_object*);
@ -138,7 +137,6 @@ lean_object* l_List_forM___main___at___private_Init_Lean_Elab_SynthesizeSyntheti
 uint8_t l_List_isEmpty___rarg(lean_object*);
 extern lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1;
 lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_7__synthesizeSyntheticMVarsStep(uint8_t, uint8_t, lean_object*, lean_object*);
-lean_object* l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_4__synthesizePendingCoeInstMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_indentExpr(lean_object*);
 lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_7__synthesizeSyntheticMVarsStep___closed__5;
@ -1551,22 +1549,6 @@ x_7 = l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_1__resumeElabTerm(x_1,
 return x_7;
 }
 }
-lean_object* l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-lean_object* x_4; 
-x_4 = lean_apply_1(x_1, x_3);
-return x_4;
-}
-}
-lean_object* l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1___rarg___boxed), 3, 0);
-return x_2;
-}
-}
 lean_object* _init_l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___lambda__1___closed__1() {
 _start:
 {
@ -1912,7 +1894,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; 
 x_1 = l_EStateM_MonadState___closed__2;
-x_2 = lean_alloc_closure((void*)(l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1___rarg___boxed), 3, 1);
+x_2 = lean_alloc_closure((void*)(l_ReaderT_lift___at_Lean_Elab_Term_Lean_Elab_MonadMacroAdapter___spec__1___rarg___boxed), 3, 1);
 lean_closure_set(x_2, 0, x_1);
 return x_2;
 }
@ -1937,15 +1919,6 @@ lean_dec(x_3);
 return x_11;
 }
 }
-lean_object* l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-lean_object* x_4; 
-x_4 = l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1___rarg(x_1, x_2, x_3);
-lean_dec(x_2);
-return x_4;
-}
-}
 lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
 _start:
 {
--- a/stage0/stdlib/Init/Lean/Elab/Tactic/Basic.c
+++ b/stage0/stdlib/Init/Lean/Elab/Tactic/Basic.c
--- a/stage0/stdlib/Init/Lean/Elab/Term.c
+++ b/stage0/stdlib/Init/Lean/Elab/Term.c
--- a/stage0/stdlib/Init/Lean/Elab/TermBinders.c
+++ b/stage0/stdlib/Init/Lean/Elab/TermBinders.c
@ -139,6 +139,7 @@ lean_object* l_Lean_Elab_Term_getCurrMacroScope(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_TermBinders_5__matchBinder___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabArrow___lambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_expandOptType(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_withLocalDecl___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabArrow___lambda__1___closed__6;
 lean_object* l_Lean_Elab_Term_mkFreshFVarId(lean_object*);
 uint8_t l_coeDecidableEq(uint8_t);
@ -225,7 +226,9 @@ lean_object* l_Lean_Elab_Term_withLetDecl(lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabDepArrow___closed__2;
 lean_object* l___private_Init_Lean_Elab_TermBinders_2__expandBinderIdent(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_mkHole___closed__2;
+lean_object* l_Lean_Elab_Term_withLocalDecl(lean_object*);
 lean_object* l_Lean_Elab_Term_elabBinders___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_withLocalDecl___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_TermBinders_4__expandBinderModifier___closed__3;
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 extern lean_object* l_Lean_mkOptionalNode___closed__2;
@ -17130,6 +17133,445 @@ x_5 = l_Lean_Elab_Term_addBuiltinTermElab(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
+lean_object* l_Lean_Elab_Term_withLocalDecl___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; 
+x_7 = l_Lean_Elab_Term_mkFreshFVarId___rarg(x_6);
+x_8 = lean_ctor_get(x_5, 0);
+lean_inc(x_8);
+x_9 = lean_ctor_get(x_7, 0);
+lean_inc(x_9);
+x_10 = lean_ctor_get(x_7, 1);
+lean_inc(x_10);
+lean_dec(x_7);
+x_11 = lean_ctor_get(x_5, 1);
+lean_inc(x_11);
+x_12 = lean_ctor_get(x_5, 2);
+lean_inc(x_12);
+x_13 = lean_ctor_get(x_5, 3);
+lean_inc(x_13);
+x_14 = lean_ctor_get(x_5, 4);
+lean_inc(x_14);
+x_15 = lean_ctor_get(x_5, 5);
+lean_inc(x_15);
+x_16 = lean_ctor_get(x_5, 6);
+lean_inc(x_16);
+x_17 = lean_ctor_get(x_5, 7);
+lean_inc(x_17);
+x_18 = lean_ctor_get(x_5, 8);
+lean_inc(x_18);
+x_19 = lean_ctor_get(x_5, 9);
+lean_inc(x_19);
+x_20 = !lean_is_exclusive(x_8);
+if (x_20 == 0)
+{
+uint8_t x_21; uint8_t x_22; uint8_t x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; uint8_t x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33; 
+x_21 = lean_ctor_get_uint8(x_5, sizeof(void*)*10);
+x_22 = lean_ctor_get_uint8(x_5, sizeof(void*)*10 + 1);
+x_23 = lean_ctor_get_uint8(x_5, sizeof(void*)*10 + 2);
+x_24 = lean_ctor_get(x_8, 0);
+x_25 = lean_ctor_get(x_8, 1);
+x_26 = lean_ctor_get(x_8, 2);
+x_27 = lean_ctor_get(x_8, 3);
+x_28 = lean_ctor_get(x_8, 4);
+x_29 = 0;
+lean_inc(x_3);
+lean_inc(x_9);
+x_30 = lean_local_ctx_mk_local_decl(x_25, x_9, x_2, x_3, x_29);
+x_31 = l_Lean_mkFVar(x_9);
+lean_inc(x_5);
+x_32 = l_Lean_Elab_Term_isClass(x_1, x_3, x_5, x_10);
+x_33 = !lean_is_exclusive(x_5);
+if (x_33 == 0)
+{
+lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; 
+x_34 = lean_ctor_get(x_5, 9);
+lean_dec(x_34);
+x_35 = lean_ctor_get(x_5, 8);
+lean_dec(x_35);
+x_36 = lean_ctor_get(x_5, 7);
+lean_dec(x_36);
+x_37 = lean_ctor_get(x_5, 6);
+lean_dec(x_37);
+x_38 = lean_ctor_get(x_5, 5);
+lean_dec(x_38);
+x_39 = lean_ctor_get(x_5, 4);
+lean_dec(x_39);
+x_40 = lean_ctor_get(x_5, 3);
+lean_dec(x_40);
+x_41 = lean_ctor_get(x_5, 2);
+lean_dec(x_41);
+x_42 = lean_ctor_get(x_5, 1);
+lean_dec(x_42);
+x_43 = lean_ctor_get(x_5, 0);
+lean_dec(x_43);
+if (lean_obj_tag(x_32) == 0)
+{
+lean_object* x_44; 
+x_44 = lean_ctor_get(x_32, 0);
+lean_inc(x_44);
+if (lean_obj_tag(x_44) == 0)
+{
+lean_object* x_45; lean_object* x_46; 
+x_45 = lean_ctor_get(x_32, 1);
+lean_inc(x_45);
+lean_dec(x_32);
+lean_ctor_set(x_8, 1, x_30);
+x_46 = lean_apply_3(x_4, x_31, x_5, x_45);
+return x_46;
+}
+else
+{
+lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; 
+x_47 = lean_ctor_get(x_32, 1);
+lean_inc(x_47);
+lean_dec(x_32);
+x_48 = lean_ctor_get(x_44, 0);
+lean_inc(x_48);
+lean_dec(x_44);
+lean_inc(x_31);
+x_49 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_49, 0, x_48);
+lean_ctor_set(x_49, 1, x_31);
+x_50 = lean_array_push(x_26, x_49);
+lean_ctor_set(x_8, 2, x_50);
+lean_ctor_set(x_8, 1, x_30);
+x_51 = lean_apply_3(x_4, x_31, x_5, x_47);
+return x_51;
+}
+}
+else
+{
+uint8_t x_52; 
+lean_free_object(x_5);
+lean_dec(x_31);
+lean_dec(x_30);
+lean_free_object(x_8);
+lean_dec(x_28);
+lean_dec(x_27);
+lean_dec(x_26);
+lean_dec(x_24);
+lean_dec(x_19);
+lean_dec(x_18);
+lean_dec(x_17);
+lean_dec(x_16);
+lean_dec(x_15);
+lean_dec(x_14);
+lean_dec(x_13);
+lean_dec(x_12);
+lean_dec(x_11);
+lean_dec(x_4);
+x_52 = !lean_is_exclusive(x_32);
+if (x_52 == 0)
+{
+return x_32;
+}
+else
+{
+lean_object* x_53; lean_object* x_54; lean_object* x_55; 
+x_53 = lean_ctor_get(x_32, 0);
+x_54 = lean_ctor_get(x_32, 1);
+lean_inc(x_54);
+lean_inc(x_53);
+lean_dec(x_32);
+x_55 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_55, 0, x_53);
+lean_ctor_set(x_55, 1, x_54);
+return x_55;
+}
+}
+}
+else
+{
+lean_dec(x_5);
+if (lean_obj_tag(x_32) == 0)
+{
+lean_object* x_56; 
+x_56 = lean_ctor_get(x_32, 0);
+lean_inc(x_56);
+if (lean_obj_tag(x_56) == 0)
+{
+lean_object* x_57; lean_object* x_58; lean_object* x_59; 
+x_57 = lean_ctor_get(x_32, 1);
+lean_inc(x_57);
+lean_dec(x_32);
+lean_ctor_set(x_8, 1, x_30);
+x_58 = lean_alloc_ctor(0, 10, 3);
+lean_ctor_set(x_58, 0, x_8);
+lean_ctor_set(x_58, 1, x_11);
+lean_ctor_set(x_58, 2, x_12);
+lean_ctor_set(x_58, 3, x_13);
+lean_ctor_set(x_58, 4, x_14);
+lean_ctor_set(x_58, 5, x_15);
+lean_ctor_set(x_58, 6, x_16);
+lean_ctor_set(x_58, 7, x_17);
+lean_ctor_set(x_58, 8, x_18);
+lean_ctor_set(x_58, 9, x_19);
+lean_ctor_set_uint8(x_58, sizeof(void*)*10, x_21);
+lean_ctor_set_uint8(x_58, sizeof(void*)*10 + 1, x_22);
+lean_ctor_set_uint8(x_58, sizeof(void*)*10 + 2, x_23);
+x_59 = lean_apply_3(x_4, x_31, x_58, x_57);
+return x_59;
+}
+else
+{
+lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; 
+x_60 = lean_ctor_get(x_32, 1);
+lean_inc(x_60);
+lean_dec(x_32);
+x_61 = lean_ctor_get(x_56, 0);
+lean_inc(x_61);
+lean_dec(x_56);
+lean_inc(x_31);
+x_62 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_62, 0, x_61);
+lean_ctor_set(x_62, 1, x_31);
+x_63 = lean_array_push(x_26, x_62);
+lean_ctor_set(x_8, 2, x_63);
+lean_ctor_set(x_8, 1, x_30);
+x_64 = lean_alloc_ctor(0, 10, 3);
+lean_ctor_set(x_64, 0, x_8);
+lean_ctor_set(x_64, 1, x_11);
+lean_ctor_set(x_64, 2, x_12);
+lean_ctor_set(x_64, 3, x_13);
+lean_ctor_set(x_64, 4, x_14);
+lean_ctor_set(x_64, 5, x_15);
+lean_ctor_set(x_64, 6, x_16);
+lean_ctor_set(x_64, 7, x_17);
+lean_ctor_set(x_64, 8, x_18);
+lean_ctor_set(x_64, 9, x_19);
+lean_ctor_set_uint8(x_64, sizeof(void*)*10, x_21);
+lean_ctor_set_uint8(x_64, sizeof(void*)*10 + 1, x_22);
+lean_ctor_set_uint8(x_64, sizeof(void*)*10 + 2, x_23);
+x_65 = lean_apply_3(x_4, x_31, x_64, x_60);
+return x_65;
+}
+}
+else
+{
+lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; 
+lean_dec(x_31);
+lean_dec(x_30);
+lean_free_object(x_8);
+lean_dec(x_28);
+lean_dec(x_27);
+lean_dec(x_26);
+lean_dec(x_24);
+lean_dec(x_19);
+lean_dec(x_18);
+lean_dec(x_17);
+lean_dec(x_16);
+lean_dec(x_15);
+lean_dec(x_14);
+lean_dec(x_13);
+lean_dec(x_12);
+lean_dec(x_11);
+lean_dec(x_4);
+x_66 = lean_ctor_get(x_32, 0);
+lean_inc(x_66);
+x_67 = lean_ctor_get(x_32, 1);
+lean_inc(x_67);
+if (lean_is_exclusive(x_32)) {
+ lean_ctor_release(x_32, 0);
+ lean_ctor_release(x_32, 1);
+ x_68 = x_32;
+} else {
+ lean_dec_ref(x_32);
+ x_68 = lean_box(0);
+}
+if (lean_is_scalar(x_68)) {
+ x_69 = lean_alloc_ctor(1, 2, 0);
+} else {
+ x_69 = x_68;
+}
+lean_ctor_set(x_69, 0, x_66);
+lean_ctor_set(x_69, 1, x_67);
+return x_69;
+}
+}
+}
+else
+{
+uint8_t x_70; uint8_t x_71; uint8_t x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; uint8_t x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; 
+x_70 = lean_ctor_get_uint8(x_5, sizeof(void*)*10);
+x_71 = lean_ctor_get_uint8(x_5, sizeof(void*)*10 + 1);
+x_72 = lean_ctor_get_uint8(x_5, sizeof(void*)*10 + 2);
+x_73 = lean_ctor_get(x_8, 0);
+x_74 = lean_ctor_get(x_8, 1);
+x_75 = lean_ctor_get(x_8, 2);
+x_76 = lean_ctor_get(x_8, 3);
+x_77 = lean_ctor_get(x_8, 4);
+lean_inc(x_77);
+lean_inc(x_76);
+lean_inc(x_75);
+lean_inc(x_74);
+lean_inc(x_73);
+lean_dec(x_8);
+x_78 = 0;
+lean_inc(x_3);
+lean_inc(x_9);
+x_79 = lean_local_ctx_mk_local_decl(x_74, x_9, x_2, x_3, x_78);
+x_80 = l_Lean_mkFVar(x_9);
+lean_inc(x_5);
+x_81 = l_Lean_Elab_Term_isClass(x_1, x_3, x_5, x_10);
+if (lean_is_exclusive(x_5)) {
+ lean_ctor_release(x_5, 0);
+ lean_ctor_release(x_5, 1);
+ lean_ctor_release(x_5, 2);
+ lean_ctor_release(x_5, 3);
+ lean_ctor_release(x_5, 4);
+ lean_ctor_release(x_5, 5);
+ lean_ctor_release(x_5, 6);
+ lean_ctor_release(x_5, 7);
+ lean_ctor_release(x_5, 8);
+ lean_ctor_release(x_5, 9);
+ x_82 = x_5;
+} else {
+ lean_dec_ref(x_5);
+ x_82 = lean_box(0);
+}
+if (lean_obj_tag(x_81) == 0)
+{
+lean_object* x_83; 
+x_83 = lean_ctor_get(x_81, 0);
+lean_inc(x_83);
+if (lean_obj_tag(x_83) == 0)
+{
+lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; 
+x_84 = lean_ctor_get(x_81, 1);
+lean_inc(x_84);
+lean_dec(x_81);
+x_85 = lean_alloc_ctor(0, 5, 0);
+lean_ctor_set(x_85, 0, x_73);
+lean_ctor_set(x_85, 1, x_79);
+lean_ctor_set(x_85, 2, x_75);
+lean_ctor_set(x_85, 3, x_76);
+lean_ctor_set(x_85, 4, x_77);
+if (lean_is_scalar(x_82)) {
+ x_86 = lean_alloc_ctor(0, 10, 3);
+} else {
+ x_86 = x_82;
+}
+lean_ctor_set(x_86, 0, x_85);
+lean_ctor_set(x_86, 1, x_11);
+lean_ctor_set(x_86, 2, x_12);
+lean_ctor_set(x_86, 3, x_13);
+lean_ctor_set(x_86, 4, x_14);
+lean_ctor_set(x_86, 5, x_15);
+lean_ctor_set(x_86, 6, x_16);
+lean_ctor_set(x_86, 7, x_17);
+lean_ctor_set(x_86, 8, x_18);
+lean_ctor_set(x_86, 9, x_19);
+lean_ctor_set_uint8(x_86, sizeof(void*)*10, x_70);
+lean_ctor_set_uint8(x_86, sizeof(void*)*10 + 1, x_71);
+lean_ctor_set_uint8(x_86, sizeof(void*)*10 + 2, x_72);
+x_87 = lean_apply_3(x_4, x_80, x_86, x_84);
+return x_87;
+}
+else
+{
+lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; 
+x_88 = lean_ctor_get(x_81, 1);
+lean_inc(x_88);
+lean_dec(x_81);
+x_89 = lean_ctor_get(x_83, 0);
+lean_inc(x_89);
+lean_dec(x_83);
+lean_inc(x_80);
+x_90 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_90, 0, x_89);
+lean_ctor_set(x_90, 1, x_80);
+x_91 = lean_array_push(x_75, x_90);
+x_92 = lean_alloc_ctor(0, 5, 0);
+lean_ctor_set(x_92, 0, x_73);
+lean_ctor_set(x_92, 1, x_79);
+lean_ctor_set(x_92, 2, x_91);
+lean_ctor_set(x_92, 3, x_76);
+lean_ctor_set(x_92, 4, x_77);
+if (lean_is_scalar(x_82)) {
+ x_93 = lean_alloc_ctor(0, 10, 3);
+} else {
+ x_93 = x_82;
+}
+lean_ctor_set(x_93, 0, x_92);
+lean_ctor_set(x_93, 1, x_11);
+lean_ctor_set(x_93, 2, x_12);
+lean_ctor_set(x_93, 3, x_13);
+lean_ctor_set(x_93, 4, x_14);
+lean_ctor_set(x_93, 5, x_15);
+lean_ctor_set(x_93, 6, x_16);
+lean_ctor_set(x_93, 7, x_17);
+lean_ctor_set(x_93, 8, x_18);
+lean_ctor_set(x_93, 9, x_19);
+lean_ctor_set_uint8(x_93, sizeof(void*)*10, x_70);
+lean_ctor_set_uint8(x_93, sizeof(void*)*10 + 1, x_71);
+lean_ctor_set_uint8(x_93, sizeof(void*)*10 + 2, x_72);
+x_94 = lean_apply_3(x_4, x_80, x_93, x_88);
+return x_94;
+}
+}
+else
+{
+lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; 
+lean_dec(x_82);
+lean_dec(x_80);
+lean_dec(x_79);
+lean_dec(x_77);
+lean_dec(x_76);
+lean_dec(x_75);
+lean_dec(x_73);
+lean_dec(x_19);
+lean_dec(x_18);
+lean_dec(x_17);
+lean_dec(x_16);
+lean_dec(x_15);
+lean_dec(x_14);
+lean_dec(x_13);
+lean_dec(x_12);
+lean_dec(x_11);
+lean_dec(x_4);
+x_95 = lean_ctor_get(x_81, 0);
+lean_inc(x_95);
+x_96 = lean_ctor_get(x_81, 1);
+lean_inc(x_96);
+if (lean_is_exclusive(x_81)) {
+ lean_ctor_release(x_81, 0);
+ lean_ctor_release(x_81, 1);
+ x_97 = x_81;
+} else {
+ lean_dec_ref(x_81);
+ x_97 = lean_box(0);
+}
+if (lean_is_scalar(x_97)) {
+ x_98 = lean_alloc_ctor(1, 2, 0);
+} else {
+ x_98 = x_97;
+}
+lean_ctor_set(x_98, 0, x_95);
+lean_ctor_set(x_98, 1, x_96);
+return x_98;
+}
+}
+}
+}
+lean_object* l_Lean_Elab_Term_withLocalDecl(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_withLocalDecl___rarg___boxed), 6, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_Elab_Term_withLocalDecl___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; 
+x_7 = l_Lean_Elab_Term_withLocalDecl___rarg(x_1, x_2, x_3, x_4, x_5, x_6);
+lean_dec(x_1);
+return x_7;
+}
+}
 lean_object* l_Lean_Elab_Term_withLetDecl___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
 _start:
 {
--- a/stage0/stdlib/Init/Lean/Elab/Util.c
+++ b/stage0/stdlib/Init/Lean/Elab/Util.c
@ -22,7 +22,6 @@ lean_object* l_AssocList_replace___main___at_Lean_Elab_ElabFnTable_insert___spec
 lean_object* l_AssocList_foldlM___main___at_Lean_Elab_ElabFnTable_insert___spec__29(lean_object*);
 lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Util_6__ElabAttribute_add___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_Macro_throwUnsupported___closed__1;
 extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;
 lean_object* l_AssocList_contains___main___at_Lean_Elab_ElabFnTable_insert___spec__26___rarg___boxed(lean_object*, lean_object*);
 extern lean_object* l___private_Init_Lean_Parser_Parser_27__BuiltinParserAttribute_add___closed__2;
@ -32,6 +31,7 @@ lean_object* l_Lean_Elab_mkMacroAttribute(lean_object*);
 lean_object* l_Lean_Elab_mkElabAttributeAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Util_2__throwUnexpectedElabType(lean_object*);
 lean_object* l_Lean_Elab_macroAttribute___closed__2;
+lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MacroScopesView_format___boxed(lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_Elab_ElabFnTable_insert___spec__24___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_String_toFormat(lean_object*);
@ -76,7 +76,7 @@ lean_object* l_Lean_Elab_registerBuiltinMacroAttr___lambda__1___closed__2;
 lean_object* l___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers(lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
 lean_object* l_AssocList_find___main___at_Lean_Elab_ElabFnTable_insert___spec__6___rarg(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_mkMacroAttribute___closed__3;
 lean_object* l___private_Init_Lean_Elab_Util_1__ElabAttribute_mkInitial___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_SMap_empty___at_Lean_Elab_ElabAttribute_inhabited___spec__1___closed__2;
@ -137,6 +137,7 @@ lean_object* l_HashMapImp_expand___at_Lean_Elab_ElabFnTable_insert___spec__16___
 lean_object* l_Lean_Elab_registerBuiltinMacroAttr___lambda__1___closed__1;
 lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
 extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__2;
+lean_object* l_finally___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Util_2__throwUnexpectedElabType___rarg___closed__3;
 lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Elab_mkElabAttributeAux___spec__3___rarg___closed__1;
 lean_object* l_Lean_Elab_ElabAttributeExtensionState_inhabited___closed__1;
@ -160,7 +161,7 @@ lean_object* l_Nat_repr(lean_object*);
 lean_object* l___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Char_HasRepr___closed__1;
 lean_object* l_Lean_Elab_registerBuiltinMacroAttr___lambda__1___closed__4;
-lean_object* l_Lean_Elab_getMacros(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_getMacros(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_PersistentHashMap_insertAux___main___rarg___closed__3;
 lean_object* l_Lean_Syntax_prettyPrint(lean_object*);
 lean_object* l_mkHashMap___at_Lean_Elab_mkBuiltinMacroFnTable___spec__2(lean_object*);
@ -174,7 +175,7 @@ lean_object* l_List_foldl___main___at_Lean_Elab_addMacroStack___spec__1___closed
 lean_object* lean_eval_const(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_registerBuiltinMacroAttr___lambda__1___closed__3;
 lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Elab_mkElabAttributeAux___spec__3___rarg___closed__2;
-lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at_Lean_Elab_mkElabAttributeAux___spec__2(lean_object*);
 lean_object* l_Lean_SMap_empty___at_Lean_Elab_ElabAttributeExtensionState_inhabited___spec__1___closed__1;
 lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Elab_mkElabAttributeAux___spec__3___rarg(lean_object*, lean_object*);
@ -238,7 +239,7 @@ lean_object* l_Lean_Elab_syntaxNodeKindOfAttrParam___boxed(lean_object*, lean_ob
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
 lean_object* l_PersistentHashMap_find_x3f___at_Lean_Elab_getMacros___spec__2(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_registerBuiltinMacroAttr___closed__2;
-lean_object* l_Lean_Elab_getMacros___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_getMacros___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_insertAux___main___at_Lean_Elab_ElabFnTable_insert___spec__11___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_ElabAttribute_inhabited___closed__3;
 lean_object* l_Lean_Elab_macroAttribute;
@ -253,7 +254,7 @@ uint8_t l_USize_decLe(size_t, size_t);
 lean_object* l_HashMapImp_insert___at_Lean_Elab_ElabFnTable_insert___spec__25___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_mkElabAttribute(lean_object*);
 lean_object* l_AssocList_foldlM___main___at_Lean_Elab_ElabFnTable_insert___spec__18___rarg(lean_object*, lean_object*);
-lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(lean_object*, lean_object*, lean_object*);
+lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_nameToExprAux___main(lean_object*);
 lean_object* l_Lean_SMap_empty___at_Lean_Elab_mkBuiltinMacroFnTable___spec__1___closed__2;
@ -348,7 +349,7 @@ lean_object* l_Lean_mkConst(lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_Elab_ElabFnTable_insert___spec__13___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_registerBuiltinMacroAttr___closed__4;
-lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns(lean_object*, lean_object*, lean_object*);
+lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__4;
 extern lean_object* l_Lean_initAttr;
 lean_object* l_Array_iterateMAux___main___at_Lean_Elab_ElabFnTable_insert___spec__24(lean_object*);
@ -6217,50 +6218,57 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
 if (lean_obj_tag(x_2) == 0)
 {
-lean_object* x_4; 
+lean_object* x_5; lean_object* x_6; 
 lean_dec(x_3);
 lean_dec(x_1);
-x_4 = l_Lean_Macro_throwUnsupported___closed__1;
-return x_4;
+x_5 = lean_box(1);
+x_6 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_6, 0, x_5);
+lean_ctor_set(x_6, 1, x_4);
+return x_6;
 }
 else
 {
-lean_object* x_5; lean_object* x_6; lean_object* x_7; 
-x_5 = lean_ctor_get(x_2, 0);
-lean_inc(x_5);
-x_6 = lean_ctor_get(x_2, 1);
-lean_inc(x_6);
+lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+x_7 = lean_ctor_get(x_2, 0);
+lean_inc(x_7);
+x_8 = lean_ctor_get(x_2, 1);
+lean_inc(x_8);
 lean_dec(x_2);
 lean_inc(x_3);
 lean_inc(x_1);
-x_7 = lean_apply_2(x_5, x_1, x_3);
-if (lean_obj_tag(x_7) == 0)
+x_9 = lean_apply_3(x_7, x_1, x_3, x_4);
+if (lean_obj_tag(x_9) == 0)
 {
-lean_dec(x_7);
-x_2 = x_6;
-goto _start;
+lean_dec(x_8);
+lean_dec(x_3);
+lean_dec(x_1);
+return x_9;
 }
 else
 {
-lean_dec(x_6);
-lean_dec(x_3);
-lean_dec(x_1);
-return x_7;
+lean_object* x_10; 
+x_10 = lean_ctor_get(x_9, 1);
+lean_inc(x_10);
+lean_dec(x_9);
+x_2 = x_8;
+x_4 = x_10;
+goto _start;
 }
 }
 }
 }
-lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
-lean_object* x_4; 
-x_4 = l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(x_1, x_2, x_3);
-return x_4;
+lean_object* x_5; 
+x_5 = l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(x_1, x_2, x_3, x_4);
+return x_5;
 }
 }
 lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Elab_getMacros___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
@ -6481,38 +6489,41 @@ return x_9;
 }
 }
 }
-lean_object* l_Lean_Elab_getMacros(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_Elab_getMacros(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
-lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
 lean_inc(x_2);
-x_4 = l_Lean_Syntax_getKind(x_2);
-x_5 = l_Lean_Elab_macroAttribute;
-x_6 = lean_ctor_get(x_5, 1);
-lean_inc(x_6);
-x_7 = l_Lean_PersistentEnvExtension_getState___rarg(x_6, x_1);
-lean_dec(x_6);
-x_8 = lean_ctor_get(x_7, 1);
-lean_inc(x_8);
+x_5 = l_Lean_Syntax_getKind(x_2);
+x_6 = l_Lean_Elab_macroAttribute;
+x_7 = lean_ctor_get(x_6, 1);
+lean_inc(x_7);
+x_8 = l_Lean_PersistentEnvExtension_getState___rarg(x_7, x_1);
 lean_dec(x_7);
-x_9 = l_Lean_SMap_find_x3f___at_Lean_Elab_getMacros___spec__1(x_8, x_4);
-lean_dec(x_4);
-if (lean_obj_tag(x_9) == 0)
+x_9 = lean_ctor_get(x_8, 1);
+lean_inc(x_9);
+lean_dec(x_8);
+x_10 = l_Lean_SMap_find_x3f___at_Lean_Elab_getMacros___spec__1(x_9, x_5);
+lean_dec(x_5);
+if (lean_obj_tag(x_10) == 0)
 {
-lean_object* x_10; 
+lean_object* x_11; lean_object* x_12; 
 lean_dec(x_3);
 lean_dec(x_2);
-x_10 = l_Lean_Macro_throwUnsupported___closed__1;
-return x_10;
+x_11 = lean_box(1);
+x_12 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_12, 0, x_11);
+lean_ctor_set(x_12, 1, x_4);
+return x_12;
 }
 else
 {
-lean_object* x_11; lean_object* x_12; 
-x_11 = lean_ctor_get(x_9, 0);
-lean_inc(x_11);
-lean_dec(x_9);
-x_12 = l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(x_2, x_11, x_3);
-return x_12;
+lean_object* x_13; lean_object* x_14; 
+x_13 = lean_ctor_get(x_10, 0);
+lean_inc(x_13);
+lean_dec(x_10);
+x_14 = l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(x_2, x_13, x_3, x_4);
+return x_14;
 }
 }
 }
@ -6576,90 +6587,114 @@ lean_dec(x_2);
 return x_3;
 }
 }
-lean_object* l_Lean_Elab_getMacros___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_Elab_getMacros___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
-lean_object* x_4; 
-x_4 = l_Lean_Elab_getMacros(x_1, x_2, x_3);
+lean_object* x_5; 
+x_5 = l_Lean_Elab_getMacros(x_1, x_2, x_3, x_4);
 lean_dec(x_1);
-return x_4;
+return x_5;
 }
 }
-lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
 _start:
 {
-lean_object* x_7; lean_object* x_8; lean_object* x_9; 
-x_7 = lean_environment_main_module(x_6);
-x_8 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_8, 0, x_7);
-lean_ctor_set(x_8, 1, x_1);
-lean_inc(x_3);
-x_9 = lean_apply_2(x_2, x_3, x_8);
-if (lean_obj_tag(x_9) == 0)
+lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_9 = lean_environment_main_module(x_1);
+x_10 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_10, 0, x_9);
+lean_ctor_set(x_10, 1, x_2);
+lean_inc(x_4);
+x_11 = lean_apply_3(x_3, x_4, x_10, x_8);
+if (lean_obj_tag(x_11) == 0)
 {
-lean_object* x_10; 
-lean_dec(x_5);
-x_10 = lean_ctor_get(x_9, 0);
-lean_inc(x_10);
-lean_dec(x_9);
-if (lean_obj_tag(x_10) == 0)
-{
-lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
-x_11 = lean_ctor_get(x_10, 0);
-lean_inc(x_11);
-lean_dec(x_10);
-x_12 = lean_ctor_get(x_4, 2);
+lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+lean_dec(x_4);
+x_12 = lean_ctor_get(x_11, 0);
 lean_inc(x_12);
-lean_dec(x_4);
-x_13 = lean_alloc_ctor(2, 1, 0);
-lean_ctor_set(x_13, 0, x_11);
-x_14 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_14, 0, x_13);
-x_15 = lean_apply_3(x_12, lean_box(0), x_3, x_14);
-return x_15;
-}
-else
-{
-lean_object* x_16; lean_object* x_17; 
-lean_dec(x_3);
-x_16 = lean_ctor_get(x_4, 3);
-lean_inc(x_16);
-lean_dec(x_4);
-x_17 = lean_apply_1(x_16, lean_box(0));
+x_13 = lean_ctor_get(x_11, 1);
+lean_inc(x_13);
+lean_dec(x_11);
+x_14 = lean_ctor_get(x_5, 3);
+lean_inc(x_14);
+lean_dec(x_5);
+x_15 = lean_apply_1(x_14, x_13);
+x_16 = lean_alloc_closure((void*)(l_finally___rarg___lambda__1___boxed), 3, 2);
+lean_closure_set(x_16, 0, x_6);
+lean_closure_set(x_16, 1, x_12);
+x_17 = lean_apply_4(x_7, lean_box(0), lean_box(0), x_15, x_16);
 return x_17;
 }
+else
+{
+lean_object* x_18; 
+lean_dec(x_7);
+lean_dec(x_6);
+x_18 = lean_ctor_get(x_11, 0);
+lean_inc(x_18);
+lean_dec(x_11);
+if (lean_obj_tag(x_18) == 0)
+{
+lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
+x_19 = lean_ctor_get(x_18, 0);
+lean_inc(x_19);
+lean_dec(x_18);
+x_20 = lean_ctor_get(x_5, 4);
+lean_inc(x_20);
+lean_dec(x_5);
+x_21 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_21, 0, x_19);
+x_22 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_22, 0, x_21);
+x_23 = lean_apply_3(x_20, lean_box(0), x_4, x_22);
+return x_23;
 }
 else
 {
-lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; 
+lean_object* x_24; lean_object* x_25; 
 lean_dec(x_4);
-lean_dec(x_3);
-x_18 = lean_ctor_get(x_9, 0);
-lean_inc(x_18);
-lean_dec(x_9);
-x_19 = lean_ctor_get(x_5, 0);
-lean_inc(x_19);
+x_24 = lean_ctor_get(x_5, 5);
+lean_inc(x_24);
 lean_dec(x_5);
-x_20 = lean_ctor_get(x_19, 1);
-lean_inc(x_20);
-lean_dec(x_19);
-x_21 = lean_apply_2(x_20, lean_box(0), x_18);
-return x_21;
+x_25 = lean_apply_1(x_24, lean_box(0));
+return x_25;
 }
 }
 }
-lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+}
+lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; 
+x_8 = lean_ctor_get(x_1, 2);
+lean_inc(x_8);
+lean_inc(x_6);
+x_9 = lean_alloc_closure((void*)(l_Lean_Elab_adaptMacro___rarg___lambda__1), 8, 7);
+lean_closure_set(x_9, 0, x_7);
+lean_closure_set(x_9, 1, x_2);
+lean_closure_set(x_9, 2, x_3);
+lean_closure_set(x_9, 3, x_4);
+lean_closure_set(x_9, 4, x_1);
+lean_closure_set(x_9, 5, x_5);
+lean_closure_set(x_9, 6, x_6);
+x_10 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_8, x_9);
+return x_10;
+}
+}
+lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
 lean_object* x_7; lean_object* x_8; lean_object* x_9; 
 x_7 = lean_ctor_get(x_1, 0);
 lean_inc(x_7);
-x_8 = lean_alloc_closure((void*)(l_Lean_Elab_adaptMacro___rarg___lambda__1), 6, 5);
-lean_closure_set(x_8, 0, x_6);
-lean_closure_set(x_8, 1, x_2);
-lean_closure_set(x_8, 2, x_3);
-lean_closure_set(x_8, 3, x_1);
+lean_inc(x_5);
+x_8 = lean_alloc_closure((void*)(l_Lean_Elab_adaptMacro___rarg___lambda__2), 7, 6);
+lean_closure_set(x_8, 0, x_1);
+lean_closure_set(x_8, 1, x_6);
+lean_closure_set(x_8, 2, x_2);
+lean_closure_set(x_8, 3, x_3);
 lean_closure_set(x_8, 4, x_4);
+lean_closure_set(x_8, 5, x_5);
 x_9 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_7, x_8);
 return x_9;
 }
@ -6673,7 +6708,7 @@ lean_inc(x_5);
 x_6 = lean_ctor_get(x_2, 1);
 lean_inc(x_6);
 lean_inc(x_5);
-x_7 = lean_alloc_closure((void*)(l_Lean_Elab_adaptMacro___rarg___lambda__2), 6, 5);
+x_7 = lean_alloc_closure((void*)(l_Lean_Elab_adaptMacro___rarg___lambda__3), 6, 5);
 lean_closure_set(x_7, 0, x_2);
 lean_closure_set(x_7, 1, x_3);
 lean_closure_set(x_7, 2, x_4);
--- a/stage0/stdlib/Init/LeanInit.c
+++ b/stage0/stdlib/Init/LeanInit.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.LeanInit
-// Imports: Init.Data.String.Basic Init.Data.Array.Basic Init.Data.UInt Init.Data.Hashable Init.Control.Reader Init.Control.Except
+// Imports: Init.Data.String.Basic Init.Data.Array.Basic Init.Data.UInt Init.Data.Hashable Init.Control.Reader Init.Control.EState
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -31,7 +31,6 @@ lean_object* l___private_Init_LeanInit_1__eraseMacroScopesAux___main___closed__1
 lean_object* l_Lean_MacroM_monadQuotation;
 lean_object* l_Lean_Name_eraseMacroScopes(lean_object*);
 lean_object* l_Lean_Syntax_isNatLitAux(lean_object*, lean_object*);
-lean_object* l_Lean_Macro_throwUnsupported___closed__1;
 lean_object* l_Array_mapSepElemsM___boxed(lean_object*);
 lean_object* lean_mk_empty_array_with_capacity(lean_object*);
 lean_object* l___private_Init_LeanInit_12__decodeQuotedChar___boxed__const__1;
@ -47,7 +46,7 @@ lean_object* l_Lean_Macro_throwUnsupported___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_identKind___closed__1;
 lean_object* l_Lean_fieldIdxKind___closed__2;
 lean_object* l_Lean_Syntax_getOptional_x3f(lean_object*);
-lean_object* l_Lean_MacroM_monadQuotation___lambda__2(lean_object*);
+lean_object* l_Lean_MacroM_monadQuotation___lambda__2(lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_8__decodeHexDigit___boxed(lean_object*, lean_object*);
 uint32_t l_Lean_idBeginEscape;
 lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___boxed(lean_object*);
@ -79,6 +78,7 @@ lean_object* l___private_Init_LeanInit_7__decodeOctalLitAux(lean_object*, lean_o
 lean_object* l_Lean_isIdRest___boxed(lean_object*);
 lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
 uint8_t l_Lean_isIdBeginEscape(uint32_t);
+lean_object* l_Lean_Macro_withFreshMacroScope(lean_object*);
 lean_object* l___private_Init_LeanInit_9__decodeHexLitAux___main(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_HasToString___closed__1;
 lean_object* l_Lean_mkNameSimple(lean_object*);
@ -137,7 +137,6 @@ lean_object* l_Lean_mkStxNumLit(lean_object*, lean_object*);
 lean_object* l_Lean_Name_HasAppend___closed__1;
 lean_object* l_Array_mapSepElems___boxed(lean_object*, lean_object*);
 uint8_t l_Lean_Name_hasMacroScopes(lean_object*);
-lean_object* l_Lean_MacroM_monadQuotation___lambda__3(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_isLit_x3f(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_termIdToAntiquot___closed__4;
 lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main___at_Array_mapSepElems___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
@ -154,7 +153,7 @@ lean_object* l___private_Init_LeanInit_7__decodeOctalLitAux___boxed(lean_object*
 lean_object* l_Array_mapSepElemsM(lean_object*);
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l_Lean_choiceKind___closed__2;
-lean_object* l_Lean_MacroM_monadQuotation___lambda__2___boxed(lean_object*);
+lean_object* l_Lean_MacroM_monadQuotation___lambda__2___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_strLitKind;
 lean_object* l_Lean_Syntax_isStrLit_x3f(lean_object*);
 lean_object* l_Array_getSepElems(lean_object*);
@ -164,7 +163,7 @@ lean_object* l_Lean_Syntax_getId___boxed(lean_object*);
 lean_object* l___private_Init_LeanInit_13__decodeNameLitAux(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_isFieldIdx_x3f(lean_object*);
 lean_object* l_Substring_takeWhileAux___main___at___private_Init_LeanInit_13__decodeNameLitAux___main___spec__2(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Macro_addMacroScope(lean_object*, lean_object*);
+lean_object* l_Lean_Macro_addMacroScope(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_14__filterSepElemsMAux___main___at_Array_filterSepElems___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkTermIdFrom___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getHeadInfo(lean_object*);
@ -243,7 +242,7 @@ uint8_t l_UInt32_decEq(uint32_t, uint32_t);
 lean_object* l_Lean_Syntax_inhabited;
 lean_object* l_Lean_mkAppStx___closed__5;
 lean_object* l_Lean_mkHole(lean_object*);
-lean_object* l_Lean_MacroM_monadQuotation___lambda__1___boxed(lean_object*);
+lean_object* l_Lean_MacroM_monadQuotation___lambda__1___boxed(lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_3__extractImported(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_5__extractMacroScopesAux___main(lean_object*, lean_object*);
 uint8_t l_Lean_Syntax_hasArgs(lean_object*);
@ -265,6 +264,7 @@ lean_object* l_Lean_Syntax_getHeadInfo___boxed(lean_object*);
 lean_object* l___private_Init_LeanInit_11__decodeNatLitVal___boxed(lean_object*);
 lean_object* l___private_Init_LeanInit_11__decodeNatLitVal___closed__1;
 lean_object* l_Lean_Syntax_getOptionalIdent_x3f(lean_object*);
+lean_object* l_Lean_Macro_throwUnsupported___rarg(lean_object*);
 extern lean_object* l___private_Init_Util_1__mkPanicMessage___closed__2;
 lean_object* l___private_Init_LeanInit_7__decodeOctalLitAux___main(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_NameGenerator_curr(lean_object*);
@ -305,6 +305,7 @@ lean_object* l_Lean_ParserDescr_inhabited;
 lean_object* l_Lean_Syntax_decodeNameLit___boxed(lean_object*);
 lean_object* lean_string_length(lean_object*);
 lean_object* l_Lean_MacroM_monadQuotation___closed__1;
+lean_object* l_Lean_Macro_withFreshMacroScope___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_nameLitKind___closed__2;
 uint8_t l_Lean_isSubScriptAlnum(uint32_t);
 lean_object* l_List_foldl___main___at_Lean_MacroScopesView_review___spec__1(lean_object*, lean_object*);
@ -331,7 +332,7 @@ lean_object* l___private_Init_LeanInit_14__filterSepElemsMAux___main___rarg___la
 lean_object* l_Array_filterSepElemsM___at_Array_filterSepElems___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_9__decodeHexLitAux(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_MacroM_monadQuotation___lambda__1(lean_object*);
+lean_object* l_Lean_MacroM_monadQuotation___lambda__1(lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_14__filterSepElemsMAux___boxed(lean_object*);
 uint8_t l_UInt32_decLe(uint32_t, uint32_t);
 lean_object* l_Lean_mkAppStx___closed__2;
@ -2616,36 +2617,38 @@ return x_35;
 }
 }
 }
-lean_object* l_Lean_Macro_addMacroScope(lean_object* x_1, lean_object* x_2) {
+lean_object* l_Lean_Macro_addMacroScope(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_3 = lean_ctor_get(x_2, 0);
-lean_inc(x_3);
-x_4 = lean_ctor_get(x_2, 1);
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+x_4 = lean_ctor_get(x_2, 0);
 lean_inc(x_4);
+x_5 = lean_ctor_get(x_2, 1);
+lean_inc(x_5);
 lean_dec(x_2);
-x_5 = l_Lean_addMacroScope(x_3, x_1, x_4);
-x_6 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_6, 0, x_5);
-return x_6;
+x_6 = l_Lean_addMacroScope(x_4, x_1, x_5);
+x_7 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_7, 0, x_6);
+lean_ctor_set(x_7, 1, x_3);
+return x_7;
 }
 }
-lean_object* _init_l_Lean_Macro_throwUnsupported___closed__1() {
+lean_object* l_Lean_Macro_throwUnsupported___rarg(lean_object* x_1) {
 _start:
 {
-lean_object* x_1; lean_object* x_2; 
-x_1 = lean_box(1);
-x_2 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_2, 0, x_1);
-return x_2;
+lean_object* x_2; lean_object* x_3; 
+x_2 = lean_box(1);
+x_3 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_3, 0, x_2);
+lean_ctor_set(x_3, 1, x_1);
+return x_3;
 }
 }
 lean_object* l_Lean_Macro_throwUnsupported(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = l_Lean_Macro_throwUnsupported___closed__1;
+x_3 = lean_alloc_closure((void*)(l_Lean_Macro_throwUnsupported___rarg), 1, 0);
 return x_3;
 }
 }
@ -2658,33 +2661,65 @@ lean_dec(x_2);
 return x_3;
 }
 }
-lean_object* l_Lean_MacroM_monadQuotation___lambda__1(lean_object* x_1) {
+lean_object* l_Lean_Macro_withFreshMacroScope___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; 
-x_2 = lean_ctor_get(x_1, 1);
-lean_inc(x_2);
-x_3 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_3, 0, x_2);
-return x_3;
+lean_object* x_4; lean_object* x_5; uint8_t x_6; 
+x_4 = lean_unsigned_to_nat(1u);
+x_5 = lean_nat_add(x_3, x_4);
+x_6 = !lean_is_exclusive(x_2);
+if (x_6 == 0)
+{
+lean_object* x_7; lean_object* x_8; 
+x_7 = lean_ctor_get(x_2, 1);
+lean_dec(x_7);
+lean_ctor_set(x_2, 1, x_3);
+x_8 = lean_apply_2(x_1, x_2, x_5);
+return x_8;
+}
+else
+{
+lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_9 = lean_ctor_get(x_2, 0);
+lean_inc(x_9);
+lean_dec(x_2);
+x_10 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_10, 0, x_9);
+lean_ctor_set(x_10, 1, x_3);
+x_11 = lean_apply_2(x_1, x_10, x_5);
+return x_11;
 }
 }
-lean_object* l_Lean_MacroM_monadQuotation___lambda__2(lean_object* x_1) {
+}
+lean_object* l_Lean_Macro_withFreshMacroScope(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; 
-x_2 = lean_ctor_get(x_1, 0);
-lean_inc(x_2);
-x_3 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_3, 0, x_2);
-return x_3;
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Macro_withFreshMacroScope___rarg), 3, 0);
+return x_2;
 }
 }
-lean_object* l_Lean_MacroM_monadQuotation___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_MacroM_monadQuotation___lambda__1(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_4; 
-x_4 = lean_apply_1(x_2, x_3);
+lean_object* x_3; lean_object* x_4; 
+x_3 = lean_ctor_get(x_1, 1);
+lean_inc(x_3);
+x_4 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_4, 0, x_3);
+lean_ctor_set(x_4, 1, x_2);
+return x_4;
+}
+}
+lean_object* l_Lean_MacroM_monadQuotation___lambda__2(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; 
+x_3 = lean_ctor_get(x_1, 0);
+lean_inc(x_3);
+x_4 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_4, 0, x_3);
+lean_ctor_set(x_4, 1, x_2);
 return x_4;
 }
 }
@ -2692,7 +2727,7 @@ lean_object* _init_l_Lean_MacroM_monadQuotation___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_MacroM_monadQuotation___lambda__1___boxed), 1, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_MacroM_monadQuotation___lambda__1___boxed), 2, 0);
 return x_1;
 }
 }
@ -2700,7 +2735,7 @@ lean_object* _init_l_Lean_MacroM_monadQuotation___closed__2() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_MacroM_monadQuotation___lambda__2___boxed), 1, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_MacroM_monadQuotation___lambda__2___boxed), 2, 0);
 return x_1;
 }
 }
@ -2708,7 +2743,7 @@ lean_object* _init_l_Lean_MacroM_monadQuotation___closed__3() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_MacroM_monadQuotation___lambda__3), 3, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_Macro_withFreshMacroScope), 1, 0);
 return x_1;
 }
 }
@ -2734,22 +2769,22 @@ x_1 = l_Lean_MacroM_monadQuotation___closed__4;
 return x_1;
 }
 }
-lean_object* l_Lean_MacroM_monadQuotation___lambda__1___boxed(lean_object* x_1) {
+lean_object* l_Lean_MacroM_monadQuotation___lambda__1___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_2; 
-x_2 = l_Lean_MacroM_monadQuotation___lambda__1(x_1);
+lean_object* x_3; 
+x_3 = l_Lean_MacroM_monadQuotation___lambda__1(x_1, x_2);
 lean_dec(x_1);
-return x_2;
+return x_3;
 }
 }
-lean_object* l_Lean_MacroM_monadQuotation___lambda__2___boxed(lean_object* x_1) {
+lean_object* l_Lean_MacroM_monadQuotation___lambda__2___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_2; 
-x_2 = l_Lean_MacroM_monadQuotation___lambda__2(x_1);
+lean_object* x_3; 
+x_3 = l_Lean_MacroM_monadQuotation___lambda__2(x_1, x_2);
 lean_dec(x_1);
-return x_2;
+return x_3;
 }
 }
 lean_object* l_Lean_mkIdentFrom(lean_object* x_1, lean_object* x_2) {
@ -6489,7 +6524,7 @@ lean_object* initialize_Init_Data_Array_Basic(lean_object*);
 lean_object* initialize_Init_Data_UInt(lean_object*);
 lean_object* initialize_Init_Data_Hashable(lean_object*);
 lean_object* initialize_Init_Control_Reader(lean_object*);
-lean_object* initialize_Init_Control_Except(lean_object*);
+lean_object* initialize_Init_Control_EState(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_LeanInit(lean_object* w) {
 lean_object * res;
@ -6510,7 +6545,7 @@ lean_dec_ref(res);
 res = initialize_Init_Control_Reader(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = initialize_Init_Control_Except(lean_io_mk_world());
+res = initialize_Init_Control_EState(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 l_Lean_idBeginEscape = _init_l_Lean_idBeginEscape();
@ -6617,8 +6652,6 @@ l_Lean_MacroScopesView_inhabited___closed__1 = _init_l_Lean_MacroScopesView_inha
 lean_mark_persistent(l_Lean_MacroScopesView_inhabited___closed__1);
 l_Lean_MacroScopesView_inhabited = _init_l_Lean_MacroScopesView_inhabited();
 lean_mark_persistent(l_Lean_MacroScopesView_inhabited);
-l_Lean_Macro_throwUnsupported___closed__1 = _init_l_Lean_Macro_throwUnsupported___closed__1();
-lean_mark_persistent(l_Lean_Macro_throwUnsupported___closed__1);
 l_Lean_MacroM_monadQuotation___closed__1 = _init_l_Lean_MacroM_monadQuotation___closed__1();
 lean_mark_persistent(l_Lean_MacroM_monadQuotation___closed__1);
 l_Lean_MacroM_monadQuotation___closed__2 = _init_l_Lean_MacroM_monadQuotation___closed__2();