chore: update stage0

stage0/src/Lean/Compiler.lean

@@ -14,3 +14,7 @@ import Lean.Compiler.IR
 import Lean.Compiler.CSimpAttr
 import Lean.Compiler.FFI
 import Lean.Compiler.NoncomputableAttr
+import Lean.Compiler.CompilerM
+import Lean.Compiler.LCNF
+import Lean.Compiler.Decl
+import Lean.Compiler.Main

stage0/src/Lean/Compiler/CompilerM.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.InferType
+
+namespace Lean.Compiler
+
+structure CompilerM.State where
+  lctx     : LocalContext
+  letFVars : Array Expr := #[]
+
+abbrev CompilerM := StateRefT CompilerM.State CoreM
+
+@[inline] def liftMetaM (x : MetaM α) : CompilerM α := do
+  x.run' { lctx := (← get).lctx }
+
+def inferType (e : Expr) : CompilerM Expr := liftMetaM <| Meta.inferType e
+
+def whnf (e : Expr) : CompilerM Expr := liftMetaM <| Meta.whnf e
+
+def isProp (e : Expr) : CompilerM Bool := liftMetaM <| Meta.isProp e
+
+def isTypeFormerType (e : Expr) : CompilerM Bool := liftMetaM <| Meta.isTypeFormerType e
+
+def mkLocalDecl (binderName : Name) (type : Expr) (bi := BinderInfo.default) : CompilerM Expr := do
+  let fvarId ← mkFreshFVarId
+  modify fun s => { s with lctx := s.lctx.mkLocalDecl fvarId binderName type bi }
+  return .fvar fvarId
+
+def mkLetDecl (binderName : Name) (type : Expr) (value : Expr) (nonDep : Bool) : CompilerM Expr := do
+  let fvarId ← mkFreshFVarId
+  let x := .fvar fvarId
+  modify fun s => { s with lctx := s.lctx.mkLetDecl fvarId binderName type value nonDep, letFVars := s.letFVars.push x }
+  return x
+
+def visitLambda (e : Expr) : CompilerM (Array Expr × Expr) :=
+  go e #[]
+where
+  go (e : Expr) (fvars : Array Expr) := do
+    if let .lam binderName type body binderInfo := e then
+      let type := type.instantiateRev fvars
+      let fvar ← mkLocalDecl binderName type binderInfo
+      go body (fvars.push fvar)
+    else
+      return (fvars, e.instantiateRev fvars)
+
+def withNewScopeImp (x : CompilerM α) : CompilerM α := do
+  let s ← get
+  modify fun s => { s with letFVars := #[] }
+  try x finally set s
+
+def withNewScope [MonadFunctorT CompilerM m] (x : m α) : m α :=
+  monadMap (m := CompilerM) withNewScopeImp x
+
+class VisitLet (m : Type → Type) where
+  visitLet : Expr → (Expr → m Expr) → m Expr
+
+export VisitLet (visitLet)
+
+def visitLetImp (e : Expr) (f : Expr → CompilerM Expr) : CompilerM Expr :=
+  go e #[]
+where
+  go (e : Expr) (fvars : Array Expr) : CompilerM Expr := do
+    if let .letE binderName type value body nonDep := e then
+      let type := type.instantiateRev fvars
+      let value := value.instantiateRev fvars
+      let value ← f value
+      let fvar ← mkLetDecl binderName type value nonDep
+      go body (fvars.push fvar)
+    else
+      return e.instantiateRev fvars
+
+instance : VisitLet CompilerM where
+  visitLet := visitLetImp
+
+instance [VisitLet m] : VisitLet (ReaderT ρ m) where
+  visitLet e f ctx := visitLet e (f · ctx)
+
+instance [VisitLet m] : VisitLet (StateRefT' ω σ m) := inferInstanceAs (VisitLet (ReaderT _ _))
+
+def mkLetUsingScope (e : Expr) : CompilerM Expr :=
+  return (← get).lctx.mkLambda (← get).letFVars e
+
+def mkLambda (xs : Array Expr) (e : Expr) : CompilerM Expr :=
+  return (← get).lctx.mkLambda xs e
+
+end Lean.Compiler

stage0/src/Lean/Compiler/Decl.lean

@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Transform
+import Lean.Compiler.LCNF
+
+namespace Lean.Compiler
+
+/--
+Declaration being processed by the Lean to Lean compiler passes.
+-/
+structure Decl where
+  name  : Name
+  type  : Expr
+  value : Expr
+
+/--
+Inline constants tagged with the `[macroInline]` attribute occurring in `e`.
+-/
+def macroInline (e : Expr) : CoreM Expr :=
+  Core.transform e fun e => do
+    let .const declName us := e.getAppFn | return .visit e
+    unless hasMacroInlineAttribute (← getEnv) declName do return .visit e
+    let val ← Core.instantiateValueLevelParams (← getConstInfo declName) us
+    return .visit <| val.beta e.getAppArgs
+
+/--
+Replace nested occurrences of `unsafeRec` names with the safe ones.
+-/
+private def replaceUnsafeRecNames (value : Expr) : CoreM Expr :=
+  Core.transform value fun e =>
+    match e with
+    | .const declName us =>
+      if let some safeDeclName := isUnsafeRecName? declName then
+        return .done (.const safeDeclName us)
+      else
+        return .done e
+    | _ => return .visit e
+
+/--
+Convert the given declaration from the Lean environment into `Decl`.
+
+Remarks:
+- If the declaration has an unsafe-rec version, we use it.
+- We eta-expand the declaration value.
+- We expand declarations tagged with the `[MacroInline]` attribute
+-/
+def toDecl (declName : Name) : CoreM Decl := do
+  let env ← getEnv
+  let some info := env.find? (mkUnsafeRecName declName) <|> env.find? declName | throwError "declaration `{declName}` not found"
+  let some value := info.value? | throwError "declaration `{declName}` does not have a value"
+  Meta.MetaM.run' do
+    let value ← Meta.lambdaTelescope value fun xs body => do Meta.mkLambdaFVars xs (← Meta.etaExpand body)
+    let value ← replaceUnsafeRecNames value
+    let value ← macroInline value
+    let value ← toLCNF {} value
+    return { name := declName, type := info.type, value }
+
+end Lean.Compiler

stage0/src/Lean/Compiler/LCNF.lean

@@ -0,0 +1,142 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Match.MatcherInfo
+import Lean.Meta.Transform
+import Lean.Compiler.InlineAttrs
+import Lean.Compiler.CompilerM
+
+namespace Lean.Compiler
+/-!
+# Lean Compiler Normal Form (LCNF)
+
+It is based on the [A-normal form](https://en.wikipedia.org/wiki/A-normal_form),
+and the approach described in the paper
+[Compiling  without continuations](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/compiling-without-continuations.pdf).
+-/
+
+/--
+Return `true` if `e` is a `lcProof` application.
+Recall that we use `lcProof` to erase all nested proofs.
+-/
+def isLCProof (e : Expr) : Bool :=
+  e.isAppOfArity ``lcProof 1
+
+/--
+Recursors, noConfusion, constructors, and matchers are not treated as regular
+functions by the code generator. We eta-expand all of them to make sure they are
+not partially applied.
+-/
+def shouldEtaExpand (declName : Name) : CoreM Bool := do
+  let env ← getEnv
+  if isCasesOnRecursor env declName then return true
+  if isNoConfusion env declName then return true
+  if (← isRec declName) then return true
+  if (← Meta.isMatcher declName) then return true
+  if env.isConstructor declName then return true
+  if declName == ``Quot.lift then return true
+  return false
+
+/--
+Return `true` if `mdata` should be preserved.
+Right now, we don't preserve any `MData`, but this may
+change in the future when we add support for debugging information
+-/
+def isCompilerRelevantMData (_mdata : MData) : Bool :=
+  false
+
+namespace ToLCNF
+
+structure Context where
+  root : Bool
+
+structure State where
+  cache     : ExprMap Expr := {}
+
+abbrev M := ReaderT Context $ StateRefT State CompilerM
+
+def mkFreshLetDecl (e : Expr) : M Expr := do
+  if (← read).root then
+    return e
+  else
+    mkLetDecl (← mkFreshUserName `x) (← inferType e) e (nonDep := false)
+
+def withNewRoot (x : M α) : M α := do
+  let s ← get
+  try
+    withReader (fun _ => { root := true }) <| Compiler.withNewScope x
+  finally
+    set s
+
+/--
+Put the given expression in `LCNF`.
+
+- Nested proofs are replaced with `lcProof`-applications.
+- Eta-expand applications of declarations that satisfy `shouldEtaExpand`.
+- Put computationally relevant expressions in A-normal form.
+-/
+partial def toLCNF (lctx : LocalContext) (e : Expr) : CoreM Expr := do
+  let ((e, _), s) ← visit e |>.run { root := true } |>.run {} |>.run { lctx }
+  return s.lctx.mkLambda s.letFVars e
+where
+  visitChild (e : Expr) : M Expr :=
+    withReader (fun _ => { root := false }) <| visit e
+
+  visitApp (f : Expr) (args : Array Expr) : M Expr := do
+    -- TODO: handle special cases
+    let f := f
+    let args ← args.mapM visitChild
+    mkFreshLetDecl <| mkAppN f args
+
+  visitLambda (e : Expr) : M Expr := do
+    let r ← withNewRoot do
+      let (as, e) ← Compiler.visitLambda e
+      let e ← mkLetUsingScope (← visit e)
+      mkLambda as e
+    mkFreshLetDecl r
+
+  visitMData (mdata : MData) (e : Expr) : M Expr := do
+    if isCompilerRelevantMData mdata then
+      mkFreshLetDecl <| .mdata mdata (← visitChild e)
+    else
+      visit e
+
+  visitProj (s : Name) (i : Nat) (e : Expr) : M Expr := do
+    mkFreshLetDecl <| .proj s i (← visitChild e)
+
+  visit (e : Expr) : M Expr := withIncRecDepth do
+    match e with
+    | .mvar .. => throwError "unexpected occurrence of metavariable in code generator{indentExpr e}"
+    | .bvar .. => unreachable!
+    | .fvar .. | .sort .. | .forallE .. => return e -- Do nothing
+    | _ =>
+    if isLCProof e then
+      return e
+    let type ← inferType e
+    if (← isProp type) then
+      /- We replace proofs with `lcProof` applications. -/
+      return mkApp (mkConst ``lcProof) type
+    if (← isTypeFormerType type) then
+      /- Types and Type formers are not put into A-normal form. -/
+      return e
+    if let some e := (← get).cache.find? e then
+      return e
+    let r ← match e with
+      | .app ..     => e.withApp fun f args => visitApp f args
+      | .const ..   => visitApp e #[]
+      | .proj s i e => visitProj s i e
+      | .mdata d e  => visitMData d e
+      | .lam ..     => visitLambda e
+      | .letE ..    => visit (← visitLet e visitChild)
+      | .lit ..     => mkFreshLetDecl e
+      | _           => pure e
+    modify fun s => { s with cache := s.cache.insert e r }
+    return r
+
+end ToLCNF
+
+export ToLCNF (toLCNF)
+
+end Lean.Compiler

stage0/src/Lean/Compiler/Main.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Compiler.LCNF
+import Lean.Compiler.Decl
+
+namespace Lean.Compiler
+
+/--
+We do not generate code for `declName` if
+- Its type is a proposition.
+- Its type is a type former.
+- It is tagged as `[macroInline]`.
+- It is matcher auxiliary function.
+- It is a type class instance.
+
+Remark: we still generate code for declarations tagged as `[inline]`
+and `[specialize]` since they can be partially applied.
+-/
+def shouldGenerateCode (declName : Name) : CoreM Bool := do
+  if (← isCompIrrelevant |>.run') then return false
+  if (← Meta.isMatcher declName) then return false
+  if hasMacroInlineAttribute (← getEnv) declName then return false
+  -- TODO: check if type class instance
+  return true
+where
+  isCompIrrelevant : MetaM Bool := do
+    let info ← getConstInfo declName
+    Meta.isProp info.type <||> Meta.isTypeFormerType info.type
+
+def compile (declNames : Array Name) : CoreM Unit := do
+  let declNames ← declNames.filterM shouldGenerateCode
+  let decls ← declNames.mapM toDecl
+  -- WIP
+  for decl in decls do
+    trace[Meta.debug] "{decl.name} := {decl.value}"
+    pure ()
+
+end Lean.Compiler

stage0/src/Lean/Elab/Syntax.lean

@@ -53,11 +53,17 @@ def ensureUnaryOutput (x : Term × Nat) : Term :=
 @[inline] private def withNestedParser (x : ToParserDescr) : ToParserDescr := do
   withReader (fun ctx => { ctx with leftRec := false, first := false }) x
 
-/-- (Try to) a term info for the category `catName` at `ref`. -/
+/-- (Try to) add a term info for the category `catName` at `ref`. -/
 def addCategoryInfo (ref : Syntax) (catName : Name) : TermElabM Unit := do
-    let declName := ``Lean.Parser.Category ++ catName
-    if (← getEnv).contains declName then
-      addTermInfo' ref (Lean.mkConst declName)
+  let declName := ``Lean.Parser.Category ++ catName
+  if (← getEnv).contains declName then
+    addTermInfo' ref (Lean.mkConst declName)
+
+/-- (Try to) add a term info for the alias with info `info` at `ref`. -/
+def addAliasInfo (ref : Syntax) (info : Parser.ParserAliasInfo) : TermElabM Unit := do
+  if (← getInfoState).enabled then
+    if (← getEnv).contains info.declName then
+      addTermInfo' ref (Lean.mkConst info.declName)
 
 def checkLeftRec (stx : Syntax) : ToParserDescrM Bool := do
   let ctx ← read
@@ -161,6 +167,7 @@ where
   processAlias (id : Syntax) (args : Array Syntax) := do
     let aliasName := id.getId.eraseMacroScopes
     let info ← Parser.getParserAliasInfo aliasName
+    addAliasInfo id info
     let args ← args.mapM (withNestedParser ∘ process)
     let (args, stackSz) := if let some stackSz := info.stackSz? then
       if !info.autoGroupArgs then
@@ -205,14 +212,14 @@ where
     let sep := stx[3]
     let psep ← if stx[4].isNone then `(ParserDescr.symbol $sep) else ensureUnaryOutput <$> withNestedParser do process stx[4][1]
     let allowTrailingSep := !stx[5].isNone
-    return (← `(ParserDescr.sepBy $p $sep $psep $(quote allowTrailingSep)), 1)
+    return (← `((with_annotate_term $(stx[0]) @ParserDescr.sepBy) $p $sep $psep $(quote allowTrailingSep)), 1)
 
   processSepBy1 (stx : Syntax) := do
     let p ← ensureUnaryOutput <$> withNestedParser do process stx[1]
     let sep := stx[3]
     let psep ← if stx[4].isNone then `(ParserDescr.symbol $sep) else ensureUnaryOutput <$> withNestedParser do process stx[4][1]
     let allowTrailingSep := !stx[5].isNone
-    return (← `(ParserDescr.sepBy1 $p $sep $psep $(quote allowTrailingSep)), 1)
+    return (← `((with_annotate_term $(stx[0]) @ParserDescr.sepBy1) $p $sep $psep $(quote allowTrailingSep)), 1)
 
   isValidAtom (s : String) : Bool :=
     !s.isEmpty &&
@@ -235,9 +242,8 @@ where
     | none => throwUnsupportedSyntax
 
   processNonReserved (stx : Syntax) := do
-    match stx[1].isStrLit? with
-    | some atom => return (← `(ParserDescr.nonReservedSymbol $(quote atom) false), 1)
-    | none      => throwUnsupportedSyntax
+    let some atom := stx[1].isStrLit? | throwUnsupportedSyntax
+    return (← `((with_annotate_term $(stx[0]) @ParserDescr.nonReservedSymbol) $(quote atom) false), 1)
 
 
 end Term

stage0/src/Lean/Elab/Tactic/Config.lean

@@ -27,7 +27,7 @@ macro (name := configElab) doc?:(docComment)? "declare_config_elab" elabName:ide
   )
 
 open Linter.MissingDocs in
-@[missingDocsHandler Elab.Tactic.configElab]
+@[builtinMissingDocsHandler Elab.Tactic.configElab]
 def checkConfigElab : SimpleHandler := mkSimpleHandler "config elab"
 
 end Lean.Elab.Tactic

stage0/src/Lean/Linter/MissingDocs.lean

@@ -116,7 +116,7 @@ def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) : CommandElabM Unit := do
   else if k == ``classInductive then lintNamed id "public inductive"
   else if k == ``«structure» then lintNamed id "public structure"
 
-@[missingDocsHandler declaration]
+@[builtinMissingDocsHandler declaration]
 def checkDecl : SimpleHandler := fun stx => do
   let head := stx[0]; let rest := stx[1]
   if head[2][0].getKind == ``«private» then return -- not private
@@ -145,13 +145,13 @@ def checkDecl : SimpleHandler := fun stx => do
             for stx in stx[2].getArgs do
               lintField rest[1][0] stx "public field"
 
-@[missingDocsHandler «initialize»]
+@[builtinMissingDocsHandler «initialize»]
 def checkInit : SimpleHandler := fun stx => do
   if stx[2].isNone then return
   if stx[0][2][0].getKind != ``«private» && stx[0][0].isNone then
     lintNamed stx[2][0] "initializer"
 
-@[missingDocsHandler «syntax»]
+@[builtinMissingDocsHandler «syntax»]
 def checkSyntax : SimpleHandler := fun stx => do
   if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
     if stx[5].isNone then lint stx[3] "syntax"
@@ -161,40 +161,43 @@ def mkSimpleHandler (name : String) : SimpleHandler := fun stx => do
   if stx[0].isNone then
     lintNamed stx[2] name
 
-@[missingDocsHandler syntaxAbbrev]
+@[builtinMissingDocsHandler syntaxAbbrev]
 def checkSyntaxAbbrev : SimpleHandler := mkSimpleHandler "syntax"
 
-@[missingDocsHandler syntaxCat]
+@[builtinMissingDocsHandler syntaxCat]
 def checkSyntaxCat : SimpleHandler := mkSimpleHandler "syntax category"
 
-@[missingDocsHandler «macro»]
+@[builtinMissingDocsHandler «macro»]
 def checkMacro : SimpleHandler := fun stx => do
   if stx[0].isNone && stx[1][0][0].getKind != ``«local» then
     if stx[4].isNone then lint stx[2] "macro"
     else lintNamed stx[4][0][3] "macro"
 
-@[missingDocsHandler «elab»]
+@[builtinMissingDocsHandler «elab»]
 def checkElab : SimpleHandler := fun stx => do
   if stx[0].isNone && stx[1][0][0].getKind != ``«local» then
     if stx[4].isNone then lint stx[2] "elab"
     else lintNamed stx[4][0][3] "elab"
 
-@[missingDocsHandler classAbbrev]
+@[builtinMissingDocsHandler classAbbrev]
 def checkClassAbbrev : SimpleHandler := fun stx => do
   let head := stx[0]
   if head[2][0].getKind != ``«private» && head[0].isNone then
     lintNamed stx[3] "class abbrev"
 
-@[missingDocsHandler Parser.Tactic.declareSimpLikeTactic]
+@[builtinMissingDocsHandler Parser.Tactic.declareSimpLikeTactic]
 def checkSimpLike : SimpleHandler := mkSimpleHandler "simp-like tactic"
 
-@[missingDocsHandler Option.registerBuiltinOption, missingDocsHandler Option.registerOption]
+@[builtinMissingDocsHandler Option.registerBuiltinOption]
+def checkRegisterBuiltinOption : SimpleHandler := mkSimpleHandler "option"
+
+@[builtinMissingDocsHandler Option.registerOption]
 def checkRegisterOption : SimpleHandler := mkSimpleHandler "option"
 
-@[missingDocsHandler registerSimpAttr]
+@[builtinMissingDocsHandler registerSimpAttr]
 def checkRegisterSimpAttr : SimpleHandler := mkSimpleHandler "simp attr"
 
-@[missingDocsHandler «in»]
+@[builtinMissingDocsHandler «in»]
 def handleIn : Handler := fun _ stx => do
   if stx[0].getKind == ``«set_option» then
     let opts ← Elab.elabSetOption stx[0][1] stx[0][2]
@@ -203,6 +206,6 @@ def handleIn : Handler := fun _ stx => do
   else
     missingDocs stx[2]
 
-@[missingDocsHandler «mutual»]
+@[builtinMissingDocsHandler «mutual»]
 def handleMutual : Handler := fun _ stx => do
   stx[1].getArgs.forM missingDocs

stage0/src/Lean/Meta/InferType.lean

@@ -363,6 +363,9 @@ partial def isTypeQuick : Expr → MetaM LBool
   | .mvar mvarId      => do let mvarType  ← inferMVarType mvarId;  isArrowType mvarType 0
   | .app f ..         => isTypeQuickApp f 1
 
+/--
+Return `true` iff the type of `e` is a `Sort _`.
+-/
 def isType (e : Expr) : MetaM Bool := do
   match (← isTypeQuick e) with
   | .true  => return true
@@ -374,6 +377,9 @@ def isType (e : Expr) : MetaM Bool := do
     | .sort .. => return true
     | _        => return false
 
+/--
+Return true iff `type` is `Sort _` or `As → Sort _`.
+-/
 partial def isTypeFormerType (type : Expr) : MetaM Bool := do
   let type ← whnfD type
   match type with
@@ -383,8 +389,9 @@ partial def isTypeFormerType (type : Expr) : MetaM Bool := do
   | _ => return false
 
 /--
-  Return true iff `e : Sort _` or `e : (forall As, Sort _)`.
-  Remark: it subsumes `isType` -/
+Return true iff `e : Sort _` or `e : (forall As, Sort _)`.
+Remark: it subsumes `isType`
+-/
 def isTypeFormer (e : Expr) : MetaM Bool := do
   isTypeFormerType (← inferType e)
 

stage0/src/Lean/Parser.lean

@@ -42,7 +42,7 @@ builtin_initialize
   register_parser_alias orelse
   register_parser_alias andthen { stackSz? := none }
 
-  registerAlias "notFollowedBy" (notFollowedBy · "element")
+  registerAlias "notFollowedBy" ``notFollowedBy (notFollowedBy · "element")
   Parenthesizer.registerAlias "notFollowedBy" notFollowedBy.parenthesizer
   Formatter.registerAlias "notFollowedBy" notFollowedBy.formatter
 

stage0/src/Lean/Parser/Extension.lean

@@ -210,6 +210,7 @@ def getBinaryAlias {α} (mapRef : IO.Ref (AliasTable α)) (aliasName : Name) : I
 abbrev ParserAliasValue := AliasValue Parser
 
 structure ParserAliasInfo where
+  declName : Name := .anonymous
   /-- Number of syntax nodes produced by this parser. `none` means "sum of input sizes". -/
   stackSz? : Option Nat := some 1
   /-- Whether arguments should be wrapped in `group(·)` if they do not produce exactly one syntax node. -/
@@ -223,11 +224,11 @@ def getParserAliasInfo (aliasName : Name) : IO ParserAliasInfo := do
   return (← parserAliases2infoRef.get).findD aliasName {}
 
 -- Later, we define macro `register_parser_alias` which registers a parser, formatter and parenthesizer
-def registerAlias (aliasName : Name) (p : ParserAliasValue) (kind? : Option SyntaxNodeKind := none) (info : ParserAliasInfo := {}) : IO Unit := do
+def registerAlias (aliasName declName : Name) (p : ParserAliasValue) (kind? : Option SyntaxNodeKind := none) (info : ParserAliasInfo := {}) : IO Unit := do
   registerAliasCore parserAliasesRef aliasName p
   if let some kind := kind? then
     parserAlias2kindRef.modify (·.insert aliasName kind)
-  parserAliases2infoRef.modify (·.insert aliasName info)
+  parserAliases2infoRef.modify (·.insert aliasName { info with declName })
 
 instance : Coe Parser ParserAliasValue := { coe := AliasValue.const }
 instance : Coe (Parser → Parser) ParserAliasValue := { coe := AliasValue.unary }

stage0/src/Lean/Parser/Extra.lean

@@ -175,7 +175,7 @@ macro_rules
     let [(fullDeclName, [])] ← Macro.resolveGlobalName declName.getId |
       Macro.throwError "expected non-overloaded constant name"
     let aliasName := aliasName?.getD (Syntax.mkStrLit declName.getId.toString)
-    `(do Parser.registerAlias $aliasName $declName $(info?.getD (Unhygienic.run `({}))) (kind? := some $(kind?.getD (quote fullDeclName)))
+    `(do Parser.registerAlias $aliasName ``$declName $declName $(info?.getD (Unhygienic.run `({}))) (kind? := some $(kind?.getD (quote fullDeclName)))
          PrettyPrinter.Formatter.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `formatter))
          PrettyPrinter.Parenthesizer.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `parenthesizer)))
 

stage0/src/runtime/object.cpp

@@ -1112,7 +1112,7 @@ extern "C" LEAN_EXPORT object * lean_nat_big_mod(object * a1, object * a2) {
             lean_inc(a1);
             return a1;
         } else {
-            return lean_box((mpz_value(a1) % mpz::of_size_t(n2)).get_unsigned_int());
+            return mpz_to_nat(mpz_value(a1) % mpz::of_size_t(n2));
         }
     } else {
         lean_assert(mpz_value(a2) != 0);

stage0/stdlib/Lean/Compiler.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.Compiler
-// Imports: Init Lean.Compiler.InlineAttrs Lean.Compiler.Specialize Lean.Compiler.ConstFolding Lean.Compiler.ClosedTermCache Lean.Compiler.ExternAttr Lean.Compiler.ImplementedByAttr Lean.Compiler.NeverExtractAttr Lean.Compiler.IR Lean.Compiler.CSimpAttr Lean.Compiler.FFI Lean.Compiler.NoncomputableAttr
+// Imports: Init Lean.Compiler.InlineAttrs Lean.Compiler.Specialize Lean.Compiler.ConstFolding Lean.Compiler.ClosedTermCache Lean.Compiler.ExternAttr Lean.Compiler.ImplementedByAttr Lean.Compiler.NeverExtractAttr Lean.Compiler.IR Lean.Compiler.CSimpAttr Lean.Compiler.FFI Lean.Compiler.NoncomputableAttr Lean.Compiler.CompilerM Lean.Compiler.LCNF Lean.Compiler.Decl Lean.Compiler.Main
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -25,6 +25,10 @@ lean_object* initialize_Lean_Compiler_IR(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Compiler_CSimpAttr(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Compiler_FFI(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Compiler_NoncomputableAttr(uint8_t builtin, lean_object*);
+lean_object* initialize_Lean_Compiler_CompilerM(uint8_t builtin, lean_object*);
+lean_object* initialize_Lean_Compiler_LCNF(uint8_t builtin, lean_object*);
+lean_object* initialize_Lean_Compiler_Decl(uint8_t builtin, lean_object*);
+lean_object* initialize_Lean_Compiler_Main(uint8_t builtin, lean_object*);
 static bool _G_initialized = false;
 LEAN_EXPORT lean_object* initialize_Lean_Compiler(uint8_t builtin, lean_object* w) {
 lean_object * res;
@@ -66,6 +70,18 @@ lean_dec_ref(res);
 res = initialize_Lean_Compiler_NoncomputableAttr(builtin, lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Lean_Compiler_CompilerM(builtin, lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Compiler_LCNF(builtin, lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Compiler_Decl(builtin, lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Compiler_Main(builtin, lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Lean/Elab/MacroArgUtil.c

@@ -268,7 +268,7 @@ if (x_8 == 0)
 {
 lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12; 
 x_9 = lean_ctor_get(x_7, 0);
-x_10 = lean_ctor_get(x_9, 0);
+x_10 = lean_ctor_get(x_9, 1);
 lean_inc(x_10);
 lean_dec(x_9);
 x_11 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_expandMacroArg_mkAntiquotNode___spec__1___lambda__1___closed__1;
@@ -299,7 +299,7 @@ x_18 = lean_ctor_get(x_7, 1);
 lean_inc(x_18);
 lean_inc(x_17);
 lean_dec(x_7);
-x_19 = lean_ctor_get(x_17, 0);
+x_19 = lean_ctor_get(x_17, 1);
 lean_inc(x_19);
 lean_dec(x_17);
 x_20 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_expandMacroArg_mkAntiquotNode___spec__1___lambda__1___closed__1;
@@ -435,7 +435,7 @@ lean_inc(x_40);
 x_41 = lean_ctor_get(x_39, 1);
 lean_inc(x_41);
 lean_dec(x_39);
-x_42 = lean_ctor_get(x_40, 0);
+x_42 = lean_ctor_get(x_40, 1);
 lean_inc(x_42);
 lean_dec(x_40);
 x_43 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_expandMacroArg_mkAntiquotNode___spec__1___lambda__1___closed__1;
@@ -666,7 +666,7 @@ lean_inc(x_40);
 x_41 = lean_ctor_get(x_39, 1);
 lean_inc(x_41);
 lean_dec(x_39);
-x_42 = lean_ctor_get(x_40, 0);
+x_42 = lean_ctor_get(x_40, 1);
 lean_inc(x_42);
 lean_dec(x_40);
 x_43 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_expandMacroArg_mkAntiquotNode___spec__1___lambda__1___closed__1;
@@ -2670,7 +2670,7 @@ lean_inc(x_40);
 x_41 = lean_ctor_get(x_39, 1);
 lean_inc(x_41);
 lean_dec(x_39);
-x_42 = lean_ctor_get(x_40, 0);
+x_42 = lean_ctor_get(x_40, 1);
 lean_inc(x_42);
 lean_dec(x_40);
 x_43 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_expandMacroArg_mkAntiquotNode___spec__1___lambda__1___closed__1;
@@ -2900,7 +2900,7 @@ lean_inc(x_40);
 x_41 = lean_ctor_get(x_39, 1);
 lean_inc(x_41);
 lean_dec(x_39);
-x_42 = lean_ctor_get(x_40, 0);
+x_42 = lean_ctor_get(x_40, 1);
 lean_inc(x_42);
 lean_dec(x_40);
 x_43 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_expandMacroArg_mkAntiquotNode___spec__1___lambda__1___closed__1;

stage0/stdlib/Lean/Elab/Tactic/Config.c

@@ -31,6 +31,7 @@ lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__15;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__18;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__100;
+lean_object* l_Lean_Linter_MissingDocs_SimpleHandler_toHandler___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__110;
 lean_object* l_Lean_Syntax_getOptional_x3f(lean_object*);
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__46;
@@ -97,6 +98,7 @@ static lean_object* l_Lean_Elab_Tactic_configElab___closed__17;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__167;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__124;
 static lean_object* l_Lean_Elab_Tactic_configElab___closed__8;
+LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_checkConfigElab(lean_object*);
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__63;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__177;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__262;
@@ -186,6 +188,7 @@ static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______ma
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__151;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__39;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__169;
+static lean_object* l___regBuiltin_Lean_Elab_Tactic_checkConfigElab___closed__1;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__90;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__102;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__148;
@@ -200,6 +203,7 @@ static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______ma
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__209;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__12;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__226;
+static lean_object* l___regBuiltin_Lean_Elab_Tactic_checkConfigElab___closed__2;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__141;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__223;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__205;
@@ -312,6 +316,7 @@ static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______ma
 static lean_object* l_Lean_Elab_Tactic_configElab___closed__10;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__204;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__237;
+lean_object* l_Lean_Linter_MissingDocs_addBuiltinHandler(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__69;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__194;
 static lean_object* l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__82;
@@ -4360,6 +4365,34 @@ lean_dec(x_1);
 return x_5;
 }
 }
+static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_checkConfigElab___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_checkConfigElab___boxed), 4, 0);
+return x_1;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_checkConfigElab___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l___regBuiltin_Lean_Elab_Tactic_checkConfigElab___closed__1;
+x_2 = lean_alloc_closure((void*)(l_Lean_Linter_MissingDocs_SimpleHandler_toHandler___boxed), 6, 1);
+lean_closure_set(x_2, 0, x_1);
+return x_2;
+}
+}
+LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_checkConfigElab(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_2 = l_Lean_Elab_Tactic_configElab___closed__8;
+x_3 = l___regBuiltin_Lean_Elab_Tactic_checkConfigElab___closed__2;
+x_4 = l_Lean_Linter_MissingDocs_addBuiltinHandler(x_2, x_3, x_1);
+return x_4;
+}
+}
 lean_object* initialize_Init(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Meta_Eval(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Elab_Tactic_Basic(uint8_t builtin, lean_object*);
@@ -4963,6 +4996,13 @@ l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab
 lean_mark_persistent(l_Lean_Elab_Tactic___aux__Lean__Elab__Tactic__Config______macroRules__Lean__Elab__Tactic__configElab__1___closed__262);
 l_Lean_Elab_Tactic_checkConfigElab___closed__1 = _init_l_Lean_Elab_Tactic_checkConfigElab___closed__1();
 lean_mark_persistent(l_Lean_Elab_Tactic_checkConfigElab___closed__1);
+l___regBuiltin_Lean_Elab_Tactic_checkConfigElab___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_checkConfigElab___closed__1();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_checkConfigElab___closed__1);
+l___regBuiltin_Lean_Elab_Tactic_checkConfigElab___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_checkConfigElab___closed__2();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_checkConfigElab___closed__2);
+res = l___regBuiltin_Lean_Elab_Tactic_checkConfigElab(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Lean/Parser/Do.c

@@ -1365,7 +1365,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Term_doIfLetPure___elambda__1(lean_object
 static lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__15;
 static lean_object* l___regBuiltin_Lean_Parser_Term_doUnless_parenthesizer___closed__2;
 static lean_object* l_Lean_Parser_Term_doSeqItem___elambda__1___closed__1;
-lean_object* l_Lean_Parser_registerAlias(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_registerAlias(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Parser_Term_doElem_quot_parenthesizer___closed__6;
 static lean_object* l_Lean_Parser_Term_doUnless___elambda__1___closed__13;
 static lean_object* l_Lean_Parser_Term_doDbgTrace_parenthesizer___closed__3;
@@ -5968,13 +5968,15 @@ return x_2;
 static lean_object* _init_l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__5() {
 _start:
 {
-lean_object* x_1; uint8_t x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__4;
-x_2 = 1;
-x_3 = lean_alloc_ctor(0, 1, 1);
-lean_ctor_set(x_3, 0, x_1);
-lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
-return x_3;
+lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__4;
+x_3 = 1;
+x_4 = lean_alloc_ctor(0, 2, 1);
+lean_ctor_set(x_4, 0, x_1);
+lean_ctor_set(x_4, 1, x_2);
+lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_3);
+return x_4;
 }
 }
 static lean_object* _init_l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__6() {
@@ -6050,16 +6052,6 @@ return x_3;
 static lean_object* _init_l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__14() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Parser_Term_termBeforeDo;
-x_2 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_2, 0, x_1);
-return x_2;
-}
-}
-static lean_object* _init_l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__15() {
-_start:
-{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__2;
 x_2 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__12;
@@ -6067,11 +6059,21 @@ x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;
 }
 }
+static lean_object* _init_l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__15() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Parser_Term_termBeforeDo;
+x_2 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
 static lean_object* _init_l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__16() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__15;
+x_1 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__14;
 x_2 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
@@ -6116,170 +6118,172 @@ return x_2;
 LEAN_EXPORT lean_object* l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189_(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__1;
-x_3 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__2;
-x_4 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__3;
-x_5 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__5;
-x_6 = l_Lean_Parser_registerAlias(x_2, x_3, x_4, x_5, x_1);
-if (lean_obj_tag(x_6) == 0)
+x_3 = l_Lean_Parser_Term_doSeq___elambda__1___closed__2;
+x_4 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__2;
+x_5 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__3;
+x_6 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__5;
+x_7 = l_Lean_Parser_registerAlias(x_2, x_3, x_4, x_5, x_6, x_1);
+if (lean_obj_tag(x_7) == 0)
 {
-lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
-x_7 = lean_ctor_get(x_6, 1);
-lean_inc(x_7);
-lean_dec(x_6);
-x_8 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__8;
-x_9 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__7;
-x_10 = l_Lean_Parser_registerAliasCore___rarg(x_8, x_2, x_9, x_7);
-if (lean_obj_tag(x_10) == 0)
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_8 = lean_ctor_get(x_7, 1);
+lean_inc(x_8);
+lean_dec(x_7);
+x_9 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__8;
+x_10 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__7;
+x_11 = l_Lean_Parser_registerAliasCore___rarg(x_9, x_2, x_10, x_8);
+if (lean_obj_tag(x_11) == 0)
 {
-lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
-x_11 = lean_ctor_get(x_10, 1);
-lean_inc(x_11);
-lean_dec(x_10);
-x_12 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__11;
-x_13 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__10;
-x_14 = l_Lean_Parser_registerAliasCore___rarg(x_12, x_2, x_13, x_11);
-if (lean_obj_tag(x_14) == 0)
+lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
+x_12 = lean_ctor_get(x_11, 1);
+lean_inc(x_12);
+lean_dec(x_11);
+x_13 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__11;
+x_14 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__10;
+x_15 = l_Lean_Parser_registerAliasCore___rarg(x_13, x_2, x_14, x_12);
+if (lean_obj_tag(x_15) == 0)
 {
-lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; 
-x_15 = lean_ctor_get(x_14, 1);
-lean_inc(x_15);
-lean_dec(x_14);
-x_16 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__13;
-x_17 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__14;
-x_18 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__16;
-x_19 = l_Lean_Parser_registerAlias(x_16, x_17, x_18, x_5, x_15);
-if (lean_obj_tag(x_19) == 0)
+lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; 
+x_16 = lean_ctor_get(x_15, 1);
+lean_inc(x_16);
+lean_dec(x_15);
+x_17 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__13;
+x_18 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__14;
+x_19 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__15;
+x_20 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__16;
+x_21 = l_Lean_Parser_registerAlias(x_17, x_18, x_19, x_20, x_6, x_16);
+if (lean_obj_tag(x_21) == 0)
 {
-lean_object* x_20; lean_object* x_21; lean_object* x_22; 
-x_20 = lean_ctor_get(x_19, 1);
-lean_inc(x_20);
-lean_dec(x_19);
-x_21 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__18;
-x_22 = l_Lean_Parser_registerAliasCore___rarg(x_8, x_16, x_21, x_20);
-if (lean_obj_tag(x_22) == 0)
+lean_object* x_22; lean_object* x_23; lean_object* x_24; 
+x_22 = lean_ctor_get(x_21, 1);
+lean_inc(x_22);
+lean_dec(x_21);
+x_23 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__18;
+x_24 = l_Lean_Parser_registerAliasCore___rarg(x_9, x_17, x_23, x_22);
+if (lean_obj_tag(x_24) == 0)
 {
-lean_object* x_23; lean_object* x_24; lean_object* x_25; 
-x_23 = lean_ctor_get(x_22, 1);
-lean_inc(x_23);
-lean_dec(x_22);
-x_24 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__20;
-x_25 = l_Lean_Parser_registerAliasCore___rarg(x_12, x_16, x_24, x_23);
-return x_25;
+lean_object* x_25; lean_object* x_26; lean_object* x_27; 
+x_25 = lean_ctor_get(x_24, 1);
+lean_inc(x_25);
+lean_dec(x_24);
+x_26 = l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_189____closed__20;
+x_27 = l_Lean_Parser_registerAliasCore___rarg(x_13, x_17, x_26, x_25);
+return x_27;
 }
 else
 {
-uint8_t x_26; 
-x_26 = !lean_is_exclusive(x_22);
-if (x_26 == 0)
+uint8_t x_28; 
+x_28 = !lean_is_exclusive(x_24);
+if (x_28 == 0)
 {
-return x_22;
+return x_24;
 }
 else
 {
-lean_object* x_27; lean_object* x_28; lean_object* x_29; 
-x_27 = lean_ctor_get(x_22, 0);
-x_28 = lean_ctor_get(x_22, 1);
-lean_inc(x_28);
-lean_inc(x_27);
-lean_dec(x_22);
-x_29 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_29, 0, x_27);
-lean_ctor_set(x_29, 1, x_28);
-return x_29;
+lean_object* x_29; lean_object* x_30; lean_object* x_31; 
+x_29 = lean_ctor_get(x_24, 0);
+x_30 = lean_ctor_get(x_24, 1);
+lean_inc(x_30);
+lean_inc(x_29);
+lean_dec(x_24);
+x_31 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_31, 0, x_29);
+lean_ctor_set(x_31, 1, x_30);
+return x_31;
 }
 }
 }
 else
 {
-uint8_t x_30; 
-x_30 = !lean_is_exclusive(x_19);
-if (x_30 == 0)
+uint8_t x_32; 
+x_32 = !lean_is_exclusive(x_21);
+if (x_32 == 0)
 {
-return x_19;
+return x_21;
 }
 else
 {
-lean_object* x_31; lean_object* x_32; lean_object* x_33; 
-x_31 = lean_ctor_get(x_19, 0);
-x_32 = lean_ctor_get(x_19, 1);
-lean_inc(x_32);
-lean_inc(x_31);
-lean_dec(x_19);
-x_33 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_33, 0, x_31);
-lean_ctor_set(x_33, 1, x_32);
-return x_33;
+lean_object* x_33; lean_object* x_34; lean_object* x_35; 
+x_33 = lean_ctor_get(x_21, 0);
+x_34 = lean_ctor_get(x_21, 1);
+lean_inc(x_34);
+lean_inc(x_33);
+lean_dec(x_21);
+x_35 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_35, 0, x_33);
+lean_ctor_set(x_35, 1, x_34);
+return x_35;
 }
 }
 }
 else
 {
-uint8_t x_34; 
-x_34 = !lean_is_exclusive(x_14);
-if (x_34 == 0)
+uint8_t x_36; 
+x_36 = !lean_is_exclusive(x_15);
+if (x_36 == 0)
 {
-return x_14;
+return x_15;
 }
 else
 {
-lean_object* x_35; lean_object* x_36; lean_object* x_37; 
-x_35 = lean_ctor_get(x_14, 0);
-x_36 = lean_ctor_get(x_14, 1);
-lean_inc(x_36);
-lean_inc(x_35);
-lean_dec(x_14);
-x_37 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_37, 0, x_35);
-lean_ctor_set(x_37, 1, x_36);
-return x_37;
+lean_object* x_37; lean_object* x_38; lean_object* x_39; 
+x_37 = lean_ctor_get(x_15, 0);
+x_38 = lean_ctor_get(x_15, 1);
+lean_inc(x_38);
+lean_inc(x_37);
+lean_dec(x_15);
+x_39 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_39, 0, x_37);
+lean_ctor_set(x_39, 1, x_38);
+return x_39;
 }
 }
 }
 else
 {
-uint8_t x_38; 
-x_38 = !lean_is_exclusive(x_10);
-if (x_38 == 0)
+uint8_t x_40; 
+x_40 = !lean_is_exclusive(x_11);
+if (x_40 == 0)
 {
-return x_10;
+return x_11;
 }
 else
 {
-lean_object* x_39; lean_object* x_40; lean_object* x_41; 
-x_39 = lean_ctor_get(x_10, 0);
-x_40 = lean_ctor_get(x_10, 1);
-lean_inc(x_40);
-lean_inc(x_39);
-lean_dec(x_10);
-x_41 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_41, 0, x_39);
-lean_ctor_set(x_41, 1, x_40);
-return x_41;
+lean_object* x_41; lean_object* x_42; lean_object* x_43; 
+x_41 = lean_ctor_get(x_11, 0);
+x_42 = lean_ctor_get(x_11, 1);
+lean_inc(x_42);
+lean_inc(x_41);
+lean_dec(x_11);
+x_43 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_43, 0, x_41);
+lean_ctor_set(x_43, 1, x_42);
+return x_43;
 }
 }
 }
 else
 {
-uint8_t x_42; 
-x_42 = !lean_is_exclusive(x_6);
-if (x_42 == 0)
+uint8_t x_44; 
+x_44 = !lean_is_exclusive(x_7);
+if (x_44 == 0)
 {
-return x_6;
+return x_7;
 }
 else
 {
-lean_object* x_43; lean_object* x_44; lean_object* x_45; 
-x_43 = lean_ctor_get(x_6, 0);
-x_44 = lean_ctor_get(x_6, 1);
-lean_inc(x_44);
-lean_inc(x_43);
-lean_dec(x_6);
-x_45 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_45, 0, x_43);
-lean_ctor_set(x_45, 1, x_44);
-return x_45;
+lean_object* x_45; lean_object* x_46; lean_object* x_47; 
+x_45 = lean_ctor_get(x_7, 0);
+x_46 = lean_ctor_get(x_7, 1);
+lean_inc(x_46);
+lean_inc(x_45);
+lean_dec(x_7);
+x_47 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_47, 0, x_45);
+lean_ctor_set(x_47, 1, x_46);
+return x_47;
 }
 }
 }

stage0/stdlib/Lean/Parser/Tactic.c

@@ -262,7 +262,7 @@ lean_object* l_Lean_Parser_sepBy1_parenthesizer___boxed(lean_object*, lean_objec
 static lean_object* l_Lean_Parser_Tactic_match___elambda__1___closed__17;
 static lean_object* l_Lean_Parser_Tactic_unknown_parenthesizer___closed__4;
 static lean_object* l_Lean_Parser_Tactic_match___closed__2;
-lean_object* l_Lean_Parser_registerAlias(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_registerAlias(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_generalizingParam_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_unknown_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Parser_Tactic_unknown___closed__7;
@@ -462,32 +462,22 @@ return x_3;
 static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__3() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Parser_Tactic_tacticSeq;
-x_2 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_2, 0, x_1);
-return x_2;
-}
-}
-static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__4() {
-_start:
-{
 lean_object* x_1; 
 x_1 = lean_mk_string_from_bytes("Lean", 4);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__5() {
+static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__4;
+x_2 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__3;
 x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__6() {
+static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__5() {
 _start:
 {
 lean_object* x_1; 
@@ -495,17 +485,17 @@ x_1 = lean_mk_string_from_bytes("Parser", 6);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__7() {
+static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__5;
-x_2 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__6;
+x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__4;
+x_2 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__5;
 x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__8() {
+static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__7() {
 _start:
 {
 lean_object* x_1; 
@@ -513,12 +503,22 @@ x_1 = lean_mk_string_from_bytes("Tactic", 6);
 return x_1;
 }
 }
+static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__8() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__6;
+x_2 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__7;
+x_3 = l_Lean_Name_str___override(x_1, x_2);
+return x_3;
+}
+}
 static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__9() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__7;
-x_2 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__8;
+x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__8;
+x_2 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__1;
 x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;
 }
@@ -526,18 +526,18 @@ return x_3;
 static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__10() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__9;
-x_2 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__1;
-x_3 = l_Lean_Name_str___override(x_1, x_2);
-return x_3;
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Parser_Tactic_tacticSeq;
+x_2 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
 }
 }
 static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__11() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__10;
+x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__9;
 x_2 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
@@ -556,13 +556,15 @@ return x_2;
 static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__13() {
 _start:
 {
-lean_object* x_1; uint8_t x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__12;
-x_2 = 1;
-x_3 = lean_alloc_ctor(0, 1, 1);
-lean_ctor_set(x_3, 0, x_1);
-lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
-return x_3;
+lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__12;
+x_3 = 1;
+x_4 = lean_alloc_ctor(0, 2, 1);
+lean_ctor_set(x_4, 0, x_1);
+lean_ctor_set(x_4, 1, x_2);
+lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_3);
+return x_4;
 }
 }
 static lean_object* _init_l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__14() {
@@ -620,75 +622,76 @@ return x_1;
 LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6_(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__2;
-x_3 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__3;
-x_4 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__11;
-x_5 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__13;
-x_6 = l_Lean_Parser_registerAlias(x_2, x_3, x_4, x_5, x_1);
-if (lean_obj_tag(x_6) == 0)
+x_3 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__9;
+x_4 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__10;
+x_5 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__11;
+x_6 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__13;
+x_7 = l_Lean_Parser_registerAlias(x_2, x_3, x_4, x_5, x_6, x_1);
+if (lean_obj_tag(x_7) == 0)
 {
-lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
-x_7 = lean_ctor_get(x_6, 1);
-lean_inc(x_7);
-lean_dec(x_6);
-x_8 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__16;
-x_9 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__15;
-x_10 = l_Lean_Parser_registerAliasCore___rarg(x_8, x_2, x_9, x_7);
-if (lean_obj_tag(x_10) == 0)
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_8 = lean_ctor_get(x_7, 1);
+lean_inc(x_8);
+lean_dec(x_7);
+x_9 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__16;
+x_10 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__15;
+x_11 = l_Lean_Parser_registerAliasCore___rarg(x_9, x_2, x_10, x_8);
+if (lean_obj_tag(x_11) == 0)
 {
-lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
-x_11 = lean_ctor_get(x_10, 1);
-lean_inc(x_11);
-lean_dec(x_10);
-x_12 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__19;
-x_13 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__18;
-x_14 = l_Lean_Parser_registerAliasCore___rarg(x_12, x_2, x_13, x_11);
-return x_14;
+lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
+x_12 = lean_ctor_get(x_11, 1);
+lean_inc(x_12);
+lean_dec(x_11);
+x_13 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__19;
+x_14 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__18;
+x_15 = l_Lean_Parser_registerAliasCore___rarg(x_13, x_2, x_14, x_12);
+return x_15;
 }
 else
 {
-uint8_t x_15; 
-x_15 = !lean_is_exclusive(x_10);
-if (x_15 == 0)
+uint8_t x_16; 
+x_16 = !lean_is_exclusive(x_11);
+if (x_16 == 0)
 {
-return x_10;
+return x_11;
 }
 else
 {
-lean_object* x_16; lean_object* x_17; lean_object* x_18; 
-x_16 = lean_ctor_get(x_10, 0);
-x_17 = lean_ctor_get(x_10, 1);
+lean_object* x_17; lean_object* x_18; lean_object* x_19; 
+x_17 = lean_ctor_get(x_11, 0);
+x_18 = lean_ctor_get(x_11, 1);
+lean_inc(x_18);
 lean_inc(x_17);
-lean_inc(x_16);
-lean_dec(x_10);
-x_18 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_18, 0, x_16);
-lean_ctor_set(x_18, 1, x_17);
-return x_18;
+lean_dec(x_11);
+x_19 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_19, 0, x_17);
+lean_ctor_set(x_19, 1, x_18);
+return x_19;
 }
 }
 }
 else
 {
-uint8_t x_19; 
-x_19 = !lean_is_exclusive(x_6);
-if (x_19 == 0)
+uint8_t x_20; 
+x_20 = !lean_is_exclusive(x_7);
+if (x_20 == 0)
 {
-return x_6;
+return x_7;
 }
 else
 {
-lean_object* x_20; lean_object* x_21; lean_object* x_22; 
-x_20 = lean_ctor_get(x_6, 0);
-x_21 = lean_ctor_get(x_6, 1);
+lean_object* x_21; lean_object* x_22; lean_object* x_23; 
+x_21 = lean_ctor_get(x_7, 0);
+x_22 = lean_ctor_get(x_7, 1);
+lean_inc(x_22);
 lean_inc(x_21);
-lean_inc(x_20);
-lean_dec(x_6);
-x_22 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_22, 0, x_20);
-lean_ctor_set(x_22, 1, x_21);
-return x_22;
+lean_dec(x_7);
+x_23 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_23, 0, x_21);
+lean_ctor_set(x_23, 1, x_22);
+return x_23;
 }
 }
 }
@@ -802,7 +805,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_unknown___elambda__1___closed__2(
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__9;
+x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__8;
 x_2 = l_Lean_Parser_Tactic_unknown___elambda__1___closed__1;
 x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;
@@ -1563,7 +1566,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_nestedTactic___close
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__9;
+x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__8;
 x_2 = l___regBuiltin_Lean_Parser_Tactic_nestedTactic___closed__1;
 x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;
@@ -1871,7 +1874,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_match___elambda__1___closed__2()
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__9;
+x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__8;
 x_2 = l_Lean_Parser_Tactic_match___elambda__1___closed__1;
 x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;
@@ -3188,7 +3191,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_introMatch___elambda__1___closed_
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__9;
+x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__8;
 x_2 = l_Lean_Parser_Tactic_introMatch___elambda__1___closed__1;
 x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;
@@ -3871,7 +3874,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_decide___elambda__1___closed__2()
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__9;
+x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__8;
 x_2 = l_Lean_Parser_Tactic_decide___elambda__1___closed__1;
 x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;
@@ -4471,7 +4474,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_nativeDecide___elambda__1___close
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__9;
+x_1 = l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_6____closed__8;
 x_2 = l_Lean_Parser_Tactic_nativeDecide___elambda__1___closed__1;
 x_3 = l_Lean_Name_str___override(x_1, x_2);
 return x_3;