chore: update stage0

stage0/src/Lean/Elab/Inductive.lean

@@ -9,7 +9,7 @@ import Lean.Util.CollectLevelParams
 import Lean.Util.Constructions
 import Lean.Meta.CollectFVars
 import Lean.Meta.SizeOf
-import Lean.Meta.ProofBelow
+import Lean.Meta.IndPredBelow
 import Lean.Elab.Command
 import Lean.Elab.DefView
 import Lean.Elab.DeclUtil
@@ -518,7 +518,7 @@ def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
   runTermElabM view0.declName fun vars => withRef ref do
     mkInductiveDecl vars views
     mkSizeOfInstances view0.declName
-    mkProofBelow view0.declName
+    Lean.Meta.IndPredBelow.mkBelow view0.declName
   applyDerivingHandlers views
 
 end Lean.Elab.Command

stage0/src/Lean/Elab/Match.lean

@@ -778,7 +778,64 @@ private def getIndicesToInclude (discrs : Array Expr) (idx : Nat) : TermElabM (A
         result := result.push arg
     return result
 
-private partial def elabMatchAltViews (discrs : Array Expr) (matchType : Expr) (altViews : Array MatchAltView) : TermElabM (Array Expr × Expr × Array (AltLHS × Expr) × Bool) := do
+/--
+  "Generalize" variables that depend on the discriminants.
+
+  Remarks and limitations:
+  - If `matchType` is a proposition, then we generalize even when the user did not provide `(generalizing := true)`.
+    Motivation: users should have control about the actual `match`-expressions in their programs.
+  - We currently do not generalize let-decls.
+  - We abort generalization if the new `matchType` is type incorrect.
+  - Only discriminants that are free variables are considered during specialization.
+  - We "generalize" by adding new discriminants and pattern variables. We do not "clear" the generalized variables,
+    but they become inaccessible since they are shadowed by the patterns variables. We assume this is ok since
+    this is the exact behavior users would get if they had written it by hand. Recall there is no `clear` in term mode.
+-/
+private def generalize (discrs : Array Expr) (matchType : Expr) (altViews : Array MatchAltView) (generalizing? : Option Bool) : TermElabM (Array Expr × Expr × Array MatchAltView × Bool) := do
+  let gen ←
+    match generalizing? with
+    | some g => pure g
+    | _ => isProp matchType
+  if !gen then
+    return (discrs, matchType, altViews, false)
+  else
+    let ysFVarIds ← getFVarsToGeneralize discrs
+    /- let-decls are currently being ignored by the generalizer. -/
+    let ysFVarIds ← ysFVarIds.filterM fun fvarId => return !(← getLocalDecl fvarId).isLet
+    if ysFVarIds.isEmpty then
+      return (discrs, matchType, altViews, false)
+    else
+      let ys := ysFVarIds.map mkFVar
+      -- trace[Meta.debug] "ys: {ys}, discrs: {discrs}"
+      let matchType' ← forallBoundedTelescope matchType discrs.size fun ds type => do
+        let type ← mkForallFVars ys type
+        let (discrs', ds') := Array.unzip <| Array.zip discrs ds |>.filter fun (di, d) => di.isFVar
+        let type := type.replaceFVars discrs' ds'
+        mkForallFVars ds type
+      -- trace[Meta.debug] "matchType': {matchType'}"
+      if (← isTypeCorrect matchType') then
+        let discrs := discrs ++ ys
+        let altViews ← altViews.mapM fun altView => do
+          let patternVars ← getPatternsVars altView.patterns
+          -- We traverse backwards because we want to keep the most recent names.
+          -- For example, if `ys` contains `#[h, h]`, we want to make sure `mkFreshUsername is applied to the first `h`,
+          -- since it is already shadowed by the second.
+          let ysUserNames ← ys.foldrM (init := #[]) fun ys ysUserNames => do
+            let yDecl ← getLocalDecl ys.fvarId!
+            let mut yUserName := yDecl.userName
+            if ysUserNames.contains yUserName then
+              yUserName ← mkFreshUserName yUserName
+            -- Explicitly provided pattern variables shadow `y`
+            else if patternVars.any fun | PatternVar.localVar x => x == yUserName | _ => false then
+              yUserName ← mkFreshUserName yUserName
+            return ysUserNames.push yUserName
+          let ysIds ← ysUserNames.reverse.mapM fun n => return mkIdentFrom (← getRef) n
+          return { altView with patterns := altView.patterns ++ ysIds }
+        return (discrs, matchType', altViews, true)
+      else
+        return (discrs, matchType, altViews, true)
+
+private partial def elabMatchAltViews (generalizing? : Option Bool) (discrs : Array Expr) (matchType : Expr) (altViews : Array MatchAltView) : TermElabM (Array Expr × Expr × Array (AltLHS × Expr) × Bool) := do
   loop discrs matchType altViews none
 where
   /-
@@ -787,8 +844,9 @@ where
   loop (discrs : Array Expr) (matchType : Expr) (altViews : Array MatchAltView) (first? : Option (SavedState × Exception))
       : TermElabM (Array Expr × Expr × Array (AltLHS × Expr) × Bool) := do
     let s ← saveState
-    match ← altViews.mapM (fun alt => elabMatchAltView alt matchType) |>.run with
-    | Except.ok alts => return (discrs, matchType, alts, first?.isSome)
+    let (discrs', matchType', altViews', refined) ← generalize discrs matchType altViews generalizing?
+    match ← altViews'.mapM (fun altView => elabMatchAltView altView matchType') |>.run with
+    | Except.ok alts => return (discrs', matchType', alts, first?.isSome || refined)
     | Except.error { idx := idx, ex := ex } =>
       let indices ← getIndicesToInclude discrs idx
       if indices.isEmpty then
@@ -897,64 +955,6 @@ private def isMatchUnit? (altLHSS : List Match.AltLHS) (rhss : Array Expr) : Met
     | Expr.lam _ _ b _ => return if b.hasLooseBVars then none else b
     | _ => return none
   | _ => return none
-
-/--
-  "Generalize" variables that depend on the discriminants.
-
-  Remarks and limitations:
-  - If `matchType` is a proposition, then we generalize even when the user did not provide `(generalizing := true)`.
-    Motivation: users should have control about the actual `match`-expressions in their programs.
-  - We currently do not generalize let-decls.
-  - We abort generalization if the new `matchType` is type incorrect.
-  - Only discriminants that are free variables are considered during specialization.
-  - We "generalize" by adding new discriminants and pattern variables. We do not "clear" the generalized variables,
-    but they become inaccessible since they are shadowed by the patterns variables. We assume this is ok since
-    this is the exact behavior users would get if they had written it by hand. Recall there is no `clear` in term mode.
--/
-private def generalize (discrs : Array Expr) (matchType : Expr) (altViews : Array MatchAltView) (generalizing? : Option Bool) : TermElabM (Array Expr × Expr × Array MatchAltView × Bool) := do
-  let gen ←
-    match generalizing? with
-    | some g => pure g
-    | _ => isProp matchType
-  if !gen then
-    return (discrs, matchType, altViews, false)
-  else
-    let ysFVarIds ← getFVarsToGeneralize discrs
-    /- let-decls are currently being ignored by the generalizer. -/
-    let ysFVarIds ← ysFVarIds.filterM fun fvarId => return !(← getLocalDecl fvarId).isLet
-    if ysFVarIds.isEmpty then
-      return (discrs, matchType, altViews, false)
-    else
-      let ys := ysFVarIds.map mkFVar
-      -- trace[Meta.debug] "ys: {ys}, discrs: {discrs}"
-      let matchType' ← forallBoundedTelescope matchType discrs.size fun ds type => do
-        let type ← mkForallFVars ys type
-        let (discrs', ds') := Array.unzip <| Array.zip discrs ds |>.filter fun (di, d) => di.isFVar
-        let type := type.replaceFVars discrs' ds'
-        mkForallFVars ds type
-      -- trace[Meta.debug] "matchType': {matchType'}"
-      if (← isTypeCorrect matchType') then
-        let discrs := discrs ++ ys
-        let altViews ← altViews.mapM fun altView => do
-          let patternVars ← getPatternsVars altView.patterns
-          -- We traverse backwards because we want to keep the most recent names.
-          -- For example, if `ys` contains `#[h, h]`, we want to make sure `mkFreshUsername is applied to the first `h`,
-          -- since it is already shadowed by the second.
-          let ysUserNames ← ys.foldrM (init := #[]) fun ys ysUserNames => do
-            let yDecl ← getLocalDecl ys.fvarId!
-            let mut yUserName := yDecl.userName
-            if ysUserNames.contains yUserName then
-              yUserName ← mkFreshUserName yUserName
-            -- Explicitly provided pattern variables shadow `y`
-            else if patternVars.any fun | PatternVar.localVar x => x == yUserName | _ => false then
-              yUserName ← mkFreshUserName yUserName
-            return ysUserNames.push yUserName
-          let ysIds ← ysUserNames.reverse.mapM fun n => return mkIdentFrom (← getRef) n
-          return { altView with patterns := altView.patterns ++ ysIds }
-        return (discrs, matchType', altViews, true)
-      else
-        return (discrs, matchType, altViews, true)
-
 private def elabMatchAux (generalizing? : Option Bool) (discrStxs : Array Syntax) (altViews : Array MatchAltView) (matchOptType : Syntax) (expectedType : Expr)
     : TermElabM Expr := do
   let mut generalizing? := generalizing?
@@ -964,11 +964,9 @@ private def elabMatchAux (generalizing? : Option Bool) (discrStxs : Array Syntax
     generalizing? := some false
   let (discrs, matchType, altLHSS, isDep, rhss) ← commitIfDidNotPostpone do
     let ⟨discrs, matchType, isDep, altViews⟩ ← elabMatchTypeAndDiscrs discrStxs matchOptType altViews expectedType
-    let (discrs, matchType, altViews, gen) ← generalize discrs matchType altViews generalizing?
-    let isDep := isDep || gen
     let matchAlts ← liftMacroM <| expandMacrosInPatterns altViews
     trace[Elab.match] "matchType: {matchType}"
-    let (discrs, matchType, alts, refined) ← elabMatchAltViews discrs matchType matchAlts
+    let (discrs, matchType, alts, refined) ← elabMatchAltViews generalizing? discrs matchType matchAlts
     let isDep := isDep || refined
     /-
      We should not use `synthesizeSyntheticMVarsNoPostponing` here. Otherwise, we will not be

stage0/src/Lean/Meta.lean

@@ -29,7 +29,7 @@ import Lean.Meta.PPGoal
 import Lean.Meta.UnificationHint
 import Lean.Meta.Inductive
 import Lean.Meta.SizeOf
-import Lean.Meta.ProofBelow
+import Lean.Meta.IndPredBelow
 import Lean.Meta.Coe
 import Lean.Meta.SortLocalDecls
 import Lean.Meta.CollectFVars

stage0/src/Lean/Meta/IndPredBelow.lean

@@ -8,23 +8,21 @@ import Lean.Util.Constructions
 import Lean.Meta.Transform
 import Lean.Meta.Tactic
 
-namespace Lean.Meta
-
-namespace ProofBelow
+namespace Lean.Meta.IndPredBelow
 
 /--
-  The context used in the creation of the `ProofBelow` scheme for inductive predicates.
+  The context used in the creation of the `below` scheme for inductive predicates.
 -/  
 structure Context where
   motives : Array (Name × Expr)
   typeInfos : Array InductiveVal
-  proofBelowNames : Array Name
+  belowNames : Array Name
   headers : Array Expr
   numParams : Nat
 
 /--
   Collection of variables used to keep track of the positions of binders in the construction
-  of `ProofBelow` motives and constructors.
+  of `below` motives and constructors.
 -/
 structure Variables where
   target : Array Expr
@@ -57,7 +55,7 @@ def mkContext (declName : Name) : MetaM Context := do
     typeInfos := typeInfos
     numParams := indVal.numParams
     headers := ←headers
-    proofBelowNames := ←indVal.all.toArray.mapM (·.appendAfter "ProofBelow") }
+    belowNames := ←indVal.all.toArray.map (· ++ `below) }
 where 
   motiveName (motiveTypes : Array Expr) (i : Nat) : MetaM Name := 
     if motiveTypes.size > 1 
@@ -89,7 +87,7 @@ where
     
 partial def mkCtorType 
     (ctx : Context) 
-    (proofBelowIdx : Nat) 
+    (belowIdx : Nat) 
     (originalCtor : ConstructorVal) : MetaM Expr := 
   forallTelescope originalCtor.type fun xs t => addHeaderVars 
     { innerType := t
@@ -101,7 +99,7 @@ partial def mkCtorType
 where
   addHeaderVars (vars : Variables) := do
     let headersWithNames ← ctx.headers.mapIdxM fun idx header =>
-      (ctx.proofBelowNames[idx], fun _ => pure header)
+      (ctx.belowNames[idx], fun _ => pure header)
 
     withLocalDeclsD headersWithNames fun xs =>
       addMotives { vars with indVal := xs } 
@@ -118,7 +116,7 @@ where
       let binder := vars.args[i]
       let binderType ←inferType binder
       if ←checkCount binderType then
-        mkProofBelowBinder vars binder binderType fun indValIdx x =>
+        mkBelowBinder vars binder binderType fun indValIdx x =>
           mkMotiveBinder vars indValIdx binder binderType fun y =>
             modifyBinders { vars with target := vars.target ++ #[binder, x, y]} i.succ
       else modifyBinders { vars with target := vars.target.push binder } i.succ
@@ -130,7 +128,7 @@ where
         mkAppN 
           (mkConst originalCtor.name $ ctx.typeInfos[0].levelParams.map mkLevelParam)
           (vars.params ++ vars.args)
-      let innerType := mkAppN vars.indVal[proofBelowIdx] $
+      let innerType := mkAppN vars.indVal[belowIdx] $
         vars.params ++ vars.motives ++ args[ctx.numParams:] ++ #[hApp]
       let x ← mkForallFVars vars.target innerType 
       replaceTempVars vars x
@@ -139,7 +137,7 @@ where
     let levelParams := 
       ctx.typeInfos[0].levelParams.map mkLevelParam
 
-    ctor.replaceFVars vars.indVal $ ctx.proofBelowNames.map fun indVal =>
+    ctor.replaceFVars vars.indVal $ ctx.belowNames.map fun indVal =>
       mkConst indVal levelParams
   
   checkCount (domain : Expr) : MetaM Bool := do
@@ -156,7 +154,7 @@ where
     
     return cnt == 1
   
-  mkProofBelowBinder 
+  mkBelowBinder 
       (vars : Variables) 
       (binder : Expr) 
       (domain : Expr) 
@@ -200,7 +198,7 @@ where
 
 def mkConstructor (ctx : Context) (i : Nat) (ctor : Name) : MetaM Constructor := do
   let ctorInfo ← getConstInfoCtor ctor
-  let name := ctor.updatePrefix ctx.proofBelowNames[i]
+  let name := ctor.updatePrefix ctx.belowNames[i]
   let type ← mkCtorType ctx i ctorInfo
   return { 
     name := name
@@ -211,11 +209,11 @@ def mkInductiveType
     (i : Fin ctx.typeInfos.size) 
     (indVal : InductiveVal) : MetaM InductiveType := do
   return {
-    name := ctx.proofBelowNames[i]
+    name := ctx.belowNames[i]
     type := ctx.headers[i]
     ctors := ←indVal.ctors.mapM (mkConstructor ctx i) }
 
-def mkProofBelowDecl (ctx : Context) : MetaM Declaration := do
+def mkBelowDecl (ctx : Context) : MetaM Declaration := do
   let lparams := ctx.typeInfos[0].levelParams
   Declaration.inductDecl 
     lparams 
@@ -254,7 +252,7 @@ where
     let motives ← ctx.motives.mapIdxM fun idx (_, motive) => do
       let motive ← instantiateForall motive params
       forallTelescope motive fun xs _ => do
-      mkLambdaFVars xs $ mkAppN (mkConst ctx.proofBelowNames[idx] levelParams) $ (params ++ motives ++ xs)
+      mkLambdaFVars xs $ mkAppN (mkConst ctx.belowNames[idx] levelParams) $ (params ++ motives ++ xs)
     withMVarContext m do
     let recursorInfo ← getConstInfo $ mkRecName indVal.name
     let recLevels := 
@@ -267,11 +265,11 @@ where
   applyCtors (ms : List MVarId) : MetaM $ List MVarId := do
     let mss ← ms.toArray.mapIdxM fun idx m => do
       let m ← introNPRec m 
-      (←getMVarType m).withApp fun proofBelow args =>
+      (←getMVarType m).withApp fun below args =>
       args.back.withApp fun ctor args =>
-      let ctor := ctor.constName!.updatePrefix proofBelow.constName!
+      let ctor := ctor.constName!.updatePrefix below.constName!
       withMVarContext m do
-      let ctor := mkConst ctor proofBelow.constLevels!
+      let ctor := mkConst ctor below.constLevels!
       apply m ctor 
     return mss.foldr List.append []
 
@@ -334,32 +332,31 @@ where
         let args := params ++ motives ++ ys
         let premise :=
           mkAppN 
-            (mkConst ctx.proofBelowNames[idx.val] levels) args
+            (mkConst ctx.belowNames[idx.val] levels) args
         let conclusion :=
           mkAppN motives[idx] ys
         mkForallFVars ys (←mkArrow premise conclusion)
     (←name, mkDomain)
 
-end ProofBelow
 
-def mkProofBelow (declName : Name) : MetaM Unit := do
+def mkBelow (declName : Name) : MetaM Unit := do
   if (←isInductivePredicate declName) then
     let x ← getConstInfoInduct declName
     if x.isRec then
-      let ctx ← ProofBelow.mkContext declName
-      let decl ← ProofBelow.mkProofBelowDecl ctx
+      let ctx ← IndPredBelow.mkContext declName
+      let decl ← IndPredBelow.mkBelowDecl ctx
       addDecl decl
-      trace[Meta.ProofBelow] "added {ctx.proofBelowNames}"
-      ctx.proofBelowNames.forM Lean.mkCasesOn
+      trace[Meta.IndPredBelow] "added {ctx.belowNames}"
+      ctx.belowNames.forM Lean.mkCasesOn
       for i in [:ctx.typeInfos.size] do
         try
-          let decl ← ProofBelow.mkBrecOnDecl ctx i
+          let decl ← IndPredBelow.mkBrecOnDecl ctx i
           addDecl decl
-        catch e => trace[Meta.ProofBelow] "failed to prove brecOn for {ctx.proofBelowNames[i]}\n{e.toMessageData}"
-    else trace[Meta.ProofBelow] "Not recursive"
-  else trace[Meta.ProofBelow] "Not inductive predicate"
+        catch e => trace[Meta.IndPredBelow] "failed to prove brecOn for {ctx.belowNames[i]}\n{e.toMessageData}"
+    else trace[Meta.IndPredBelow] "Not recursive"
+  else trace[Meta.IndPredBelow] "Not inductive predicate"
 
 builtin_initialize
-  registerTraceClass `Meta.ProofBelow
+  registerTraceClass `Meta.IndPredBelow
 
-end Lean.Meta
+end Lean.Meta.IndPredBelow

stage0/stdlib/Lean/Elab/Inductive.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.Elab.Inductive
-// Imports: Init Lean.Util.ReplaceLevel Lean.Util.ReplaceExpr Lean.Util.CollectLevelParams Lean.Util.Constructions Lean.Meta.CollectFVars Lean.Meta.SizeOf Lean.Meta.ProofBelow Lean.Elab.Command Lean.Elab.DefView Lean.Elab.DeclUtil Lean.Elab.Deriving.Basic
+// Imports: Init Lean.Util.ReplaceLevel Lean.Util.ReplaceExpr Lean.Util.CollectLevelParams Lean.Util.Constructions Lean.Meta.CollectFVars Lean.Meta.SizeOf Lean.Meta.IndPredBelow Lean.Elab.Command Lean.Elab.DefView Lean.Elab.DeclUtil Lean.Elab.Deriving.Basic
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -16,7 +16,6 @@ extern "C" {
 lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_checkParamsAndResultType_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_checkParamsAndResultType___lambda__1___closed__4;
 lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors(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_mkProofBelow(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabHeaderAux___lambda__2___closed__1;
 lean_object* lean_expr_update_forall(lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* lean_array_set(lean_object*, lean_object*, lean_object*);
@@ -553,6 +552,7 @@ lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM_visit___at___private_Lean_El
 lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___lambda__1(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_Array_contains___at_Lean_Elab_Command_accLevelAtCtor___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_indentExpr(lean_object*);
+lean_object* l_Lean_Meta_IndPredBelow_mkBelow(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_shouldInferResultUniverse_match__1(lean_object*);
 lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_withInductiveLocalDecls_loop___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*, lean_object*);
 lean_object* l_Lean_Elab_Term_withAutoBoundImplicit___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -18563,7 +18563,7 @@ lean_object* x_19; lean_object* x_20;
 x_19 = lean_ctor_get(x_18, 1);
 lean_inc(x_19);
 lean_dec(x_18);
-x_20 = l_Lean_Meta_mkProofBelow(x_4, x_8, x_9, x_10, x_11, x_19);
+x_20 = l_Lean_Meta_IndPredBelow_mkBelow(x_4, x_8, x_9, x_10, x_11, x_19);
 return x_20;
 }
 else
@@ -18672,7 +18672,7 @@ lean_object* x_40; lean_object* x_41;
 x_40 = lean_ctor_get(x_39, 1);
 lean_inc(x_40);
 lean_dec(x_39);
-x_41 = l_Lean_Meta_mkProofBelow(x_4, x_8, x_9, x_36, x_11, x_40);
+x_41 = l_Lean_Meta_IndPredBelow_mkBelow(x_4, x_8, x_9, x_36, x_11, x_40);
 return x_41;
 }
 else
@@ -19076,7 +19076,7 @@ lean_object* initialize_Lean_Util_CollectLevelParams(lean_object*);
 lean_object* initialize_Lean_Util_Constructions(lean_object*);
 lean_object* initialize_Lean_Meta_CollectFVars(lean_object*);
 lean_object* initialize_Lean_Meta_SizeOf(lean_object*);
-lean_object* initialize_Lean_Meta_ProofBelow(lean_object*);
+lean_object* initialize_Lean_Meta_IndPredBelow(lean_object*);
 lean_object* initialize_Lean_Elab_Command(lean_object*);
 lean_object* initialize_Lean_Elab_DefView(lean_object*);
 lean_object* initialize_Lean_Elab_DeclUtil(lean_object*);
@@ -19107,7 +19107,7 @@ lean_dec_ref(res);
 res = initialize_Lean_Meta_SizeOf(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = initialize_Lean_Meta_ProofBelow(lean_io_mk_world());
+res = initialize_Lean_Meta_IndPredBelow(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 res = initialize_Lean_Elab_Command(lean_io_mk_world());

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

@@ -85,11 +85,11 @@ lean_object* l_Lean_Syntax_getHeadInfo(lean_object*);
 lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Util_0__Lean_Elab_expandMacro_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_7999____closed__1;
 lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTermAux___spec__2___closed__3;
 lean_object* l_List_forIn_loop___at_Lean_Elab_Tactic_evalEraseAuxDiscrs___spec__7___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_Syntax_setKind(lean_object*, lean_object*);
 lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
+extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_8556____closed__1;
 lean_object* l___regBuiltin_Lean_Elab_Tactic_evalEraseAuxDiscrs___closed__1;
 extern lean_object* l___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_sortFVarIds___closed__1;
 extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_19003____closed__5;
@@ -1593,7 +1593,7 @@ lean_dec(x_277);
 x_316 = lean_ctor_get(x_6, 0);
 lean_inc(x_316);
 lean_dec(x_6);
-x_317 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_7999____closed__1;
+x_317 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_8556____closed__1;
 x_318 = l_Lean_Name_appendIndexAfter(x_317, x_316);
 x_319 = l_Lean_Name_append(x_1, x_318);
 x_320 = l_Lean_mkIdentFrom(x_30, x_319);

stage0/stdlib/Lean/Meta.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.Meta
-// Imports: Init Lean.Meta.Basic Lean.Meta.LevelDefEq Lean.Meta.WHNF Lean.Meta.InferType Lean.Meta.FunInfo Lean.Meta.ExprDefEq Lean.Meta.DiscrTree Lean.Meta.Reduce Lean.Meta.Instances Lean.Meta.AbstractMVars Lean.Meta.SynthInstance Lean.Meta.AppBuilder Lean.Meta.Tactic Lean.Meta.KAbstract Lean.Meta.RecursorInfo Lean.Meta.GeneralizeTelescope Lean.Meta.Match Lean.Meta.ReduceEval Lean.Meta.Closure Lean.Meta.AbstractNestedProofs Lean.Meta.ForEachExpr Lean.Meta.Transform Lean.Meta.PPGoal Lean.Meta.UnificationHint Lean.Meta.Inductive Lean.Meta.SizeOf Lean.Meta.ProofBelow Lean.Meta.Coe Lean.Meta.SortLocalDecls Lean.Meta.CollectFVars Lean.Meta.GeneralizeVars
+// Imports: Init Lean.Meta.Basic Lean.Meta.LevelDefEq Lean.Meta.WHNF Lean.Meta.InferType Lean.Meta.FunInfo Lean.Meta.ExprDefEq Lean.Meta.DiscrTree Lean.Meta.Reduce Lean.Meta.Instances Lean.Meta.AbstractMVars Lean.Meta.SynthInstance Lean.Meta.AppBuilder Lean.Meta.Tactic Lean.Meta.KAbstract Lean.Meta.RecursorInfo Lean.Meta.GeneralizeTelescope Lean.Meta.Match Lean.Meta.ReduceEval Lean.Meta.Closure Lean.Meta.AbstractNestedProofs Lean.Meta.ForEachExpr Lean.Meta.Transform Lean.Meta.PPGoal Lean.Meta.UnificationHint Lean.Meta.Inductive Lean.Meta.SizeOf Lean.Meta.IndPredBelow Lean.Meta.Coe Lean.Meta.SortLocalDecls Lean.Meta.CollectFVars Lean.Meta.GeneralizeVars
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -40,7 +40,7 @@ lean_object* initialize_Lean_Meta_PPGoal(lean_object*);
 lean_object* initialize_Lean_Meta_UnificationHint(lean_object*);
 lean_object* initialize_Lean_Meta_Inductive(lean_object*);
 lean_object* initialize_Lean_Meta_SizeOf(lean_object*);
-lean_object* initialize_Lean_Meta_ProofBelow(lean_object*);
+lean_object* initialize_Lean_Meta_IndPredBelow(lean_object*);
 lean_object* initialize_Lean_Meta_Coe(lean_object*);
 lean_object* initialize_Lean_Meta_SortLocalDecls(lean_object*);
 lean_object* initialize_Lean_Meta_CollectFVars(lean_object*);
@@ -131,7 +131,7 @@ lean_dec_ref(res);
 res = initialize_Lean_Meta_SizeOf(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = initialize_Lean_Meta_ProofBelow(lean_io_mk_world());
+res = initialize_Lean_Meta_IndPredBelow(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 res = initialize_Lean_Meta_Coe(lean_io_mk_world());