chore: update stage0

stage0/src/Init/Data/Array/Basic.lean

@@ -294,13 +294,22 @@ match findSomeRev? a f with
 | some b => b
 | none   => panic! "failed to find element"
 
+@[specialize] partial def findIdxMAux {m : Type → Type u} [Monad m] (a : Array α) (p : α → m Bool) : Nat → m (Option Nat)
+| i =>
+  if h : i < a.size then
+    condM (p (a.get ⟨i, h⟩)) (pure (some i)) (findIdxMAux (i+1))
+  else
+    pure none
+
+@[inline] def findIdxM? {m : Type → Type u} [Monad m] (a : Array α) (p : α → m Bool) : m (Option Nat) :=
+findIdxMAux a p 0
+
 @[specialize] partial def findIdxAux (a : Array α) (p : α → Bool) : Nat → Option Nat
 | i =>
   if h : i < a.size then
-     let idx : Fin a.size := ⟨i, h⟩;
-     if p (a.get idx) then some i
-     else findIdxAux (i+1)
-  else none
+    if p (a.get ⟨i, h⟩) then some i else findIdxAux (i+1)
+  else
+    none
 
 @[inline] def findIdx? (a : Array α) (p : α → Bool) : Option Nat :=
 findIdxAux a p 0
@@ -310,6 +319,9 @@ match findIdxAux a p 0 with
 | some i => i
 | none   => panic! "failed to find element"
 
+def getIdx? [HasBeq α] (a : Array α) (v : α) : Option Nat :=
+a.findIdx? $ fun a => a == v
+
 end
 
 section

stage0/src/Init/Lean/Meta.lean

@@ -19,6 +19,7 @@ import Init.Lean.Meta.AppBuilder
 import Init.Lean.Meta.Tactic
 import Init.Lean.Meta.Message
 import Init.Lean.Meta.KAbstract
+import Init.Lean.Meta.RecursorInfo
 
 namespace Lean
 export Meta (MetaM)

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

@@ -0,0 +1,274 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Data.Nat.Control
+import Init.Lean.AuxRecursor
+import Init.Lean.Util.FindExpr
+import Init.Lean.Meta.ExprDefEq
+
+namespace Lean
+namespace Meta
+
+inductive RecursorUnivLevelPos
+| motive                -- marks where the universe of the motive should go
+| majorType (idx : Nat) -- marks where the #idx universe of the major premise type goes
+
+instance RecursorUnivLevelPos.hasToString : HasToString RecursorUnivLevelPos :=
+⟨fun pos => match pos with
+  | RecursorUnivLevelPos.motive        => "<motive-univ>"
+  | RecursorUnivLevelPos.majorType idx => toString idx⟩
+
+structure RecursorInfo :=
+(recursorName  : Name)
+(typeName      : Name)
+(univLevelPos  : List RecursorUnivLevelPos)
+(depElim       : Bool)
+(recursive     : Bool)
+(numArgs       : Nat) -- Total number of arguments
+(majorPos      : Nat)
+(paramsPos     : List (Option Nat)) -- Position of the recursor parameters in the major premise
+(indicesPos    : List Nat) -- Position of the recursor indices in the major premise
+(produceMotive : List Bool) -- If the i-th element is true then i-th minor premise produces the motive
+
+namespace RecursorInfo
+
+def numParams (info : RecursorInfo) : Nat := info.paramsPos.length
+def numIndices (info : RecursorInfo) : Nat := info.indicesPos.length
+def motivePos (info : RecursorInfo) : Nat := info.numParams
+def firstIndexPos (info : RecursorInfo) : Nat := info.majorPos - info.numIndices
+
+def isMinor (info : RecursorInfo) (pos : Nat) : Bool :=
+if pos ≤ info.motivePos then false
+else if info.firstIndexPos ≤ pos && pos ≤ info.majorPos then false
+else true
+
+def numMinors (info : RecursorInfo) : Nat :=
+let r := info.numArgs;
+let r := r - info.motivePos - 1;
+r - (info.majorPos + 1 - info.firstIndexPos)
+
+instance : HasToString RecursorInfo :=
+⟨fun info =>
+  "{\n" ++
+  "  name           := " ++ toString info.recursorName ++ "\n" ++
+  "  type           := " ++ toString info.typeName ++ "\n" ++
+  "  univs          := " ++ toString info.univLevelPos ++ "\n" ++
+  "  depElim        := " ++ toString info.depElim ++ "\n" ++
+  "  recursive      := " ++ toString info.recursive ++ "\n" ++
+  "  numArgs        := " ++ toString info.numArgs ++ "\n" ++
+  "  numParams      := " ++ toString info.numParams ++ "\n" ++
+  "  numIndices     := " ++ toString info.numIndices ++ "\n" ++
+  "  numMinors      := " ++ toString info.numMinors ++ "\n" ++
+  "  major          := " ++ toString info.majorPos ++ "\n" ++
+  "  motive         := " ++ toString info.motivePos ++ "\n" ++
+  "  paramsAtMajor  := " ++ toString info.paramsPos ++ "\n" ++
+  "  indicesAtMajor := " ++ toString info.indicesPos ++ "\n" ++
+  "  produceMotive  := " ++ toString info.produceMotive ++ "\n" ++
+  "}"⟩
+
+end RecursorInfo
+
+private def mkRecursorInfoForKernelRec (declName : Name) (val : RecursorVal) : MetaM RecursorInfo := do
+indInfo ← getConstInfo val.getInduct;
+match indInfo with
+| ConstantInfo.inductInfo ival =>
+  let numLParams    := ival.lparams.length;
+  let univLevelPos  := (List.range numLParams).map RecursorUnivLevelPos.majorType;
+  let univLevelPos  := if val.lparams.length == numLParams then univLevelPos else RecursorUnivLevelPos.motive :: univLevelPos;
+  let produceMotive := List.replicate val.nminors true;
+  let paramsPos     := (List.range val.nparams).map some;
+  let indicesPos    := (List.range val.nindices).map (fun pos => val.nparams + pos);
+  let numArgs       := val.nindices + val.nparams + val.nminors + val.nmotives + 1;
+  pure {
+   recursorName  := declName,
+   typeName      := val.getInduct,
+   univLevelPos  := univLevelPos,
+   majorPos      := val.getMajorIdx,
+   depElim       := true,
+   recursive     := ival.isRec,
+   produceMotive := produceMotive,
+   paramsPos     := paramsPos,
+   indicesPos    := indicesPos,
+   numArgs       := numArgs
+  }
+| _ => throw $ Exception.other "ill-formed builtin recursor"
+
+private def getMajorPosIfAuxRecursor? (declName : Name) (majorPos? : Option Nat) : MetaM (Option Nat) :=
+if majorPos?.isSome then pure majorPos?
+else do
+  env ← getEnv;
+  if !isAuxRecursor env declName then pure none
+  else match declName with
+  | Name.str p s _ =>
+    if s != "recOn" && s != "casesOn" && s != "brecOn" then
+      pure none
+    else do
+      recInfo ← getConstInfo (mkNameStr p "rec");
+      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"
+  | _ => pure none
+
+private def checkMotive (declName : Name) (motive : Expr) (motiveArgs : Array Expr) : MetaM Unit :=
+unless (motive.isFVar && motiveArgs.all Expr.isFVar) $ throw $ Exception.other
+  ("invalid user defined recursor '" ++ toString declName ++ "', result type must be of the form (C t), " ++
+   "where C is a bound variable, and t is a (possibly empty) sequence of bound variables")
+
+/- Compute number of parameters for (user-defined) recursor.
+   We assume a parameter is anything that occurs before the motive -/
+private partial def getNumParams (xs : Array Expr) (motive : Expr) : Nat → Nat
+| i =>
+  if h : i < xs.size then
+    let x := xs.get ⟨i, h⟩;
+    if motive == x then i
+    else getNumParams (i+1)
+  else
+    i
+
+private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs : Array Expr) (motive : Expr) (motiveArgs : Array Expr)
+    : MetaM (Expr × Nat × Bool) := do
+match majorPos? with
+| some majorPos =>
+  if h : majorPos < xs.size then
+    let major   := xs.get ⟨majorPos, h⟩;
+    let depElim := motiveArgs.contains major;
+    pure (major, majorPos, depElim)
+  else throw $ Exception.other
+    ("invalid major premise position for user defined recursor, recursor has only " ++ toString xs.size ++ " arguments")
+| none => do
+  when motiveArgs.isEmpty $ throw $ Exception.other
+    ("invalid user defined recursor, '" ++ toString declName ++ "' does not support dependent elimination, " ++
+     "and position of the major premise was not specified " ++
+     "(solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)");
+  let major := motiveArgs.back;
+  match xs.getIdx? major with
+  | some majorPos => pure (major, majorPos, true)
+  | none          => throw $ Exception.other ("ill-formed recursor '" ++ toString declName ++ "'")
+
+private def getParamsPos (declName : Name) (xs : Array Expr) (numParams : Nat) (Iargs : Array Expr) : MetaM (List (Option Nat)) := do
+paramsPos ← numParams.foldM
+  (fun i (paramsPos : Array (Option Nat)) => do
+    let x := xs.get! i;
+    j? ← Iargs.findIdxM? $ fun Iarg => isDefEq Iarg x;
+    match j? with
+    | some j => pure $ paramsPos.push (some j)
+    | none   => do
+      localDecl ← getLocalDecl x.fvarId!;
+      if localDecl.binderInfo.isInstImplicit then
+        pure $ paramsPos.push none
+      else
+        throw $ Exception.other
+          ("invalid user defined recursor '" ++ toString declName ++ "' , type of the major premise does not contain the recursor parameter"))
+  #[];
+pure paramsPos.toList
+
+private def getIndicesPos (declName : Name) (xs : Array Expr) (majorPos numIndices : Nat) (Iargs : Array Expr) : MetaM (List Nat) := do
+indicesPos ← numIndices.foldM
+  (fun i (indicesPos : Array Nat) => do
+    let i := majorPos - numIndices + i;
+    let x := xs.get! i;
+    -- trace! `Meta ("getIndicesPos " ++ toString i ++ ": " ++ x);
+    j? ← Iargs.findIdxM? $ fun Iarg => isDefEq Iarg x;
+    match j? with
+    | some j => pure $ indicesPos.push j
+    | none   => throw $ Exception.other
+      ("invalid user defined recursor '" ++ toString declName ++ "' , type of the major premise does not contain the recursor index"))
+  #[];
+pure indicesPos.toList
+
+private def getMotiveLevel (declName : Name) (motiveResultType : Expr) : MetaM Level :=
+match motiveResultType with
+| Expr.sort u@(Level.zero _) _    => pure u
+| Expr.sort u@(Level.param _ _) _ => pure u
+| _                               => throw $ Exception.other
+ ("invalid user defined recursor '" ++ toString declName ++ "' , motive result sort must be Prop or (Sort u) where u is a universe level parameter")
+
+private def getUnivLevelPos (declName : Name) (lparams : List Name) (motiveLvl : Level) (Ilevels : List Level) : MetaM (List RecursorUnivLevelPos) := do
+let Ilevels := Ilevels.toArray;
+univLevelPos ← lparams.foldlM
+  (fun (univLevelPos : Array RecursorUnivLevelPos) p =>
+    if motiveLvl == mkLevelParam p then
+      pure $ univLevelPos.push RecursorUnivLevelPos.motive
+    else
+      match Ilevels.findIdx? $ fun u => u == mkLevelParam p with
+      | some i => pure $ univLevelPos.push $ RecursorUnivLevelPos.majorType i
+      | none   => throw $ Exception.other
+        ("invalid user defined recursor '" ++ toString declName ++ "' , major premise type does not contain universe level parameter '" ++ toString p ++ "'"))
+  #[];
+pure univLevelPos.toList
+
+private def getProduceMotiveAndRecursive (xs : Array Expr) (numParams numIndices majorPos : Nat) (motive : Expr) : MetaM (List Bool × Bool) := do
+(produceMotive, rec) ← xs.size.foldM
+  (fun i (p : Array Bool × Bool) =>
+    if i < numParams + 1 then pure p -- skip parameters and motive
+    else if majorPos - numIndices ≤ i && i ≤ majorPos then pure p -- skip indices and major premise
+    else do -- process minor premise
+      let (produceMotive, rec) := p;
+      let x := xs.get! i;
+      xType ← inferType x;
+      forallTelescopeReducing xType $ fun minorArgs minorResultType => minorResultType.withApp $ fun res _ => do
+        -- trace! `Meta ("xType: " ++ xType ++ ", motive: " ++ motive ++ ", " ++ minorArgs ++ ", " ++ res);
+        let produceMotive := produceMotive.push (res == motive);
+        rec ← if rec then pure rec else minorArgs.anyM $ fun minorArg => do {
+          minorArgType ← inferType minorArg;
+          pure $ (minorArgType.find? $ fun e => e == motive).isSome
+        };
+        pure (produceMotive, rec))
+  (#[], false);
+pure (produceMotive.toList, rec)
+
+private def checkMotiveResultType (declName : Name) (motiveArgs : Array Expr) (motiveResultType : Expr) (motiveTypeParams : Array Expr) : MetaM Unit :=
+when (!motiveResultType.isSort || motiveArgs.size != motiveTypeParams.size) $ throw $ Exception.other
+  ("invalid user defined recursor '" ++ toString declName ++ "', motive must have a type of the form "
+   ++ "(C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of variables (aka parameters), "
+   ++ "(i : B A) is a (possibly empty) telescope (aka indices), and I is a constant")
+
+private def mkRecursorInfoAux (cinfo : ConstantInfo) (majorPos? : Option Nat) : MetaM RecursorInfo := do
+let declName := cinfo.name;
+majorPos? ← getMajorPosIfAuxRecursor? declName majorPos?;
+forallTelescopeReducing cinfo.type $ fun xs type => type.withApp $ fun motive motiveArgs => do
+  checkMotive declName motive motiveArgs;
+  let numParams := getNumParams xs motive 0;
+  (major, majorPos, depElim) ← getMajorPosDepElim declName majorPos? xs motive motiveArgs;
+  let numIndices := if depElim then motiveArgs.size - 1 else motiveArgs.size;
+  when (majorPos < numIndices) $ throw $ Exception.other
+    ("invalid user defined recursor '" ++ toString declName ++ "', indices must occur before major premise");
+  majorType ← inferType major;
+  majorType.withApp $ fun I Iargs =>
+  match I with
+  | Expr.const Iname Ilevels _ => do
+    paramsPos ← getParamsPos declName xs numParams Iargs;
+    indicesPos ← getIndicesPos declName xs majorPos numIndices Iargs;
+    motiveType ← inferType motive;
+    forallTelescopeReducing motiveType $ fun motiveTypeParams motiveResultType => do
+      checkMotiveResultType declName motiveArgs motiveResultType motiveTypeParams;
+      motiveLvl ← getMotiveLevel declName motiveResultType;
+      univLevelPos ← getUnivLevelPos declName cinfo.lparams motiveLvl Ilevels;
+      (produceMotive, recursive) ← getProduceMotiveAndRecursive xs numParams numIndices majorPos motive;
+      pure {
+        recursorName  := declName,
+        typeName      := Iname,
+        univLevelPos  := univLevelPos,
+        majorPos      := majorPos,
+        depElim       := depElim,
+        recursive     := recursive,
+        produceMotive := produceMotive,
+        paramsPos     := paramsPos,
+        indicesPos    := indicesPos,
+        numArgs       := xs.size
+      }
+  | _ => throw $ Exception.other
+    ("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
+cinfo ← getConstInfo declName;
+match cinfo with
+| ConstantInfo.recInfo val => mkRecursorInfoForKernelRec declName val
+| _                        => mkRecursorInfoAux cinfo majorPos?
+
+end Meta
+end Lean

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

@@ -49,5 +49,22 @@ match e.getAppFn with
   | _ => pure none
 | _ => pure none
 
+@[specialize] private partial def whnfHeadPredAux (pred : Expr → MetaM Bool) : Expr → MetaM Expr
+| e => Lean.WHNF.whnfEasyCases getLocalDecl getExprMVarAssignment? e $ fun e => do
+  e ← whnfCore e;
+  condM (pred e)
+    (do
+      e? ← unfoldDefinition? e;
+      match e? with
+      | some e => whnfHeadPredAux e
+      | none   => pure e)
+    (pure e)
+
+def whnfHeadPred (e : Expr) (pred : Expr → MetaM Bool) : MetaM Expr :=
+whnfHeadPredAux pred e
+
+def whnfUntil (e : Expr) (declName : Name) : MetaM Expr :=
+whnfHeadPredAux (fun e => pure $ e.isAppOf declName) e
+
 end Meta
 end Lean

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

@@ -36,7 +36,13 @@ def ident' : Parser := ident <|> underscore
 @[builtinTacticParser] def «allGoals»   := parser! nonReservedSymbol "allGoals " >> tacticParser
 @[builtinTacticParser] def «skip»       := parser! nonReservedSymbol "skip"
 @[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
-
+def majorPremise := parser! optional (try (ident >> " : ")) >> 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)
+def generalizingVars := optional (" generalizing " >> many1 ident)
+@[builtinTacticParser] def «induction»  := parser! nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> withAlts
 @[builtinTacticParser] def paren        := parser! "(" >> nonEmptySeq >> ")"
 @[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"
 @[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"

stage0/stdlib/Init/Data/Array/Basic.c

@@ -86,6 +86,7 @@ lean_object* l_Array_filter(lean_object*);
 lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Array_foldr___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Data_Array_Basic_1__swapAtPanic_x21___rarg___closed__3;
 lean_object* l_Array_insertAtAux___main(lean_object*);
+lean_object* l_Array_findIdxM_x3f(lean_object*, lean_object*);
 lean_object* l_Array_iterateM_u2082Aux___main___at_Array_foldlM_u2082___spec__1(lean_object*, lean_object*);
 lean_object* l_Array_empty___closed__1;
 lean_object* l_Array_modifyOp(lean_object*);
@@ -116,6 +117,7 @@ lean_object* l_Array_reverseAux(lean_object*);
 lean_object* l_Array_foldl_u2082___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_forMAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Array_isEqvAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_findIdxMAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_findRevMAux___main___at_Array_findRev_x3f___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_findIdxAux___main___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_foldlStepMAux___main___at_Array_getEvenElems___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -124,6 +126,7 @@ lean_object* lean_array_get_size(lean_object*);
 lean_object* l_Array_findSomeRevM_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
 lean_object* l_Array_getEvenElems___rarg___boxed(lean_object*);
+lean_object* l_Array_findIdxM_x3f___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_findSomeMAux___main___at_Array_findSome_x3f___spec__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_umapM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_map___rarg(lean_object*, lean_object*);
@@ -153,7 +156,9 @@ lean_object* l_Array_foldlM_u2082(lean_object*, lean_object*);
 lean_object* l_Array_foldlFrom___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_mapM(lean_object*, lean_object*);
 uint8_t l_Array_isEqvAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_getIdx_x3f(lean_object*);
 lean_object* l_Array_anyRange___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_findIdxMAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_anyFrom___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_foldlStepMAux(lean_object*, lean_object*);
 lean_object* l_Array_findSomeRevMAux___main___at_Array_findSomeRev_x3f___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -214,6 +219,7 @@ lean_object* l_Array_iterateM_u2082Aux(lean_object*, lean_object*);
 lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Array_toList___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l_Array_extract___rarg___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_findIdxAux___main___at_Array_getIdx_x3f___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Array_append___spec__1(lean_object*);
 uint8_t l_Array_all___rarg(lean_object*, lean_object*);
 lean_object* l_Array_filterMAux___main(lean_object*);
@@ -221,6 +227,7 @@ lean_object* l_Array_eraseIdx_x27___rarg___boxed(lean_object*, lean_object*);
 lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*);
 uint8_t l_Array_anyRangeMAux___main___at_Array_anyFrom___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Array_anyRangeMAux___main___at_Array_any___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_getIdx_x3f___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_get_x3f___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Array_findIdx_x3f___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Array_mapM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -267,6 +274,7 @@ lean_object* l_Array_shrink___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at_Array_allM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at_Array_allRangeM___spec__1___rarg___lambda__1(lean_object*, uint8_t);
 lean_object* l_Array_iterateMAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_findIdxMAux___main(lean_object*, lean_object*);
 lean_object* l_Array_mkEmpty___boxed(lean_object*, lean_object*);
 lean_object* l_Array_findSomeMAux___main___at_Array_findSome_x21___spec__1(lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at_Array_anyRange___spec__1(lean_object*);
@@ -314,6 +322,7 @@ lean_object* l_Array_findRevM_x3f___rarg(lean_object*, lean_object*, lean_object
 lean_object* l_Array_HasBeq___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_swapAt___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_filterAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_findIdxAux___main___at_Array_getIdx_x3f___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_HasEmptyc(lean_object*);
 lean_object* l_Array_findSomeMAux(lean_object*, lean_object*);
 lean_object* l_List_toArrayAux___main(lean_object*);
@@ -345,6 +354,8 @@ lean_object* l___private_Init_Data_Array_Basic_4__foldrRangeMAux___main(lean_obj
 lean_object* l_Array_swapAt___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_feraseIdx___rarg(lean_object*, lean_object*);
 uint8_t l_Array_contains___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_findIdxMAux___main___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_getIdx_x3f___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_find_x3f___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Array_getOp___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_data___boxed(lean_object*, lean_object*, lean_object*);
@@ -428,6 +439,7 @@ lean_object* l_Array_findMAux(lean_object*, lean_object*);
 lean_object* l_Array_findSomeMAux___main___at_Array_findSome_x21___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_filterAux___main(lean_object*);
 lean_object* l_Array_Inhabited(lean_object*);
+lean_object* l_Array_findIdxMAux(lean_object*, lean_object*);
 lean_object* l___private_Init_Data_Array_Basic_1__swapAtPanic_x21(lean_object*);
 lean_object* l_Array_indexOfAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_forRevMAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -471,6 +483,7 @@ lean_object* l_Array_findIdx_x3f(lean_object*);
 lean_object* l_Array_findRevMAux___main___at_Array_findRev_x3f___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_feraseIdx___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Array_findRevMAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_findIdxMAux___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
 lean_object* l_Array_getOp___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_toList___rarg(lean_object*);
 lean_object* l_Array_swapAt_x21___rarg(lean_object*, lean_object*, lean_object*);
@@ -500,6 +513,7 @@ lean_object* l_Array_findIdx_x21___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Array_findSomeRev_x21(lean_object*, lean_object*);
 lean_object* l_Array_findIdx_x21___rarg___closed__1;
 lean_object* l_Array_forRevMAux(lean_object*);
+lean_object* l_Array_findIdxAux___main___at_Array_getIdx_x3f___spec__1(lean_object*);
 lean_object* l_Array_iterate(lean_object*, lean_object*);
 lean_object* l_Array_forMAux(lean_object*);
 lean_object* l_List_toArrayAux___main___rarg(lean_object*, lean_object*);
@@ -3161,6 +3175,128 @@ lean_dec(x_2);
 return x_4;
 }
 }
+lean_object* l_Array_findIdxMAux___main___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint8_t x_5) {
+_start:
+{
+if (x_5 == 0)
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; 
+x_6 = lean_unsigned_to_nat(1u);
+x_7 = lean_nat_add(x_1, x_6);
+lean_dec(x_1);
+x_8 = l_Array_findIdxMAux___main___rarg(x_2, x_3, x_4, x_7);
+return x_8;
+}
+else
+{
+lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+lean_dec(x_4);
+lean_dec(x_3);
+x_9 = lean_ctor_get(x_2, 0);
+lean_inc(x_9);
+lean_dec(x_2);
+x_10 = lean_ctor_get(x_9, 1);
+lean_inc(x_10);
+lean_dec(x_9);
+x_11 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_11, 0, x_1);
+x_12 = lean_apply_2(x_10, lean_box(0), x_11);
+return x_12;
+}
+}
+}
+lean_object* l_Array_findIdxMAux___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; uint8_t x_6; 
+x_5 = lean_array_get_size(x_2);
+x_6 = lean_nat_dec_lt(x_4, x_5);
+lean_dec(x_5);
+if (x_6 == 0)
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_7 = lean_ctor_get(x_1, 0);
+lean_inc(x_7);
+lean_dec(x_1);
+x_8 = lean_ctor_get(x_7, 1);
+lean_inc(x_8);
+lean_dec(x_7);
+x_9 = lean_box(0);
+x_10 = lean_apply_2(x_8, lean_box(0), x_9);
+return x_10;
+}
+else
+{
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
+x_11 = lean_ctor_get(x_1, 1);
+lean_inc(x_11);
+x_12 = lean_array_fget(x_2, x_4);
+lean_inc(x_3);
+x_13 = lean_apply_1(x_3, x_12);
+x_14 = lean_alloc_closure((void*)(l_Array_findIdxMAux___main___rarg___lambda__1___boxed), 5, 4);
+lean_closure_set(x_14, 0, x_4);
+lean_closure_set(x_14, 1, x_1);
+lean_closure_set(x_14, 2, x_2);
+lean_closure_set(x_14, 3, x_3);
+x_15 = lean_apply_4(x_11, lean_box(0), lean_box(0), x_13, x_14);
+return x_15;
+}
+}
+}
+lean_object* l_Array_findIdxMAux___main(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_alloc_closure((void*)(l_Array_findIdxMAux___main___rarg), 4, 0);
+return x_3;
+}
+}
+lean_object* l_Array_findIdxMAux___main___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+uint8_t x_6; lean_object* x_7; 
+x_6 = lean_unbox(x_5);
+lean_dec(x_5);
+x_7 = l_Array_findIdxMAux___main___rarg___lambda__1(x_1, x_2, x_3, x_4, x_6);
+return x_7;
+}
+}
+lean_object* l_Array_findIdxMAux___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Array_findIdxMAux___main___rarg(x_1, x_2, x_3, x_4);
+return x_5;
+}
+}
+lean_object* l_Array_findIdxMAux(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_alloc_closure((void*)(l_Array_findIdxMAux___rarg), 4, 0);
+return x_3;
+}
+}
+lean_object* l_Array_findIdxM_x3f___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; lean_object* x_5; 
+x_4 = lean_unsigned_to_nat(0u);
+x_5 = l_Array_findIdxMAux___main___rarg(x_1, x_2, x_3, x_4);
+return x_5;
+}
+}
+lean_object* l_Array_findIdxM_x3f(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_alloc_closure((void*)(l_Array_findIdxM_x3f___rarg), 3, 0);
+return x_3;
+}
+}
 lean_object* l_Array_findIdxAux___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@@ -3277,7 +3413,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l___private_Init_Data_Array_Basic_1__swapAtPanic_x21___rarg___closed__3;
-x_2 = lean_unsigned_to_nat(311u);
+x_2 = lean_unsigned_to_nat(320u);
 x_3 = lean_unsigned_to_nat(12u);
 x_4 = l_Array_findSome_x21___rarg___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@@ -3325,6 +3461,95 @@ lean_dec(x_1);
 return x_3;
 }
 }
+lean_object* l_Array_findIdxAux___main___at_Array_getIdx_x3f___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; uint8_t x_6; 
+x_5 = lean_array_get_size(x_3);
+x_6 = lean_nat_dec_lt(x_4, x_5);
+lean_dec(x_5);
+if (x_6 == 0)
+{
+lean_object* x_7; 
+lean_dec(x_4);
+lean_dec(x_2);
+lean_dec(x_1);
+x_7 = lean_box(0);
+return x_7;
+}
+else
+{
+lean_object* x_8; lean_object* x_9; uint8_t x_10; 
+x_8 = lean_array_fget(x_3, x_4);
+lean_inc(x_1);
+lean_inc(x_2);
+x_9 = lean_apply_2(x_1, x_8, x_2);
+x_10 = lean_unbox(x_9);
+lean_dec(x_9);
+if (x_10 == 0)
+{
+lean_object* x_11; lean_object* x_12; 
+x_11 = lean_unsigned_to_nat(1u);
+x_12 = lean_nat_add(x_4, x_11);
+lean_dec(x_4);
+x_4 = x_12;
+goto _start;
+}
+else
+{
+lean_object* x_14; 
+lean_dec(x_2);
+lean_dec(x_1);
+x_14 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_14, 0, x_4);
+return x_14;
+}
+}
+}
+}
+lean_object* l_Array_findIdxAux___main___at_Array_getIdx_x3f___spec__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Array_findIdxAux___main___at_Array_getIdx_x3f___spec__1___rarg___boxed), 4, 0);
+return x_2;
+}
+}
+lean_object* l_Array_getIdx_x3f___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; lean_object* x_5; 
+x_4 = lean_unsigned_to_nat(0u);
+x_5 = l_Array_findIdxAux___main___at_Array_getIdx_x3f___spec__1___rarg(x_1, x_3, x_2, x_4);
+return x_5;
+}
+}
+lean_object* l_Array_getIdx_x3f(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Array_getIdx_x3f___rarg___boxed), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Array_findIdxAux___main___at_Array_getIdx_x3f___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Array_findIdxAux___main___at_Array_getIdx_x3f___spec__1___rarg(x_1, x_2, x_3, x_4);
+lean_dec(x_3);
+return x_5;
+}
+}
+lean_object* l_Array_getIdx_x3f___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Array_getIdx_x3f___rarg(x_1, x_2, x_3);
+lean_dec(x_2);
+return x_4;
+}
+}
 lean_object* l_Array_anyRangeMAux___main___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, uint8_t x_6) {
 _start:
 {
@@ -7763,7 +7988,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l___private_Init_Data_Array_Basic_1__swapAtPanic_x21___rarg___closed__3;
-x_2 = lean_unsigned_to_nat(672u);
+x_2 = lean_unsigned_to_nat(684u);
 x_3 = lean_unsigned_to_nat(20u);
 x_4 = l_Array_insertAt___rarg___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);

stage0/stdlib/Init/Lean/Meta.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean.Meta
-// Imports: Init.Lean.Meta.Basic Init.Lean.Meta.LevelDefEq Init.Lean.Meta.WHNF Init.Lean.Meta.InferType Init.Lean.Meta.FunInfo Init.Lean.Meta.ExprDefEq Init.Lean.Meta.DiscrTree Init.Lean.Meta.Reduce Init.Lean.Meta.Instances Init.Lean.Meta.AbstractMVars Init.Lean.Meta.SynthInstance Init.Lean.Meta.AppBuilder Init.Lean.Meta.Tactic Init.Lean.Meta.Message Init.Lean.Meta.KAbstract
+// Imports: Init.Lean.Meta.Basic Init.Lean.Meta.LevelDefEq Init.Lean.Meta.WHNF Init.Lean.Meta.InferType Init.Lean.Meta.FunInfo Init.Lean.Meta.ExprDefEq Init.Lean.Meta.DiscrTree Init.Lean.Meta.Reduce Init.Lean.Meta.Instances Init.Lean.Meta.AbstractMVars Init.Lean.Meta.SynthInstance Init.Lean.Meta.AppBuilder Init.Lean.Meta.Tactic Init.Lean.Meta.Message Init.Lean.Meta.KAbstract Init.Lean.Meta.RecursorInfo
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -28,6 +28,7 @@ lean_object* initialize_Init_Lean_Meta_AppBuilder(lean_object*);
 lean_object* initialize_Init_Lean_Meta_Tactic(lean_object*);
 lean_object* initialize_Init_Lean_Meta_Message(lean_object*);
 lean_object* initialize_Init_Lean_Meta_KAbstract(lean_object*);
+lean_object* initialize_Init_Lean_Meta_RecursorInfo(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Lean_Meta(lean_object* w) {
 lean_object * res;
@@ -78,6 +79,9 @@ lean_dec_ref(res);
 res = initialize_Init_Lean_Meta_KAbstract(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Lean_Meta_RecursorInfo(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