chore: update stage0

2020-01-16 11:35:35 -08:00 · 2020-01-16 11:35:35 -08:00 · 0bc637018c
commit 0bc637018c
parent 685e0f619b
18 changed files with 10413 additions and 2584 deletions
--- a/stage0/src/Init/Lean/Elab/Command.lean
+++ b/stage0/src/Init/Lean/Elab/Command.lean
@ -175,14 +175,14 @@ ctx ← read; s ← get;
 when (ctx.currRecDepth == s.maxRecDepth) $ throwError ref maxRecDepthErrorMessage;
 adaptReader (fun (ctx : Context) => { currRecDepth := ctx.currRecDepth + 1, .. ctx }) x

-private def elabCommandUsing (stx : Syntax) : List CommandElab → CommandElabM Unit
+private def elabCommandUsing (s : State) (stx : Syntax) : List CommandElab → CommandElabM Unit
 | []                => do
  let refFmt := stx.prettyPrint;
  throwError stx ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
 | (elabFn::elabFns) => catch (elabFn stx)
  (fun ex => match ex with
    | Exception.error _           => throw ex
-    | Exception.unsupportedSyntax => elabCommandUsing elabFns)
+    | Exception.unsupportedSyntax => do set s; elabCommandUsing elabFns)

 /- Elaborate `x` with `stx` on the macro stack -/
@[inline] def withMacroExpansion {α} (stx : Syntax) (x : CommandElabM α) : CommandElabM α :=
@ -190,25 +190,24 @@ adaptReader (fun (ctx : Context) => { macroStack := stx :: ctx.macroStack, .. ct

 partial def elabCommand : Syntax → CommandElabM Unit
 | stx => withIncRecDepth stx $ withFreshMacroScope $ match stx with
-  | Syntax.node _ _ => do
-    trace `Elab.step stx $ fun _ => stx;
-    s ← get;
-    let table := (commandElabAttribute.ext.getState s.env).table;
-    let k := stx.getKind;
-    match table.find? k with
-    | some elabFns => elabCommandUsing stx elabFns
-    | none         => do
-      scp ← getCurrMacroScope;
-      env ← getEnv;
-      match expandMacro env stx scp with
-      | some stx' => withMacroExpansion stx $
-        if stx'.getKind == nullKind then
-          -- list of commands => elaborate in order
-          -- The parser will only ever return a single command at a time, but syntax quotations can return multiple ones
-          stx'.getArgs.forM elabCommand
-        else
-          elabCommand stx'
-      | none      => throwError stx ("command '" ++ toString k ++ "' has not been implemented")
+  | Syntax.node k args =>
+    if k == nullKind then
+      -- list of commands => elaborate in order
+      -- The parser will only ever return a single command at a time, but syntax quotations can return multiple ones
+      args.forM elabCommand
+    else do
+      trace `Elab.step stx $ fun _ => stx;
+      s ← get;
+      let table := (commandElabAttribute.ext.getState s.env).table;
+      let k := stx.getKind;
+      match table.find? k with
+      | some elabFns => elabCommandUsing s stx elabFns
+      | none         => do
+        scp ← getCurrMacroScope;
+        env ← getEnv;
+        match expandMacro env stx scp with
+        | some stx' => withMacroExpansion stx $ elabCommand stx'
+        | none      => throwError stx ("command '" ++ toString k ++ "' has not been implemented")
  | _ => throwError stx "unexpected command"

 /-- Adapt a syntax transformation to a regular, command-producing elaborator. -/
--- a/stage0/src/Init/Lean/Elab/Quotation.lean
+++ b/stage0/src/Init/Lean/Elab/Quotation.lean
@ -108,10 +108,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
  let preresolved := resolveGlobalName env currNamespace openDecls val ++ preresolved;
  let val := quote val;
  -- `scp` is bound in stxQuot.expand
-  val ← `(addMacroScope $val scp);
-  let args := quote preresolved;
-  -- TODO: simplify quotations when we're no longer limited by name resolution in the old frontend
-  `(Syntax.ident none (String.toSubstring $(quote (toString rawVal))) $val $args)
+  `(Syntax.ident none (String.toSubstring $(quote (toString rawVal))) (addMacroScope $val scp) $(quote preresolved))
 -- if antiquotation, insert contents as-is, else recurse
 | stx@(Syntax.node k args) =>
  if isAntiquot stx then
--- a/stage0/src/Init/Lean/Elab/Syntax.lean
+++ b/stage0/src/Init/Lean/Elab/Syntax.lean
@ -182,7 +182,61 @@ adaptExpander $ fun stx => match_syntax stx with
 /- We just ignore Lean3 notation declaration commands. -/
@[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure ()
@[builtinCommandElab «reserve»] def elabReserve : CommandElab := fun _ => pure ()
-@[builtinCommandElab «notation»] def elabNotation : CommandElab := fun _ => pure ()
+
+-- wrap all occurrences of the given `ident` nodes in antiquotations
+private partial def antiquote (vars : Array Syntax) : Syntax → Syntax
+| stx => match_syntax stx with
+| `($id:ident) => if (vars.findIdx? (fun var => var.getId == id.getId)).isSome then Syntax.node `antiquot #[mkAtom "$", Unhygienic.run `($id:ident), mkNullNode, mkNullNode] else stx
+| _ => match stx with
+  | Syntax.node k args => Syntax.node k (args.map antiquote)
+  | stx => stx
+
+/- Convert `notation` command lhs item into a `syntax` command item -/
+def expandNotationItemIntoSyntaxItem (stx : Syntax) : CommandElabM Syntax :=
+let k := stx.getKind;
+if k == `Lean.Parser.Command.identPrec then
+  pure $ Syntax.node `Lean.Parser.Syntax.cat #[mkIdentFrom stx `term,  stx.getArg 1]
+else if k == `Lean.Parser.Command.quotedSymbolPrec then
+  match (stx.getArg 0).getArg 1 with
+  | Syntax.atom info val => pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit val info, stx.getArg 1]
+  | _                    => throwUnsupportedSyntax
+else if k == `Lean.Parser.Command.strLitPrec then
+  pure $ Syntax.node `Lean.Parser.Syntax.atom stx.getArgs
+else
+  throwUnsupportedSyntax
+
+/- Convert `notation` command lhs item a pattern element -/
+def expandNotationItemIntoPattern (stx : Syntax) : CommandElabM Syntax :=
+let k := stx.getKind;
+if k == `Lean.Parser.Command.identPrec then
+  let item := stx.getArg 0;
+  pure $ mkNode `antiquot #[mkAtom "$", Term.mkTermIdFromIdent item, mkNullNode, mkNullNode]
+else if k == `Lean.Parser.Command.quotedSymbolPrec then
+  pure $ (stx.getArg 0).getArg 1
+else if k == `Lean.Parser.Command.strLitPrec then
+  match (stx.getArg 0).isStrLit? with
+  | some str => pure $ mkAtomFrom stx str
+  | none     => throwUnsupportedSyntax
+else
+  throwUnsupportedSyntax
+
+@[builtinCommandElab «notation»] def elabNotation : CommandElab :=
+adaptExpander $ fun stx => match_syntax stx with
+| `(notation $items* := $rhs) => do
+  -- build parser
+  syntaxParts ← items.mapM expandNotationItemIntoSyntaxItem;
+  let cat := mkIdentFrom stx `term;
+  -- build macro
+  let vars := items.filter $ fun item => item.getKind == `Lean.Parser.Command.identPrec;
+  let vars := vars.map $ fun var => var.getArg 0;
+  let rhs := antiquote vars rhs;
+  patArgs ← items.mapM expandNotationItemIntoPattern;
+  scp ← getCurrMacroScope;
+  -- manually create hygienic kind name
+  let kind := addMacroScope `myParser scp;
+  let pat := Syntax.node kind patArgs;
+  `(syntax [$(mkIdentFrom stx kind)] $syntaxParts* : $cat macro | `($pat) => `($rhs))
+| _ => throwUnsupportedSyntax

 end Command
 end Elab
--- a/stage0/src/Init/Lean/Elab/Tactic.lean
+++ b/stage0/src/Init/Lean/Elab/Tactic.lean
@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Init.Lean.Elab.Term
+import Init.Lean.Elab.Tactic.Basic

 namespace Lean
 namespace Elab
--- a/stage0/src/Init/Lean/Elab/Tactic/Basic.lean
+++ b/stage0/src/Init/Lean/Elab/Tactic/Basic.lean
@ -0,0 +1,149 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich
+-/
+prelude
+import Init.Lean.Elab.Util
+import Init.Lean.Elab.Term
+
+namespace Lean
+namespace Elab
+namespace Tactic
+
+structure Context extends toTermCtx : Term.Context :=
+(main : Expr)
+
+structure State extends toTermState : Term.State :=
+(goals : List Expr)
+
+instance State.inhabited : Inhabited State := ⟨{ goals := [], toTermState := arbitrary _ }⟩
+
+abbrev Exception := Elab.Exception
+
+abbrev TacticElabM := ReaderT Context (EStateM Exception State)
+
+abbrev TacticElab := Syntax → TacticElabM Unit
+
+def liftTermElabM {α} (x : TermElabM α) : TacticElabM α :=
+fun ctx s => match x ctx.toTermCtx s.toTermState with
+ | EStateM.Result.ok a newS                         => EStateM.Result.ok a { toTermState := newS, .. s }
+ | EStateM.Result.error (Term.Exception.ex ex) newS => EStateM.Result.error ex { toTermState := newS, .. s }
+ | EStateM.Result.error Term.Exception.postpone _   => unreachable!
+
+def getEnv : TacticElabM Environment := do s ← get; pure s.env
+def getMCtx : TacticElabM MetavarContext := do s ← get; pure s.mctx
+def getLCtx : TacticElabM LocalContext := do ctx ← read; pure ctx.lctx
+def getLocalInsts : TacticElabM LocalInstances := do ctx ← read; pure ctx.localInstances
+def getOptions : TacticElabM Options := do ctx ← read; pure ctx.config.opts
+
+def addContext (msg : MessageData) : TacticElabM MessageData := liftTermElabM $ Term.addContext msg
+
+instance monadLog : MonadLog TacticElabM :=
+{ getCmdPos   := do ctx ← read; pure ctx.cmdPos,
+  getFileMap  := do ctx ← read; pure ctx.fileMap,
+  getFileName := do ctx ← read; pure ctx.fileName,
+  addContext  := addContext,
+  logMessage  := fun msg => modify $ fun s => { messages := s.messages.add msg, .. s } }
+
+def throwError {α} (ref : Syntax) (msgData : MessageData) : TacticElabM α :=  liftTermElabM $ Term.throwError ref msgData
+def throwUnsupportedSyntax {α} : TacticElabM α := liftTermElabM $ Term.throwUnsupportedSyntax
+
+@[inline] def withIncRecDepth {α} (ref : Syntax) (x : TacticElabM α) : TacticElabM α := do
+ctx ← read;
+when (ctx.currRecDepth == ctx.maxRecDepth) $ throwError ref maxRecDepthErrorMessage;
+adaptReader (fun (ctx : Context) => { currRecDepth := ctx.currRecDepth + 1, .. ctx }) x
+
+protected def getCurrMacroScope : TacticElabM MacroScope := do ctx ← read; pure ctx.currMacroScope
+
+@[inline] protected def withFreshMacroScope {α} (x : TacticElabM α) : TacticElabM α := do
+fresh ← modifyGet (fun st => (st.nextMacroScope, { st with nextMacroScope := st.nextMacroScope + 1 }));
+adaptReader (fun (ctx : Context) => { ctx with currMacroScope := fresh }) x
+
+instance monadQuotation : MonadQuotation TacticElabM := {
+  getCurrMacroScope   := Tactic.getCurrMacroScope,
+  withFreshMacroScope := @Tactic.withFreshMacroScope
+}
+
+abbrev TacticElabTable := ElabFnTable TacticElab
+def mkBuiltinTacticElabTable : IO (IO.Ref TacticElabTable) :=  IO.mkRef {}
+@[init mkBuiltinTacticElabTable] constant builtinTacticElabTable : IO.Ref TacticElabTable := arbitrary _
+
+def addBuiltinTacticElab (k : SyntaxNodeKind) (declName : Name) (elab : TacticElab) : IO Unit := do
+m ← builtinTacticElabTable.get;
+when (m.contains k) $
+  throw (IO.userError ("invalid builtin tactic elaborator, elaborator for '" ++ toString k ++ "' has already been defined"));
+builtinTacticElabTable.modify $ fun m => m.insert k elab
+
+def declareBuiltinTacticElab (env : Environment) (kind : SyntaxNodeKind) (declName : Name) : IO Environment :=
+let name := `_regBuiltinTacticElab ++ declName;
+let type := mkApp (mkConst `IO) (mkConst `Unit);
+let val  := mkAppN (mkConst `Lean.Elab.Tactic.addBuiltinTacticElab) #[toExpr kind, toExpr declName, mkConst declName];
+let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
+match env.addAndCompile {} decl with
+-- TODO: pretty print error
+| Except.error _ => throw (IO.userError ("failed to emit registration code for builtin tactic elaborator '" ++ toString declName ++ "'"))
+| Except.ok env  => IO.ofExcept (setInitAttr env name)
+
+@[init] def registerBuiltinTacticElabAttr : IO Unit :=
+registerBuiltinAttribute {
+ name  := `builtinTacticElab,
+ descr := "Builtin tactic elaborator",
+ add   := fun env declName arg persistent => do {
+   unless persistent $ throw (IO.userError ("invalid attribute 'builtinTacticElab', must be persistent"));
+   kind ← IO.ofExcept $ syntaxNodeKindOfAttrParam env `Lean.Parser.Tactic arg;
+   match env.find? declName with
+   | none  => throw $ IO.userError "unknown declaration"
+   | some decl =>
+     match decl.type with
+     | Expr.const `Lean.Elab.Tactic.TacticElab _ _ => declareBuiltinTacticElab env kind declName
+     | _ => throw (IO.userError ("unexpected tactic elaborator type at '" ++ toString declName ++ "' `TacticElab` expected"))
+ },
+ applicationTime := AttributeApplicationTime.afterCompilation
+}
+
+abbrev TacticElabAttribute := ElabAttribute TacticElab
+def mkTacticElabAttribute : IO TacticElabAttribute :=
+mkElabAttribute TacticElab `tacticElab `Lean.Parser.Tactic `Lean.Elab.Tactic.TacticElab "tactic" builtinTacticElabTable
+@[init mkTacticElabAttribute] constant tacticElabAttribute : TacticElabAttribute := arbitrary _
+
+def logTrace (cls : Name) (ref : Syntax) (msg : MessageData) : TacticElabM Unit := liftTermElabM $ Term.logTrace cls ref msg
+@[inline] def trace (cls : Name) (ref : Syntax) (msg : Unit → MessageData) : TacticElabM Unit := liftTermElabM $ Term.trace cls ref msg
+@[inline] def traceAtCmdPos (cls : Name) (msg : Unit → MessageData) : TacticElabM Unit := liftTermElabM $ Term.traceAtCmdPos cls msg
+def dbgTrace {α} [HasToString α] (a : α) : TacticElabM Unit :=_root_.dbgTrace (toString a) $ fun _ => pure ()
+
+private def elabTacticUsing (s : State) (stx : Syntax) : List TacticElab → TacticElabM Unit
+| []                => do
+  let refFmt := stx.prettyPrint;
+  throwError stx ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
+| (elabFn::elabFns) => catch (elabFn stx)
+  (fun ex => match ex with
+    | Exception.error _           => throw ex
+    | Exception.unsupportedSyntax => do set s; elabTacticUsing elabFns)
+
+/- Elaborate `x` with `stx` on the macro stack -/
+@[inline] def withMacroExpansion {α} (stx : Syntax) (x : TacticElabM α) : TacticElabM α :=
+adaptReader (fun (ctx : Context) => { macroStack := stx :: ctx.macroStack, .. ctx }) x
+
+partial def elabTactic : Syntax → TacticElabM Unit
+| stx => withIncRecDepth stx $ withFreshMacroScope $ match stx with
+  | Syntax.node k args => do
+    trace `Elab.step stx $ fun _ => stx;
+    s ← get;
+    let table := (tacticElabAttribute.ext.getState s.env).table;
+    let k := stx.getKind;
+    match table.find? k with
+    | some elabFns => elabTacticUsing s stx elabFns
+      | none         => do
+        scp ← getCurrMacroScope;
+        env ← getEnv;
+        match expandMacro env stx scp with
+        | some stx' => withMacroExpansion stx $ elabTactic stx'
+        | none      => throwError stx ("tactic '" ++ toString k ++ "' has not been implemented")
+  | _ => throwError stx "unexpected command"
+
+
+end Tactic
+
+end Elab
+end Lean
--- a/stage0/src/Init/Lean/Elab/Term.lean
+++ b/stage0/src/Init/Lean/Elab/Term.lean
@ -113,7 +113,7 @@ def addContext (msg : MessageData) : TermElabM MessageData := do
 env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions;
 pure (MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msg)

-instance TermElabM.MonadLog : MonadLog TermElabM :=
+instance monadLog : MonadLog TermElabM :=
 { getCmdPos   := do ctx ← read; pure ctx.cmdPos,
  getFileMap  := do ctx ← read; pure ctx.fileMap,
  getFileName := do ctx ← read; pure ctx.fileName,
@ -146,7 +146,7 @@ pure ctx.currMacroScope
 fresh ← modifyGet (fun st => (st.nextMacroScope, { st with nextMacroScope := st.nextMacroScope + 1 }));
 adaptReader (fun (ctx : Context) => { ctx with currMacroScope := fresh }) x

-instance TermElabM.MonadQuotation : MonadQuotation TermElabM := {
+instance monadQuotation : MonadQuotation TermElabM := {
  getCurrMacroScope   := Term.getCurrMacroScope,
  withFreshMacroScope := @Term.withFreshMacroScope
 }
@ -469,7 +469,7 @@ private def elabTermUsing (s : State) (stx : Syntax) (expectedType? : Option Exp
 | (elabFn::elabFns) => catch (elabFn stx expectedType?)
  (fun ex => match ex with
    | Exception.ex (Elab.Exception.error errMsg)    => if errToSorry then exceptionToSorry stx errMsg expectedType? else throw ex
-    | Exception.ex Elab.Exception.unsupportedSyntax => elabTermUsing elabFns
+    | Exception.ex Elab.Exception.unsupportedSyntax => do set s; elabTermUsing elabFns
    | Exception.postpone          =>
      if catchExPostpone then do
        /- If `elab` threw `Exception.postpone`, we reset any state modifications.
--- a/stage0/src/Init/Lean/Parser/Syntax.lean
+++ b/stage0/src/Init/Lean/Parser/Syntax.lean
@ -19,7 +19,7 @@ categoryParser `syntax rbp
 namespace Syntax
 def maxPrec := parser! nonReservedSymbol "max" true
 def precedenceLit : Parser := numLit <|> maxPrec
-def «precedence» := parser! " : " >> precedenceLit
+def «precedence» := parser! ":" >> precedenceLit
@[builtinSyntaxParser] def paren     := parser! "(" >> many1 syntaxParser >> ")"
@[builtinSyntaxParser] def cat       := parser! ident >> optional (try «precedence»)
@[builtinSyntaxParser] def atom      := parser! strLit >> optional (try «precedence»)
--- a/stage0/src/Init/Lean/Parser/Tactic.lean
+++ b/stage0/src/Init/Lean/Parser/Tactic.lean
@ -19,24 +19,22 @@ registerBuiltinDynamicParserAttribute `tacticParser `tactic
@[inline] def tacticParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
 categoryParser `tactic rbp

-def tacticSeq {k : ParserKind} : Parser k :=
-sepBy1 tacticParser "; " true
-
 namespace Tactic

+def seq := parser! sepBy1 tacticParser "; " true
@[builtinTacticParser] def «intro» := parser! nonReservedSymbol "intro " >> optional ident
@[builtinTacticParser] def «intros» := parser! nonReservedSymbol "intros " >> many ident
@[builtinTacticParser] def «assumption» := parser! nonReservedSymbol "assumption"
@[builtinTacticParser] def «apply» := parser! nonReservedSymbol "apply " >> termParser
-@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> tacticSeq >> "end"
-@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> tacticSeq >> "}"
+@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"
+@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"
@[builtinTacticParser] def orelse := tparser! pushLeading >> " <|> " >> tacticParser 1

 end Tactic

 namespace Term

-@[builtinTermParser] def tacticBlock := parser! symbol "begin " appPrec >> tacticSeq >> "end"
+@[builtinTermParser] def tacticBlock := parser! symbol "begin " appPrec >> Tactic.seq >> "end"

 end Term

--- a/stage0/stdlib/CMakeLists.txt
+++ b/stage0/stdlib/CMakeLists.txt
--- a/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
+++ b/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
@ -259,6 +259,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBAnd___closed__2;
 lean_object* l_Lean_Elab_Term_elabDiv___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabDollar___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabLE___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 lean_object* l_Lean_Elab_Term_elabOrElse(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabCons(lean_object*);
 lean_object* l_List_lengthAux___main___rarg(lean_object*, lean_object*);
@ -444,8 +445,8 @@ lean_object* l_Lean_Syntax_getArgs(lean_object*);
 lean_object* l_Lean_Elab_Term_elabLE___closed__4;
 lean_object* l_Lean_Elab_Term_elabOrM___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabIff___closed__1;
+extern lean_object* l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabCons___closed__3;
-extern lean_object* l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 extern lean_object* l_Lean_Parser_Term_paren___elambda__1___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabDollarProj___closed__3;
 lean_object* l_Lean_Elab_Term_elabSubtype___closed__1;
@ -510,7 +511,6 @@ lean_object* l_Lean_Elab_Term_elabAnoymousCtor(lean_object*, lean_object*, lean_
 lean_object* l_Lean_Elab_Term_elabAndThen___closed__2;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabEquiv(lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabEq___closed__3;
-extern lean_object* l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabGE___closed__3;
 lean_object* l_Lean_Elab_Term_elabMapConst___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -1391,9 +1391,9 @@ x_117 = lean_array_push(x_116, x_98);
 x_118 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_118, 0, x_69);
 lean_ctor_set(x_118, 1, x_117);
-x_119 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_119 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_120 = lean_array_push(x_119, x_118);
-x_121 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_121 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_122 = lean_array_push(x_120, x_121);
 x_123 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_124 = lean_alloc_ctor(1, 2, 0);
@ -1477,9 +1477,9 @@ x_167 = lean_array_push(x_166, x_148);
 x_168 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_168, 0, x_69);
 lean_ctor_set(x_168, 1, x_167);
-x_169 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_169 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_170 = lean_array_push(x_169, x_168);
-x_171 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_171 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_172 = lean_array_push(x_170, x_171);
 x_173 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_174 = lean_alloc_ctor(1, 2, 0);
@ -1829,9 +1829,9 @@ x_36 = l_Lean_nullKind___closed__2;
 x_37 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_37, 0, x_36);
 lean_ctor_set(x_37, 1, x_35);
-x_38 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_38 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_39 = lean_array_push(x_38, x_37);
-x_40 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_40 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_41 = lean_array_push(x_39, x_40);
 x_42 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_43 = lean_alloc_ctor(1, 2, 0);
@ -1902,9 +1902,9 @@ x_80 = l_Lean_nullKind___closed__2;
 x_81 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_81, 0, x_80);
 lean_ctor_set(x_81, 1, x_79);
-x_82 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_82 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_83 = lean_array_push(x_82, x_81);
-x_84 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_84 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_85 = lean_array_push(x_83, x_84);
 x_86 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_87 = lean_alloc_ctor(1, 2, 0);
@ -2062,9 +2062,9 @@ x_149 = lean_array_push(x_142, x_148);
 x_150 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_150, 0, x_108);
 lean_ctor_set(x_150, 1, x_149);
-x_151 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_151 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_152 = lean_array_push(x_151, x_150);
-x_153 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_153 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_154 = lean_array_push(x_152, x_153);
 x_155 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_156 = lean_alloc_ctor(1, 2, 0);
@ -2143,9 +2143,9 @@ x_197 = lean_array_push(x_190, x_196);
 x_198 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_198, 0, x_108);
 lean_ctor_set(x_198, 1, x_197);
-x_199 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_199 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_200 = lean_array_push(x_199, x_198);
-x_201 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_201 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_202 = lean_array_push(x_200, x_201);
 x_203 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_204 = lean_alloc_ctor(1, 2, 0);
@ -2845,9 +2845,9 @@ x_29 = lean_array_push(x_21, x_28);
 x_30 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_30, 0, x_27);
 lean_ctor_set(x_30, 1, x_29);
-x_31 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_31 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_32 = lean_array_push(x_31, x_30);
-x_33 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_33 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_34 = lean_array_push(x_32, x_33);
 x_35 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_36 = lean_alloc_ctor(1, 2, 0);
@ -2910,9 +2910,9 @@ x_67 = lean_array_push(x_59, x_66);
 x_68 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_68, 0, x_65);
 lean_ctor_set(x_68, 1, x_67);
-x_69 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_69 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_70 = lean_array_push(x_69, x_68);
-x_71 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_71 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_72 = lean_array_push(x_70, x_71);
 x_73 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_74 = lean_alloc_ctor(1, 2, 0);
@ -3176,9 +3176,9 @@ x_37 = lean_array_push(x_29, x_36);
 x_38 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_38, 0, x_35);
 lean_ctor_set(x_38, 1, x_37);
-x_39 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_39 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_40 = lean_array_push(x_39, x_38);
-x_41 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_41 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_42 = lean_array_push(x_40, x_41);
 x_43 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_44 = lean_alloc_ctor(1, 2, 0);
@ -3240,9 +3240,9 @@ x_75 = lean_array_push(x_67, x_74);
 x_76 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_76, 0, x_73);
 lean_ctor_set(x_76, 1, x_75);
-x_77 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_77 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_78 = lean_array_push(x_77, x_76);
-x_79 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_79 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_80 = lean_array_push(x_78, x_79);
 x_81 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_82 = lean_alloc_ctor(1, 2, 0);
@ -3347,9 +3347,9 @@ x_129 = lean_array_push(x_121, x_128);
 x_130 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_130, 0, x_127);
 lean_ctor_set(x_130, 1, x_129);
-x_131 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_131 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_132 = lean_array_push(x_131, x_130);
-x_133 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_133 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_134 = lean_array_push(x_132, x_133);
 x_135 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_136 = lean_alloc_ctor(1, 2, 0);
@ -3411,9 +3411,9 @@ x_167 = lean_array_push(x_159, x_166);
 x_168 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_168, 0, x_165);
 lean_ctor_set(x_168, 1, x_167);
-x_169 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_169 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_170 = lean_array_push(x_169, x_168);
-x_171 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_171 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_172 = lean_array_push(x_170, x_171);
 x_173 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_174 = lean_alloc_ctor(1, 2, 0);
@ -3559,9 +3559,9 @@ x_236 = lean_array_push(x_229, x_235);
 x_237 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_237, 0, x_204);
 lean_ctor_set(x_237, 1, x_236);
-x_238 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_238 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_239 = lean_array_push(x_238, x_237);
-x_240 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_240 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_241 = lean_array_push(x_239, x_240);
 x_242 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_243 = lean_alloc_ctor(1, 2, 0);
@ -3622,9 +3622,9 @@ x_273 = lean_array_push(x_266, x_272);
 x_274 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_274, 0, x_204);
 lean_ctor_set(x_274, 1, x_273);
-x_275 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_275 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_276 = lean_array_push(x_275, x_274);
-x_277 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_277 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_278 = lean_array_push(x_276, x_277);
 x_279 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_280 = lean_alloc_ctor(1, 2, 0);
@ -3729,9 +3729,9 @@ x_327 = lean_array_push(x_320, x_326);
 x_328 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_328, 0, x_204);
 lean_ctor_set(x_328, 1, x_327);
-x_329 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_329 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_330 = lean_array_push(x_329, x_328);
-x_331 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_331 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_332 = lean_array_push(x_330, x_331);
 x_333 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_334 = lean_alloc_ctor(1, 2, 0);
@ -3792,9 +3792,9 @@ x_364 = lean_array_push(x_357, x_363);
 x_365 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_365, 0, x_204);
 lean_ctor_set(x_365, 1, x_364);
-x_366 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_366 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_367 = lean_array_push(x_366, x_365);
-x_368 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_368 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_369 = lean_array_push(x_367, x_368);
 x_370 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_371 = lean_alloc_ctor(1, 2, 0);
@ -4643,9 +4643,9 @@ x_86 = l_Lean_nullKind___closed__2;
 x_87 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_87, 0, x_86);
 lean_ctor_set(x_87, 1, x_85);
-x_88 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_88 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_89 = lean_array_push(x_88, x_87);
-x_90 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_90 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_91 = lean_array_push(x_89, x_90);
 x_92 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_93 = lean_alloc_ctor(1, 2, 0);
@ -4732,9 +4732,9 @@ x_134 = l_Lean_nullKind___closed__2;
 x_135 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_135, 0, x_134);
 lean_ctor_set(x_135, 1, x_133);
-x_136 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_136 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_137 = lean_array_push(x_136, x_135);
-x_138 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_138 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_139 = lean_array_push(x_137, x_138);
 x_140 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_141 = lean_alloc_ctor(1, 2, 0);
@ -4827,9 +4827,9 @@ x_185 = l_Lean_nullKind___closed__2;
 x_186 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_186, 0, x_185);
 lean_ctor_set(x_186, 1, x_184);
-x_187 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_187 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_188 = lean_array_push(x_187, x_186);
-x_189 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_189 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_190 = lean_array_push(x_188, x_189);
 x_191 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_192 = lean_alloc_ctor(1, 2, 0);
@ -4931,9 +4931,9 @@ x_242 = l_Lean_nullKind___closed__2;
 x_243 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_243, 0, x_242);
 lean_ctor_set(x_243, 1, x_241);
-x_244 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
+x_244 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__42;
 x_245 = lean_array_push(x_244, x_243);
-x_246 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
+x_246 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__50;
 x_247 = lean_array_push(x_245, x_246);
 x_248 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_249 = lean_alloc_ctor(1, 2, 0);
--- a/stage0/stdlib/Init/Lean/Elab/Command.c
+++ b/stage0/stdlib/Init/Lean/Elab/Command.c
--- a/stage0/stdlib/Init/Lean/Elab/Quotation.c
+++ b/stage0/stdlib/Init/Lean/Elab/Quotation.c
--- a/stage0/stdlib/Init/Lean/Elab/Syntax.c
+++ b/stage0/stdlib/Init/Lean/Elab/Syntax.c
--- a/stage0/stdlib/Init/Lean/Elab/Tactic.c
+++ b/stage0/stdlib/Init/Lean/Elab/Tactic.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean.Elab.Tactic
-// Imports: Init.Lean.Elab.Term
+// Imports: Init.Lean.Elab.Term Init.Lean.Elab.Tactic.Basic
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -118,6 +118,7 @@ return x_5;
 }
 }
 lean_object* initialize_Init_Lean_Elab_Term(lean_object*);
+lean_object* initialize_Init_Lean_Elab_Tactic_Basic(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Lean_Elab_Tactic(lean_object* w) {
 lean_object * res;
@ -126,6 +127,9 @@ _G_initialized = true;
 res = initialize_Init_Lean_Elab_Term(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Lean_Elab_Tactic_Basic(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 l_Lean_Elab_Term_elabTacticBlock___closed__1 = _init_l_Lean_Elab_Term_elabTacticBlock___closed__1();
 lean_mark_persistent(l_Lean_Elab_Term_elabTacticBlock___closed__1);
 l_Lean_Elab_Term_elabTacticBlock___closed__2 = _init_l_Lean_Elab_Term_elabTacticBlock___closed__2();
--- 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
@ -26,7 +26,7 @@ extern lean_object* l_Lean_Name_toString___closed__1;
 lean_object* l___private_Init_Lean_Elab_Term_6__expandCDotInApp(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkForall(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__1;
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___closed__6;
+lean_object* l_Lean_Elab_Term_monadQuotation;
 lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__8;
 lean_object* l___private_Init_Lean_Elab_Term_7__exceptionToSorry___closed__3;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabNum(lean_object*);
@ -58,8 +58,8 @@ extern lean_object* l_Lean_nullKind;
 lean_object* l_Lean_Meta_whnfForall(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__8;
 lean_object* l_Lean_Elab_Term_elabTermAux___main___closed__6;
+lean_object* l_Lean_Elab_Term_monadLog___lambda__3___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_7__exceptionToSorry(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_TermElabM_MonadQuotation;
 extern lean_object* l_Lean_MessageData_ofList___closed__3;
 lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__2;
 lean_object* lean_array_uget(lean_object*, size_t);
@ -73,12 +73,12 @@ lean_object* l_Lean_Elab_Term_ensureHasType___closed__2;
 lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__2;
 extern lean_object* l_IO_Prim_fopenFlags___closed__12;
 lean_object* l_Lean_Elab_Term_resettingSynthInstanceCacheWhen(lean_object*);
+lean_object* l_Lean_Elab_Term_monadLog___closed__3;
 lean_object* l_Lean_Format_pretty(lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabChar___closed__3;
 lean_object* l_Lean_Elab_Term_getDeclName_x3f(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_14__synthesizeSyntheticMVar___closed__2;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabChar___closed__2;
-lean_object* l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__3;
 lean_object* l_Lean_Elab_Term_registerBuiltinTermElabAttr___closed__3;
 lean_object* l_Lean_SMap_empty___at_Lean_Elab_Term_mkBuiltinTermElabTable___spec__1___closed__1;
 lean_object* l_Lean_Meta_mkForall(lean_object*, lean_object*, lean_object*, lean_object*);
@ -88,6 +88,7 @@ extern lean_object* l_Option_get_x21___rarg___closed__3;
 lean_object* l_Lean_Meta_mkAppM(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_levelMVarToParam___closed__1;
 lean_object* l_Lean_Elab_Term_elabParen(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_ReaderT_read___at_Lean_Elab_Term_monadLog___spec__1(lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabNum___closed__2;
 extern lean_object* l_Lean_maxRecDepthErrorMessage;
 extern lean_object* l_Lean_nameToExprAux___main___closed__4;
@ -105,7 +106,6 @@ lean_object* l___private_Init_Lean_Elab_Term_14__synthesizeSyntheticMVar___close
 lean_object* l_Lean_Meta_Exception_toMessageData(lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_21__resolveLocalName___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_18__mkPairsAux___main___closed__1;
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog;
 lean_object* l_Lean_mkMVar(lean_object*);
 extern lean_object* l_Array_empty___closed__1;
 lean_object* lean_environment_find(lean_object*, lean_object*);
@ -135,6 +135,7 @@ lean_object* l_Lean_Elab_Term_mkForallUsedOnly___boxed(lean_object*, lean_object
 lean_object* lean_io_ref_get(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__5;
 lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__6;
+lean_object* l_Lean_Elab_Term_monadQuotation___closed__2;
 lean_object* l___private_Init_Lean_Elab_Term_18__mkPairsAux___main___closed__9;
 lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHole(lean_object*);
@ -144,11 +145,9 @@ lean_object* l_Lean_Elab_Term_decLevel(lean_object*, lean_object*, lean_object*,
 uint8_t l_PersistentHashMap_containsAtAux___main___at_Lean_Parser_mkFreshKindAux___main___spec__3(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabParen___closed__3;
 lean_object* lean_local_ctx_find_from_user_name(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__2;
 lean_object* l_Lean_Elab_Term_getMVarDecl(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabListLit___closed__1;
 lean_object* l_Lean_Elab_Term_mkLambda(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__1;
 extern lean_object* l_Lean_Literal_type___closed__3;
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
@ -157,6 +156,7 @@ lean_object* l___private_Init_Lean_Elab_Term_17__synthesizeSyntheticMVarsAux___m
 lean_object* l_Lean_Elab_Term_resetSynthInstanceCache(lean_object*);
 lean_object* l_Lean_Elab_Term_mkForallUsedOnly(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_inferType___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_monadLog___closed__7;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabListLit___closed__2;
 lean_object* lean_string_append(lean_object*, lean_object*);
 extern lean_object* l_Lean_Meta_Exception_toStr___closed__1;
@ -165,7 +165,6 @@ lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lea
 lean_object* l_Lean_Elab_Term_ensureType(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabBadCDot___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___closed__3;
 lean_object* l_PersistentArray_push___rarg(lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabTypeStx___closed__2;
 extern lean_object* l_String_splitAux___main___closed__1;
@ -188,6 +187,7 @@ size_t l_USize_shiftRight(size_t, size_t);
 lean_object* l_Lean_Elab_Term_withLCtx___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_11__resumePostponed___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabArrayLit___closed__6;
+lean_object* l_Lean_Elab_Term_monadLog___closed__10;
 lean_object* l_Lean_Elab_Term_resolveName___closed__6;
 lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars(uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabTypeStx___rarg(lean_object*);
@ -197,14 +197,12 @@ lean_object* l_Lean_Elab_Term_elabParen___closed__6;
 extern lean_object* l_Lean_Parser_Term_tupleTail___elambda__1___closed__2;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabTypeStx___closed__1;
 extern lean_object* l_Lean_Parser_Term_cons___elambda__1___closed__1;
-lean_object* l_ReaderT_read___at_Lean_Elab_Term_TermElabM_MonadLog___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_dbgTrace___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_sort___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_adaptMacro___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Meta_MetaHasEval___rarg___closed__4;
 lean_object* l_Lean_Elab_Term_assignExprMVar(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_13__checkWithDefault___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_ReaderT_bind___at_Lean_Elab_Term_TermElabM_MonadLog___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Exception_hasToString(lean_object*);
 extern lean_object* l_Array_iterateMAux___main___at_Lean_mkAppStx___spec__1___closed__1;
 lean_object* l_Lean_Elab_Term_elabParen___closed__5;
@ -232,7 +230,6 @@ lean_object* l___private_Init_Lean_Elab_Term_9__elabTermUsing___main___closed__1
 lean_object* l_IO_ofExcept___at_Lean_registerClassAttr___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_getTraceState(lean_object*);
 lean_object* l_Lean_Elab_Term_mkFreshTypeMVar(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___closed__7;
 lean_object* l_Lean_Elab_Term_elabTermAux___main___closed__1;
 lean_object* l___private_Init_Lean_Elab_Term_21__resolveLocalName(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkFreshAnonymousIdent(lean_object*, lean_object*, lean_object*);
@ -242,6 +239,7 @@ lean_object* l_Lean_Elab_Term_elabTermAux___main___boxed(lean_object*, lean_obje
 lean_object* l_Lean_Elab_Term_whnf(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabArrayLit(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_getOptions(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_monadLog___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabParen___closed__1;
 lean_object* l___private_Init_Lean_Elab_Term_10__resumeElabTerm___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabListLit___closed__1;
@ -261,13 +259,13 @@ lean_object* l_HashMapImp_find_x3f___at_Lean_Elab_Term_elabTermAux___main___spec
 lean_object* l_ReaderT_lift___at___private_Init_Lean_Elab_Term_11__resumePostponed___spec__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_synthesizeUsingDefault(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_withIncRecDepth___rarg___closed__1;
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___closed__11;
 lean_object* l_Lean_Elab_Term_elabListLit___closed__2;
 extern lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___closed__5;
 lean_object* l___private_Init_Lean_Elab_Term_18__mkPairsAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkFreshAnonymousName___boxed(lean_object*);
 extern lean_object* l_Lean_Meta_dbgTrace___rarg___closed__1;
 lean_object* l_Lean_Elab_Term_mkConst___closed__6;
+lean_object* l_Lean_Elab_Term_monadLog___closed__5;
 lean_object* l___private_Init_Lean_Elab_Term_2__fromMetaException(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_withIncRecDepth___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_20__resolveLocalNameAux(lean_object*, lean_object*, lean_object*);
@ -278,6 +276,7 @@ lean_object* l_Lean_Elab_Term_elabParen___closed__4;
 lean_object* l_Lean_Elab_Term_withIncRecDepth___rarg___closed__2;
 lean_object* l_Lean_Elab_Term_elabLevel(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_15__synthesizeSyntheticMVarsStep___closed__9;
+lean_object* l_Lean_Elab_Term_monadLog___closed__1;
 lean_object* l_List_forM___main___at___private_Init_Lean_Elab_Term_16__reportStuckSyntheticMVars___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_isCharLit_x3f(lean_object*);
 lean_object* l_Array_isEqvAux___main___at_Lean_Elab_Term_withMVarContext___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -301,8 +300,6 @@ lean_object* l_Lean_Elab_Term_levelMVarToParam(lean_object*, lean_object*, lean_
 lean_object* l___private_Init_Lean_Elab_Term_15__synthesizeSyntheticMVarsStep___closed__4;
 lean_object* l_Lean_Elab_Term_observing(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkLet___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__4(lean_object*, lean_object*, lean_object*);
-lean_object* l_ReaderT_bind___at_Lean_Elab_Term_TermElabM_MonadLog___spec__2(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_declareBuiltinTermElab(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_withMacroExpansion(lean_object*);
 lean_object* l_Lean_Elab_Term_getTraceState___rarg(lean_object*);
@ -328,6 +325,7 @@ lean_object* l_Lean_Elab_Term_getCurrNamespace(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_23__mkConsts(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_throwUnsupportedSyntax___rarg(lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSort___closed__3;
+lean_object* l_Lean_Elab_Term_monadLog___closed__8;
 extern lean_object* l_Lean_Expr_isSyntheticSorry___closed__1;
 lean_object* l___private_Init_Lean_Elab_Term_9__elabTermUsing___main(lean_object*, lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_isExprMVarAssigned___boxed(lean_object*, lean_object*, lean_object*);
@ -353,10 +351,8 @@ lean_object* l_Lean_Elab_Term_mkConst___closed__2;
 lean_object* l___private_Init_Lean_Elab_Term_8__postponeElabTerm___closed__4;
 lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabStr___closed__1;
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___closed__10;
 lean_object* l___private_Init_Lean_Elab_Term_16__reportStuckSyntheticMVars(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_TermElabM_inhabited(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__3___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkInstMVar(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__6;
 lean_object* l___private_Init_Lean_Elab_Term_15__synthesizeSyntheticMVarsStep___closed__10;
@ -377,10 +373,12 @@ lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
 lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_Term_15__synthesizeSyntheticMVarsStep___spec__2___closed__8;
 lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_Term_15__synthesizeSyntheticMVarsStep___spec__2___closed__9;
 lean_object* l___private_Init_Lean_Elab_Term_1__mkMessageAux(lean_object*, lean_object*, lean_object*, uint8_t);
+lean_object* l_Lean_Elab_Term_monadQuotation___closed__1;
 lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_Term_15__synthesizeSyntheticMVarsStep___spec__2___closed__4;
 lean_object* l_Lean_Elab_Term_withNode___rarg___closed__1;
 lean_object* l___private_Init_Lean_Elab_Term_9__elabTermUsing___main___closed__2;
 lean_object* l_Lean_Elab_Term_elabTypeStx(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_monadLog___closed__6;
 lean_object* l_Lean_Elab_Term_withFreshMacroScope(lean_object*);
 lean_object* l_Lean_Elab_Term_resolveName___closed__7;
 size_t l_Lean_Name_hash(lean_object*);
@ -416,6 +414,7 @@ lean_object* l_Lean_Elab_Term_throwError___rarg(lean_object*, lean_object*, lean
 lean_object* l_Lean_Elab_Term_adaptMacro(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_log___at_Lean_Elab_Term_logTrace___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__5;
+lean_object* l_Lean_Elab_Term_monadLog___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_elabTypeStx___rarg___closed__1;
 extern lean_object* l_Lean_Elab_Exception_hasToString___closed__1;
@ -441,6 +440,7 @@ lean_object* l___private_Init_Lean_Elab_Term_8__postponeElabTerm___closed__2;
 uint8_t l_PersistentHashMap_contains___at_Lean_Elab_Term_addBuiltinTermElab___spec__4(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__1;
 extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__7;
+lean_object* l_Lean_Elab_Term_monadLog___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_14__synthesizeSyntheticMVar___closed__3;
 lean_object* l_Lean_Elab_Term_mkAppM___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_getCurrMacroScope___boxed(lean_object*, lean_object*);
@ -492,14 +492,13 @@ lean_object* l_Lean_Meta_whnf(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_17__synthesizeSyntheticMVarsAux___main(uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSort___closed__2;
 lean_object* l_Lean_Elab_Term_isClass(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_TermElabResult_inhabited;
 lean_object* l_Lean_Elab_Term_withMVarContext___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabArrayLit___closed__4;
 lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_Term_15__synthesizeSyntheticMVarsStep___spec__2___closed__2;
 lean_object* l_Lean_Elab_Term_TermElabM_inhabited___boxed(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__4___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkFreshAnonymousIdent___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabTermAux___main___closed__3;
 extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__3;
@ -517,13 +516,13 @@ lean_object* l_Lean_Elab_Term_mkConst___closed__3;
 lean_object* l_Lean_Elab_Term_resolveName___closed__4;
 lean_object* l_Lean_Elab_Term_withNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_nullKind___closed__2;
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__3(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_ParametricAttribute_setParam___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_termElabAttribute;
 lean_object* l_Lean_Elab_Term_expandCDot_x3f___closed__1;
 lean_object* l_fix1___rarg___lambda__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabArrayLit___closed__10;
 lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_Term_15__synthesizeSyntheticMVarsStep___spec__2___closed__1;
+lean_object* l_Lean_Elab_Term_monadLog___closed__2;
 lean_object* l_Lean_Elab_Term_mkTermIdFromIdent(lean_object*);
 extern lean_object* l_Lean_Meta_Exception_toStr___closed__7;
 lean_object* l_Lean_mkAtomFrom(lean_object*, lean_object*);
@ -531,7 +530,6 @@ lean_object* l_Lean_Elab_Term_getDeclName_x3f___boxed(lean_object*, lean_object*
 lean_object* l_Lean_Elab_Term_isDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_18__mkPairsAux___main___closed__7;
 lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__10;
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_ConstantInfo_lparams(lean_object*);
 lean_object* l_Lean_Elab_Term_mkFreshAnonymousName(lean_object*);
 uint8_t l___private_Init_Lean_Elab_Term_4__hasCDot(lean_object*);
@ -577,6 +575,7 @@ lean_object* l_PersistentHashMap_contains___at_Lean_Elab_Term_addBuiltinTermElab
 lean_object* l_Lean_Elab_Term_TermElabM_inhabited___rarg(lean_object*);
 uint8_t l_Lean_Expr_isMVar(lean_object*);
 lean_object* l_Lean_Elab_Term_mkHole(lean_object*);
+lean_object* l_Lean_Elab_Term_monadLog___closed__9;
 lean_object* l_Lean_Elab_Term_termElabAttribute___closed__6;
 lean_object* l_Lean_Meta_mkFreshExprMVar(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_5__expandCDot___closed__1;
@ -594,13 +593,13 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabArrayLit___closed__2;
 extern lean_object* l_Bool_HasRepr___closed__2;
 lean_object* l_Lean_Elab_Term_ensureType___closed__2;
 lean_object* l_Lean_Elab_Term_registerBuiltinTermElabAttr___lambda__1___closed__2;
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___closed__1;
 lean_object* l_Lean_Environment_addAndCompile(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_registerSyntheticMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getKind(lean_object*);
 lean_object* l_PersistentHashMap_find_x3f___at_Lean_Elab_Term_elabTermAux___main___spec__2(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_registerBuiltinTermElabAttr___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_registerBuiltinTermElabAttr(lean_object*);
+lean_object* l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_decLevel___closed__3;
 extern lean_object* l_Lean_Parser_Term_paren___elambda__1___closed__1;
@ -619,9 +618,9 @@ lean_object* l_Lean_Elab_Term_elabTerm___boxed(lean_object*, lean_object*, lean_
 extern lean_object* l_Lean_Parser_Term_app___elambda__1___closed__2;
 extern lean_object* l_Lean_EnvExtension_setState___closed__1;
 lean_object* l_Lean_Elab_Term_liftLevelM___rarg___boxed(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___closed__9;
 lean_object* l_Lean_Elab_Term_tryPostponeIfMVar___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_whnfCore(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_monadLog___lambda__4___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Init_Util_1__mkPanicMessage___closed__2;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabParen___closed__2;
 lean_object* l_Lean_Elab_Term_resettingSynthInstanceCacheWhen___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
@ -668,26 +667,24 @@ lean_object* l_Lean_Elab_Term_registerBuiltinTermElabAttr___lambda__1___closed__
 lean_object* lean_io_ref_set(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabStr___closed__3;
 lean_object* l_Lean_Elab_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___closed__8;
 lean_object* l_Lean_Elab_Term_getEnv(lean_object*);
 lean_object* l_Lean_Elab_Term_getOpenDecls(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabListLit(lean_object*);
 lean_object* l_Lean_Elab_Term_elabArrayLit___closed__3;
 extern lean_object* l_Lean_mkOptionalNode___closed__1;
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___closed__5;
 lean_object* l_Lean_Elab_Term_tryEnsureHasType_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_decLevel___closed__4;
 lean_object* l_Lean_Elab_Term_elabChar___closed__3;
 lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__12;
 lean_object* l_Lean_Meta_mkLambda(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_KernelException_toMessageData___closed__12;
+lean_object* l_Lean_Elab_Term_monadLog___closed__11;
 extern lean_object* l_Lean_Expr_Inhabited;
 lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_addBuiltinTermElab(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabStr(lean_object*);
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___closed__2;
 uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHole___closed__3;
@ -714,14 +711,17 @@ lean_object* l_Lean_Elab_Term_mkFreshLevelMVar___boxed(lean_object*, lean_object
 lean_object* l_Lean_Elab_Term_setTraceState(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_tryPostpone(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkPairs(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_monadLog___lambda__3(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_tryEnsureHasType_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Term_3__fromMetaState___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_monadQuotation___closed__3;
 extern lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__4;
 lean_object* l_Lean_Meta_mkFreshLevelMVar___rarg(lean_object*);
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 extern lean_object* l_Lean_MetavarContext_Inhabited___closed__1;
 lean_object* l___private_Init_Lean_Elab_Term_18__mkPairsAux___main___closed__6;
 uint8_t l_Lean_SMap_contains___at_Lean_Elab_Term_addBuiltinTermElab___spec__1(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_monadLog___lambda__4(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabNum(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_3__fromMetaState(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabListLit___closed__3;
@ -767,10 +767,8 @@ lean_object* l_List_forM___main___at___private_Init_Lean_Elab_Term_16__reportStu
 lean_object* l_Lean_Message_toString(lean_object*);
 lean_object* l_Lean_mkAppB(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_char___elambda__1___closed__2;
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at_Lean_Elab_Term_expandCDot_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_indentExpr(lean_object*);
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___closed__4;
 lean_object* l_Lean_Elab_Term_trace(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_AssocList_contains___main___at_Lean_Elab_Term_addBuiltinTermElab___spec__3___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkFreshInstanceName___boxed(lean_object*);
@ -808,11 +806,12 @@ lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_syntaxNodeKindOfAttrParam(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_6__expandCDotInApp___main(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkForall___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_monadLog;
 lean_object* l_Lean_Elab_Term_getMCtx___rarg(lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Term_3__fromMetaState___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentArray_foldlM___at___private_Init_Lean_Elab_Term_3__fromMetaState___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_monadLog___closed__4;
 lean_object* l___private_Init_Lean_Elab_Term_9__elabTermUsing___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_23__mkConsts___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_liftMetaM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabArrayLit___closed__7;
@ -821,6 +820,7 @@ lean_object* l_Lean_Elab_Term_mkFreshInstanceName___rarg___closed__2;
 lean_object* l_Lean_mkApp3(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Expr_isSort(lean_object*);
 lean_object* l_Lean_Meta_decLevel_x3f(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_monadLog___lambda__2(lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Init_Lean_Parser_Parser_18__BuiltinParserAttribute_add___closed__2;
 lean_object* l_Lean_Elab_Term_expandCDot_x3f(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_NameGenerator_Inhabited___closed__3;
@ -1376,7 +1376,7 @@ lean_dec(x_2);
 return x_4;
 }
 }
-lean_object* l_ReaderT_read___at_Lean_Elab_Term_TermElabM_MonadLog___spec__1(lean_object* x_1, lean_object* x_2) {
+lean_object* l_ReaderT_read___at_Lean_Elab_Term_monadLog___spec__1(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
@ -1386,7 +1386,7 @@ lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
-lean_object* l_ReaderT_bind___at_Lean_Elab_Term_TermElabM_MonadLog___spec__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+lean_object* l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
 lean_object* x_5; 
@ -1429,15 +1429,15 @@ return x_12;
 }
 }
 }
-lean_object* l_ReaderT_bind___at_Lean_Elab_Term_TermElabM_MonadLog___spec__2(lean_object* x_1, lean_object* x_2) {
+lean_object* l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_TermElabM_MonadLog___spec__2___rarg), 4, 0);
+x_3 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2___rarg), 4, 0);
 return x_3;
 }
 }
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_Elab_Term_monadLog___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; lean_object* x_5; 
@ -1449,7 +1449,7 @@ lean_ctor_set(x_5, 1, x_3);
 return x_5;
 }
 }
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_Elab_Term_monadLog___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; lean_object* x_5; 
@ -1461,7 +1461,7 @@ lean_ctor_set(x_5, 1, x_3);
 return x_5;
 }
 }
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_Elab_Term_monadLog___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; lean_object* x_5; 
@ -1473,7 +1473,7 @@ lean_ctor_set(x_5, 1, x_3);
 return x_5;
 }
 }
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__4(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_Elab_Term_monadLog___lambda__4(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 uint8_t x_4; 
@ -1522,75 +1522,75 @@ return x_18;
 }
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__1() {
+lean_object* _init_l_Lean_Elab_Term_monadLog___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_ReaderT_read___at_Lean_Elab_Term_TermElabM_MonadLog___spec__1), 2, 0);
+x_1 = lean_alloc_closure((void*)(l_ReaderT_read___at_Lean_Elab_Term_monadLog___spec__1), 2, 0);
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__2() {
+lean_object* _init_l_Lean_Elab_Term_monadLog___closed__2() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_TermElabM_MonadLog___lambda__1___boxed), 3, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_monadLog___lambda__1___boxed), 3, 0);
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__3() {
+lean_object* _init_l_Lean_Elab_Term_monadLog___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Elab_Term_TermElabM_MonadLog___closed__1;
-x_2 = l_Lean_Elab_Term_TermElabM_MonadLog___closed__2;
-x_3 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_TermElabM_MonadLog___spec__2___rarg), 4, 2);
+x_1 = l_Lean_Elab_Term_monadLog___closed__1;
+x_2 = l_Lean_Elab_Term_monadLog___closed__2;
+x_3 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2___rarg), 4, 2);
 lean_closure_set(x_3, 0, x_1);
 lean_closure_set(x_3, 1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__4() {
+lean_object* _init_l_Lean_Elab_Term_monadLog___closed__4() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_TermElabM_MonadLog___lambda__2___boxed), 3, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_monadLog___lambda__2___boxed), 3, 0);
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__5() {
+lean_object* _init_l_Lean_Elab_Term_monadLog___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Elab_Term_TermElabM_MonadLog___closed__1;
-x_2 = l_Lean_Elab_Term_TermElabM_MonadLog___closed__4;
-x_3 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_TermElabM_MonadLog___spec__2___rarg), 4, 2);
+x_1 = l_Lean_Elab_Term_monadLog___closed__1;
+x_2 = l_Lean_Elab_Term_monadLog___closed__4;
+x_3 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2___rarg), 4, 2);
 lean_closure_set(x_3, 0, x_1);
 lean_closure_set(x_3, 1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__6() {
+lean_object* _init_l_Lean_Elab_Term_monadLog___closed__6() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_TermElabM_MonadLog___lambda__3___boxed), 3, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_monadLog___lambda__3___boxed), 3, 0);
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__7() {
+lean_object* _init_l_Lean_Elab_Term_monadLog___closed__7() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Elab_Term_TermElabM_MonadLog___closed__1;
-x_2 = l_Lean_Elab_Term_TermElabM_MonadLog___closed__6;
-x_3 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_TermElabM_MonadLog___spec__2___rarg), 4, 2);
+x_1 = l_Lean_Elab_Term_monadLog___closed__1;
+x_2 = l_Lean_Elab_Term_monadLog___closed__6;
+x_3 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2___rarg), 4, 2);
 lean_closure_set(x_3, 0, x_1);
 lean_closure_set(x_3, 1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__8() {
+lean_object* _init_l_Lean_Elab_Term_monadLog___closed__8() {
 _start:
 {
 lean_object* x_1; 
@ -1598,14 +1598,14 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_addContext___boxed), 3, 0);
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__9() {
+lean_object* _init_l_Lean_Elab_Term_monadLog___closed__9() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
-x_1 = l_Lean_Elab_Term_TermElabM_MonadLog___closed__3;
-x_2 = l_Lean_Elab_Term_TermElabM_MonadLog___closed__5;
-x_3 = l_Lean_Elab_Term_TermElabM_MonadLog___closed__7;
-x_4 = l_Lean_Elab_Term_TermElabM_MonadLog___closed__8;
+x_1 = l_Lean_Elab_Term_monadLog___closed__3;
+x_2 = l_Lean_Elab_Term_monadLog___closed__5;
+x_3 = l_Lean_Elab_Term_monadLog___closed__7;
+x_4 = l_Lean_Elab_Term_monadLog___closed__8;
 x_5 = lean_alloc_ctor(0, 4, 0);
 lean_ctor_set(x_5, 0, x_1);
 lean_ctor_set(x_5, 1, x_2);
@ -1614,69 +1614,69 @@ lean_ctor_set(x_5, 3, x_4);
 return x_5;
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__10() {
+lean_object* _init_l_Lean_Elab_Term_monadLog___closed__10() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_TermElabM_MonadLog___lambda__4___boxed), 3, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_monadLog___lambda__4___boxed), 3, 0);
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__11() {
+lean_object* _init_l_Lean_Elab_Term_monadLog___closed__11() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Elab_Term_TermElabM_MonadLog___closed__9;
-x_2 = l_Lean_Elab_Term_TermElabM_MonadLog___closed__10;
+x_1 = l_Lean_Elab_Term_monadLog___closed__9;
+x_2 = l_Lean_Elab_Term_monadLog___closed__10;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadLog() {
+lean_object* _init_l_Lean_Elab_Term_monadLog() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Elab_Term_TermElabM_MonadLog___closed__11;
+x_1 = l_Lean_Elab_Term_monadLog___closed__11;
 return x_1;
 }
 }
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_Elab_Term_monadLog___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; 
-x_4 = l_Lean_Elab_Term_TermElabM_MonadLog___lambda__1(x_1, x_2, x_3);
+x_4 = l_Lean_Elab_Term_monadLog___lambda__1(x_1, x_2, x_3);
 lean_dec(x_2);
 lean_dec(x_1);
 return x_4;
 }
 }
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_Elab_Term_monadLog___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; 
-x_4 = l_Lean_Elab_Term_TermElabM_MonadLog___lambda__2(x_1, x_2, x_3);
+x_4 = l_Lean_Elab_Term_monadLog___lambda__2(x_1, x_2, x_3);
 lean_dec(x_2);
 lean_dec(x_1);
 return x_4;
 }
 }
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_Elab_Term_monadLog___lambda__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; 
-x_4 = l_Lean_Elab_Term_TermElabM_MonadLog___lambda__3(x_1, x_2, x_3);
+x_4 = l_Lean_Elab_Term_monadLog___lambda__3(x_1, x_2, x_3);
 lean_dec(x_2);
 lean_dec(x_1);
 return x_4;
 }
 }
-lean_object* l_Lean_Elab_Term_TermElabM_MonadLog___lambda__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_Elab_Term_monadLog___lambda__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; 
-x_4 = l_Lean_Elab_Term_TermElabM_MonadLog___lambda__4(x_1, x_2, x_3);
+x_4 = l_Lean_Elab_Term_monadLog___lambda__4(x_1, x_2, x_3);
 lean_dec(x_2);
 return x_4;
 }
@ -2414,7 +2414,7 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_withFreshMacroScope___rarg), 3
 return x_2;
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__1() {
+lean_object* _init_l_Lean_Elab_Term_monadQuotation___closed__1() {
 _start:
 {
 lean_object* x_1; 
@ -2422,7 +2422,7 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_getCurrMacroScope___boxed), 2,
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__2() {
+lean_object* _init_l_Lean_Elab_Term_monadQuotation___closed__2() {
 _start:
 {
 lean_object* x_1; 
@ -2430,23 +2430,23 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_withFreshMacroScope), 1, 0);
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__3() {
+lean_object* _init_l_Lean_Elab_Term_monadQuotation___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__1;
-x_2 = l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__2;
+x_1 = l_Lean_Elab_Term_monadQuotation___closed__1;
+x_2 = l_Lean_Elab_Term_monadQuotation___closed__2;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Elab_Term_TermElabM_MonadQuotation() {
+lean_object* _init_l_Lean_Elab_Term_monadQuotation() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__3;
+x_1 = l_Lean_Elab_Term_monadQuotation___closed__3;
 return x_1;
 }
 }
@ -11422,13 +11422,15 @@ return x_29;
 }
 else
 {
-lean_object* x_30; 
 lean_dec(x_21);
-x_30 = lean_ctor_get(x_20, 1);
-lean_inc(x_30);
 lean_dec(x_20);
-x_6 = x_19;
-x_8 = x_30;
+lean_inc(x_1);
+{
+lean_object* _tmp_5 = x_19;
+lean_object* _tmp_7 = x_1;
+x_6 = _tmp_5;
+x_8 = _tmp_7;
+}
 goto _start;
 }
 }
@ -11437,37 +11439,37 @@ else
 lean_dec(x_19);
 if (x_5 == 0)
 {
-uint8_t x_32; 
+uint8_t x_31; 
 lean_dec(x_7);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_32 = !lean_is_exclusive(x_20);
-if (x_32 == 0)
+x_31 = !lean_is_exclusive(x_20);
+if (x_31 == 0)
 {
-lean_object* x_33; 
-x_33 = lean_ctor_get(x_20, 0);
-lean_dec(x_33);
+lean_object* x_32; 
+x_32 = lean_ctor_get(x_20, 0);
+lean_dec(x_32);
 return x_20;
 }
 else
 {
-lean_object* x_34; lean_object* x_35; 
-x_34 = lean_ctor_get(x_20, 1);
-lean_inc(x_34);
+lean_object* x_33; lean_object* x_34; 
+x_33 = lean_ctor_get(x_20, 1);
+lean_inc(x_33);
 lean_dec(x_20);
-x_35 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_35, 0, x_21);
-lean_ctor_set(x_35, 1, x_34);
-return x_35;
+x_34 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_34, 0, x_21);
+lean_ctor_set(x_34, 1, x_33);
+return x_34;
 }
 }
 else
 {
-lean_object* x_36; 
+lean_object* x_35; 
 lean_dec(x_20);
-x_36 = l___private_Init_Lean_Elab_Term_8__postponeElabTerm(x_2, x_3, x_7, x_1);
-return x_36;
+x_35 = l___private_Init_Lean_Elab_Term_8__postponeElabTerm(x_2, x_3, x_7, x_1);
+return x_35;
 }
 }
 }
@ -16672,7 +16674,7 @@ lean_closure_set(x_8, 1, x_1);
 lean_closure_set(x_8, 2, x_3);
 lean_closure_set(x_8, 3, x_2);
 x_9 = l___private_Init_Lean_Elab_Term_11__resumePostponed___closed__1;
-x_10 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_TermElabM_MonadLog___spec__2___rarg), 4, 2);
+x_10 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2___rarg), 4, 2);
 lean_closure_set(x_10, 0, x_9);
 lean_closure_set(x_10, 1, x_8);
 x_11 = l_Lean_Elab_Term_withMVarContext___rarg(x_3, x_10, x_5, x_6);
@ -18524,7 +18526,7 @@ lean_closure_set(x_15, 1, x_14);
 x_16 = lean_alloc_closure((void*)(l_List_filterAuxM___main___at_Lean_Elab_Term_synthesizeUsingDefault___spec__1___lambda__1___boxed), 5, 2);
 lean_closure_set(x_16, 0, x_13);
 lean_closure_set(x_16, 1, x_11);
-x_17 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_TermElabM_MonadLog___spec__2___rarg), 4, 2);
+x_17 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2___rarg), 4, 2);
 lean_closure_set(x_17, 0, x_15);
 lean_closure_set(x_17, 1, x_16);
 lean_inc(x_3);
@ -18617,7 +18619,7 @@ lean_closure_set(x_34, 1, x_33);
 x_35 = lean_alloc_closure((void*)(l_List_filterAuxM___main___at_Lean_Elab_Term_synthesizeUsingDefault___spec__1___lambda__1___boxed), 5, 2);
 lean_closure_set(x_35, 0, x_32);
 lean_closure_set(x_35, 1, x_30);
-x_36 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_TermElabM_MonadLog___spec__2___rarg), 4, 2);
+x_36 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2___rarg), 4, 2);
 lean_closure_set(x_36, 0, x_34);
 lean_closure_set(x_36, 1, x_35);
 lean_inc(x_3);
@ -19004,7 +19006,7 @@ x_10 = lean_alloc_closure((void*)(l_Lean_Elab_Term_getMVarDecl___boxed), 3, 1);
 lean_closure_set(x_10, 0, x_9);
 x_11 = lean_alloc_closure((void*)(l_List_forM___main___at___private_Init_Lean_Elab_Term_16__reportStuckSyntheticMVars___spec__1___lambda__1___boxed), 4, 1);
 lean_closure_set(x_11, 0, x_6);
-x_12 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_TermElabM_MonadLog___spec__2___rarg), 4, 2);
+x_12 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2___rarg), 4, 2);
 lean_closure_set(x_12, 0, x_10);
 lean_closure_set(x_12, 1, x_11);
 lean_inc(x_2);
@ -23296,44 +23298,44 @@ l_Lean_Elab_Term_TermElabResult_inhabited___closed__1 = _init_l_Lean_Elab_Term_T
 lean_mark_persistent(l_Lean_Elab_Term_TermElabResult_inhabited___closed__1);
 l_Lean_Elab_Term_TermElabResult_inhabited = _init_l_Lean_Elab_Term_TermElabResult_inhabited();
 lean_mark_persistent(l_Lean_Elab_Term_TermElabResult_inhabited);
-l_Lean_Elab_Term_TermElabM_MonadLog___closed__1 = _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__1();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadLog___closed__1);
-l_Lean_Elab_Term_TermElabM_MonadLog___closed__2 = _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__2();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadLog___closed__2);
-l_Lean_Elab_Term_TermElabM_MonadLog___closed__3 = _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__3();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadLog___closed__3);
-l_Lean_Elab_Term_TermElabM_MonadLog___closed__4 = _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__4();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadLog___closed__4);
-l_Lean_Elab_Term_TermElabM_MonadLog___closed__5 = _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__5();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadLog___closed__5);
-l_Lean_Elab_Term_TermElabM_MonadLog___closed__6 = _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__6();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadLog___closed__6);
-l_Lean_Elab_Term_TermElabM_MonadLog___closed__7 = _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__7();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadLog___closed__7);
-l_Lean_Elab_Term_TermElabM_MonadLog___closed__8 = _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__8();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadLog___closed__8);
-l_Lean_Elab_Term_TermElabM_MonadLog___closed__9 = _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__9();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadLog___closed__9);
-l_Lean_Elab_Term_TermElabM_MonadLog___closed__10 = _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__10();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadLog___closed__10);
-l_Lean_Elab_Term_TermElabM_MonadLog___closed__11 = _init_l_Lean_Elab_Term_TermElabM_MonadLog___closed__11();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadLog___closed__11);
-l_Lean_Elab_Term_TermElabM_MonadLog = _init_l_Lean_Elab_Term_TermElabM_MonadLog();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadLog);
+l_Lean_Elab_Term_monadLog___closed__1 = _init_l_Lean_Elab_Term_monadLog___closed__1();
+lean_mark_persistent(l_Lean_Elab_Term_monadLog___closed__1);
+l_Lean_Elab_Term_monadLog___closed__2 = _init_l_Lean_Elab_Term_monadLog___closed__2();
+lean_mark_persistent(l_Lean_Elab_Term_monadLog___closed__2);
+l_Lean_Elab_Term_monadLog___closed__3 = _init_l_Lean_Elab_Term_monadLog___closed__3();
+lean_mark_persistent(l_Lean_Elab_Term_monadLog___closed__3);
+l_Lean_Elab_Term_monadLog___closed__4 = _init_l_Lean_Elab_Term_monadLog___closed__4();
+lean_mark_persistent(l_Lean_Elab_Term_monadLog___closed__4);
+l_Lean_Elab_Term_monadLog___closed__5 = _init_l_Lean_Elab_Term_monadLog___closed__5();
+lean_mark_persistent(l_Lean_Elab_Term_monadLog___closed__5);
+l_Lean_Elab_Term_monadLog___closed__6 = _init_l_Lean_Elab_Term_monadLog___closed__6();
+lean_mark_persistent(l_Lean_Elab_Term_monadLog___closed__6);
+l_Lean_Elab_Term_monadLog___closed__7 = _init_l_Lean_Elab_Term_monadLog___closed__7();
+lean_mark_persistent(l_Lean_Elab_Term_monadLog___closed__7);
+l_Lean_Elab_Term_monadLog___closed__8 = _init_l_Lean_Elab_Term_monadLog___closed__8();
+lean_mark_persistent(l_Lean_Elab_Term_monadLog___closed__8);
+l_Lean_Elab_Term_monadLog___closed__9 = _init_l_Lean_Elab_Term_monadLog___closed__9();
+lean_mark_persistent(l_Lean_Elab_Term_monadLog___closed__9);
+l_Lean_Elab_Term_monadLog___closed__10 = _init_l_Lean_Elab_Term_monadLog___closed__10();
+lean_mark_persistent(l_Lean_Elab_Term_monadLog___closed__10);
+l_Lean_Elab_Term_monadLog___closed__11 = _init_l_Lean_Elab_Term_monadLog___closed__11();
+lean_mark_persistent(l_Lean_Elab_Term_monadLog___closed__11);
+l_Lean_Elab_Term_monadLog = _init_l_Lean_Elab_Term_monadLog();
+lean_mark_persistent(l_Lean_Elab_Term_monadLog);
 l_Lean_Elab_Term_throwUnsupportedSyntax___rarg___closed__1 = _init_l_Lean_Elab_Term_throwUnsupportedSyntax___rarg___closed__1();
 lean_mark_persistent(l_Lean_Elab_Term_throwUnsupportedSyntax___rarg___closed__1);
 l_Lean_Elab_Term_withIncRecDepth___rarg___closed__1 = _init_l_Lean_Elab_Term_withIncRecDepth___rarg___closed__1();
 lean_mark_persistent(l_Lean_Elab_Term_withIncRecDepth___rarg___closed__1);
 l_Lean_Elab_Term_withIncRecDepth___rarg___closed__2 = _init_l_Lean_Elab_Term_withIncRecDepth___rarg___closed__2();
 lean_mark_persistent(l_Lean_Elab_Term_withIncRecDepth___rarg___closed__2);
-l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__1 = _init_l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__1();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__1);
-l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__2 = _init_l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__2();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__2);
-l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__3 = _init_l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__3();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadQuotation___closed__3);
-l_Lean_Elab_Term_TermElabM_MonadQuotation = _init_l_Lean_Elab_Term_TermElabM_MonadQuotation();
-lean_mark_persistent(l_Lean_Elab_Term_TermElabM_MonadQuotation);
+l_Lean_Elab_Term_monadQuotation___closed__1 = _init_l_Lean_Elab_Term_monadQuotation___closed__1();
+lean_mark_persistent(l_Lean_Elab_Term_monadQuotation___closed__1);
+l_Lean_Elab_Term_monadQuotation___closed__2 = _init_l_Lean_Elab_Term_monadQuotation___closed__2();
+lean_mark_persistent(l_Lean_Elab_Term_monadQuotation___closed__2);
+l_Lean_Elab_Term_monadQuotation___closed__3 = _init_l_Lean_Elab_Term_monadQuotation___closed__3();
+lean_mark_persistent(l_Lean_Elab_Term_monadQuotation___closed__3);
+l_Lean_Elab_Term_monadQuotation = _init_l_Lean_Elab_Term_monadQuotation();
+lean_mark_persistent(l_Lean_Elab_Term_monadQuotation);
 l_PersistentHashMap_empty___at_Lean_Elab_Term_mkBuiltinTermElabTable___spec__3 = _init_l_PersistentHashMap_empty___at_Lean_Elab_Term_mkBuiltinTermElabTable___spec__3();
 lean_mark_persistent(l_PersistentHashMap_empty___at_Lean_Elab_Term_mkBuiltinTermElabTable___spec__3);
 l_Lean_SMap_empty___at_Lean_Elab_Term_mkBuiltinTermElabTable___spec__1___closed__1 = _init_l_Lean_SMap_empty___at_Lean_Elab_Term_mkBuiltinTermElabTable___spec__1___closed__1();
--- a/stage0/stdlib/Init/Lean/Parser/Syntax.c
+++ b/stage0/stdlib/Init/Lean/Parser/Syntax.c
@ -170,6 +170,7 @@ lean_object* l_Lean_Parser_Command_prefix___closed__4;
 lean_object* l_Lean_Parser_Command_infixl___closed__3;
 lean_object* l_Lean_Parser_Syntax_lookahead___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Command_infix___elambda__1___closed__1;
+lean_object* l_Lean_Parser_Syntax_precedence___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Command_macro___closed__3;
 lean_object* l_Lean_Parser_Syntax_cat___closed__1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_orelse(lean_object*);
@ -233,6 +234,7 @@ lean_object* l_Lean_Parser_Syntax_try___elambda__1(lean_object*, lean_object*, l
 lean_object* l_Lean_Parser_Command_notation;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_notation(lean_object*);
 lean_object* l_Lean_Parser_Syntax_ident___elambda__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Syntax_precedence___closed__6;
 lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Command_postfix___closed__5;
 lean_object* l_Lean_Parser_Command_postfix___elambda__1___closed__3;
@ -309,6 +311,7 @@ lean_object* l_Lean_Parser_Command_reserve___closed__1;
 lean_object* l_Lean_Parser_Syntax_precedence___closed__2;
 lean_object* l_Lean_Parser_Command_reserve___closed__2;
 lean_object* l_Lean_Parser_Syntax_sepBy___elambda__1___closed__1;
+lean_object* l_Lean_Parser_Syntax_precedence___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Syntax_maxPrec___elambda__1___closed__4;
 extern lean_object* l_Lean_Parser_Term_haveAssign___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Syntax_sepBy___closed__2;
@ -389,6 +392,7 @@ lean_object* l_Lean_Parser_Command_notation___closed__2;
 lean_object* l_Lean_Parser_Syntax_str___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Syntax_sepBy1___elambda__1___closed__1;
 lean_object* l_Lean_Parser_mergeOrElseErrors(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Syntax_precedence___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Syntax_cat___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_reserve___closed__6;
 lean_object* l_Lean_Parser_Syntax_maxPrec___closed__5;
@ -418,6 +422,7 @@ lean_object* l_Lean_Parser_Syntax_lookahead___elambda__1(lean_object*, lean_obje
 lean_object* l_Lean_Parser_symbolInfo(lean_object*, lean_object*);
 lean_object* l___regBuiltinParser_Lean_Parser_Command_mixfix(lean_object*);
 lean_object* l_Lean_Parser_Command_mixfix___closed__3;
+extern lean_object* l___private_Init_Util_1__mkPanicMessage___closed__2;
 lean_object* l_Lean_Parser_Command_notation___closed__8;
 extern lean_object* l_Lean_Parser_epsilonInfo;
 lean_object* l_Lean_Parser_Command_mixfix___closed__6;
@ -443,6 +448,7 @@ lean_object* l_Lean_Parser_Command_mixfixSymbol;
 lean_object* l_Lean_Parser_Command_quotedSymbolPrec___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Syntax_sepBy1___closed__3;
 lean_object* l_Lean_Parser_Syntax_sepBy1___closed__5;
+lean_object* l_Lean_Parser_Syntax_precedence___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Command_notation___closed__9;
 lean_object* l_Lean_Parser_Syntax_lookahead___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Command_macro___elambda__1___closed__4;
@ -990,6 +996,47 @@ x_5 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3, x_4);
 return x_5;
 }
 }
+lean_object* _init_l_Lean_Parser_Syntax_precedence___elambda__1___closed__5() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l___private_Init_Util_1__mkPanicMessage___closed__2;
+x_2 = l_String_trim(x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_Parser_Syntax_precedence___elambda__1___closed__6() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Char_HasRepr___closed__1;
+x_2 = l_Lean_Parser_Syntax_precedence___elambda__1___closed__5;
+x_3 = lean_string_append(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Syntax_precedence___elambda__1___closed__7() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Syntax_precedence___elambda__1___closed__6;
+x_2 = l_Char_HasRepr___closed__1;
+x_3 = lean_string_append(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Syntax_precedence___elambda__1___closed__8() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Parser_Syntax_precedence___elambda__1___closed__7;
+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_Parser_Syntax_precedence___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@ -1062,13 +1109,13 @@ lean_object* x_31; lean_object* x_32; uint8_t x_33;
 x_31 = lean_ctor_get(x_30, 1);
 lean_inc(x_31);
 lean_dec(x_30);
-x_32 = l_Lean_Parser_Term_typeAscription___elambda__1___closed__6;
+x_32 = l_Lean_Parser_Syntax_precedence___elambda__1___closed__5;
 x_33 = lean_string_dec_eq(x_31, x_32);
 lean_dec(x_31);
 if (x_33 == 0)
 {
 lean_object* x_34; lean_object* x_35; 
-x_34 = l_Lean_Parser_Term_typeAscription___elambda__1___closed__9;
+x_34 = l_Lean_Parser_Syntax_precedence___elambda__1___closed__8;
 lean_inc(x_8);
 x_35 = l_Lean_Parser_ParserState_mkErrorsAt(x_27, x_34, x_8);
 x_17 = x_35;
@ -1084,7 +1131,7 @@ else
 {
 lean_object* x_36; lean_object* x_37; 
 lean_dec(x_30);
-x_36 = l_Lean_Parser_Term_typeAscription___elambda__1___closed__9;
+x_36 = l_Lean_Parser_Syntax_precedence___elambda__1___closed__8;
 lean_inc(x_8);
 x_37 = l_Lean_Parser_ParserState_mkErrorsAt(x_27, x_36, x_8);
 x_17 = x_37;
@ -1095,7 +1142,7 @@ else
 {
 lean_object* x_38; lean_object* x_39; 
 lean_dec(x_28);
-x_38 = l_Lean_Parser_Term_typeAscription___elambda__1___closed__9;
+x_38 = l_Lean_Parser_Syntax_precedence___elambda__1___closed__8;
 lean_inc(x_8);
 x_39 = l_Lean_Parser_ParserState_mkErrorsAt(x_27, x_38, x_8);
 x_17 = x_39;
@ -1136,38 +1183,48 @@ return x_25;
 lean_object* _init_l_Lean_Parser_Syntax_precedence___closed__1() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Parser_Syntax_precedenceLit;
-x_2 = lean_ctor_get(x_1, 0);
-lean_inc(x_2);
-x_3 = l_Lean_Parser_Term_typeAscription___closed__1;
-x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
-return x_4;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Parser_Syntax_precedence___elambda__1___closed__5;
+x_3 = l_Lean_Parser_symbolInfo(x_2, x_1);
+return x_3;
 }
 }
 lean_object* _init_l_Lean_Parser_Syntax_precedence___closed__2() {
 _start:
 {
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_Parser_Syntax_precedenceLit;
+x_2 = lean_ctor_get(x_1, 0);
+lean_inc(x_2);
+x_3 = l_Lean_Parser_Syntax_precedence___closed__1;
+x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
+return x_4;
+}
+}
+lean_object* _init_l_Lean_Parser_Syntax_precedence___closed__3() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Syntax_precedence___elambda__1___closed__2;
-x_2 = l_Lean_Parser_Syntax_precedence___closed__1;
+x_2 = l_Lean_Parser_Syntax_precedence___closed__2;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Syntax_precedence___closed__3() {
+lean_object* _init_l_Lean_Parser_Syntax_precedence___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_Lean_Parser_Syntax_precedence___elambda__1___closed__4;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Parser_Syntax_precedence___closed__2;
+x_3 = l_Lean_Parser_Syntax_precedence___closed__3;
 x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
 return x_4;
 }
 }
-lean_object* _init_l_Lean_Parser_Syntax_precedence___closed__4() {
+lean_object* _init_l_Lean_Parser_Syntax_precedence___closed__5() {
 _start:
 {
 lean_object* x_1; 
@ -1175,12 +1232,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Syntax_precedence___elambda__1),
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Syntax_precedence___closed__5() {
+lean_object* _init_l_Lean_Parser_Syntax_precedence___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Syntax_precedence___closed__3;
-x_2 = l_Lean_Parser_Syntax_precedence___closed__4;
+x_1 = l_Lean_Parser_Syntax_precedence___closed__4;
+x_2 = l_Lean_Parser_Syntax_precedence___closed__5;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@ -1191,7 +1248,7 @@ lean_object* _init_l_Lean_Parser_Syntax_precedence() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Syntax_precedence___closed__5;
+x_1 = l_Lean_Parser_Syntax_precedence___closed__6;
 return x_1;
 }
 }
@ -10447,6 +10504,14 @@ l_Lean_Parser_Syntax_precedence___elambda__1___closed__3 = _init_l_Lean_Parser_S
 lean_mark_persistent(l_Lean_Parser_Syntax_precedence___elambda__1___closed__3);
 l_Lean_Parser_Syntax_precedence___elambda__1___closed__4 = _init_l_Lean_Parser_Syntax_precedence___elambda__1___closed__4();
 lean_mark_persistent(l_Lean_Parser_Syntax_precedence___elambda__1___closed__4);
+l_Lean_Parser_Syntax_precedence___elambda__1___closed__5 = _init_l_Lean_Parser_Syntax_precedence___elambda__1___closed__5();
+lean_mark_persistent(l_Lean_Parser_Syntax_precedence___elambda__1___closed__5);
+l_Lean_Parser_Syntax_precedence___elambda__1___closed__6 = _init_l_Lean_Parser_Syntax_precedence___elambda__1___closed__6();
+lean_mark_persistent(l_Lean_Parser_Syntax_precedence___elambda__1___closed__6);
+l_Lean_Parser_Syntax_precedence___elambda__1___closed__7 = _init_l_Lean_Parser_Syntax_precedence___elambda__1___closed__7();
+lean_mark_persistent(l_Lean_Parser_Syntax_precedence___elambda__1___closed__7);
+l_Lean_Parser_Syntax_precedence___elambda__1___closed__8 = _init_l_Lean_Parser_Syntax_precedence___elambda__1___closed__8();
+lean_mark_persistent(l_Lean_Parser_Syntax_precedence___elambda__1___closed__8);
 l_Lean_Parser_Syntax_precedence___closed__1 = _init_l_Lean_Parser_Syntax_precedence___closed__1();
 lean_mark_persistent(l_Lean_Parser_Syntax_precedence___closed__1);
 l_Lean_Parser_Syntax_precedence___closed__2 = _init_l_Lean_Parser_Syntax_precedence___closed__2();
@ -10457,6 +10522,8 @@ l_Lean_Parser_Syntax_precedence___closed__4 = _init_l_Lean_Parser_Syntax_precede
 lean_mark_persistent(l_Lean_Parser_Syntax_precedence___closed__4);
 l_Lean_Parser_Syntax_precedence___closed__5 = _init_l_Lean_Parser_Syntax_precedence___closed__5();
 lean_mark_persistent(l_Lean_Parser_Syntax_precedence___closed__5);
+l_Lean_Parser_Syntax_precedence___closed__6 = _init_l_Lean_Parser_Syntax_precedence___closed__6();
+lean_mark_persistent(l_Lean_Parser_Syntax_precedence___closed__6);
 l_Lean_Parser_Syntax_precedence = _init_l_Lean_Parser_Syntax_precedence();
 lean_mark_persistent(l_Lean_Parser_Syntax_precedence);
 l_Lean_Parser_Syntax_paren___elambda__1___closed__1 = _init_l_Lean_Parser_Syntax_paren___elambda__1___closed__1();
--- a/stage0/stdlib/Init/Lean/Parser/Tactic.c
+++ b/stage0/stdlib/Init/Lean/Parser/Tactic.c