chore: update stage0

stage0/src/Init/Core.lean

@@ -140,7 +140,7 @@ structure Iff (a b : Prop) : Prop :=
 
 @[matchPattern] def rfl {α : Sort u} {a : α} : a = a := Eq.refl a
 
-theorem Eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
+theorem Eq.subst {α : Sort u} {motive : α → Prop} {a b : α} (h₁ : a = b) (h₂ : motive a) : motive b :=
   Eq.ndrec h₂ h₁
 
 theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=

stage0/src/Init/LeanInit.lean

@@ -278,8 +278,90 @@ partial def getHeadInfo : Syntax → Option SourceInfo
   | node _ args      => args.findSome? getHeadInfo
   | _                => none
 
+partial def getTailInfo : Syntax → Option SourceInfo
+  | atom info _   => info
+  | ident info .. => info
+  | node _ args   => args.findSomeRev? getTailInfo
+  | _             => none
+
+@[specialize] private partial def updateLast {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) :=
+  if i == 0 then none
+  else
+    let i := i - 1;
+    let v := a.get! i;
+    match f v with
+    | some v => some $ a.set! i v
+    | none   => updateLast a f i
+
+partial def setTailInfoAux (info : SourceInfo) : Syntax → Option Syntax
+  | atom _ val             => some $ atom info val
+  | ident _ rawVal val pre => some $ ident info rawVal val pre
+  | node k args            =>
+    match updateLast args (setTailInfoAux info) args.size with
+    | some args => some $ node k args
+    | none      => none
+  | stx                    => none
+
+def setTailInfo (stx : Syntax) (info : SourceInfo) : Syntax :=
+  match setTailInfoAux info stx with
+  | some stx => stx
+  | none     => stx
+
+def unsetTrailing (stx : Syntax) : Syntax :=
+  match stx.getTailInfo with
+  | none      => stx
+  | some info => stx.setTailInfo { info with trailing := none }
+
+@[specialize] private partial def updateFirst {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) :=
+  if h : i < a.size then
+    let v := a.get ⟨i, h⟩;
+    match f v with
+    | some v => some $ a.set ⟨i, h⟩ v
+    | none   => updateFirst a f (i+1)
+  else
+    none
+
+partial def setHeadInfoAux (info : SourceInfo) : Syntax → Option Syntax
+  | atom _ val             => some $ atom info val
+  | ident _ rawVal val pre => some $ ident info rawVal val pre
+  | node k args            =>
+    match updateFirst args (setHeadInfoAux info) 0 with
+    | some args => some $ node k args
+    | noxne     => none
+  | stx                    => none
+
+def setHeadInfo (stx : Syntax) (info : SourceInfo) : Syntax :=
+  match setHeadInfoAux info stx with
+  | some stx => stx
+  | none     => stx
+
+def setInfo (info : SourceInfo) : Syntax → Syntax
+  | atom _ val             => atom info val
+  | ident _ rawVal val pre => ident info rawVal val pre
+  | stx                    => stx
+
+partial def replaceInfo (info : SourceInfo) : Syntax → Syntax
+  | node k args => node k $ args.map (replaceInfo info)
+  | stx         => setInfo info stx
+
+def copyInfo (s : Syntax) (source : Syntax) : Syntax :=
+  match source.getHeadInfo with
+  | none      => s
+  | some info => s.setHeadInfo info
+
+def copyTailInfo (s : Syntax) (source : Syntax) : Syntax :=
+  match source.getTailInfo with
+  | none      => s
+  | some info => s.setTailInfo info
+
 end Syntax
 
+def mkAtom (val : String) : Syntax :=
+  Syntax.atom {} val
+
+@[inline] def mkNode (k : SyntaxNodeKind) (args : Array Syntax) : Syntax :=
+  Syntax.node k args
+
 /- Syntax objects for a Lean module. -/
 structure Module :=
   (header   : Syntax)

stage0/src/Lean/Elab/Match.lean

@@ -748,12 +748,23 @@ private def elabMatchAux (discrStxs : Array Syntax) (altViews : Array MatchAltVi
    ```
   -/
   synthesizeUsingDefault
-  -- TODO report error if matchType or altLHSS.toList have metavars
   let rhss := alts.map Prod.snd
-  let altLHSS := alts.map Prod.fst
+  let matchType ← instantiateMVars matchType
+  let altLHSS ← alts.toList.mapM fun alt => do
+    let altLHS ← Match.instantiateAltLHSMVars alt.1
+    withRef altLHS.ref do
+      for d in altLHS.fvarDecls do
+        if d.hasExprMVar then
+          withExistingLocalDecls altLHS.fvarDecls do
+            throwError! "invalid match-expression, type of pattern variable '{d.toExpr}' contains metavariables{indentExpr d.type}"
+      for p in altLHS.patterns do
+        if p.hasExprMVar then
+          withExistingLocalDecls altLHS.fvarDecls do
+            throwError! "invalid match-expression, pattern contains metavariables{indentExpr (← p.toExpr)}"
+      pure altLHS
   let numDiscrs := discrs.size
   let matcherName ← mkAuxName `match
-  let matcherResult ← mkMatcher matcherName matchType numDiscrs altLHSS.toList
+  let matcherResult ← mkMatcher matcherName matchType numDiscrs altLHSS
   let motive ← forallBoundedTelescope matchType numDiscrs fun xs matchType => mkLambdaFVars xs matchType
   reportMatcherResultErrors matcherResult
   let r := mkApp matcherResult.matcher motive

stage0/src/Lean/Elab/PreDefinition/Structural.lean

@@ -206,6 +206,21 @@ private partial def toBelow (below : Expr) (numIndParams : Nat) (recArg : Expr)
   withBelowDict below numIndParams fun C belowDict =>
     toBelowAux C belowDict recArg below
 
+/--
+  Return true iff `e` contains an application `recFnName .. t ..` where the term `t` is
+  the argument we are trying to recurse on, and it contains loose bound variables.
+
+  We use this test to decide whether we should process a matcher-application as a regular
+  applicaton or not. That is, whether we should push the `below` argument should be affected by the matcher or not.
+  If `e` does not contain an application of the form `recFnName .. t ..`, then we know
+  the recursion doesn't depend on any pattern variable in this matcher.
+-/
+private def recArgHasLooseBVarsAt (recFnName : Name) (recArgInfo : RecArgInfo) (e : Expr) : Bool :=
+  let recArgPos := recArgInfo.fixedParams.size + recArgInfo.pos
+  let app?   := e.find? fun e =>
+     e.isAppOf recFnName && e.getAppNumArgs > recArgPos && (e.getArg! recArgPos).hasLooseBVars
+  app?.isSome
+
 private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo) (below : Expr) (e : Expr) : MetaM Expr :=
   let rec loop : Expr → Expr → MetaM Expr
     | below, e@(Expr.lam n d b c) => do
@@ -244,25 +259,10 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
       let matcherApp? ← matchMatcherApp? e
       match matcherApp? with
       | some matcherApp =>
-        /- If none of the alternatives contain a recursive application, we process it as a regular one. -/
-        if matcherApp.alts.all fun alt => !containsRecFn recFnName alt then
+        if !recArgHasLooseBVarsAt recFnName recArgInfo e then
           processApp e
         else
           /- Here is an example we currently not handle
-             ```
-             def f (xs : List Nat) : Nat :=
-             match xs with
-             | [] => 0
-             | y::ys =>
-               match ys with
-               | [] => 1
-               | zs => f ys + 1
-             ```
-             We are matching on `ys`, but still using `ys` in the second alternative.
-             If we push the `below` argument over the dependent match it will be able to eliminate recursive call using `zs`.
-             To make it work, users have to write the second alternative as `| zs => f zs + 1`
-             We considered trying `processApp e` first, and only if fails trying the code below.
-             This trick is sufficient for solving the example above, but it is not sufficient for the slightly more complicated example:
              ```
              def g (xs : List Nat) : Nat :=
              match xs with
@@ -271,22 +271,14 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
                match ys with
                | []       => 1
                | _::_::zs => g zs + 1
-               | _        => g ys + 2
+               | zs       => g ys + 2
              ```
-             To make it work, users would have to write the last alternative as
-             ```
-             | zs => g zs + 2
-             ```
-             If this is too annoying in practice, we may replace `ys` with the matching term.
-             This may generate weird error messages, when it doesn't work.
-          -/
+             We are matching on `ys`, but still using `ys` in the third alternative.
+             If we push the `below` argument over the dependent match it will be able to eliminate recursive call using `zs`.
+             To make it work, users have to write the third alternative as `| zs => g zs + 2`
+             If this is too annoying in practice, we may replace `ys` with the matching term, but
+             this may generate weird error messages, when it doesn't work. -/
           let matcherApp ← mapError (matcherApp.addArg below) (fun msg => "failed to add `below` argument to 'matcher' application" ++ indentD msg)
-          let mut discrs := matcherApp.discrs
-          for i in [:discrs.size] do
-            let discr ← processApp discrs[i]
-            trace[Elab.definition.structural]! "new discr [{i}]: {discr}"
-            discrs := discrs.set! i discr
-          trace[Elab.definition.structural]! "discrs: {discrs}"
           let altsNew ← (Array.zip matcherApp.alts matcherApp.altNumParams).mapM fun (alt, numParams) =>
             lambdaTelescope alt fun xs altBody => do
               trace[Elab.definition.structural]! "altNumParams: {numParams}, xs: {xs}"
@@ -294,7 +286,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
                 throwError! "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
               let belowForAlt := xs[numParams - 1]
               mkLambdaFVars xs (← loop belowForAlt altBody)
-          pure { matcherApp with discrs := discrs, alts := altsNew }.toExpr
+          pure { matcherApp with alts := altsNew }.toExpr
       | none => processApp e
     | _, e => ensureNoRecFn recFnName e
   loop below e

stage0/src/Lean/LocalContext.lean

@@ -85,6 +85,10 @@ def updateBinderInfo : LocalDecl → BinderInfo → LocalDecl
 def toExpr (decl : LocalDecl) : Expr :=
   mkFVar decl.fvarId
 
+def hasExprMVar : LocalDecl → Bool
+  | cdecl (type := t) ..              => t.hasExprMVar
+  | ldecl (type := t) (value := v) .. => t.hasExprMVar || v.hasExprMVar
+
 end LocalDecl
 
 open Std (PersistentHashMap PersistentArray PArray)

stage0/src/Lean/Meta/Match/Match.lean

@@ -66,13 +66,35 @@ def replaceFVarId (fvarId : FVarId) (v : Expr) (p : Pattern) : Pattern :=
   let s : FVarSubst := {}
   p.applyFVarSubst (s.insert fvarId v)
 
+partial def hasExprMVar : Pattern → Bool
+  | inaccessible e => e.hasExprMVar
+  | ctor _ _ ps fs => ps.any (·.hasExprMVar) || fs.any hasExprMVar
+  | val e          => e.hasExprMVar
+  | as _ p         => hasExprMVar p
+  | arrayLit t xs  => t.hasExprMVar || xs.any hasExprMVar
+  | _              => false
+
 end Pattern
 
+partial def instantiatePatternMVars : Pattern → MetaM Pattern
+  | Pattern.inaccessible e      => return Pattern.inaccessible (← instantiateMVars e)
+  | Pattern.val e               => return Pattern.val (← instantiateMVars e)
+  | Pattern.ctor n us ps fields => return Pattern.ctor n us (← ps.mapM instantiateMVars) (← fields.mapM instantiatePatternMVars)
+  | Pattern.as x p              => return Pattern.as x (← instantiatePatternMVars p)
+  | Pattern.arrayLit t xs       => return Pattern.arrayLit (← instantiateMVars t) (← xs.mapM instantiatePatternMVars)
+  | p                   => return p
+
 structure AltLHS :=
   (ref        : Syntax)
   (fvarDecls  : List LocalDecl) -- Free variables used in the patterns.
   (patterns   : List Pattern)   -- We use `List Pattern` since we have nary match-expressions.
 
+def instantiateAltLHSMVars (altLHS : AltLHS) : MetaM AltLHS :=
+  return { altLHS with
+    fvarDecls := (← altLHS.fvarDecls.mapM instantiateLocalDeclMVars),
+    patterns  := (← altLHS.patterns.mapM instantiatePatternMVars)
+  }
+
 structure Alt :=
   (ref       : Syntax)
   (idx       : Nat) -- for generating error messages

stage0/src/Lean/Meta/Tactic/Induction.lean

@@ -134,7 +134,7 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi
       let indices ← recursorInfo.indicesPos.toArray.mapM fun idxPos => do
         if idxPos ≥ majorTypeArgs.size then throwTacticEx `induction mvarId msg!"major premise type is ill-formed{indentExpr majorType}"
         let idx := majorTypeArgs.get! idxPos
-        unless idx.isFVar do throwTacticEx `induction mvarId msg!"major premise type index {idx} is not variable{indentExpr majorType}"
+        unless idx.isFVar do throwTacticEx `induction mvarId msg!"major premise type index {idx} is not a variable{indentExpr majorType}"
         majorTypeArgs.size.forM fun i => do
           let arg := majorTypeArgs[i]
           if i != idxPos && arg == idx then

stage0/src/Lean/Parser/Term.lean

@@ -119,7 +119,10 @@ Note that we did not add a `explicitShortBinder` parser since `(α) → α →
 -/
 @[builtinTermParser] def depArrow := parser! bracketedBinder true >> checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser
 
-def simpleBinder := parser! many1 binderIdent
+def simpleBinder := parser!
+  (checkInsideQuot >> many1 binderIdent >> optType)
+  <|>
+  (checkOutsideQuot >> many1 binderIdent)
 @[builtinTermParser]
 def «forall» := parser!:leadPrec unicodeSymbol "∀ " "forall" >> many1 (ppSpace >> (simpleBinder <|> bracketedBinder)) >> ", " >> termParser
 
@@ -138,7 +141,8 @@ def matchDiscr := parser! optional («try» (ident >> checkNoWsBefore "no space
 @[builtinTermParser] def «nomatch»  := parser!:leadPrec "nomatch " >> termParser
 
 def funImplicitBinder := «try» (lookahead ("{" >> many1 binderIdent >> (" : " <|> "}"))) >> implicitBinder
-def funBinder : Parser := funImplicitBinder <|> instBinder <|> termParser maxPrec
+def funSimpleBinder   := parser! «try» (lookahead (many1 binderIdent >> " : ")) >> many1 binderIdent >> optType
+def funBinder : Parser := funImplicitBinder <|> instBinder <|> (checkInsideQuot >> funSimpleBinder) <|> termParser maxPrec
 -- NOTE: we use `nodeWithAntiquot` to ensure that `fun $b => ...` remains a `term` antiquotation
 def basicFun : Parser := nodeWithAntiquot "basicFun" `Lean.Parser.Term.basicFun (many1 (ppSpace >> funBinder) >> darrow >> termParser)
 @[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts false)

stage0/src/Lean/Syntax.lean

@@ -197,77 +197,6 @@ partial def getTailWithPos : Syntax → Option Syntax
   | node _ args                          => args.findSomeRev? getTailWithPos
   | _                                    => none
 
-partial def getTailInfo : Syntax → Option SourceInfo
-  | atom info _   => info
-  | ident info .. => info
-  | node _ args   => args.findSomeRev? getTailInfo
-  | _             => none
-
-@[specialize] private partial def updateLast {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) :=
-  if i == 0 then none
-  else
-    let i := i - 1;
-    let v := a.get! i;
-    match f v with
-    | some v => some $ a.set! i v
-    | none   => updateLast a f i
-
-partial def setTailInfoAux (info : SourceInfo) : Syntax → Option Syntax
-  | atom _ val             => some $ atom info val
-  | ident _ rawVal val pre => some $ ident info rawVal val pre
-  | node k args            =>
-    match updateLast args (setTailInfoAux info) args.size with
-    | some args => some $ node k args
-    | none      => none
-  | stx                    => none
-
-def setTailInfo (stx : Syntax) (info : SourceInfo) : Syntax :=
-  match setTailInfoAux info stx with
-  | some stx => stx
-  | none     => stx
-
-def unsetTrailing (stx : Syntax) : Syntax :=
-  match stx.getTailInfo with
-  | none      => stx
-  | some info => stx.setTailInfo { info with trailing := none }
-
-@[specialize] private partial def updateFirst {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) :=
-  if h : i < a.size then
-    let v := a.get ⟨i, h⟩;
-    match f v with
-    | some v => some $ a.set ⟨i, h⟩ v
-    | none   => updateFirst a f (i+1)
-  else
-    none
-
-partial def setHeadInfoAux (info : SourceInfo) : Syntax → Option Syntax
-  | atom _ val             => some $ atom info val
-  | ident _ rawVal val pre => some $ ident info rawVal val pre
-  | node k args            =>
-    match updateFirst args (setHeadInfoAux info) 0 with
-    | some args => some $ node k args
-    | noxne     => none
-  | stx                    => none
-
-def setHeadInfo (stx : Syntax) (info : SourceInfo) : Syntax :=
-  match setHeadInfoAux info stx with
-  | some stx => stx
-  | none     => stx
-
-def setInfo (info : SourceInfo) : Syntax → Syntax
-  | atom _ val             => atom info val
-  | ident _ rawVal val pre => ident info rawVal val pre
-  | stx                    => stx
-
-partial def replaceInfo (info : SourceInfo) : Syntax → Syntax
-  | node k args => node k $ args.map (replaceInfo info)
-  | stx         => setInfo info stx
-
-def copyInfo (s : Syntax) (source : Syntax) : Syntax :=
-  match source.getHeadInfo with
-  | none      => s
-  | some info => s.setHeadInfo info
-
 private def reprintLeaf (info : SourceInfo) (val : String) : String :=
   -- no source info => add gracious amounts of whitespace to definitely separate tokens
   -- Note that the proper pretty printer does not use this function.
@@ -423,12 +352,6 @@ def mkSimpleAtom (val : String) : Syntax :=
 def mkListNode (args : Array Syntax) : Syntax :=
   Syntax.node nullKind args
 
-def mkAtom (val : String) : Syntax :=
-  Syntax.atom {} val
-
-@[inline] def mkNode (k : SyntaxNodeKind) (args : Array Syntax) : Syntax :=
-  Syntax.node k args
-
 @[export lean_mk_syntax_str_lit]
 def mkStxStrLitAux (val : String) : Syntax :=
   mkStxStrLit val

stage0/stdlib/Lean/LocalContext.c

@@ -39,6 +39,7 @@ lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlMA
 lean_object* l_Lean_LocalDecl_setValue_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_LocalDecl_value_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_foldRev_loop___at_Lean_LocalContext_mkForall___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_LocalDecl_hasExprMVar___boxed(lean_object*);
 lean_object* l_Lean_LocalContext_foldlM___at_Lean_LocalContext_foldl___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_LocalContext_addDecl_match__1___rarg(lean_object*, lean_object*);
 lean_object* l_Array_findSomeRevM_x3f_find___at_Lean_LocalContext_findDeclRev_x3f___spec__6___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -173,6 +174,7 @@ lean_object* l_Lean_LocalDecl_value(lean_object*);
 lean_object* l_Std_PersistentArray_anyM___at_Lean_LocalContext_anyM___spec__1___rarg(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Name_hasMacroScopes(lean_object*);
 lean_object* l_Array_findSomeRevM_x3f_find___at_Lean_LocalContext_findFromUserName_x3f___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_LocalDecl_hasExprMVar_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* lean_local_ctx_num_indices(lean_object*);
 lean_object* l_Lean_LocalDecl_isLet___boxed(lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
@@ -209,6 +211,7 @@ lean_object* l_Lean_LocalContext_Lean_LocalContext___instance__2___closed__1;
 lean_object* l_Array_foldlMUnsafe_fold___at_Lean_LocalContext_foldl___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_LocalContext_foldlM___at_Lean_LocalContext_foldl___spec__1(lean_object*);
 lean_object* l_Lean_LocalDecl_value_x3f_match__1(lean_object*);
+uint8_t l_Lean_Expr_hasExprMVar(lean_object*);
 lean_object* l_Lean_LocalDecl_updateBinderInfo_match__1(lean_object*);
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_LocalContext_isSubPrefixOfAux_match__1(lean_object*);
@@ -365,7 +368,9 @@ uint8_t l_Array_anyMUnsafe_any___at_Lean_LocalContext_isSubPrefixOfAux___spec__1
 lean_object* l_Array_anyMUnsafe_any___at_Lean_LocalContext_anyM___spec__3___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Std_PersistentArray_anyMAux___at_Lean_LocalContext_any___spec__2(lean_object*, lean_object*);
 lean_object* l_Lean_LocalDecl_binderInfo_match__1(lean_object*);
+lean_object* l_Lean_LocalDecl_hasExprMVar_match__1(lean_object*);
 lean_object* l_Lean_LocalDecl_binderInfoEx_match__1(lean_object*);
+uint8_t l_Lean_LocalDecl_hasExprMVar(lean_object*);
 lean_object* l_Lean_LocalContext_get_x21___closed__2;
 lean_object* l_Std_PersistentArray_anyM___at_Lean_LocalContext_anyM___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t);
 lean_object* l_Lean_LocalContext_renameUserName_match__2___rarg(lean_object*, lean_object*);
@@ -1894,6 +1899,98 @@ lean_dec(x_1);
 return x_2;
 }
 }
+lean_object* l_Lean_LocalDecl_hasExprMVar_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9; lean_object* x_10; 
+lean_dec(x_3);
+x_4 = lean_ctor_get(x_1, 0);
+lean_inc(x_4);
+x_5 = lean_ctor_get(x_1, 1);
+lean_inc(x_5);
+x_6 = lean_ctor_get(x_1, 2);
+lean_inc(x_6);
+x_7 = lean_ctor_get(x_1, 3);
+lean_inc(x_7);
+x_8 = lean_ctor_get_uint8(x_1, sizeof(void*)*4);
+lean_dec(x_1);
+x_9 = lean_box(x_8);
+x_10 = lean_apply_5(x_2, x_4, x_5, x_6, x_7, 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; uint8_t x_16; lean_object* x_17; lean_object* x_18; 
+lean_dec(x_2);
+x_11 = lean_ctor_get(x_1, 0);
+lean_inc(x_11);
+x_12 = lean_ctor_get(x_1, 1);
+lean_inc(x_12);
+x_13 = lean_ctor_get(x_1, 2);
+lean_inc(x_13);
+x_14 = lean_ctor_get(x_1, 3);
+lean_inc(x_14);
+x_15 = lean_ctor_get(x_1, 4);
+lean_inc(x_15);
+x_16 = lean_ctor_get_uint8(x_1, sizeof(void*)*5);
+lean_dec(x_1);
+x_17 = lean_box(x_16);
+x_18 = lean_apply_6(x_3, x_11, x_12, x_13, x_14, x_15, x_17);
+return x_18;
+}
+}
+}
+lean_object* l_Lean_LocalDecl_hasExprMVar_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_LocalDecl_hasExprMVar_match__1___rarg), 3, 0);
+return x_2;
+}
+}
+uint8_t l_Lean_LocalDecl_hasExprMVar(lean_object* x_1) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_2; uint8_t x_3; 
+x_2 = lean_ctor_get(x_1, 3);
+x_3 = l_Lean_Expr_hasExprMVar(x_2);
+return x_3;
+}
+else
+{
+lean_object* x_4; lean_object* x_5; uint8_t x_6; 
+x_4 = lean_ctor_get(x_1, 3);
+x_5 = lean_ctor_get(x_1, 4);
+x_6 = l_Lean_Expr_hasExprMVar(x_4);
+if (x_6 == 0)
+{
+uint8_t x_7; 
+x_7 = l_Lean_Expr_hasExprMVar(x_5);
+return x_7;
+}
+else
+{
+uint8_t x_8; 
+x_8 = 1;
+return x_8;
+}
+}
+}
+}
+lean_object* l_Lean_LocalDecl_hasExprMVar___boxed(lean_object* x_1) {
+_start:
+{
+uint8_t x_2; lean_object* x_3; 
+x_2 = l_Lean_LocalDecl_hasExprMVar(x_1);
+lean_dec(x_1);
+x_3 = lean_box(x_2);
+return x_3;
+}
+}
 static lean_object* _init_l_Lean_LocalContext_fvarIdToDecl___default___closed__1() {
 _start:
 {
@@ -3047,7 +3144,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; 
 x_1 = l_Lean_LocalDecl_value___closed__1;
 x_2 = l_Lean_LocalContext_get_x21___closed__1;
-x_3 = lean_unsigned_to_nat(143u);
+x_3 = lean_unsigned_to_nat(147u);
 x_4 = lean_unsigned_to_nat(14u);
 x_5 = l_Lean_LocalContext_get_x21___closed__2;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -8357,7 +8454,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; 
 x_1 = l_Lean_LocalDecl_value___closed__1;
 x_2 = l_Nat_foldRev_loop___at_Lean_LocalContext_mkBinding___spec__1___closed__1;
-x_3 = lean_unsigned_to_nat(327u);
+x_3 = lean_unsigned_to_nat(331u);
 x_4 = lean_unsigned_to_nat(14u);
 x_5 = l_Lean_LocalContext_get_x21___closed__2;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

stage0/stdlib/Lean/Meta/Tactic/Induction.c

@@ -5420,7 +5420,7 @@ static lean_object* _init_l_Array_mapMUnsafe_map___at_Lean_Meta_induction___spec
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string(" is not variable");
+x_1 = lean_mk_string(" is not a variable");
 return x_1;
 }
 }