chore: update stage0

stage0/src/Init/Lean/Attributes.lean

@@ -309,8 +309,10 @@ structure ParametricAttribute (α : Type) :=
 (ext  : PersistentEnvExtension (Name × α) (Name × α) (NameMap α))
 
 def registerParametricAttribute {α : Type} [Inhabited α] (name : Name) (descr : String)
-       (getParam : Environment → Name → Syntax → Except String α)
-       (afterSet : Environment → Name → α → Except String Environment := fun env _ _ => Except.ok env) : IO (ParametricAttribute α) := do
+    (getParam : Environment → Name → Syntax → Except String α)
+    (afterSet : Environment → Name → α → Except String Environment := fun env _ _ => Except.ok env)
+    (appTime := AttributeApplicationTime.afterTypeChecking)
+    : IO (ParametricAttribute α) := do
 ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
   name            := name,
   mkInitial       := pure {},
@@ -324,6 +326,7 @@ ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← register
 let attrImpl : AttributeImpl := {
   name  := name,
   descr := descr,
+  applicationTime := appTime,
   add   := fun env decl args persistent => do
     unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
     unless (env.getModuleIdxFor? decl).isNone $

stage0/src/Init/Lean/Declaration.lean

@@ -213,4 +213,8 @@ constant instantiateTypeLevelParams (c : @& ConstantInfo) (ls : @& List Level) :
 constant instantiateValueLevelParams (c : @& ConstantInfo) (ls : @& List Level) : Expr := arbitrary _
 
 end ConstantInfo
+
+def mkRecFor (declName : Name) : Name :=
+mkNameStr declName "rec"
+
 end Lean

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

@@ -8,3 +8,4 @@ import Init.Lean.Elab.Term
 import Init.Lean.Elab.Tactic.Basic
 import Init.Lean.Elab.Tactic.ElabTerm
 import Init.Lean.Elab.Tactic.Induction
+import Init.Lean.Elab.Tactic.Generalize

stage0/src/Init/Lean/Elab/Tactic/Basic.lean

@@ -76,6 +76,10 @@ def isExprMVarAssigned (mvarId : MVarId) : TacticM Bool := liftTermElabM $ Term.
 def assignExprMVar (mvarId : MVarId) (val : Expr) : TacticM Unit := liftTermElabM $ Term.assignExprMVar mvarId val
 def ensureHasType (ref : Syntax) (expectedType? : Option Expr) (e : Expr) : TacticM Expr := liftTermElabM $ Term.ensureHasType ref expectedType? e
 def reportUnsolvedGoals (ref : Syntax) (goals : List MVarId) : TacticM Unit := liftTermElabM $ Term.reportUnsolvedGoals ref goals
+def inferType (ref : Syntax) (e : Expr) : TacticM Expr := liftTermElabM $ Term.inferType ref e
+def whnf (ref : Syntax) (e : Expr) : TacticM Expr := liftTermElabM $ Term.whnf ref e
+def whnfCore (ref : Syntax) (e : Expr) : TacticM Expr := liftTermElabM $ Term.whnfCore ref e
+def unfoldDefinition? (ref : Syntax) (e : Expr) : TacticM (Option Expr) := liftTermElabM $ Term.unfoldDefinition? ref e
 
 /-- Collect unassigned metavariables -/
 def collectMVars (ref : Syntax) (e : Expr) : TacticM (List MVarId) := do
@@ -257,11 +261,23 @@ def ensureHasNoMVars (ref : Syntax) (e : Expr) : TacticM Unit := do
 e ← instantiateMVars ref e;
 when e.hasMVar $ throwError ref ("tactic failed, resulting expression contains metavariables" ++ indentExpr e)
 
-@[inline] def liftMetaTactic (ref : Syntax) (tactic : MVarId → MetaM (List MVarId)) : TacticM Unit := do
+def withMainMVarContext {α} (ref : Syntax) (x : TacticM α) : TacticM α := do
+(mvarId, _) ← getMainGoal ref;
+withMVarContext mvarId x
+
+@[inline] def liftMetaMAtMain {α} (ref : Syntax) (x : MVarId → MetaM α) : TacticM α := do
+(g, _) ← getMainGoal ref;
+withMVarContext g $ liftMetaM ref $ x g
+
+@[inline] def liftMetaTacticAux {α} (ref : Syntax) (tactic : MVarId → MetaM (α × List MVarId)) : TacticM α := do
 (g, gs) ← getMainGoal ref;
 withMVarContext g $ do
-  gs' ← liftMetaM ref $ tactic g;
-  setGoals (gs' ++ gs)
+  (a, gs') ← liftMetaM ref $ tactic g;
+  setGoals (gs' ++ gs);
+  pure a
+
+@[inline] def liftMetaTactic (ref : Syntax) (tactic : MVarId → MetaM (List MVarId)) : TacticM Unit :=
+liftMetaTacticAux ref (fun mvarId => do gs ← tactic mvarId; pure ((), gs))
 
 def done (ref : Syntax) : TacticM Unit := do
 gs ← getUnsolvedGoals;
@@ -347,17 +363,21 @@ fun stx => match_syntax stx with
     pure [mvarId]
   | _                       => throwUnsupportedSyntax
 
+def getFVarId (id : Syntax) : TacticM FVarId := do
+fvar? ← liftTermElabM $ Term.isLocalTermId? id true;
+match fvar? with
+| some fvar => pure fvar.fvarId!
+| none      => throwError id ("unknown variable '" ++ toString id.getId ++ "'")
+
+def getFVarIds (ids : Array Syntax) : TacticM (Array FVarId) :=
+ids.mapM getFVarId
+
 @[builtinTactic «revert»] def evalRevert : Tactic :=
 fun stx => match_syntax stx with
   | `(tactic| revert $hs*) => do
      (g, gs) ← getMainGoal stx;
      withMVarContext g $ do
-       fvarIds ← hs.mapM $ fun h => do {
-         fvar? ← liftTermElabM $ Term.isLocalTermId? h true;
-         match fvar? with
-         | some fvar => pure fvar.fvarId!
-         | none      => throwError h ("unknown variable '" ++ toString h.getId ++ "'")
-       };
+       fvarIds ← getFVarIds hs;
        (_, g) ← liftMetaM stx $ Meta.revert g fvarIds;
        setGoals (g :: gs)
   | _                     => throwUnsupportedSyntax
@@ -366,12 +386,9 @@ def forEachVar (ref : Syntax) (hs : Array Syntax) (tac : MVarId → FVarId → M
 hs.forM $ fun h => do
   (g, gs) ← getMainGoal ref;
   withMVarContext g $ do
-    fvar? ← liftTermElabM $ Term.isLocalTermId? h true;
-    match fvar? with
-    | none      => throwError h ("unknown variable '" ++ toString h.getId ++ "'")
-    | some fvar => do
-      g ← liftMetaM ref $ tac g fvar.fvarId!;
-      setGoals (g :: gs)
+    fvarId ← getFVarId h;
+    g ← liftMetaM ref $ tac g fvarId;
+    setGoals (g :: gs)
 
 @[builtinTactic «clear»] def evalClear : Tactic :=
 fun stx => match_syntax stx with

stage0/src/Init/Lean/Elab/Tactic/Generalize.lean

@@ -0,0 +1,77 @@
+/-
+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.Meta.Tactic.Generalize
+import Init.Lean.Meta.Check
+import Init.Lean.Meta.Tactic.Intro
+import Init.Lean.Elab.Tactic.ElabTerm
+
+namespace Lean
+namespace Elab
+namespace Tactic
+
+private def getAuxHypothesisName (stx : Syntax) : Option Name :=
+if (stx.getArg 1).isNone then none
+else some ((stx.getArg 1).getIdAt 0)
+
+private def getVarName (stx : Syntax) : Name :=
+stx.getIdAt 4
+
+private def evalGeneralizeFinalize (mvarId : MVarId) (e : Expr) (target : Expr) : MetaM (List MVarId) := do
+tag         ← Meta.getMVarTag mvarId;
+eType       ← Meta.inferType e;
+u           ← Meta.getLevel eType;
+mvar' ← Meta.mkFreshExprSyntheticOpaqueMVar target tag;
+let rfl    := mkApp2 (Lean.mkConst `Eq.refl [u]) eType e;
+let val    := mkApp2 mvar' e rfl;
+Meta.assignExprMVar mvarId val;
+let mvarId' := mvar'.mvarId!;
+(_, mvarId') ← Meta.introN mvarId' 2 [] false;
+pure [mvarId']
+
+private def evalGeneralizeWithEq (ref : Syntax) (h : Name) (e : Expr) (x : Name) : TacticM Unit :=
+liftMetaTactic ref $ fun mvarId => do
+  mvarId      ← Meta.generalize mvarId e x;
+  mvarDecl    ← Meta.getMVarDecl mvarId;
+  match mvarDecl.type with
+  | Expr.forallE _ _ b _ => do
+    (_, mvarId) ← Meta.intro1 mvarId false;
+    eType       ← Meta.inferType e;
+    u           ← Meta.getLevel eType;
+    let eq     := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0);
+    let target := Lean.mkForall x BinderInfo.default eType $ Lean.mkForall h BinderInfo.default eq (b.liftLooseBVars 0 1);
+    evalGeneralizeFinalize mvarId e target
+  | _ => throw $ Meta.Exception.other "unexpected type after generalize"
+
+-- If generalizing fails, fall back to not replacing anything
+private def evalGeneralizeFallback (ref : Syntax) (h : Name) (e : Expr) (x : Name) : TacticM Unit :=
+liftMetaTactic ref $ fun mvarId => do
+  eType       ← Meta.inferType e;
+  u           ← Meta.getLevel eType;
+  mvarType    ← Meta.getMVarType mvarId;
+  let eq     := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0);
+  let target := Lean.mkForall x BinderInfo.default eType $ Lean.mkForall h BinderInfo.default eq mvarType;
+  evalGeneralizeFinalize mvarId e target
+
+def evalGeneralizeAux (ref : Syntax) (h? : Option Name) (e : Expr) (x : Name) : TacticM Unit :=
+match h? with
+| none   => liftMetaTactic ref $ fun mvarId => do
+  mvarId ← Meta.generalize mvarId e x;
+  (_, mvarId) ← Meta.intro1 mvarId false;
+  pure [mvarId]
+| some h =>
+  evalGeneralizeWithEq ref h e x <|> evalGeneralizeFallback ref h e x
+
+@[builtinTactic «generalize»] def evalGeneralize : Tactic :=
+fun stx => do
+  let h? := getAuxHypothesisName stx;
+  let x  := getVarName stx;
+  e ← elabTerm (stx.getArg 2) none;
+  evalGeneralizeAux stx h? e x
+
+end Tactic
+end Elab
+end Lean

stage0/src/Init/Lean/Elab/Tactic/Induction.lean

@@ -4,15 +4,194 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Init.Lean.Elab.Tactic.Basic
+import Init.Lean.Meta.RecursorInfo
+import Init.Lean.Elab.Tactic.ElabTerm
+import Init.Lean.Elab.Tactic.Generalize
 
 namespace Lean
 namespace Elab
 namespace Tactic
 
+-- Recall that
+-- majorPremise := parser! optional (try (ident >> " : ")) >> termParser
+
+private def getAuxHypothesisName (stx : Syntax) : Option Name :=
+if ((stx.getArg 1).getArg 0).isNone then none
+else some (((stx.getArg 1).getArg 0).getIdAt 0)
+
+private def getMajor (stx : Syntax) : Syntax :=
+(stx.getArg 1).getArg 1
+
+private def elabMajor (ref : Syntax) (h? : Option Name) (major : Syntax) : TacticM Expr := do
+match h? with
+| none   => withMainMVarContext ref $ elabTerm major none
+| some h => withMainMVarContext ref $ do
+  lctx ← getLCtx;
+  let x := lctx.getUnusedName `x;
+  major ← elabTerm major none;
+  evalGeneralizeAux ref h? major x;
+  withMainMVarContext ref $ do
+    lctx ← getLCtx;
+    match lctx.findFromUserName? x with
+    | some decl => pure decl.toExpr
+    | none      => throwError ref "failed to generalize"
+
+private def generalizeMajor (ref : Syntax) (major : Expr) : TacticM Expr := do
+match major with
+| Expr.fvar _ _ => pure major
+| _ => do
+  liftMetaTacticAux ref $ fun mvarId => do
+    mvarId ← Meta.generalize mvarId major `x;
+    (fvarId, mvarId) ← Meta.intro1 mvarId;
+    pure (mkFVar fvarId, [mvarId])
+
+/-
+  Recall that
+  ```
+  generalizingVars := optional (" generalizing " >> many1 ident)
+  «induction»  := parser! nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> withAlts
+  ```
+  `stx` is syntax for `induction`. -/
+private def getGeneralizingFVarIds (stx : Syntax) : TacticM (Array FVarId) :=
+let generalizingStx := stx.getArg 3;
+if generalizingStx.isNone then pure #[]
+else withMainMVarContext stx $ do
+  trace `Elab.induction stx $ fun _ => generalizingStx;
+  let vars := (generalizingStx.getArg 1).getArgs;
+  getFVarIds vars
+
+-- process `generalizingVars` subterm of induction Syntax `stx`.
+private def generalizeVars (stx : Syntax) (major : Expr) : TacticM Nat := do
+fvarIds ← getGeneralizingFVarIds stx;
+liftMetaTacticAux stx $ fun mvarId => do
+  (fvarIds, mvarId') ← Meta.revert mvarId fvarIds;
+  when (fvarIds.contains major.fvarId!) $
+    Meta.throwTacticEx `induction mvarId "major premise depends on variable being generalized";
+  pure (fvarIds.size, [mvarId'])
+
+private def getAlts (withAlts : Syntax) : Array Syntax :=
+(withAlts.getArg 2).getArgs.getSepElems
+
+/-
+  Given an `inductionAlt` of the form
+  ```
+  nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> termParser
+  ``` -/
+private def getAltName (alt : Syntax) : Name := (alt.getArg 0).getId.eraseMacroScopes
+private def getAltVarNames (alt : Syntax) : Array Name := (alt.getArg 1).getArgs.map Syntax.getId
+private def getAltRHS (alt : Syntax) : Syntax := alt.getArg 3
+
+/-
+  Given alts of the form
+  ```
+  nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> termParser
+  ```
+  esnure the first `ident'` is `_` or a constructor name.
+-/
+private def checkAltCtorNames (alts : Array Syntax) (ctorNames : List Name) : TacticM Unit :=
+alts.forM $ fun alt => do
+  let n := getAltName alt;
+  trace `Elab.checkAlt alt $ fun _ => n ++ ", " ++ alt;
+  unless (n == `_ || ctorNames.any (fun ctorName => n.isSuffixOf ctorName)) $
+    throwError (alt.getArg 0) ("invalid constructor name '" ++ toString n ++ "'")
+
+structure RecInfo :=
+(recName : Name)
+(altVars : Array (List Name) := #[]) -- new variable names for each minor premise
+(altRHSs : Array Syntax := #[])      -- RHS for each minor premise
+
+def getInductiveValFromMajor (ref : Syntax) (major : Expr) : TacticM InductiveVal :=
+liftMetaMAtMain ref $ fun mvarId => do
+  majorType ← Meta.inferType major;
+  majorType ← Meta.whnf majorType;
+  match majorType.getAppFn with
+  | Expr.const n _ _ => do
+    env ← Meta.getEnv;
+    match env.find? n with
+    | ConstantInfo.inductInfo val => pure val
+    | _ => Meta.throwTacticEx `induction mvarId ("major premise type is not an inductive type " ++ indentExpr majorType)
+  | _ => Meta.throwTacticEx `induction mvarId ("major premise type is not an inductive type " ++ indentExpr majorType)
+
+private partial def getRecFromUsingLoop (ref : Syntax) (baseRecName : Name) : Expr → TacticM (Option Meta.RecursorInfo)
+| majorType => do
+  let continue (majorType : Expr) : TacticM (Option Meta.RecursorInfo) := do {
+    majorType? ← unfoldDefinition? ref majorType;
+    match majorType? with
+    | some majorType => withIncRecDepth ref $ getRecFromUsingLoop majorType
+    | none           => pure none
+  };
+  majorType ← whnfCore ref majorType;
+  match majorType.getAppFn with
+  | Expr.const name _ _ => do
+    let candidate := name ++ baseRecName;
+    env ← getEnv;
+    match env.find? candidate with
+    | some _ =>
+      catch
+        (liftMetaMAtMain ref $ fun _ => do info ← Meta.mkRecursorInfo candidate; pure (some info))
+        (fun _ => continue majorType)
+    | none   => continue majorType
+  | _ => continue majorType
+
+
+def getRecFromUsing (ref : Syntax) (major : Expr) (baseRecName : Name) : TacticM Name := do
+throw $ arbitrary _
+
+/-
+  Recall that
+  ```
+  inductionAlt  : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> termParser
+  inductionAlts : Parser := withPosition $ fun pos => "|" >> sepBy1 inductionAlt (checkColGe pos.column "alternatives must be indented" >> "|")
+  withAlts : Parser := optional (" with " >> inductionAlts)
+  usingRec : Parser := optional (" using " >> ident)
+  ``` -/
+private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo :=
+let ref         := stx;
+let usingRecStx := stx.getArg 2;
+let withAlts    := stx.getArg 4;
+if usingRecStx.isNone then do
+  indVal ← getInductiveValFromMajor ref major;
+  let recName := mkRecFor indVal.name;
+  if withAlts.isNone then pure { recName := recName }
+  else do
+    let ctorNames := indVal.ctors;
+    let alts      := getAlts withAlts;
+    checkAltCtorNames alts ctorNames;
+    (altVars, altRHSs, remainingAlts, _) ← ctorNames.foldlM
+      (fun (result : Array (List Name) × Array Syntax × Array Syntax × Option Syntax) (ctorName : Name) => do
+        let (altVars, altRHSs, remainingAlts, prevAnonymousAlt?) := result;
+        match remainingAlts.findIdx? (fun alt => (getAltName alt).isSuffixOf ctorName) with
+        | some idx =>
+          let newAlt := remainingAlts.get! idx;
+          pure (altVars.push (getAltVarNames newAlt).toList, altRHSs.push (getAltRHS newAlt), remainingAlts.eraseIdx idx, prevAnonymousAlt?)
+        | none => match remainingAlts.findIdx? (fun alt => getAltName alt == `_) with
+          | some idx =>
+            let newAlt     := remainingAlts.get! idx;
+            pure (altVars.push (getAltVarNames newAlt).toList, altRHSs.push (getAltRHS newAlt), remainingAlts.eraseIdx idx, some newAlt)
+          | none => match prevAnonymousAlt? with
+            | some alt =>
+              pure (altVars.push (getAltVarNames alt).toList, altRHSs.push (getAltRHS alt), remainingAlts, prevAnonymousAlt?)
+            | none     => throwError ref ("alternative for constructor '" ++ toString ctorName ++ "' is missing"))
+      (#[], #[], alts, none);
+    unless remainingAlts.isEmpty $
+      throwError (remainingAlts.get! 0) "unused alternative";
+    pure { recName := recName, altVars := altVars, altRHSs := altRHSs }
+else do
+  let baseRecName := (usingRecStx.getIdAt 1).eraseMacroScopes;
+  let recName := getRecFromUsing ref major baseRecName;
+  -- TODO
+  throw $ arbitrary _
+
 @[builtinTactic «induction»] def evalInduction : Tactic :=
-fun stx => focus stx $
-  throwError stx ("WIP " ++ stx)
+fun stx => focus stx $ do
+  let h? := getAuxHypothesisName stx;
+  major ← elabMajor stx h? (getMajor stx);
+  major ← generalizeMajor stx major;
+  n ← generalizeVars stx major;
+  recInfo ← getRecInfo stx major;
+  goals ← getGoals;
+  throwError stx ("WIP " ++ stx ++ major ++ ", n : " ++ toString n ++ Format.line ++ goalsToMessageData goals ++
+    Format.line ++ toString recInfo.altVars ++ Format.line ++ toString recInfo.altRHSs)
 
 end Tactic
 end Elab

stage0/src/Init/Lean/Meta/Basic.lean

@@ -805,6 +805,11 @@ finally x (modify $ fun s => { mctx := mctx', .. s })
 @[init] private def regTraceClasses : IO Unit :=
 registerTraceClass `Meta
 
+def run {α} (env : Environment) (x : MetaM α) (maxRecDepth := 10000) : Except Exception α :=
+match x { maxRecDepth := maxRecDepth, currRecDepth := 0 } { env := env } with
+| EStateM.Result.ok a _     => Except.ok a
+| EStateM.Result.error ex _ => Except.error ex
+
 end Meta
 end Lean
 

stage0/src/Init/Lean/Meta/RecursorInfo.lean

@@ -8,6 +8,7 @@ import Init.Data.Nat.Control
 import Init.Lean.AuxRecursor
 import Init.Lean.Util.FindExpr
 import Init.Lean.Meta.ExprDefEq
+import Init.Lean.Meta.Message
 
 namespace Lean
 namespace Meta
@@ -106,7 +107,7 @@ else do
     if s != "recOn" && s != "casesOn" && s != "brecOn" then
       pure none
     else do
-      recInfo ← getConstInfo (mkNameStr p "rec");
+      recInfo ← getConstInfo (mkRecFor p);
       match recInfo with
       | ConstantInfo.recInfo val => pure (some (val.nparams + val.nindices + (if s == "casesOn" then 1 else val.nmotives)))
       | _                        => throw $ Exception.other "unexpected recursor information"
@@ -264,11 +265,43 @@ forallTelescopeReducing cinfo.type $ fun xs type => type.withApp $ fun motive mo
     ("invalid user defined recursor '" ++ toString declName
      ++ "', type of the major premise must be of the form (I ...), where I is a constant")
 
-def mkRecursorInfo (declName : Name) (majorPos? : Option Nat := none) : MetaM RecursorInfo := do
+private def syntaxToMajorPos (stx : Syntax) : Except String Nat :=
+match stx with
+| Syntax.node _ args =>
+  if args.size == 0 then Except.error "unexpected kind of argument"
+  else match (args.get! 0).isNatLit? with
+    | some idx =>
+      if idx == 0 then Except.error "major premise position must be greater than 0"
+      else pure (idx - 1)
+    | none => Except.error "unexpected kind of argument"
+| _ => Except.error "unexpected kind of argument"
+
+private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat := none) : MetaM RecursorInfo := do
 cinfo ← getConstInfo declName;
 match cinfo with
 | ConstantInfo.recInfo val => mkRecursorInfoForKernelRec declName val
 | _                        => mkRecursorInfoAux cinfo majorPos?
 
+def mkRecursorAttr : IO (ParametricAttribute Nat) :=
+registerParametricAttribute `recursor "user defined recursor, numerical parameter specifies position of the major premise"
+  (fun _ _ => syntaxToMajorPos)
+  (fun env declName majorPos =>
+    match Meta.run env (mkRecursorInfoCore declName (some majorPos)) with
+    | Except.ok _     => pure env
+    | Except.error ex => Except.error $ toString ex)
+
+@[init mkRecursorAttr] constant recursorAttribute : ParametricAttribute Nat := arbitrary _
+
+def getMajorPos? (env : Environment) (declName : Name) : Option Nat :=
+recursorAttribute.getParam env declName
+
+def mkRecursorInfo (declName : Name) (majorPos? : Option Nat := none) : MetaM RecursorInfo := do
+cinfo ← getConstInfo declName;
+match cinfo with
+| ConstantInfo.recInfo val => mkRecursorInfoForKernelRec declName val
+| _                        => match majorPos? with
+  | none => do env ← getEnv; mkRecursorInfoAux cinfo (getMajorPos? env declName)
+  | _    => mkRecursorInfoAux cinfo majorPos?
+
 end Meta
 end Lean

stage0/src/Init/Lean/Parser/Tactic.lean

@@ -38,7 +38,7 @@ def ident' : Parser := ident <|> underscore
 @[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
 @[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize" >> optional (try (ident >> " : ")) >> termParser 50 >> " = " >> ident
 def majorPremise := parser! optional (try (ident >> " : ")) >> termParser
-def inductionAlt  : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident >> many ident >> darrow >> termParser
+def inductionAlt  : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> termParser
 def inductionAlts : Parser := withPosition $ fun pos => "|" >> sepBy1 inductionAlt (checkColGe pos.column "alternatives must be indented" >> "|")
 def withAlts : Parser := optional (" with " >> inductionAlts)
 def usingRec : Parser := optional (" using " >> ident)

stage0/stdlib/Init/Lean/Attributes.c

@@ -193,6 +193,7 @@ lean_object* l_Lean_mkAttributeExtension___lambda__2(lean_object*);
 lean_object* l_Lean_attributeExtension___closed__4;
 lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Attributes_2__AttributeExtension_addImported___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_binSearchAux___main___at_Lean_ParametricAttribute_getParam___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_registerParametricAttribute___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_IO_Error_Inhabited___closed__1;
 lean_object* l_Lean_attrParamSyntaxToIdentifier(lean_object*);
 lean_object* l_Lean_registerParametricAttribute___rarg___closed__1;
@@ -325,7 +326,7 @@ lean_object* lean_io_initializing(lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__2;
 lean_object* l_Lean_mkAttributeImplOfConstantUnsafe___closed__2;
 lean_object* l_Lean_registerTagAttribute(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_registerParametricAttribute___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_registerParametricAttribute___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 uint8_t l_HashMapImp_contains___at_Lean_registerAttributeImplBuilder___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_EnumAttributes_setValue___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_registerEnumAttributes___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -7938,48 +7939,47 @@ x_1 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___rarg___lam
 return x_1;
 }
 }
-lean_object* l_Lean_registerParametricAttribute___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+lean_object* l_Lean_registerParametricAttribute___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, uint8_t x_6, lean_object* x_7) {
 _start:
 {
-lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
-x_7 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___rarg___lambda__2___boxed), 2, 1);
-lean_closure_set(x_7, 0, x_1);
-x_8 = l_Lean_registerTagAttribute___closed__1;
-x_9 = l_Lean_registerTagAttribute___closed__2;
-x_10 = l_Lean_registerParametricAttribute___rarg___closed__1;
-x_11 = l_Lean_registerParametricAttribute___rarg___closed__2;
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+x_8 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___rarg___lambda__2___boxed), 2, 1);
+lean_closure_set(x_8, 0, x_1);
+x_9 = l_Lean_registerTagAttribute___closed__1;
+x_10 = l_Lean_registerTagAttribute___closed__2;
+x_11 = l_Lean_registerParametricAttribute___rarg___closed__1;
+x_12 = l_Lean_registerParametricAttribute___rarg___closed__2;
 lean_inc(x_2);
-x_12 = lean_alloc_ctor(0, 6, 0);
-lean_ctor_set(x_12, 0, x_2);
-lean_ctor_set(x_12, 1, x_8);
-lean_ctor_set(x_12, 2, x_9);
-lean_ctor_set(x_12, 3, x_10);
-lean_ctor_set(x_12, 4, x_7);
-lean_ctor_set(x_12, 5, x_11);
-x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_registerParametricAttribute___spec__7___rarg(x_12, x_6);
-if (lean_obj_tag(x_13) == 0)
+x_13 = lean_alloc_ctor(0, 6, 0);
+lean_ctor_set(x_13, 0, x_2);
+lean_ctor_set(x_13, 1, x_9);
+lean_ctor_set(x_13, 2, x_10);
+lean_ctor_set(x_13, 3, x_11);
+lean_ctor_set(x_13, 4, x_8);
+lean_ctor_set(x_13, 5, x_12);
+x_14 = l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_registerParametricAttribute___spec__7___rarg(x_13, x_7);
+if (lean_obj_tag(x_14) == 0)
 {
-lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17; lean_object* x_18; lean_object* x_19; 
-x_14 = lean_ctor_get(x_13, 0);
-lean_inc(x_14);
-x_15 = lean_ctor_get(x_13, 1);
+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, 0);
+lean_inc(x_15);
+x_16 = lean_ctor_get(x_14, 1);
+lean_inc(x_16);
+lean_dec(x_14);
 lean_inc(x_15);
-lean_dec(x_13);
-lean_inc(x_14);
 lean_inc(x_2);
-x_16 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___rarg___lambda__4___boxed), 9, 4);
-lean_closure_set(x_16, 0, x_2);
-lean_closure_set(x_16, 1, x_4);
-lean_closure_set(x_16, 2, x_14);
-lean_closure_set(x_16, 3, x_5);
-x_17 = 0;
+x_17 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___rarg___lambda__4___boxed), 9, 4);
+lean_closure_set(x_17, 0, x_2);
+lean_closure_set(x_17, 1, x_4);
+lean_closure_set(x_17, 2, x_15);
+lean_closure_set(x_17, 3, x_5);
 x_18 = lean_alloc_ctor(0, 3, 1);
 lean_ctor_set(x_18, 0, x_2);
 lean_ctor_set(x_18, 1, x_3);
-lean_ctor_set(x_18, 2, x_16);
-lean_ctor_set_uint8(x_18, sizeof(void*)*3, x_17);
+lean_ctor_set(x_18, 2, x_17);
+lean_ctor_set_uint8(x_18, sizeof(void*)*3, x_6);
 lean_inc(x_18);
-x_19 = l_Lean_registerBuiltinAttribute(x_18, x_15);
+x_19 = l_Lean_registerBuiltinAttribute(x_18, x_16);
 if (lean_obj_tag(x_19) == 0)
 {
 uint8_t x_20; 
@@ -7991,7 +7991,7 @@ x_21 = lean_ctor_get(x_19, 0);
 lean_dec(x_21);
 x_22 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_22, 0, x_18);
-lean_ctor_set(x_22, 1, x_14);
+lean_ctor_set(x_22, 1, x_15);
 lean_ctor_set(x_19, 0, x_22);
 return x_19;
 }
@@ -8003,7 +8003,7 @@ lean_inc(x_23);
 lean_dec(x_19);
 x_24 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_24, 0, x_18);
-lean_ctor_set(x_24, 1, x_14);
+lean_ctor_set(x_24, 1, x_15);
 x_25 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_25, 0, x_24);
 lean_ctor_set(x_25, 1, x_23);
@@ -8014,7 +8014,7 @@ else
 {
 uint8_t x_26; 
 lean_dec(x_18);
-lean_dec(x_14);
+lean_dec(x_15);
 x_26 = !lean_is_exclusive(x_19);
 if (x_26 == 0)
 {
@@ -8042,19 +8042,19 @@ lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
-x_30 = !lean_is_exclusive(x_13);
+x_30 = !lean_is_exclusive(x_14);
 if (x_30 == 0)
 {
-return x_13;
+return x_14;
 }
 else
 {
 lean_object* x_31; lean_object* x_32; lean_object* x_33; 
-x_31 = lean_ctor_get(x_13, 0);
-x_32 = lean_ctor_get(x_13, 1);
+x_31 = lean_ctor_get(x_14, 0);
+x_32 = lean_ctor_get(x_14, 1);
 lean_inc(x_32);
 lean_inc(x_31);
-lean_dec(x_13);
+lean_dec(x_14);
 x_33 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_33, 0, x_31);
 lean_ctor_set(x_33, 1, x_32);
@@ -8067,7 +8067,7 @@ lean_object* l_Lean_registerParametricAttribute(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___rarg), 6, 0);
+x_2 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___rarg___boxed), 7, 0);
 return x_2;
 }
 }
@@ -8170,6 +8170,16 @@ x_11 = l_Lean_registerParametricAttribute___rarg___lambda__4(x_1, x_2, x_3, x_4,
 return x_11;
 }
 }
+lean_object* l_Lean_registerParametricAttribute___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+uint8_t x_8; lean_object* x_9; 
+x_8 = lean_unbox(x_6);
+lean_dec(x_6);
+x_9 = l_Lean_registerParametricAttribute___rarg(x_1, x_2, x_3, x_4, x_5, x_8, x_7);
+return x_9;
+}
+}
 lean_object* _init_l_Lean_ParametricAttribute_Inhabited___closed__1() {
 _start:
 {

stage0/stdlib/Init/Lean/Compiler/ExportAttr.c

@@ -40,6 +40,7 @@ lean_object* l_Lean_mkExportAttr___closed__2;
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
+lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_binSearchAux___main___at_Lean_getExportNameFor___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Name_inhabited;
 extern lean_object* l_String_splitAux___main___closed__1;
@@ -112,7 +113,7 @@ lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*
 uint8_t l_String_anyAux___main___at___private_Init_Lean_Compiler_ExportAttr_1__isValidCppId___spec__2(uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkExportAttr___closed__5;
 lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
-lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* l_String_anyAux___main___at___private_Init_Lean_Compiler_ExportAttr_1__isValidCppId___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkExportAttr___closed__3;
@@ -1494,47 +1495,46 @@ x_1 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___at_Lean_mk
 return x_1;
 }
 }
-lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint8_t x_5, lean_object* x_6) {
 _start:
 {
-lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
-x_6 = l_Lean_registerTagAttribute___closed__1;
-x_7 = l_Lean_registerTagAttribute___closed__2;
-x_8 = l_Lean_registerParametricAttribute___rarg___closed__1;
-x_9 = l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___closed__1;
-x_10 = l_Lean_registerParametricAttribute___rarg___closed__2;
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
+x_7 = l_Lean_registerTagAttribute___closed__1;
+x_8 = l_Lean_registerTagAttribute___closed__2;
+x_9 = l_Lean_registerParametricAttribute___rarg___closed__1;
+x_10 = l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___closed__1;
+x_11 = l_Lean_registerParametricAttribute___rarg___closed__2;
 lean_inc(x_1);
-x_11 = lean_alloc_ctor(0, 6, 0);
-lean_ctor_set(x_11, 0, x_1);
-lean_ctor_set(x_11, 1, x_6);
-lean_ctor_set(x_11, 2, x_7);
-lean_ctor_set(x_11, 3, x_8);
-lean_ctor_set(x_11, 4, x_9);
-lean_ctor_set(x_11, 5, x_10);
-x_12 = l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_mkExportAttr___spec__5(x_11, x_5);
-if (lean_obj_tag(x_12) == 0)
+x_12 = lean_alloc_ctor(0, 6, 0);
+lean_ctor_set(x_12, 0, x_1);
+lean_ctor_set(x_12, 1, x_7);
+lean_ctor_set(x_12, 2, x_8);
+lean_ctor_set(x_12, 3, x_9);
+lean_ctor_set(x_12, 4, x_10);
+lean_ctor_set(x_12, 5, x_11);
+x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_mkExportAttr___spec__5(x_12, x_6);
+if (lean_obj_tag(x_13) == 0)
 {
-lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18; 
-x_13 = lean_ctor_get(x_12, 0);
-lean_inc(x_13);
-x_14 = lean_ctor_get(x_12, 1);
+lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_14 = lean_ctor_get(x_13, 0);
+lean_inc(x_14);
+x_15 = lean_ctor_get(x_13, 1);
+lean_inc(x_15);
+lean_dec(x_13);
 lean_inc(x_14);
-lean_dec(x_12);
-lean_inc(x_13);
 lean_inc(x_1);
-x_15 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___rarg___lambda__4___boxed), 9, 4);
-lean_closure_set(x_15, 0, x_1);
-lean_closure_set(x_15, 1, x_3);
-lean_closure_set(x_15, 2, x_13);
-lean_closure_set(x_15, 3, x_4);
-x_16 = 0;
+x_16 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___rarg___lambda__4___boxed), 9, 4);
+lean_closure_set(x_16, 0, x_1);
+lean_closure_set(x_16, 1, x_3);
+lean_closure_set(x_16, 2, x_14);
+lean_closure_set(x_16, 3, x_4);
 x_17 = lean_alloc_ctor(0, 3, 1);
 lean_ctor_set(x_17, 0, x_1);
 lean_ctor_set(x_17, 1, x_2);
-lean_ctor_set(x_17, 2, x_15);
-lean_ctor_set_uint8(x_17, sizeof(void*)*3, x_16);
+lean_ctor_set(x_17, 2, x_16);
+lean_ctor_set_uint8(x_17, sizeof(void*)*3, x_5);
 lean_inc(x_17);
-x_18 = l_Lean_registerBuiltinAttribute(x_17, x_14);
+x_18 = l_Lean_registerBuiltinAttribute(x_17, x_15);
 if (lean_obj_tag(x_18) == 0)
 {
 uint8_t x_19; 
@@ -1546,7 +1546,7 @@ x_20 = lean_ctor_get(x_18, 0);
 lean_dec(x_20);
 x_21 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_21, 0, x_17);
-lean_ctor_set(x_21, 1, x_13);
+lean_ctor_set(x_21, 1, x_14);
 lean_ctor_set(x_18, 0, x_21);
 return x_18;
 }
@@ -1558,7 +1558,7 @@ lean_inc(x_22);
 lean_dec(x_18);
 x_23 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_23, 0, x_17);
-lean_ctor_set(x_23, 1, x_13);
+lean_ctor_set(x_23, 1, x_14);
 x_24 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_24, 0, x_23);
 lean_ctor_set(x_24, 1, x_22);
@@ -1569,7 +1569,7 @@ else
 {
 uint8_t x_25; 
 lean_dec(x_17);
-lean_dec(x_13);
+lean_dec(x_14);
 x_25 = !lean_is_exclusive(x_18);
 if (x_25 == 0)
 {
@@ -1597,19 +1597,19 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_29 = !lean_is_exclusive(x_12);
+x_29 = !lean_is_exclusive(x_13);
 if (x_29 == 0)
 {
-return x_12;
+return x_13;
 }
 else
 {
 lean_object* x_30; lean_object* x_31; lean_object* x_32; 
-x_30 = lean_ctor_get(x_12, 0);
-x_31 = lean_ctor_get(x_12, 1);
+x_30 = lean_ctor_get(x_13, 0);
+x_31 = lean_ctor_get(x_13, 1);
 lean_inc(x_31);
 lean_inc(x_30);
-lean_dec(x_12);
+lean_dec(x_13);
 x_32 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_32, 0, x_30);
 lean_ctor_set(x_32, 1, x_31);
@@ -1743,13 +1743,14 @@ return x_1;
 lean_object* l_Lean_mkExportAttr(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; uint8_t x_6; lean_object* x_7; 
 x_2 = l_Lean_mkExportAttr___closed__2;
 x_3 = l_Lean_mkExportAttr___closed__3;
 x_4 = l_Lean_mkExportAttr___closed__4;
 x_5 = l_Lean_mkExportAttr___closed__5;
-x_6 = l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = 0;
+x_7 = l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* l_RBNode_fold___main___at_Lean_mkExportAttr___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
@@ -1802,6 +1803,16 @@ lean_dec(x_1);
 return x_2;
 }
 }
+lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+uint8_t x_7; lean_object* x_8; 
+x_7 = lean_unbox(x_5);
+lean_dec(x_5);
+x_8 = l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1(x_1, x_2, x_3, x_4, x_7, x_6);
+return x_8;
+}
+}
 lean_object* l_Lean_mkExportAttr___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {

stage0/stdlib/Init/Lean/Compiler/ExternAttr.c

@@ -147,11 +147,12 @@ lean_object* l_Lean_getExternEntryForAux___main(lean_object*, lean_object*);
 extern lean_object* l_System_FilePath_dirName___closed__1;
 lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
+lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExternAttr___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Compiler_ExternAttr_1__syntaxToExternEntries___main___closed__3;
 lean_object* l___private_Init_Lean_Compiler_ExternAttr_1__syntaxToExternEntries___boxed(lean_object*, lean_object*, lean_object*);
 uint8_t l_UInt32_decLe(uint32_t, uint32_t);
 lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExternAttr___spec__1___closed__1;
-lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExternAttr___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExternAttr___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* l_Lean_mkSimpleFnCall(lean_object*, lean_object*);
 lean_object* l_Lean_getExternEntryFor___boxed(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Compiler_ExternAttr_1__syntaxToExternEntries___main___closed__5;
@@ -1778,47 +1779,46 @@ x_1 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___at_Lean_mk
 return x_1;
 }
 }
-lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExternAttr___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExternAttr___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint8_t x_5, lean_object* x_6) {
 _start:
 {
-lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
-x_6 = l_Lean_registerTagAttribute___closed__1;
-x_7 = l_Lean_registerTagAttribute___closed__2;
-x_8 = l_Lean_mkProjectionFnInfoExtension___closed__3;
-x_9 = l_Lean_registerParametricAttribute___at_Lean_mkExternAttr___spec__1___closed__1;
-x_10 = l_Lean_registerParametricAttribute___rarg___closed__2;
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
+x_7 = l_Lean_registerTagAttribute___closed__1;
+x_8 = l_Lean_registerTagAttribute___closed__2;
+x_9 = l_Lean_mkProjectionFnInfoExtension___closed__3;
+x_10 = l_Lean_registerParametricAttribute___at_Lean_mkExternAttr___spec__1___closed__1;
+x_11 = l_Lean_registerParametricAttribute___rarg___closed__2;
 lean_inc(x_1);
-x_11 = lean_alloc_ctor(0, 6, 0);
-lean_ctor_set(x_11, 0, x_1);
-lean_ctor_set(x_11, 1, x_6);
-lean_ctor_set(x_11, 2, x_7);
-lean_ctor_set(x_11, 3, x_8);
-lean_ctor_set(x_11, 4, x_9);
-lean_ctor_set(x_11, 5, x_10);
-x_12 = l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_mkExternAttr___spec__5(x_11, x_5);
-if (lean_obj_tag(x_12) == 0)
+x_12 = lean_alloc_ctor(0, 6, 0);
+lean_ctor_set(x_12, 0, x_1);
+lean_ctor_set(x_12, 1, x_7);
+lean_ctor_set(x_12, 2, x_8);
+lean_ctor_set(x_12, 3, x_9);
+lean_ctor_set(x_12, 4, x_10);
+lean_ctor_set(x_12, 5, x_11);
+x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_mkExternAttr___spec__5(x_12, x_6);
+if (lean_obj_tag(x_13) == 0)
 {
-lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18; 
-x_13 = lean_ctor_get(x_12, 0);
-lean_inc(x_13);
-x_14 = lean_ctor_get(x_12, 1);
+lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_14 = lean_ctor_get(x_13, 0);
+lean_inc(x_14);
+x_15 = lean_ctor_get(x_13, 1);
+lean_inc(x_15);
+lean_dec(x_13);
 lean_inc(x_14);
-lean_dec(x_12);
-lean_inc(x_13);
 lean_inc(x_1);
-x_15 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___rarg___lambda__4___boxed), 9, 4);
-lean_closure_set(x_15, 0, x_1);
-lean_closure_set(x_15, 1, x_3);
-lean_closure_set(x_15, 2, x_13);
-lean_closure_set(x_15, 3, x_4);
-x_16 = 0;
+x_16 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___rarg___lambda__4___boxed), 9, 4);
+lean_closure_set(x_16, 0, x_1);
+lean_closure_set(x_16, 1, x_3);
+lean_closure_set(x_16, 2, x_14);
+lean_closure_set(x_16, 3, x_4);
 x_17 = lean_alloc_ctor(0, 3, 1);
 lean_ctor_set(x_17, 0, x_1);
 lean_ctor_set(x_17, 1, x_2);
-lean_ctor_set(x_17, 2, x_15);
-lean_ctor_set_uint8(x_17, sizeof(void*)*3, x_16);
+lean_ctor_set(x_17, 2, x_16);
+lean_ctor_set_uint8(x_17, sizeof(void*)*3, x_5);
 lean_inc(x_17);
-x_18 = l_Lean_registerBuiltinAttribute(x_17, x_14);
+x_18 = l_Lean_registerBuiltinAttribute(x_17, x_15);
 if (lean_obj_tag(x_18) == 0)
 {
 uint8_t x_19; 
@@ -1830,7 +1830,7 @@ x_20 = lean_ctor_get(x_18, 0);
 lean_dec(x_20);
 x_21 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_21, 0, x_17);
-lean_ctor_set(x_21, 1, x_13);
+lean_ctor_set(x_21, 1, x_14);
 lean_ctor_set(x_18, 0, x_21);
 return x_18;
 }
@@ -1842,7 +1842,7 @@ lean_inc(x_22);
 lean_dec(x_18);
 x_23 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_23, 0, x_17);
-lean_ctor_set(x_23, 1, x_13);
+lean_ctor_set(x_23, 1, x_14);
 x_24 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_24, 0, x_23);
 lean_ctor_set(x_24, 1, x_22);
@@ -1853,7 +1853,7 @@ else
 {
 uint8_t x_25; 
 lean_dec(x_17);
-lean_dec(x_13);
+lean_dec(x_14);
 x_25 = !lean_is_exclusive(x_18);
 if (x_25 == 0)
 {
@@ -1881,19 +1881,19 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_29 = !lean_is_exclusive(x_12);
+x_29 = !lean_is_exclusive(x_13);
 if (x_29 == 0)
 {
-return x_12;
+return x_13;
 }
 else
 {
 lean_object* x_30; lean_object* x_31; lean_object* x_32; 
-x_30 = lean_ctor_get(x_12, 0);
-x_31 = lean_ctor_get(x_12, 1);
+x_30 = lean_ctor_get(x_13, 0);
+x_31 = lean_ctor_get(x_13, 1);
 lean_inc(x_31);
 lean_inc(x_30);
-lean_dec(x_12);
+lean_dec(x_13);
 x_32 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_32, 0, x_30);
 lean_ctor_set(x_32, 1, x_31);
@@ -1990,13 +1990,14 @@ return x_1;
 lean_object* l_Lean_mkExternAttr(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; uint8_t x_6; lean_object* x_7; 
 x_2 = l_Lean_mkExternAttr___closed__2;
 x_3 = l_Lean_mkExternAttr___closed__3;
 x_4 = l_Lean_mkExternAttr___closed__4;
 x_5 = l_Lean_mkExternAttr___closed__5;
-x_6 = l_Lean_registerParametricAttribute___at_Lean_mkExternAttr___spec__1(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = 0;
+x_7 = l_Lean_registerParametricAttribute___at_Lean_mkExternAttr___spec__1(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* l_RBNode_fold___main___at_Lean_mkExternAttr___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
@@ -2049,6 +2050,16 @@ lean_dec(x_1);
 return x_2;
 }
 }
+lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExternAttr___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+uint8_t x_7; lean_object* x_8; 
+x_7 = lean_unbox(x_5);
+lean_dec(x_5);
+x_8 = l_Lean_registerParametricAttribute___at_Lean_mkExternAttr___spec__1(x_1, x_2, x_3, x_4, x_7, x_6);
+return x_8;
+}
+}
 lean_object* l_Lean_mkExternAttr___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {

stage0/stdlib/Init/Lean/Compiler/ImplementedByAttr.c

@@ -18,6 +18,7 @@ extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensions
 lean_object* l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1___closed__1;
 lean_object* lean_nat_div(lean_object*, lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_getModuleEntries___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_mkImplementedByAttr___lambda__1___closed__1;
 lean_object* l_Lean_Compiler_mkImplementedByAttr___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_registerTagAttribute___spec__4___closed__1;
@@ -41,7 +42,7 @@ lean_object* lean_nat_add(lean_object*, lean_object*);
 extern lean_object* l_Lean_registerTagAttribute___closed__2;
 lean_object* l_Array_binSearchAux___main___at_Lean_Compiler_getImplementedBy___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Compiler_mkImplementedByAttr___spec__7(lean_object*, lean_object*);
-lean_object* l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_mkImplementedByAttr___lambda__2(lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
@@ -1116,47 +1117,46 @@ x_1 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___at_Lean_Co
 return x_1;
 }
 }
-lean_object* l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+lean_object* l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint8_t x_5, lean_object* x_6) {
 _start:
 {
-lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
-x_6 = l_Lean_registerTagAttribute___closed__1;
-x_7 = l_Lean_registerTagAttribute___closed__2;
-x_8 = l_Lean_registerParametricAttribute___rarg___closed__1;
-x_9 = l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1___closed__1;
-x_10 = l_Lean_registerParametricAttribute___rarg___closed__2;
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
+x_7 = l_Lean_registerTagAttribute___closed__1;
+x_8 = l_Lean_registerTagAttribute___closed__2;
+x_9 = l_Lean_registerParametricAttribute___rarg___closed__1;
+x_10 = l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1___closed__1;
+x_11 = l_Lean_registerParametricAttribute___rarg___closed__2;
 lean_inc(x_1);
-x_11 = lean_alloc_ctor(0, 6, 0);
-lean_ctor_set(x_11, 0, x_1);
-lean_ctor_set(x_11, 1, x_6);
-lean_ctor_set(x_11, 2, x_7);
-lean_ctor_set(x_11, 3, x_8);
-lean_ctor_set(x_11, 4, x_9);
-lean_ctor_set(x_11, 5, x_10);
-x_12 = l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_Compiler_mkImplementedByAttr___spec__5(x_11, x_5);
-if (lean_obj_tag(x_12) == 0)
+x_12 = lean_alloc_ctor(0, 6, 0);
+lean_ctor_set(x_12, 0, x_1);
+lean_ctor_set(x_12, 1, x_7);
+lean_ctor_set(x_12, 2, x_8);
+lean_ctor_set(x_12, 3, x_9);
+lean_ctor_set(x_12, 4, x_10);
+lean_ctor_set(x_12, 5, x_11);
+x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_Compiler_mkImplementedByAttr___spec__5(x_12, x_6);
+if (lean_obj_tag(x_13) == 0)
 {
-lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18; 
-x_13 = lean_ctor_get(x_12, 0);
-lean_inc(x_13);
-x_14 = lean_ctor_get(x_12, 1);
+lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_14 = lean_ctor_get(x_13, 0);
+lean_inc(x_14);
+x_15 = lean_ctor_get(x_13, 1);
+lean_inc(x_15);
+lean_dec(x_13);
 lean_inc(x_14);
-lean_dec(x_12);
-lean_inc(x_13);
 lean_inc(x_1);
-x_15 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___rarg___lambda__4___boxed), 9, 4);
-lean_closure_set(x_15, 0, x_1);
-lean_closure_set(x_15, 1, x_3);
-lean_closure_set(x_15, 2, x_13);
-lean_closure_set(x_15, 3, x_4);
-x_16 = 0;
+x_16 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___rarg___lambda__4___boxed), 9, 4);
+lean_closure_set(x_16, 0, x_1);
+lean_closure_set(x_16, 1, x_3);
+lean_closure_set(x_16, 2, x_14);
+lean_closure_set(x_16, 3, x_4);
 x_17 = lean_alloc_ctor(0, 3, 1);
 lean_ctor_set(x_17, 0, x_1);
 lean_ctor_set(x_17, 1, x_2);
-lean_ctor_set(x_17, 2, x_15);
-lean_ctor_set_uint8(x_17, sizeof(void*)*3, x_16);
+lean_ctor_set(x_17, 2, x_16);
+lean_ctor_set_uint8(x_17, sizeof(void*)*3, x_5);
 lean_inc(x_17);
-x_18 = l_Lean_registerBuiltinAttribute(x_17, x_14);
+x_18 = l_Lean_registerBuiltinAttribute(x_17, x_15);
 if (lean_obj_tag(x_18) == 0)
 {
 uint8_t x_19; 
@@ -1168,7 +1168,7 @@ x_20 = lean_ctor_get(x_18, 0);
 lean_dec(x_20);
 x_21 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_21, 0, x_17);
-lean_ctor_set(x_21, 1, x_13);
+lean_ctor_set(x_21, 1, x_14);
 lean_ctor_set(x_18, 0, x_21);
 return x_18;
 }
@@ -1180,7 +1180,7 @@ lean_inc(x_22);
 lean_dec(x_18);
 x_23 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_23, 0, x_17);
-lean_ctor_set(x_23, 1, x_13);
+lean_ctor_set(x_23, 1, x_14);
 x_24 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_24, 0, x_23);
 lean_ctor_set(x_24, 1, x_22);
@@ -1191,7 +1191,7 @@ else
 {
 uint8_t x_25; 
 lean_dec(x_17);
-lean_dec(x_13);
+lean_dec(x_14);
 x_25 = !lean_is_exclusive(x_18);
 if (x_25 == 0)
 {
@@ -1219,19 +1219,19 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_29 = !lean_is_exclusive(x_12);
+x_29 = !lean_is_exclusive(x_13);
 if (x_29 == 0)
 {
-return x_12;
+return x_13;
 }
 else
 {
 lean_object* x_30; lean_object* x_31; lean_object* x_32; 
-x_30 = lean_ctor_get(x_12, 0);
-x_31 = lean_ctor_get(x_12, 1);
+x_30 = lean_ctor_get(x_13, 0);
+x_31 = lean_ctor_get(x_13, 1);
 lean_inc(x_31);
 lean_inc(x_30);
-lean_dec(x_12);
+lean_dec(x_13);
 x_32 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_32, 0, x_30);
 lean_ctor_set(x_32, 1, x_31);
@@ -1444,13 +1444,14 @@ return x_1;
 lean_object* l_Lean_Compiler_mkImplementedByAttr(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; uint8_t x_6; lean_object* x_7; 
 x_2 = l_Lean_Compiler_mkImplementedByAttr___closed__2;
 x_3 = l_Lean_Compiler_mkImplementedByAttr___closed__3;
 x_4 = l_Lean_Compiler_mkImplementedByAttr___closed__4;
 x_5 = l_Lean_Compiler_mkImplementedByAttr___closed__5;
-x_6 = l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = 0;
+x_7 = l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* l_RBNode_fold___main___at_Lean_Compiler_mkImplementedByAttr___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
@@ -1503,6 +1504,16 @@ lean_dec(x_1);
 return x_2;
 }
 }
+lean_object* l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+uint8_t x_7; lean_object* x_8; 
+x_7 = lean_unbox(x_5);
+lean_dec(x_5);
+x_8 = l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1(x_1, x_2, x_3, x_4, x_7, x_6);
+return x_8;
+}
+}
 lean_object* l_Lean_Compiler_mkImplementedByAttr___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {

stage0/stdlib/Init/Lean/Compiler/InitAttr.c

@@ -20,6 +20,7 @@ lean_object* l___private_Init_Lean_Compiler_InitAttr_2__isUnitType___closed__1;
 extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;
 lean_object* l___private_Init_Lean_Compiler_InitAttr_2__isUnitType___boxed(lean_object*);
 lean_object* l_Lean_registerParametricAttribute___at_Lean_mkInitAttr___spec__1___closed__1;
+lean_object* l_Lean_registerParametricAttribute___at_Lean_mkInitAttr___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_div(lean_object*, lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_getModuleEntries___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_registerTagAttribute___spec__4___closed__1;
@@ -93,7 +94,7 @@ lean_object* l_Lean_mkInitAttr___closed__3;
 uint8_t l_Lean_isIOUnitInitFn(lean_object*, lean_object*);
 lean_object* lean_io_ref_reset(lean_object*, lean_object*);
 extern lean_object* l_Lean_registerEnvExtensionUnsafe___rarg___closed__2;
-lean_object* l_Lean_registerParametricAttribute___at_Lean_mkInitAttr___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_registerParametricAttribute___at_Lean_mkInitAttr___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* l_Lean_Environment_getModuleIdxFor_x3f(lean_object*, lean_object*);
 lean_object* lean_io_ref_set(lean_object*, lean_object*, lean_object*);
 lean_object* lean_get_init_fn_name_for(lean_object*, lean_object*);
@@ -1321,47 +1322,46 @@ x_1 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___at_Lean_mk
 return x_1;
 }
 }
-lean_object* l_Lean_registerParametricAttribute___at_Lean_mkInitAttr___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+lean_object* l_Lean_registerParametricAttribute___at_Lean_mkInitAttr___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint8_t x_5, lean_object* x_6) {
 _start:
 {
-lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
-x_6 = l_Lean_registerTagAttribute___closed__1;
-x_7 = l_Lean_registerTagAttribute___closed__2;
-x_8 = l_Lean_registerParametricAttribute___rarg___closed__1;
-x_9 = l_Lean_registerParametricAttribute___at_Lean_mkInitAttr___spec__1___closed__1;
-x_10 = l_Lean_registerParametricAttribute___rarg___closed__2;
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
+x_7 = l_Lean_registerTagAttribute___closed__1;
+x_8 = l_Lean_registerTagAttribute___closed__2;
+x_9 = l_Lean_registerParametricAttribute___rarg___closed__1;
+x_10 = l_Lean_registerParametricAttribute___at_Lean_mkInitAttr___spec__1___closed__1;
+x_11 = l_Lean_registerParametricAttribute___rarg___closed__2;
 lean_inc(x_1);
-x_11 = lean_alloc_ctor(0, 6, 0);
-lean_ctor_set(x_11, 0, x_1);
-lean_ctor_set(x_11, 1, x_6);
-lean_ctor_set(x_11, 2, x_7);
-lean_ctor_set(x_11, 3, x_8);
-lean_ctor_set(x_11, 4, x_9);
-lean_ctor_set(x_11, 5, x_10);
-x_12 = l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_mkInitAttr___spec__5(x_11, x_5);
-if (lean_obj_tag(x_12) == 0)
+x_12 = lean_alloc_ctor(0, 6, 0);
+lean_ctor_set(x_12, 0, x_1);
+lean_ctor_set(x_12, 1, x_7);
+lean_ctor_set(x_12, 2, x_8);
+lean_ctor_set(x_12, 3, x_9);
+lean_ctor_set(x_12, 4, x_10);
+lean_ctor_set(x_12, 5, x_11);
+x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_mkInitAttr___spec__5(x_12, x_6);
+if (lean_obj_tag(x_13) == 0)
 {
-lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18; 
-x_13 = lean_ctor_get(x_12, 0);
-lean_inc(x_13);
-x_14 = lean_ctor_get(x_12, 1);
+lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_14 = lean_ctor_get(x_13, 0);
+lean_inc(x_14);
+x_15 = lean_ctor_get(x_13, 1);
+lean_inc(x_15);
+lean_dec(x_13);
 lean_inc(x_14);
-lean_dec(x_12);
-lean_inc(x_13);
 lean_inc(x_1);
-x_15 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___rarg___lambda__4___boxed), 9, 4);
-lean_closure_set(x_15, 0, x_1);
-lean_closure_set(x_15, 1, x_3);
-lean_closure_set(x_15, 2, x_13);
-lean_closure_set(x_15, 3, x_4);
-x_16 = 0;
+x_16 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___rarg___lambda__4___boxed), 9, 4);
+lean_closure_set(x_16, 0, x_1);
+lean_closure_set(x_16, 1, x_3);
+lean_closure_set(x_16, 2, x_14);
+lean_closure_set(x_16, 3, x_4);
 x_17 = lean_alloc_ctor(0, 3, 1);
 lean_ctor_set(x_17, 0, x_1);
 lean_ctor_set(x_17, 1, x_2);
-lean_ctor_set(x_17, 2, x_15);
-lean_ctor_set_uint8(x_17, sizeof(void*)*3, x_16);
+lean_ctor_set(x_17, 2, x_16);
+lean_ctor_set_uint8(x_17, sizeof(void*)*3, x_5);
 lean_inc(x_17);
-x_18 = l_Lean_registerBuiltinAttribute(x_17, x_14);
+x_18 = l_Lean_registerBuiltinAttribute(x_17, x_15);
 if (lean_obj_tag(x_18) == 0)
 {
 uint8_t x_19; 
@@ -1373,7 +1373,7 @@ x_20 = lean_ctor_get(x_18, 0);
 lean_dec(x_20);
 x_21 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_21, 0, x_17);
-lean_ctor_set(x_21, 1, x_13);
+lean_ctor_set(x_21, 1, x_14);
 lean_ctor_set(x_18, 0, x_21);
 return x_18;
 }
@@ -1385,7 +1385,7 @@ lean_inc(x_22);
 lean_dec(x_18);
 x_23 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_23, 0, x_17);
-lean_ctor_set(x_23, 1, x_13);
+lean_ctor_set(x_23, 1, x_14);
 x_24 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_24, 0, x_23);
 lean_ctor_set(x_24, 1, x_22);
@@ -1396,7 +1396,7 @@ else
 {
 uint8_t x_25; 
 lean_dec(x_17);
-lean_dec(x_13);
+lean_dec(x_14);
 x_25 = !lean_is_exclusive(x_18);
 if (x_25 == 0)
 {
@@ -1424,19 +1424,19 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_29 = !lean_is_exclusive(x_12);
+x_29 = !lean_is_exclusive(x_13);
 if (x_29 == 0)
 {
-return x_12;
+return x_13;
 }
 else
 {
 lean_object* x_30; lean_object* x_31; lean_object* x_32; 
-x_30 = lean_ctor_get(x_12, 0);
-x_31 = lean_ctor_get(x_12, 1);
+x_30 = lean_ctor_get(x_13, 0);
+x_31 = lean_ctor_get(x_13, 1);
 lean_inc(x_31);
 lean_inc(x_30);
-lean_dec(x_12);
+lean_dec(x_13);
 x_32 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_32, 0, x_30);
 lean_ctor_set(x_32, 1, x_31);
@@ -1732,13 +1732,14 @@ return x_1;
 lean_object* l_Lean_mkInitAttr(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; uint8_t x_6; lean_object* x_7; 
 x_2 = l_Lean_mkInitAttr___closed__2;
 x_3 = l_Lean_mkInitAttr___closed__3;
 x_4 = l_Lean_mkInitAttr___closed__4;
 x_5 = l_Lean_mkInitAttr___closed__5;
-x_6 = l_Lean_registerParametricAttribute___at_Lean_mkInitAttr___spec__1(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = 0;
+x_7 = l_Lean_registerParametricAttribute___at_Lean_mkInitAttr___spec__1(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* l_RBNode_fold___main___at_Lean_mkInitAttr___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
@@ -1791,6 +1792,16 @@ lean_dec(x_1);
 return x_2;
 }
 }
+lean_object* l_Lean_registerParametricAttribute___at_Lean_mkInitAttr___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+uint8_t x_7; lean_object* x_8; 
+x_7 = lean_unbox(x_5);
+lean_dec(x_5);
+x_8 = l_Lean_registerParametricAttribute___at_Lean_mkInitAttr___spec__1(x_1, x_2, x_3, x_4, x_7, x_6);
+return x_8;
+}
+}
 lean_object* l_Lean_mkInitAttr___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {

stage0/stdlib/Init/Lean/Declaration.c

@@ -36,7 +36,9 @@ lean_object* l_Lean_ConstantInfo_hasValue___boxed(lean_object*);
 lean_object* l_Lean_ConstantInfo_name(lean_object*);
 lean_object* l_Lean_ConstantVal_inhabited;
 lean_object* l_Lean_ConstantInfo_toConstantVal___boxed(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 uint8_t l_Lean_ConstantInfo_hasValue(lean_object*);
+lean_object* l_Lean_mkRecFor___closed__1;
 lean_object* l_Lean_RecursorVal_getInduct___boxed(lean_object*);
 lean_object* l_Lean_ReducibilityHints_Inhabited;
 lean_object* l_Lean_ConstantInfo_isCtor___boxed(lean_object*);
@@ -59,6 +61,7 @@ lean_object* l_Lean_ConstantInfo_value_x21___closed__3;
 lean_object* l_Lean_ConstantInfo_value_x21(lean_object*);
 lean_object* l_Lean_ConstantInfo_hints___boxed(lean_object*);
 lean_object* lean_task_get(lean_object*);
+lean_object* l_Lean_mkRecFor(lean_object*);
 lean_object* l_Lean_ConstantInfo_type___boxed(lean_object*);
 uint8_t l_Lean_ReducibilityHints_lt(lean_object*, lean_object*);
 lean_object* _init_l_Lean_ReducibilityHints_Inhabited() {
@@ -555,6 +558,23 @@ lean_dec(x_1);
 return x_3;
 }
 }
+lean_object* _init_l_Lean_mkRecFor___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("rec");
+return x_1;
+}
+}
+lean_object* l_Lean_mkRecFor(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; 
+x_2 = l_Lean_mkRecFor___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
 lean_object* initialize_Init_Lean_Expr(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Lean_Declaration(lean_object* w) {
@@ -582,6 +602,8 @@ l_Lean_ConstantInfo_value_x21___closed__2 = _init_l_Lean_ConstantInfo_value_x21_
 lean_mark_persistent(l_Lean_ConstantInfo_value_x21___closed__2);
 l_Lean_ConstantInfo_value_x21___closed__3 = _init_l_Lean_ConstantInfo_value_x21___closed__3();
 lean_mark_persistent(l_Lean_ConstantInfo_value_x21___closed__3);
+l_Lean_mkRecFor___closed__1 = _init_l_Lean_mkRecFor___closed__1();
+lean_mark_persistent(l_Lean_mkRecFor___closed__1);
 return lean_mk_io_result(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Init/Lean/Elab/Command.c

@@ -201,6 +201,7 @@ lean_object* l___private_Init_Lean_Elab_Command_10__toCommandResult___rarg___clo
 lean_object* l_Lean_Elab_Command_elabSynth(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Command_elabUniverses___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_foldl___main___at_Lean_Elab_Command_elabExport___spec__2(lean_object*, lean_object*);
+extern lean_object* l_Lean_Meta_run___rarg___closed__5;
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabInitQuot___closed__2;
 extern lean_object* l_Lean_Meta_dbgTrace___rarg___closed__1;
 lean_object* l_Lean_Elab_Command_setOption___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -376,7 +377,6 @@ lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabEnd(lean_object*);
 lean_object* l_Lean_Elab_Command_throwAlreadyDeclaredUniverseLevel___rarg___closed__1;
 extern lean_object* l_Lean_Elab_Term_elabTermAux___main___closed__3;
 lean_object* l___private_Init_Lean_Elab_Command_13__addNamespace___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_IO_runMeta___rarg___closed__4;
 extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__3;
 lean_object* l_Lean_Elab_Command_withMacroExpansion(lean_object*);
 lean_object* l_Lean_Elab_Command_withDeclId___closed__3;
@@ -8010,7 +8010,7 @@ x_2 = lean_ctor_get(x_1, 0);
 x_3 = lean_ctor_get(x_1, 1);
 x_4 = lean_ctor_get(x_1, 3);
 x_5 = l_Lean_MetavarContext_Inhabited___closed__1;
-x_6 = l_IO_runMeta___rarg___closed__4;
+x_6 = l_Lean_Meta_run___rarg___closed__5;
 x_7 = l_Lean_NameGenerator_Inhabited___closed__3;
 x_8 = l_Lean_TraceState_Inhabited___closed__1;
 x_9 = l_PersistentArray_empty___closed__3;

stage0/stdlib/Init/Lean/Elab/Quotation.c

@@ -208,6 +208,7 @@ lean_object* l_List_replicate___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Quotation_getPatternVars(lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__3___closed__3;
 lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__1___closed__2;
+extern lean_object* l_Lean_Meta_run___rarg___closed__5;
 lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___elambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_map___main___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__1(lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_2__quoteList___main___rarg(lean_object*, lean_object*);
@@ -369,14 +370,12 @@ lean_object* l___private_Init_Lean_Elab_Quotation_11__letBindRhss___main___close
 lean_object* l_Lean_mkFVar(lean_object*);
 lean_object* l_List_head_x21___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__2___closed__3;
 lean_object* l_Lean_Elab_Term_TermElabM_inhabited___boxed(lean_object*, lean_object*);
-extern lean_object* l_IO_runMeta___rarg___closed__4;
 extern lean_object* l_Lean_nullKind___closed__1;
 lean_object* l_List_foldl___main___at___private_Init_Lean_Elab_Quotation_13__toPreterm___main___spec__8(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_8__explodeHeadPat___closed__3;
 lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_Quotation_match__syntax_expand___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Term_elabListLit___closed__5;
-extern lean_object* l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__1;
 lean_object* l_Lean_Option_hasQuote(lean_object*);
 uint8_t l_Lean_Syntax_isAtom(lean_object*);
 extern lean_object* l_Lean_nullKind___closed__2;
@@ -542,6 +541,7 @@ extern lean_object* l_Lean_Elab_Term_elabListLit___closed__3;
 extern lean_object* l_Lean_Unhygienic_run___rarg___closed__1;
 lean_object* l_Lean_mkNatLit(lean_object*);
 lean_object* l_Lean_mkStrLit(lean_object*);
+extern lean_object* l_Lean_Meta_run___rarg___closed__1;
 lean_object* l_Lean_mkCTermIdFrom(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___closed__1;
 extern lean_object* l___private_Init_Lean_Elab_Term_5__expandCDot___main___closed__4;
@@ -24904,7 +24904,7 @@ lean_inc(x_5);
 lean_dec(x_1);
 x_6 = l___private_Init_Lean_Elab_Quotation_14__oldRunTermElabM___rarg___closed__1;
 x_7 = l_List_foldl___main___at___private_Init_Lean_Elab_Quotation_14__oldRunTermElabM___spec__1(x_6, x_4);
-x_8 = l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__1;
+x_8 = l_Lean_Meta_run___rarg___closed__1;
 x_9 = l_Array_empty___closed__1;
 x_10 = lean_unsigned_to_nat(0u);
 x_11 = lean_unsigned_to_nat(10000u);
@@ -24938,7 +24938,7 @@ lean_ctor_set_uint8(x_21, sizeof(void*)*10, x_20);
 lean_ctor_set_uint8(x_21, sizeof(void*)*10 + 1, x_20);
 lean_ctor_set_uint8(x_21, sizeof(void*)*10 + 2, x_20);
 x_22 = l_Lean_MetavarContext_Inhabited___closed__1;
-x_23 = l_IO_runMeta___rarg___closed__4;
+x_23 = l_Lean_Meta_run___rarg___closed__5;
 x_24 = l_Lean_NameGenerator_Inhabited___closed__3;
 x_25 = l_Lean_TraceState_Inhabited___closed__1;
 x_26 = l_PersistentArray_empty___closed__3;

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

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean.Elab.Tactic
-// Imports: Init.Lean.Elab.Term Init.Lean.Elab.Tactic.Basic Init.Lean.Elab.Tactic.ElabTerm Init.Lean.Elab.Tactic.Induction
+// Imports: Init.Lean.Elab.Term Init.Lean.Elab.Tactic.Basic Init.Lean.Elab.Tactic.ElabTerm Init.Lean.Elab.Tactic.Induction Init.Lean.Elab.Tactic.Generalize
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -17,6 +17,7 @@ lean_object* initialize_Init_Lean_Elab_Term(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Tactic_Basic(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Tactic_ElabTerm(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Tactic_Induction(lean_object*);
+lean_object* initialize_Init_Lean_Elab_Tactic_Generalize(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Lean_Elab_Tactic(lean_object* w) {
 lean_object * res;
@@ -34,6 +35,9 @@ lean_dec_ref(res);
 res = initialize_Init_Lean_Elab_Tactic_Induction(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Lean_Elab_Tactic_Generalize(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_mk_io_result(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Init/Lean/Elab/Term.c

@@ -282,6 +282,7 @@ lean_object* l_Lean_Elab_Term_withTransparency(lean_object*);
 lean_object* l_HashMapImp_find_x3f___at_Lean_Elab_Term_elabTermAux___main___spec__5___boxed(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_byTactic___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_withIncRecDepth___rarg___closed__1;
+extern lean_object* l_Lean_Meta_run___rarg___closed__5;
 lean_object* l_Lean_Elab_Term_elabListLit___closed__2;
 lean_object* l_Lean_Elab_Term_Lean_Elab_MonadMacroAdapter___lambda__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_withConfig___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -534,7 +535,6 @@ lean_object* l_Lean_Elab_Term_mkFreshAnonymousIdent___boxed(lean_object*, lean_o
 lean_object* l_Lean_Elab_Term_elabRawNumLit(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabTermAux___main___closed__3;
 lean_object* l___private_Init_Lean_Elab_Term_13__tryCoeSort___closed__3;
-extern lean_object* l_IO_runMeta___rarg___closed__4;
 extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__3;
 lean_object* l___private_Init_Lean_Elab_Term_6__isTypeApp_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_foldMAux___main___at___private_Init_Lean_Elab_Term_18__mkFreshLevelMVars___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -935,7 +935,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_1 = l_Lean_EnvExtension_setState___closed__1;
 x_2 = l_Lean_MetavarContext_Inhabited___closed__1;
-x_3 = l_IO_runMeta___rarg___closed__4;
+x_3 = l_Lean_Meta_run___rarg___closed__5;
 x_4 = l_Lean_NameGenerator_Inhabited___closed__3;
 x_5 = l_Lean_TraceState_Inhabited___closed__1;
 x_6 = l_PersistentArray_empty___closed__3;

stage0/stdlib/Init/Lean/Meta/AppBuilder.c

@@ -64,7 +64,6 @@ lean_object* l_Lean_Expr_heq_x3f___closed__2;
 lean_object* l_Lean_Expr_iff_x3f___closed__2;
 lean_object* l_Lean_Expr_heq_x3f(lean_object*);
 lean_object* lean_instantiate_type_lparams(lean_object*, lean_object*);
-lean_object* l_Lean_Meta_mkEqRec___closed__2;
 lean_object* l_Array_forMAux___main___at___private_Init_Lean_Meta_AppBuilder_2__mkAppMFinal___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkHEqRefl___closed__1;
 lean_object* l_Lean_Expr_eq_x3f(lean_object*);
@@ -75,6 +74,7 @@ lean_object* l_Lean_Meta_mkEqRec___closed__1;
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkEqNDRec(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_iff_x3f___closed__1;
+extern lean_object* l_Lean_mkRecFor___closed__1;
 lean_object* l_Lean_Meta_mkEqTrans___closed__2;
 lean_object* l_Lean_Meta_mkCongrFun___closed__1;
 lean_object* l_Lean_mkLambda(lean_object*, uint8_t, lean_object*, lean_object*);
@@ -7770,17 +7770,9 @@ return x_210;
 lean_object* _init_l_Lean_Meta_mkEqRec___closed__1() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("rec");
-return x_1;
-}
-}
-lean_object* _init_l_Lean_Meta_mkEqRec___closed__2() {
-_start:
-{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Expr_eq_x3f___closed__2;
-x_2 = l_Lean_Meta_mkEqRec___closed__1;
+x_2 = l_Lean_mkRecFor___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@@ -7834,7 +7826,7 @@ lean_ctor_set(x_20, 2, x_17);
 lean_ctor_set(x_20, 3, x_19);
 x_21 = l_Lean_mkOptionalNode___closed__2;
 x_22 = lean_array_push(x_21, x_3);
-x_23 = l_Lean_Meta_mkEqRec___closed__2;
+x_23 = l_Lean_Meta_mkEqRec___closed__1;
 x_24 = l_Lean_Meta_mkEqSymm___closed__3;
 x_25 = lean_alloc_ctor(16, 4, 0);
 lean_ctor_set(x_25, 0, x_23);
@@ -7924,7 +7916,7 @@ lean_ctor_set(x_65, 1, x_64);
 x_66 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_66, 0, x_63);
 lean_ctor_set(x_66, 1, x_65);
-x_67 = l_Lean_Meta_mkEqRec___closed__2;
+x_67 = l_Lean_Meta_mkEqRec___closed__1;
 x_68 = l_Lean_mkConst(x_67, x_66);
 x_69 = l_Lean_Meta_mkEqNDRec___closed__4;
 x_70 = lean_array_push(x_69, x_31);
@@ -8009,7 +8001,7 @@ lean_ctor_set(x_53, 2, x_50);
 lean_ctor_set(x_53, 3, x_52);
 x_54 = l_Lean_mkOptionalNode___closed__2;
 x_55 = lean_array_push(x_54, x_1);
-x_56 = l_Lean_Meta_mkEqRec___closed__2;
+x_56 = l_Lean_Meta_mkEqRec___closed__1;
 x_57 = l_Lean_Meta_mkEqNDRec___closed__3;
 x_58 = lean_alloc_ctor(16, 4, 0);
 lean_ctor_set(x_58, 0, x_56);
@@ -8112,7 +8104,7 @@ lean_ctor_set(x_108, 1, x_107);
 x_109 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_109, 0, x_106);
 lean_ctor_set(x_109, 1, x_108);
-x_110 = l_Lean_Meta_mkEqRec___closed__2;
+x_110 = l_Lean_Meta_mkEqRec___closed__1;
 x_111 = l_Lean_mkConst(x_110, x_109);
 x_112 = l_Lean_Meta_mkEqNDRec___closed__4;
 x_113 = lean_array_push(x_112, x_31);
@@ -8195,7 +8187,7 @@ lean_ctor_set(x_96, 2, x_93);
 lean_ctor_set(x_96, 3, x_95);
 x_97 = l_Lean_mkOptionalNode___closed__2;
 x_98 = lean_array_push(x_97, x_1);
-x_99 = l_Lean_Meta_mkEqRec___closed__2;
+x_99 = l_Lean_Meta_mkEqRec___closed__1;
 x_100 = l_Lean_Meta_mkEqNDRec___closed__3;
 x_101 = lean_alloc_ctor(16, 4, 0);
 lean_ctor_set(x_101, 0, x_99);
@@ -8314,7 +8306,7 @@ lean_ctor_set(x_142, 2, x_139);
 lean_ctor_set(x_142, 3, x_141);
 x_143 = l_Lean_mkOptionalNode___closed__2;
 x_144 = lean_array_push(x_143, x_3);
-x_145 = l_Lean_Meta_mkEqRec___closed__2;
+x_145 = l_Lean_Meta_mkEqRec___closed__1;
 x_146 = l_Lean_Meta_mkEqSymm___closed__3;
 x_147 = lean_alloc_ctor(16, 4, 0);
 lean_ctor_set(x_147, 0, x_145);
@@ -8410,7 +8402,7 @@ lean_ctor_set(x_188, 1, x_187);
 x_189 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_189, 0, x_186);
 lean_ctor_set(x_189, 1, x_188);
-x_190 = l_Lean_Meta_mkEqRec___closed__2;
+x_190 = l_Lean_Meta_mkEqRec___closed__1;
 x_191 = l_Lean_mkConst(x_190, x_189);
 x_192 = l_Lean_Meta_mkEqNDRec___closed__4;
 x_193 = lean_array_push(x_192, x_154);
@@ -8500,7 +8492,7 @@ lean_ctor_set(x_176, 2, x_173);
 lean_ctor_set(x_176, 3, x_175);
 x_177 = l_Lean_mkOptionalNode___closed__2;
 x_178 = lean_array_push(x_177, x_1);
-x_179 = l_Lean_Meta_mkEqRec___closed__2;
+x_179 = l_Lean_Meta_mkEqRec___closed__1;
 x_180 = l_Lean_Meta_mkEqNDRec___closed__3;
 x_181 = lean_alloc_ctor(16, 4, 0);
 lean_ctor_set(x_181, 0, x_179);
@@ -8771,8 +8763,6 @@ l_Lean_Meta_mkEqNDRec___closed__4 = _init_l_Lean_Meta_mkEqNDRec___closed__4();
 lean_mark_persistent(l_Lean_Meta_mkEqNDRec___closed__4);
 l_Lean_Meta_mkEqRec___closed__1 = _init_l_Lean_Meta_mkEqRec___closed__1();
 lean_mark_persistent(l_Lean_Meta_mkEqRec___closed__1);
-l_Lean_Meta_mkEqRec___closed__2 = _init_l_Lean_Meta_mkEqRec___closed__2();
-lean_mark_persistent(l_Lean_Meta_mkEqRec___closed__2);
 l_Lean_Meta_mkEqMP___closed__1 = _init_l_Lean_Meta_mkEqMP___closed__1();
 lean_mark_persistent(l_Lean_Meta_mkEqMP___closed__1);
 l_Lean_Meta_mkEqMP___closed__2 = _init_l_Lean_Meta_mkEqMP___closed__2();

stage0/stdlib/Init/Lean/Meta/Basic.c

@@ -142,6 +142,7 @@ lean_object* l_Lean_Meta_shouldReduceAll(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_isClass(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstance___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_run___rarg___closed__5;
 lean_object* l_Lean_Meta_throwEx___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_dbgTrace___rarg___closed__1;
 lean_object* l_Lean_Meta_mkMetaExtension(lean_object*);
@@ -203,18 +204,19 @@ lean_object* l_Lean_Meta_metaExt___closed__2;
 lean_object* l_Lean_Meta_savingCache___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_inferTypeRef;
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_isClassExpensive___main___spec__5___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_run___rarg___closed__3;
 uint8_t l_Lean_Meta_TransparencyMode_Inhabited;
 lean_object* l_Lean_Meta_throwEx(lean_object*);
 size_t l_Lean_Expr_hash(lean_object*);
 lean_object* l_Lean_Meta_isReadOnlyExprMVar(lean_object*, lean_object*, lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_metaExt___closed__1;
+lean_object* l_Lean_Meta_run___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_pure___at_Lean_Meta_MetaExtState_inhabited___spec__1(lean_object*);
 lean_object* l_Lean_Meta_InfoCacheKey_HasBeq___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_setMVarKind(lean_object*, uint8_t, lean_object*, lean_object*);
 extern lean_object* l_PersistentArray_empty___closed__3;
 uint8_t l_Array_isEqvAux___main___at_Lean_Meta_withLocalContext___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_IO_runMeta___rarg___closed__3;
 lean_object* l_Lean_Meta_lambdaMetaTelescope(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_addContext(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkSynthPendingRef___closed__1;
@@ -223,6 +225,7 @@ lean_object* l_Lean_Meta_TransparencyMode_HasBeq___closed__1;
 lean_object* l_Lean_Meta_withNewLocalInstances(lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main(lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_8__lambdaMetaTelescopeAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Options_empty;
 extern lean_object* l_IO_Error_Inhabited___closed__1;
 lean_object* l_Lean_Meta_approxDefEq___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withAtLeastTransparency___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -231,6 +234,7 @@ lean_object* l_Lean_Meta_MetaExtState_inhabited___lambda__2___boxed(lean_object*
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescopeReducing___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Meta_TransparencyMode_beq(uint8_t, uint8_t);
 extern lean_object* l___private_Init_Lean_Environment_5__envExtensionsRef;
+lean_object* l_Lean_Meta_run___rarg___closed__2;
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_isClassExpensive___main___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_assignLevelMVar(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -252,11 +256,11 @@ lean_object* l___private_Init_Lean_Meta_Basic_4__forallTelescopeReducingAuxAux__
 lean_object* l_Lean_Meta_forallMetaTelescopeReducing___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescopeReducing___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkFVar(lean_object*);
+lean_object* l_Lean_Meta_run___rarg___closed__4;
 uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
 lean_object* l_Lean_Meta_liftStateMCtx___rarg(lean_object*, lean_object*, lean_object*);
 size_t lean_usize_of_nat(lean_object*);
 lean_object* l_Lean_Meta_mkMetaExtension___lambda__1(lean_object*, lean_object*);
-lean_object* l_IO_runMeta___rarg___closed__4;
 lean_object* l_Lean_Meta_withLocalDecl___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescopeReducing___spec__4___rarg___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_isClassExpensive___main___spec__5(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -266,6 +270,7 @@ lean_object* l_Lean_Meta_getMVarDecl___boxed(lean_object*, lean_object*, lean_ob
 lean_object* l___private_Init_Lean_Meta_Basic_4__forallTelescopeReducingAuxAux___main___at_Lean_Meta_forallTelescope___spec__1(lean_object*);
 lean_object* l_Lean_Meta_getMCtx___boxed(lean_object*);
 lean_object* l_Lean_Meta_isClassQuick(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_run(lean_object*);
 lean_object* l_IO_runMeta(lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallBoundedTelescope___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_forallMetaTelescopeReducing(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
@@ -279,9 +284,7 @@ lean_object* lean_local_ctx_mk_local_decl(lean_object*, lean_object*, lean_objec
 lean_object* l_Lean_Meta_mkIsExprDefEqAuxRef___lambda__1___closed__1;
 lean_object* l___private_Init_Lean_Meta_Basic_6__lambdaTelescopeAux___main(lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_PersistentHashMap_empty___at_IO_runMeta___spec__1;
 lean_object* l_Lean_Meta_withIncRecDepth(lean_object*);
-lean_object* l_IO_runMeta___rarg___closed__1;
 lean_object* l_Lean_Meta_assignExprMVar(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkIsExprDefEqAuxRef___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescopeReducing___spec__5(lean_object*);
@@ -291,6 +294,7 @@ lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallBound
 lean_object* l_Lean_Meta_mkIsExprDefEqAuxRef___closed__1;
 lean_object* l___private_Init_Lean_Meta_Basic_4__forallTelescopeReducingAuxAux___main___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_hasAssignableMVar(lean_object*, lean_object*, lean_object*);
+lean_object* l_PersistentHashMap_empty___at_Lean_Meta_run___spec__1___closed__1;
 lean_object* l_Lean_Meta_mkIsExprDefEqAuxRef___lambda__1___closed__2;
 lean_object* l_Lean_Meta_withNewLocalInstances___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_ParamInfo_inhabited;
@@ -313,7 +317,6 @@ lean_object* l_Lean_Meta_synthPendingRef;
 lean_object* l_Lean_Meta_getConstAux(lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* lean_metavar_ctx_assign_level(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_throwEx___rarg___boxed(lean_object*, lean_object*, lean_object*);
-lean_object* l_IO_runMeta___rarg___closed__2;
 lean_object* l_Lean_Meta_elimMVarDeps___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withMVarContext___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_1__whenDebugging___rarg(lean_object*, lean_object*, lean_object*);
@@ -348,7 +351,6 @@ lean_object* lean_metavar_ctx_find_decl(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_dbgTrace(lean_object*);
 lean_object* l_Lean_Meta_mkFreshId(lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_8__lambdaMetaTelescopeAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_PersistentHashMap_empty___at_IO_runMeta___spec__1___closed__1;
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_TransparencyMode_beq___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_metaExt___elambda__1(lean_object*);
@@ -357,6 +359,7 @@ lean_object* l___private_Init_Lean_Meta_Basic_4__forallTelescopeReducingAuxAux__
 extern lean_object* l_Lean_TraceState_Inhabited___closed__1;
 lean_object* l_Lean_Meta_inferType(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_instantiateMVars___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_PersistentHashMap_empty___at_Lean_Meta_run___spec__1;
 lean_object* lean_io_ref_set(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_5__forallTelescopeReducingAux___at_Lean_Meta_forallBoundedTelescope___spec__1(lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallBoundedTelescope___spec__4(lean_object*);
@@ -397,6 +400,7 @@ lean_object* l___private_Init_Lean_Meta_Basic_3__liftMkBindingM(lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__3(lean_object*);
 lean_object* l_Lean_Meta_mkMetaExtension___closed__3;
 lean_object* l_Lean_Meta_isClassQuick___main___closed__1;
+lean_object* l_Lean_Meta_run___rarg___closed__1;
 uint8_t l_Lean_LocalInstance_beq(lean_object*, lean_object*);
 lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Meta_mkMetaExtension___spec__1___closed__2;
 lean_object* l_Lean_Meta_resettingSynthInstanceCache___rarg___closed__1;
@@ -47834,7 +47838,7 @@ x_3 = l_Lean_registerTraceClass(x_2, x_1);
 return x_3;
 }
 }
-lean_object* _init_l_PersistentHashMap_empty___at_IO_runMeta___spec__1___closed__1() {
+lean_object* _init_l_PersistentHashMap_empty___at_Lean_Meta_run___spec__1___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
@@ -47846,15 +47850,34 @@ lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_PersistentHashMap_empty___at_IO_runMeta___spec__1() {
+lean_object* _init_l_PersistentHashMap_empty___at_Lean_Meta_run___spec__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_PersistentHashMap_empty___at_IO_runMeta___spec__1___closed__1;
+x_1 = l_PersistentHashMap_empty___at_Lean_Meta_run___spec__1___closed__1;
 return x_1;
 }
 }
-lean_object* _init_l_IO_runMeta___rarg___closed__1() {
+lean_object* _init_l_Lean_Meta_run___rarg___closed__1() {
+_start:
+{
+lean_object* x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4; 
+x_1 = l_Lean_Options_empty;
+x_2 = 0;
+x_3 = 1;
+x_4 = lean_alloc_ctor(0, 1, 7);
+lean_ctor_set(x_4, 0, x_1);
+lean_ctor_set_uint8(x_4, sizeof(void*)*1, x_2);
+lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 1, x_2);
+lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 2, x_2);
+lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 3, x_2);
+lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 4, x_2);
+lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 5, x_2);
+lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 6, x_3);
+return x_4;
+}
+}
+lean_object* _init_l_Lean_Meta_run___rarg___closed__2() {
 _start:
 {
 lean_object* x_1; 
@@ -47862,7 +47885,7 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Meta_InfoCacheKey_Hashable___boxed), 1,
 return x_1;
 }
 }
-lean_object* _init_l_IO_runMeta___rarg___closed__2() {
+lean_object* _init_l_Lean_Meta_run___rarg___closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -47870,7 +47893,7 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Meta_InfoCacheKey_HasBeq___boxed), 2, 0)
 return x_1;
 }
 }
-lean_object* _init_l_IO_runMeta___rarg___closed__3() {
+lean_object* _init_l_Lean_Meta_run___rarg___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
@@ -47882,12 +47905,12 @@ lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_IO_runMeta___rarg___closed__4() {
+lean_object* _init_l_Lean_Meta_run___rarg___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_PersistentHashMap_empty___at_IO_runMeta___spec__1;
-x_2 = l_IO_runMeta___rarg___closed__3;
+x_1 = l_PersistentHashMap_empty___at_Lean_Meta_run___spec__1;
+x_2 = l_Lean_Meta_run___rarg___closed__4;
 x_3 = l_Lean_Meta_resettingSynthInstanceCache___rarg___closed__1;
 x_4 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
@@ -47896,6 +47919,63 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
+lean_object* l_Lean_Meta_run___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
+x_4 = l_Lean_Meta_run___rarg___closed__1;
+x_5 = l_Lean_LocalContext_Inhabited___closed__2;
+x_6 = l_Array_empty___closed__1;
+x_7 = lean_unsigned_to_nat(0u);
+x_8 = lean_alloc_ctor(0, 5, 0);
+lean_ctor_set(x_8, 0, x_4);
+lean_ctor_set(x_8, 1, x_5);
+lean_ctor_set(x_8, 2, x_6);
+lean_ctor_set(x_8, 3, x_7);
+lean_ctor_set(x_8, 4, x_3);
+x_9 = l_Lean_MetavarContext_Inhabited___closed__1;
+x_10 = l_Lean_Meta_run___rarg___closed__5;
+x_11 = l_Lean_NameGenerator_Inhabited___closed__3;
+x_12 = l_Lean_TraceState_Inhabited___closed__1;
+x_13 = l_PersistentArray_empty___closed__3;
+x_14 = lean_alloc_ctor(0, 6, 0);
+lean_ctor_set(x_14, 0, x_1);
+lean_ctor_set(x_14, 1, x_9);
+lean_ctor_set(x_14, 2, x_10);
+lean_ctor_set(x_14, 3, x_11);
+lean_ctor_set(x_14, 4, x_12);
+lean_ctor_set(x_14, 5, x_13);
+x_15 = lean_apply_2(x_2, x_8, x_14);
+if (lean_obj_tag(x_15) == 0)
+{
+lean_object* x_16; lean_object* x_17; 
+x_16 = lean_ctor_get(x_15, 0);
+lean_inc(x_16);
+lean_dec(x_15);
+x_17 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_17, 0, x_16);
+return x_17;
+}
+else
+{
+lean_object* x_18; lean_object* x_19; 
+x_18 = lean_ctor_get(x_15, 0);
+lean_inc(x_18);
+lean_dec(x_15);
+x_19 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_19, 0, x_18);
+return x_19;
+}
+}
+}
+lean_object* l_Lean_Meta_run(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Meta_run___rarg), 3, 0);
+return x_2;
+}
+}
 lean_object* l_IO_runMeta___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
@@ -47911,7 +47991,7 @@ lean_ctor_set(x_9, 2, x_6);
 lean_ctor_set(x_9, 3, x_7);
 lean_ctor_set(x_9, 4, x_8);
 x_10 = l_Lean_MetavarContext_Inhabited___closed__1;
-x_11 = l_IO_runMeta___rarg___closed__4;
+x_11 = l_Lean_Meta_run___rarg___closed__5;
 x_12 = l_Lean_NameGenerator_Inhabited___closed__3;
 x_13 = l_Lean_TraceState_Inhabited___closed__1;
 x_14 = l_PersistentArray_empty___closed__3;
@@ -48162,18 +48242,20 @@ lean_mark_persistent(l___private_Init_Lean_Meta_Basic_10__regTraceClasses___clos
 res = l___private_Init_Lean_Meta_Basic_10__regTraceClasses(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-l_PersistentHashMap_empty___at_IO_runMeta___spec__1___closed__1 = _init_l_PersistentHashMap_empty___at_IO_runMeta___spec__1___closed__1();
-lean_mark_persistent(l_PersistentHashMap_empty___at_IO_runMeta___spec__1___closed__1);
-l_PersistentHashMap_empty___at_IO_runMeta___spec__1 = _init_l_PersistentHashMap_empty___at_IO_runMeta___spec__1();
-lean_mark_persistent(l_PersistentHashMap_empty___at_IO_runMeta___spec__1);
-l_IO_runMeta___rarg___closed__1 = _init_l_IO_runMeta___rarg___closed__1();
-lean_mark_persistent(l_IO_runMeta___rarg___closed__1);
-l_IO_runMeta___rarg___closed__2 = _init_l_IO_runMeta___rarg___closed__2();
-lean_mark_persistent(l_IO_runMeta___rarg___closed__2);
-l_IO_runMeta___rarg___closed__3 = _init_l_IO_runMeta___rarg___closed__3();
-lean_mark_persistent(l_IO_runMeta___rarg___closed__3);
-l_IO_runMeta___rarg___closed__4 = _init_l_IO_runMeta___rarg___closed__4();
-lean_mark_persistent(l_IO_runMeta___rarg___closed__4);
+l_PersistentHashMap_empty___at_Lean_Meta_run___spec__1___closed__1 = _init_l_PersistentHashMap_empty___at_Lean_Meta_run___spec__1___closed__1();
+lean_mark_persistent(l_PersistentHashMap_empty___at_Lean_Meta_run___spec__1___closed__1);
+l_PersistentHashMap_empty___at_Lean_Meta_run___spec__1 = _init_l_PersistentHashMap_empty___at_Lean_Meta_run___spec__1();
+lean_mark_persistent(l_PersistentHashMap_empty___at_Lean_Meta_run___spec__1);
+l_Lean_Meta_run___rarg___closed__1 = _init_l_Lean_Meta_run___rarg___closed__1();
+lean_mark_persistent(l_Lean_Meta_run___rarg___closed__1);
+l_Lean_Meta_run___rarg___closed__2 = _init_l_Lean_Meta_run___rarg___closed__2();
+lean_mark_persistent(l_Lean_Meta_run___rarg___closed__2);
+l_Lean_Meta_run___rarg___closed__3 = _init_l_Lean_Meta_run___rarg___closed__3();
+lean_mark_persistent(l_Lean_Meta_run___rarg___closed__3);
+l_Lean_Meta_run___rarg___closed__4 = _init_l_Lean_Meta_run___rarg___closed__4();
+lean_mark_persistent(l_Lean_Meta_run___rarg___closed__4);
+l_Lean_Meta_run___rarg___closed__5 = _init_l_Lean_Meta_run___rarg___closed__5();
+lean_mark_persistent(l_Lean_Meta_run___rarg___closed__5);
 return lean_mk_io_result(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Init/Lean/Meta/Instances.c

@@ -61,6 +61,7 @@ lean_object* l_Lean_Environment_getGlobalInstances___boxed(lean_object*);
 lean_object* l_Lean_Meta_mkInstanceExtension___closed__5;
 lean_object* lean_add_instance(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_LocalContext_Inhabited___closed__2;
+extern lean_object* l_Lean_Meta_run___rarg___closed__5;
 lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkInstanceExtension___closed__3;
 lean_object* l_Lean_Meta_instanceExtension___closed__5;
@@ -92,7 +93,6 @@ lean_object* l_Lean_Meta_getGlobalInstances___rarg(lean_object*);
 extern lean_object* l_PersistentArray_empty___closed__3;
 lean_object* l_Lean_Meta_instanceExtension___elambda__1(lean_object*);
 lean_object* l_Lean_Meta_addGlobalInstance___closed__1;
-extern lean_object* l_Lean_Options_empty;
 extern lean_object* l_IO_Error_Inhabited___closed__1;
 extern lean_object* l___private_Init_Lean_Environment_5__envExtensionsRef;
 lean_object* l_Lean_registerBuiltinAttribute(lean_object*, lean_object*);
@@ -102,9 +102,7 @@ size_t l_USize_mul(size_t, size_t);
 lean_object* l_PersistentHashMap_find_x3f___at_Lean_Meta_addInstanceEntry___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_instanceExtension___closed__1;
 lean_object* l_Lean_Meta_instanceExtension___closed__2;
-extern lean_object* l_IO_runMeta___rarg___closed__4;
 lean_object* l_Lean_Meta_registerInstanceAttr___lambda__1___closed__2;
-lean_object* l_Lean_Meta_addGlobalInstance___closed__4;
 lean_object* lean_add_instance_old(lean_object*, lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
 size_t l_USize_land(size_t, size_t);
@@ -159,6 +157,7 @@ extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed_
 lean_object* l_Lean_Meta_DiscrTree_insertCore___at_Lean_Meta_addInstanceEntry___spec__1___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_MetavarContext_Inhabited___closed__1;
 lean_object* l_Lean_Meta_mkInstanceExtension___closed__2;
+extern lean_object* l_Lean_Meta_run___rarg___closed__1;
 lean_object* l_Lean_Meta_instanceExtension___elambda__3(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkInstanceExtension___closed__4;
 lean_object* l_Lean_Meta_getGlobalInstances___boxed(lean_object*);
@@ -3212,27 +3211,8 @@ return x_2;
 lean_object* _init_l_Lean_Meta_addGlobalInstance___closed__3() {
 _start:
 {
-lean_object* x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4; 
-x_1 = l_Lean_Options_empty;
-x_2 = 0;
-x_3 = 1;
-x_4 = lean_alloc_ctor(0, 1, 7);
-lean_ctor_set(x_4, 0, x_1);
-lean_ctor_set_uint8(x_4, sizeof(void*)*1, x_2);
-lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 1, x_2);
-lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 2, x_2);
-lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 3, x_2);
-lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 4, x_2);
-lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 5, x_2);
-lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 6, x_3);
-return x_4;
-}
-}
-lean_object* _init_l_Lean_Meta_addGlobalInstance___closed__4() {
-_start:
-{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_1 = l_Lean_Meta_addGlobalInstance___closed__3;
+x_1 = l_Lean_Meta_run___rarg___closed__1;
 x_2 = l_Lean_LocalContext_Inhabited___closed__2;
 x_3 = l_Array_empty___closed__1;
 x_4 = lean_unsigned_to_nat(0u);
@@ -3275,7 +3255,7 @@ lean_dec(x_7);
 x_9 = l_List_map___main___at_Lean_Meta_addGlobalInstance___spec__1(x_8);
 x_10 = l_Lean_mkConst(x_2, x_9);
 x_11 = l_Lean_MetavarContext_Inhabited___closed__1;
-x_12 = l_IO_runMeta___rarg___closed__4;
+x_12 = l_Lean_Meta_run___rarg___closed__5;
 x_13 = l_Lean_NameGenerator_Inhabited___closed__3;
 x_14 = l_Lean_TraceState_Inhabited___closed__1;
 x_15 = l_PersistentArray_empty___closed__3;
@@ -3286,7 +3266,7 @@ lean_ctor_set(x_16, 2, x_12);
 lean_ctor_set(x_16, 3, x_13);
 lean_ctor_set(x_16, 4, x_14);
 lean_ctor_set(x_16, 5, x_15);
-x_17 = l_Lean_Meta_addGlobalInstance___closed__4;
+x_17 = l_Lean_Meta_addGlobalInstance___closed__3;
 lean_inc(x_10);
 x_18 = l___private_Init_Lean_Meta_Instances_1__mkInstanceKey(x_10, x_17, x_16);
 if (lean_obj_tag(x_18) == 0)
@@ -3646,8 +3626,6 @@ l_Lean_Meta_addGlobalInstance___closed__2 = _init_l_Lean_Meta_addGlobalInstance_
 lean_mark_persistent(l_Lean_Meta_addGlobalInstance___closed__2);
 l_Lean_Meta_addGlobalInstance___closed__3 = _init_l_Lean_Meta_addGlobalInstance___closed__3();
 lean_mark_persistent(l_Lean_Meta_addGlobalInstance___closed__3);
-l_Lean_Meta_addGlobalInstance___closed__4 = _init_l_Lean_Meta_addGlobalInstance___closed__4();
-lean_mark_persistent(l_Lean_Meta_addGlobalInstance___closed__4);
 l_Lean_Meta_registerInstanceAttr___lambda__1___closed__1 = _init_l_Lean_Meta_registerInstanceAttr___lambda__1___closed__1();
 lean_mark_persistent(l_Lean_Meta_registerInstanceAttr___lambda__1___closed__1);
 l_Lean_Meta_registerInstanceAttr___lambda__1___closed__2 = _init_l_Lean_Meta_registerInstanceAttr___lambda__1___closed__2();

stage0/stdlib/Init/Lean/Meta/Message.c

@@ -65,6 +65,7 @@ lean_object* l_Lean_Meta_Exception_toMessageData___closed__45;
 extern lean_object* l_Lean_LocalContext_Inhabited___closed__2;
 lean_object* l_Lean_Meta_Exception_mkAppTypeMismatchMessage___closed__11;
 lean_object* l___private_Init_Lean_Meta_Message_4__whnf_x3f(lean_object*, lean_object*);
+extern lean_object* l_Lean_Meta_run___rarg___closed__5;
 lean_object* l_Lean_Meta_Exception_toMessageData___closed__8;
 lean_object* l_Lean_KernelException_toMessageData___closed__6;
 lean_object* l_Lean_Meta_Exception_toMessageData___closed__17;
@@ -120,7 +121,6 @@ lean_object* l_Lean_Meta_Exception_toMessageData___closed__25;
 lean_object* l_Lean_Meta_whnf(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_Message_4__whnf_x3f___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_KernelException_toMessageData___closed__3;
-extern lean_object* l_IO_runMeta___rarg___closed__4;
 lean_object* l_Lean_KernelException_toMessageData___closed__40;
 lean_object* l_Lean_KernelException_toMessageData___closed__9;
 lean_object* l_Lean_Meta_Exception_toMessageData___closed__3;
@@ -176,6 +176,7 @@ lean_object* l_Lean_KernelException_toMessageData___closed__13;
 lean_object* l_Lean_Meta_Exception_mkAppTypeMismatchMessage___closed__3;
 lean_object* l___private_Init_Lean_Meta_Message_1__run_x3f___rarg(lean_object*, lean_object*);
 extern lean_object* l_Lean_MetavarContext_Inhabited___closed__1;
+extern lean_object* l_Lean_Meta_run___rarg___closed__1;
 extern lean_object* l_Lean_Meta_Exception_toStr___closed__15;
 lean_object* l_Lean_Meta_Exception_toMessageData___closed__18;
 lean_object* l_Lean_Meta_Exception_toMessageData___closed__30;
@@ -193,7 +194,6 @@ lean_object* l_Lean_mkConst(lean_object*, lean_object*);
 lean_object* l_PersistentArray_forMAux___main___at_Lean_Meta_MetaHasEval___spec__4(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_Exception_toMessageData___closed__15;
 lean_object* l_Lean_Meta_Exception_toMessageData___closed__16;
-lean_object* l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__4;
 lean_object* l_Lean_KernelException_toMessageData___closed__11;
 extern lean_object* l_Lean_NameGenerator_Inhabited___closed__3;
 lean_object* l_Lean_Meta_Exception_toMessageData___closed__20;
@@ -218,45 +218,26 @@ return x_5;
 lean_object* _init_l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__1() {
 _start:
 {
-lean_object* x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4; 
-x_1 = l_Lean_Options_empty;
-x_2 = 0;
-x_3 = 1;
-x_4 = lean_alloc_ctor(0, 1, 7);
-lean_ctor_set(x_4, 0, x_1);
-lean_ctor_set_uint8(x_4, sizeof(void*)*1, x_2);
-lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 1, x_2);
-lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 2, x_2);
-lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 3, x_2);
-lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 4, x_2);
-lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 5, x_2);
-lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 6, x_3);
-return x_4;
+lean_object* x_1; 
+x_1 = lean_mk_string("_meta_exception");
+return x_1;
 }
 }
 lean_object* _init_l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__2() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("_meta_exception");
-return x_1;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
 }
 }
 lean_object* _init_l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = lean_box(0);
-x_2 = l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__2;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__4() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__3;
+x_1 = l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__2;
 x_2 = lean_unsigned_to_nat(1u);
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
@@ -273,7 +254,7 @@ x_4 = lean_ctor_get(x_1, 1);
 x_5 = lean_ctor_get(x_1, 2);
 x_6 = lean_ctor_get(x_1, 3);
 x_7 = l_Lean_getMaxRecDepth(x_6);
-x_8 = l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__1;
+x_8 = l_Lean_Meta_run___rarg___closed__1;
 x_9 = l_Array_empty___closed__1;
 x_10 = lean_unsigned_to_nat(0u);
 lean_inc(x_5);
@@ -283,8 +264,8 @@ lean_ctor_set(x_11, 1, x_5);
 lean_ctor_set(x_11, 2, x_9);
 lean_ctor_set(x_11, 3, x_10);
 lean_ctor_set(x_11, 4, x_7);
-x_12 = l_IO_runMeta___rarg___closed__4;
-x_13 = l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__4;
+x_12 = l_Lean_Meta_run___rarg___closed__5;
+x_13 = l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__3;
 x_14 = l_Lean_TraceState_Inhabited___closed__1;
 x_15 = l_PersistentArray_empty___closed__3;
 lean_inc(x_4);
@@ -2111,7 +2092,7 @@ lean_ctor_set(x_13, 2, x_11);
 lean_ctor_set(x_13, 3, x_12);
 lean_ctor_set(x_13, 4, x_9);
 x_14 = l_Lean_MetavarContext_Inhabited___closed__1;
-x_15 = l_IO_runMeta___rarg___closed__4;
+x_15 = l_Lean_Meta_run___rarg___closed__5;
 x_16 = l_Lean_NameGenerator_Inhabited___closed__3;
 x_17 = l_Lean_TraceState_Inhabited___closed__1;
 x_18 = l_PersistentArray_empty___closed__3;
@@ -3071,8 +3052,6 @@ l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__2 = _init_l___pri
 lean_mark_persistent(l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__2);
 l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__3 = _init_l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__3();
 lean_mark_persistent(l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__3);
-l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__4 = _init_l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__4();
-lean_mark_persistent(l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__4);
 l___private_Init_Lean_Meta_Message_3__inferDomain_x3f___lambda__1___closed__1 = _init_l___private_Init_Lean_Meta_Message_3__inferDomain_x3f___lambda__1___closed__1();
 lean_mark_persistent(l___private_Init_Lean_Meta_Message_3__inferDomain_x3f___lambda__1___closed__1);
 l___private_Init_Lean_Meta_Message_3__inferDomain_x3f___lambda__1___closed__2 = _init_l___private_Init_Lean_Meta_Message_3__inferDomain_x3f___lambda__1___closed__2();

stage0/stdlib/Init/Lean/Parser/Tactic.c

@@ -165,7 +165,6 @@ lean_object* l_Lean_Parser_Tactic_usingRec___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Tactic_inductionAlts___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_traceState___closed__5;
 extern lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__5;
-lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__10;
 lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_clear___closed__3;
 lean_object* l_Lean_Parser_Tactic_refine___elambda__1___closed__3;
@@ -179,7 +178,6 @@ lean_object* l_Lean_Parser_Tactic_case___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_case;
 lean_object* l_Lean_Parser_Tactic_traceState___closed__1;
 lean_object* l_Lean_Parser_Tactic_generalize___closed__9;
-extern lean_object* l_Lean_Parser_ident___closed__2;
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_generalizingVars___elambda__1(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__3;
@@ -6771,22 +6769,21 @@ return x_3;
 lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__3() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_ident;
-x_2 = lean_ctor_get(x_1, 0);
-lean_inc(x_2);
-x_3 = l_Lean_Parser_noFirstTokenInfo(x_2);
-return x_3;
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Parser_Tactic_ident_x27___closed__2;
+x_2 = lean_alloc_closure((void*)(l_Lean_Parser_manyFn), 3, 1);
+lean_closure_set(x_2, 0, x_1);
+return x_2;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__4() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Parser_ident___closed__2;
-x_2 = lean_alloc_closure((void*)(l_Lean_Parser_manyFn), 3, 1);
-lean_closure_set(x_2, 0, x_1);
-return x_2;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Tactic_intros___closed__2;
+x_2 = l_Lean_Parser_Term_fun___closed__2;
+x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
+return x_3;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__5() {
@@ -6794,16 +6791,6 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Tactic_inductionAlt___closed__3;
-x_2 = l_Lean_Parser_Term_fun___closed__2;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__6() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_inductionAlt___closed__4;
 x_2 = l_Lean_Parser_Term_matchAlt___closed__7;
 x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
 lean_closure_set(x_3, 0, x_1);
@@ -6811,49 +6798,49 @@ lean_closure_set(x_3, 1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__7() {
+lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Parser_ident;
+x_1 = l_Lean_Parser_Tactic_ident_x27;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Parser_Tactic_inductionAlt___closed__5;
+x_3 = l_Lean_Parser_Tactic_inductionAlt___closed__4;
 x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
 return x_4;
 }
 }
-lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__8() {
+lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__7() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_ident___closed__2;
-x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__6;
+x_1 = l_Lean_Parser_Tactic_ident_x27___closed__2;
+x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__5;
 x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 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_Parser_Tactic_inductionAlt___closed__9() {
+lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__8() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_inductionAlt___closed__7;
-x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__8;
+x_1 = l_Lean_Parser_Tactic_inductionAlt___closed__6;
+x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__7;
 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_Parser_Tactic_inductionAlt___closed__10() {
+lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__9() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_Lean_Parser_Tactic_inductionAlt___closed__1;
 x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__2;
-x_3 = l_Lean_Parser_Tactic_inductionAlt___closed__9;
+x_3 = l_Lean_Parser_Tactic_inductionAlt___closed__8;
 x_4 = l_Lean_Parser_nodeWithAntiquot(x_1, x_2, x_3);
 return x_4;
 }
@@ -6862,7 +6849,7 @@ lean_object* _init_l_Lean_Parser_Tactic_inductionAlt() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Tactic_inductionAlt___closed__10;
+x_1 = l_Lean_Parser_Tactic_inductionAlt___closed__9;
 return x_1;
 }
 }
@@ -12289,8 +12276,6 @@ l_Lean_Parser_Tactic_inductionAlt___closed__8 = _init_l_Lean_Parser_Tactic_induc
 lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt___closed__8);
 l_Lean_Parser_Tactic_inductionAlt___closed__9 = _init_l_Lean_Parser_Tactic_inductionAlt___closed__9();
 lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt___closed__9);
-l_Lean_Parser_Tactic_inductionAlt___closed__10 = _init_l_Lean_Parser_Tactic_inductionAlt___closed__10();
-lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt___closed__10);
 l_Lean_Parser_Tactic_inductionAlt = _init_l_Lean_Parser_Tactic_inductionAlt();
 lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt);
 l_Lean_Parser_Tactic_inductionAlts___closed__1 = _init_l_Lean_Parser_Tactic_inductionAlts___closed__1();