chore: update stage0

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

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -6,8 +7,7 @@ Authors: Leonardo de Moura
 import Lean.Meta.Tactic.Assert
 import Lean.Meta.Match.CaseValues
 
-namespace Lean
-namespace Meta
+namespace Lean.Meta
 
 structure CaseArraySizesSubgoal :=
 (mvarId : MVarId)
@@ -19,41 +19,38 @@ instance CaseArraySizesSubgoal.inhabited : Inhabited CaseArraySizesSubgoal :=
 ⟨{ mvarId := arbitrary _ }⟩
 
 def getArrayArgType (a : Expr) : MetaM Expr := do
-aType ← inferType a;
-aType ← whnfD aType;
-unless (aType.isAppOfArity `Array 1) $
-  throwError ("array expected" ++ indentExpr a);
+let aType ← inferType a
+let aType ← whnfD aType
+unless aType.isAppOfArity `Array 1 do
+  throwError! "array expected{indentExpr a}"
 pure aType.appArg!
 
 private def mkArrayGetLit (a : Expr) (i : Nat) (n : Nat) (h : Expr) : MetaM Expr := do
-lt    ← mkLt (mkNatLit i) (mkNatLit n);
-ltPrf ← mkDecideProof lt;
+let lt    ← mkLt (mkNatLit i) (mkNatLit n)
+let ltPrf ← mkDecideProof lt
 mkAppM `Array.getLit #[a, mkNatLit i, h, ltPrf]
 
-private partial def introArrayLitAux (mvarId : MVarId) (α : Expr) (a : Expr) (n : Nat) (xNamePrefix : Name) (aSizeEqN : Expr)
-    : Nat → Array Expr → Array Expr → MetaM (Expr × Array Expr)
-| i, xs, args =>
-  if i < n then do
-    withLocalDeclD (xNamePrefix.appendIndexAfter (i+1)) α fun xi => do
-      let xs := xs.push xi;
-      ai ← mkArrayGetLit a i n aSizeEqN;
-      let args := args.push ai;
-      introArrayLitAux (i+1) xs args
-  else do
-    xsLit     ← mkArrayLit α xs.toList;
-    aEqXsLit  ← mkEq a xsLit;
-    aEqLitPrf ← mkAppM `Array.toArrayLitEq #[a, mkNatLit n, aSizeEqN];
-    withLocalDeclD `hEqALit aEqXsLit fun heq => do
-      target    ← getMVarType mvarId;
-      newTarget ← mkForallFVars (xs.push heq) target;
-      pure (newTarget, args.push aEqLitPrf)
-
 private partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNamePrefix : Name) (aSizeEqN : Expr) : MetaM MVarId := do
-α ← getArrayArgType a;
-(newTarget, args) ← introArrayLitAux mvarId α a n xNamePrefix aSizeEqN 0 #[] #[];
-tag ← getMVarTag mvarId;
-newMVar   ← mkFreshExprSyntheticOpaqueMVar newTarget tag;
-assignExprMVar mvarId (mkAppN newMVar args);
+let α ← getArrayArgType a
+let rec loop (i : Nat) (xs : Array Expr) (args : Array Expr) := do
+  if i < n then
+    withLocalDeclD (xNamePrefix.appendIndexAfter (i+1)) α fun xi => do
+      let xs := xs.push xi
+      let ai ← mkArrayGetLit a i n aSizeEqN
+      let args := args.push ai
+      loop (i+1) xs args
+  else
+    let xsLit     ← mkArrayLit α xs.toList
+    let aEqXsLit  ← mkEq a xsLit
+    let aEqLitPrf ← mkAppM `Array.toArrayLitEq #[a, mkNatLit n, aSizeEqN]
+    withLocalDeclD `hEqALit aEqXsLit fun heq => do
+      let target    ← getMVarType mvarId
+      let newTarget ← mkForallFVars (xs.push heq) target
+      pure (newTarget, args.push aEqLitPrf)
+let (newTarget, args) ← loop 0 #[] #[]
+let tag ← getMVarTag mvarId
+let newMVar   ← mkFreshExprSyntheticOpaqueMVar newTarget tag
+assignExprMVar mvarId (mkAppN newMVar args)
 pure newMVar.mvarId!
 
 /--
@@ -64,33 +61,32 @@ pure newMVar.mvarId!
   n+1) `..., (h_1 : a.size != sizes[0]), ..., (h_n : a.size != sizes[n-1]) |- C a`
   where `n = sizes.size` -/
 def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNamePrefix := `x) (hNamePrefix := `h) : MetaM (Array CaseArraySizesSubgoal) := do
-let a := mkFVar fvarId;
-α ← getArrayArgType a;
-aSize ← mkAppM `Array.size #[a];
-mvarId ← assertExt mvarId `aSize (mkConst `Nat) aSize;
-(aSizeFVarId, mvarId) ← intro1 mvarId;
-(hEq, mvarId) ← intro1 mvarId;
-subgoals ← caseValues mvarId aSizeFVarId (sizes.map mkNatLit) hNamePrefix;
+let a := mkFVar fvarId
+let α ← getArrayArgType a
+let aSize ← mkAppM `Array.size #[a]
+let mvarId ← assertExt mvarId `aSize (mkConst `Nat) aSize
+let (aSizeFVarId, mvarId) ← intro1 mvarId
+let (hEq, mvarId) ← intro1 mvarId
+let subgoals ← caseValues mvarId aSizeFVarId (sizes.map mkNatLit) hNamePrefix
 subgoals.mapIdxM fun i subgoal => do
-  let subst  := subgoal.subst;
-  let mvarId := subgoal.mvarId;
-  let hEqSz  := (subst.get hEq).fvarId!;
-  if h : i < sizes.size then do
-     let n := sizes.get ⟨i, h⟩;
-     mvarId ← clear mvarId (subgoal.newHs.get! 0);
-     mvarId ← clear mvarId (subst.get aSizeFVarId).fvarId!;
+  let subst  := subgoal.subst
+  let mvarId := subgoal.mvarId
+  let hEqSz  := (subst.get hEq).fvarId!
+  if h : i < sizes.size then
+     let n := sizes.get ⟨i, h⟩
+     let mvarId ← clear mvarId subgoal.newHs[0]
+     let mvarId ← clear mvarId (subst.get aSizeFVarId).fvarId!
      withMVarContext mvarId do
-       hEqSzSymm ← mkEqSymm (mkFVar hEqSz);
-       mvarId ← introArrayLit mvarId a n xNamePrefix hEqSzSymm;
-       (xs, mvarId)  ← introN mvarId n;
-       (hEqLit, mvarId) ← intro1 mvarId;
-       mvarId ← clear mvarId hEqSz;
-       (subst, mvarId) ← substCore mvarId hEqLit false subst;
+       let hEqSzSymm ← mkEqSymm (mkFVar hEqSz)
+       let mvarId ← introArrayLit mvarId a n xNamePrefix hEqSzSymm
+       let (xs, mvarId)  ← introN mvarId n
+       let (hEqLit, mvarId) ← intro1 mvarId
+       let mvarId ← clear mvarId hEqSz
+       let (subst, mvarId) ← substCore mvarId hEqLit false subst
        pure { mvarId := mvarId, elems := xs, subst := subst }
-  else do
-     (subst, mvarId) ← substCore mvarId hEq false subst;
-     let diseqs := subgoal.newHs.map fun fvarId => (subst.get fvarId).fvarId!;
+  else
+     let (subst, mvarId) ← substCore mvarId hEq false subst
+     let diseqs := subgoal.newHs.map fun fvarId => (subst.get fvarId).fvarId!
      pure { mvarId := mvarId, diseqs := diseqs, subst := subst }
 
-end Meta
-end Lean
+end Lean.Meta

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

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -6,8 +7,7 @@ Authors: Leonardo de Moura
 import Lean.Meta.Tactic.Subst
 import Lean.Meta.Tactic.Clear
 
-namespace Lean
-namespace Meta
+namespace Lean.Meta
 
 structure CaseValueSubgoal :=
 (mvarId : MVarId)
@@ -28,37 +28,36 @@ instance CaseValueSubgoal.inhabited : Inhabited CaseValueSubgoal :=
 def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Name := `h) (subst : FVarSubst := {})
     : MetaM (CaseValueSubgoal × CaseValueSubgoal) :=
 withMVarContext mvarId $ do
-  tag ← getMVarTag mvarId;
-  checkNotAssigned mvarId `caseValue;
-  target ← getMVarType mvarId;
-  xEqValue ← mkEq (mkFVar fvarId) value;
-  let xNeqValue := mkApp (mkConst `Not) xEqValue;
-  let thenTarget := Lean.mkForall hName BinderInfo.default xEqValue  target;
-  let elseTarget := Lean.mkForall hName BinderInfo.default xNeqValue target;
-  thenMVar ← mkFreshExprSyntheticOpaqueMVar thenTarget tag;
-  elseMVar ← mkFreshExprSyntheticOpaqueMVar elseTarget tag;
-  val ← mkAppOptM `dite #[none, xEqValue, none, thenMVar, elseMVar];
-  assignExprMVar mvarId val;
-  (elseH, elseMVarId) ← intro1P elseMVar.mvarId!;
-  let elseSubgoal := { mvarId := elseMVarId, newH := elseH, subst := subst : CaseValueSubgoal };
-  (thenH, thenMVarId) ← intro1P thenMVar.mvarId!;
-  let symm   := false;
-  let clearH := false;
-  (thenSubst, thenMVarId) ← substCore thenMVarId thenH symm subst clearH;
-  withMVarContext thenMVarId do {
-    trace! `Meta ("subst domain: " ++ toString thenSubst.domain);
-    let thenH := (thenSubst.get thenH).fvarId!;
-    trace! `Meta "searching for decl";
-    decl ← getLocalDecl thenH;
-    trace! `Meta "found decl"
-  };
-  let thenSubgoal := { mvarId := thenMVarId, newH := (thenSubst.get thenH).fvarId!, subst := thenSubst : CaseValueSubgoal };
+  let tag ← getMVarTag mvarId
+  checkNotAssigned mvarId `caseValue
+  let target ← getMVarType mvarId
+  let xEqValue ← mkEq (mkFVar fvarId) value
+  let xNeqValue := mkApp (mkConst `Not) xEqValue
+  let thenTarget := Lean.mkForall hName BinderInfo.default xEqValue  target
+  let elseTarget := Lean.mkForall hName BinderInfo.default xNeqValue target
+  let thenMVar ← mkFreshExprSyntheticOpaqueMVar thenTarget tag
+  let elseMVar ← mkFreshExprSyntheticOpaqueMVar elseTarget tag
+  let val ← mkAppOptM `dite #[none, xEqValue, none, thenMVar, elseMVar]
+  assignExprMVar mvarId val
+  let (elseH, elseMVarId) ← intro1P elseMVar.mvarId!
+  let elseSubgoal := { mvarId := elseMVarId, newH := elseH, subst := subst : CaseValueSubgoal }
+  let (thenH, thenMVarId) ← intro1P thenMVar.mvarId!
+  let symm   := false
+  let clearH := false
+  let (thenSubst, thenMVarId) ← substCore thenMVarId thenH symm subst clearH
+  withMVarContext thenMVarId do
+    trace[Meta]! "subst domain: {thenSubst.domain}"
+    let thenH := (thenSubst.get thenH).fvarId!
+    trace[Meta]! "searching for decl"
+    let decl ← getLocalDecl thenH
+    trace[Meta]! "found decl"
+  let thenSubgoal := { mvarId := thenMVarId, newH := (thenSubst.get thenH).fvarId!, subst := thenSubst : CaseValueSubgoal }
   pure (thenSubgoal, elseSubgoal)
 
 def caseValue (mvarId : MVarId) (fvarId : FVarId) (value : Expr) : MetaM (CaseValueSubgoal × CaseValueSubgoal) := do
-s ← caseValueAux mvarId fvarId value;
-appendTagSuffix s.1.mvarId `thenBranch;
-appendTagSuffix s.2.mvarId `elseBranch;
+let s ← caseValueAux mvarId fvarId value
+appendTagSuffix s.1.mvarId `thenBranch
+appendTagSuffix s.2.mvarId `elseBranch
 pure s
 
 structure CaseValuesSubgoal :=
@@ -69,23 +68,6 @@ structure CaseValuesSubgoal :=
 instance CaseValueSubgoals.inhabited : Inhabited CaseValuesSubgoal :=
 ⟨{ mvarId := arbitrary _ }⟩
 
-private def caseValuesAux (hNamePrefix : Name) (fvarId : FVarId) : Nat → MVarId → List Expr → Array FVarId → Array CaseValuesSubgoal → MetaM (Array CaseValuesSubgoal)
-| i, mvarId, [],    hs, subgoals => throwTacticEx `caseValues mvarId "list of values must not be empty"
-| i, mvarId, v::vs, hs, subgoals => do
-  (thenSubgoal, elseSubgoal) ← caseValueAux mvarId fvarId v (hNamePrefix.appendIndexAfter i) {};
-  appendTagSuffix thenSubgoal.mvarId ((`case).appendIndexAfter i);
-  thenMVarId ← hs.foldlM
-    (fun thenMVarId h => match thenSubgoal.subst.get h with
-      | Expr.fvar fvarId _ => tryClear thenMVarId fvarId
-      | _                  => pure thenMVarId)
-    thenSubgoal.mvarId;
-  let subgoals := subgoals.push { mvarId := thenMVarId, newHs := #[thenSubgoal.newH], subst := thenSubgoal.subst };
-  match vs with
-  | [] => do
-    appendTagSuffix elseSubgoal.mvarId ((`case).appendIndexAfter (i+1));
-    pure $ subgoals.push { mvarId := elseSubgoal.mvarId, newHs := hs.push elseSubgoal.newH, subst := {} }
-  | _  => caseValuesAux (i+1) elseSubgoal.mvarId vs (hs.push elseSubgoal.newH) subgoals
-
 /--
   Split goal `... |- C x` into values.size + 1 subgoals
   1) `..., (h_1 : x = value[0])  |- C value[0]`
@@ -99,7 +81,22 @@ private def caseValuesAux (hNamePrefix : Name) (fvarId : FVarId) : Nat → MVarI
   Remark: the last subgoal is for the "else" catchall case, and its `subst` is `{}`.
   Remark: the fiels `newHs` has size 1 forall but the last subgoal. -/
 def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNamePrefix := `h) : MetaM (Array CaseValuesSubgoal) :=
-caseValuesAux hNamePrefix fvarId 1 mvarId values.toList #[] #[]
+let rec loop : Nat → MVarId → List Expr → Array FVarId → Array CaseValuesSubgoal → MetaM (Array CaseValuesSubgoal)
+  | i, mvarId, [],    hs, subgoals => throwTacticEx `caseValues mvarId "list of values must not be empty"
+  | i, mvarId, v::vs, hs, subgoals => do
+    let (thenSubgoal, elseSubgoal) ← caseValueAux mvarId fvarId v (hNamePrefix.appendIndexAfter i) {}
+    appendTagSuffix thenSubgoal.mvarId ((`case).appendIndexAfter i)
+    let thenMVarId ← hs.foldlM
+      (fun thenMVarId h => match thenSubgoal.subst.get h with
+        | Expr.fvar fvarId _ => tryClear thenMVarId fvarId
+        | _                  => pure thenMVarId)
+      thenSubgoal.mvarId
+    let subgoals := subgoals.push { mvarId := thenMVarId, newHs := #[thenSubgoal.newH], subst := thenSubgoal.subst }
+    match vs with
+    | [] => do
+      appendTagSuffix elseSubgoal.mvarId ((`case).appendIndexAfter (i+1))
+      pure $ subgoals.push { mvarId := elseSubgoal.mvarId, newHs := hs.push elseSubgoal.newH, subst := {} }
+    | _  => loop (i+1) elseSubgoal.mvarId vs (hs.push elseSubgoal.newH) subgoals
+loop 1 mvarId values.toList #[] #[]
 
-end Meta
-end Lean
+end Lean.Meta

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

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -5,8 +6,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Util.ReplaceExpr
 
-namespace Lean
-namespace Meta
+namespace Lean.Meta
 
 /- A mapping from MVarId to MVarId -/
 structure MVarRenaming :=
@@ -33,5 +33,4 @@ else e.replace $ fun e => match e with
     | some newMVarId => mkMVar newMVarId
   | _ => none
 
-end Meta
-end Lean
+end Lean.Meta

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

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -13,9 +14,7 @@ import Lean.Meta.Match.MVarRenaming
 import Lean.Meta.Match.CaseValues
 import Lean.Meta.Match.CaseArraySizes
 
-namespace Lean
-namespace Meta
-namespace Match
+namespace Lean.Meta.Match
 
 inductive Pattern : Type
 | inaccessible (e : Expr) : Pattern
@@ -30,13 +29,13 @@ namespace Pattern
 instance : Inhabited Pattern := ⟨Pattern.inaccessible (arbitrary _)⟩
 
 partial def toMessageData : Pattern → MessageData
-| inaccessible e         => ".(" ++ e ++ ")"
+| inaccessible e         => msg!".({e})"
 | var varId              => mkFVar varId
 | ctor ctorName _ _ []   => ctorName
-| ctor ctorName _ _ pats => "(" ++ ctorName ++ pats.foldl (fun (msg : MessageData) pat => msg ++ " " ++ toMessageData pat) Format.nil ++ ")"
+| ctor ctorName _ _ pats => msg!"({ctorName}{pats.foldl (fun (msg : MessageData) pat => msg ++ " " ++ toMessageData pat) Format.nil})"
 | val e                  => e
-| arrayLit _ pats        => "#[" ++ MessageData.joinSep (pats.map toMessageData) ", " ++ "]"
-| as varId p             => mkFVar varId ++ "@" ++toMessageData p
+| arrayLit _ pats        => msg!"#[{MessageData.joinSep (pats.map toMessageData) ", "}]"
+| as varId p             => msg!"{mkFVar varId}@{toMessageData p}"
 
 partial def toExpr : Pattern → MetaM Expr
 | inaccessible e                 => pure e
@@ -44,27 +43,27 @@ partial def toExpr : Pattern → MetaM Expr
 | val e                          => pure e
 | as _ p                         => toExpr p
 | arrayLit type xs               => do
-  xs ← xs.mapM toExpr;
+  let xs ← xs.mapM toExpr;
   mkArrayLit type xs
 | ctor ctorName us params fields => do
-  fields ← fields.mapM toExpr;
+  let fields ← fields.mapM toExpr;
   pure $ mkAppN (mkConst ctorName us) (params ++ fields).toArray
 
 /- Apply the free variable substitution `s` to the given pattern -/
 partial def applyFVarSubst (s : FVarSubst) : Pattern → Pattern
 | inaccessible e  => inaccessible $ s.apply e
-| ctor n us ps fs => ctor n us (ps.map s.apply) $ fs.map applyFVarSubst
+| ctor n us ps fs => ctor n us (ps.map s.apply) $ fs.map (applyFVarSubst s)
 | val e           => val $ s.apply e
-| arrayLit t xs   => arrayLit (s.apply t) $ xs.map applyFVarSubst
+| arrayLit t xs   => arrayLit (s.apply t) $ xs.map (applyFVarSubst s)
 | var fvarId      => match s.find? fvarId with
   | some e => inaccessible e
   | none   => var fvarId
 | as fvarId p     => match s.find? fvarId with
-  | none   => as fvarId $ applyFVarSubst p
-  | some _ => applyFVarSubst p
+  | none   => as fvarId $ applyFVarSubst s p
+  | some _ => applyFVarSubst s p
 
 def replaceFVarId (fvarId : FVarId) (v : Expr) (p : Pattern) : Pattern :=
-let s : FVarSubst := {};
+let s : FVarSubst := {}
 p.applyFVarSubst (s.insert fvarId v)
 
 end Pattern
@@ -87,8 +86,8 @@ instance : Inhabited Alt := ⟨⟨arbitrary _, 0, arbitrary _, [], []⟩⟩
 
 partial def toMessageData (alt : Alt) : MetaM MessageData := do
 withExistingLocalDecls alt.fvarDecls do
-  let msg : List MessageData := alt.fvarDecls.map fun d => d.toExpr ++ ":(" ++ d.type ++ ")";
-  let msg : MessageData := msg ++ " |- " ++ (alt.patterns.map Pattern.toMessageData) ++ " => " ++ alt.rhs;
+  let msg : List MessageData := alt.fvarDecls.map fun d => d.toExpr ++ ":(" ++ d.type ++ ")"
+  let msg : MessageData := msg ++ " |- " ++ (alt.patterns.map Pattern.toMessageData) ++ " => " ++ alt.rhs
   addMessageContext msg
 
 def applyFVarSubst (s : FVarSubst) (alt : Alt) : Alt :=
@@ -101,7 +100,7 @@ def replaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : Alt :=
 { alt with
   patterns  := alt.patterns.map fun p => p.replaceFVarId fvarId v,
   fvarDecls :=
-    let decls := alt.fvarDecls.filter fun d => d.fvarId != fvarId;
+    let decls := alt.fvarDecls.filter fun d => d.fvarId != fvarId
     decls.map $ replaceFVarIdAtLocalDecl fvarId v,
   rhs       := alt.rhs.replaceFVarId fvarId v }
 
@@ -151,11 +150,11 @@ def checkAndReplaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : MetaM Alt :
 match alt.fvarDecls.find? fun (fvarDecl : LocalDecl) => fvarDecl.fvarId == fvarId with
 | none          => throwErrorAt alt.ref "unknown free pattern variable"
 | some fvarDecl => do
-  vType ← inferType v;
-  unlessM (isDefEqGuarded fvarDecl.type vType) $
-    withExistingLocalDecls alt.fvarDecls $ throwErrorAt alt.ref $
-      "type mismatch during dependent match-elimination at pattern variable '" ++ mkFVar fvarDecl.fvarId ++ "' with type" ++ indentExpr fvarDecl.type ++
-      Format.line ++ "expected type" ++ indentExpr vType;
+  let vType ← inferType v
+  unless (← isDefEqGuarded fvarDecl.type vType) do
+    withExistingLocalDecls alt.fvarDecls do
+      throwErrorAt alt.ref $
+        msg!"type mismatch during dependent match-elimination at pattern variable '{mkFVar fvarDecl.fvarId}' with type{indentExpr fvarDecl.type}\nexpected type{indentExpr vType}"
   pure $ replaceFVarId fvarId v alt
 
 end Alt
@@ -171,8 +170,8 @@ namespace Example
 
 partial def replaceFVarId (fvarId : FVarId) (ex : Example) : Example → Example
 | var x        => if x == fvarId then ex else var x
-| ctor n exs   => ctor n $ exs.map replaceFVarId
-| arrayLit exs => arrayLit $ exs.map replaceFVarId
+| ctor n exs   => ctor n $ exs.map (replaceFVarId fvarId ex)
+| arrayLit exs => arrayLit $ exs.map (replaceFVarId fvarId ex)
 | ex           => ex
 
 partial def applyFVarSubst (s : FVarSubst) : Example → Example
@@ -180,8 +179,8 @@ partial def applyFVarSubst (s : FVarSubst) : Example → Example
   match s.get fvarId with
   | Expr.fvar fvarId' _ => var fvarId'
   | _                   => underscore
-| ctor n exs   => ctor n $ exs.map applyFVarSubst
-| arrayLit exs => arrayLit $ exs.map applyFVarSubst
+| ctor n exs   => ctor n $ exs.map (applyFVarSubst s)
+| arrayLit exs => arrayLit $ exs.map (applyFVarSubst s)
 | ex           => ex
 
 partial def varsToUnderscore : Example → Example
@@ -218,8 +217,8 @@ instance : Inhabited Problem := ⟨{ mvarId := arbitrary _, vars := [], alts :=
 
 def toMessageData (p : Problem) : MetaM MessageData :=
 withGoalOf p do
-  alts ← p.alts.mapM Alt.toMessageData;
-  vars : List MessageData ← p.vars.mapM fun x => do { xType ← inferType x; pure (x ++ ":(" ++ xType ++ ")" : MessageData) };
+  let alts ← p.alts.mapM Alt.toMessageData
+  let vars : List MessageData ← p.vars.mapM fun x => do let xType ← inferType x; pure (x ++ ":(" ++ xType ++ ")" : MessageData)
   pure $ "remaining variables: " ++ vars
     ++ Format.line ++ "alternatives:" ++ indentD (MessageData.joinSep alts Format.line)
     ++ Format.line ++ "examples: " ++ examplesToMessageData p.examples
@@ -240,30 +239,29 @@ structure MatcherResult :=
 (unusedAltIdxs   : List Nat)
 
 /- The number of patterns in each AltLHS must be equal to majors.length -/
-private def checkNumPatterns (majors : Array Expr) (lhss : List AltLHS) : MetaM Unit :=
-let num := majors.size;
-when (lhss.any (fun lhs => lhs.patterns.length != num)) $
+private def checkNumPatterns (majors : Array Expr) (lhss : List AltLHS) : MetaM Unit := do
+let num := majors.size
+if lhss.any fun lhs => lhs.patterns.length != num then
   throwError "incorrect number of patterns"
 
 private partial def withAltsAux {α} (motive : Expr) : List AltLHS → List Alt → Array (Expr × Nat) → (List Alt → Array (Expr × Nat) → MetaM α) → MetaM α
 | [],        alts, minors, k => k alts.reverse minors
 | lhs::lhss, alts, minors, k => do
-  let xs := lhs.fvarDecls.toArray.map LocalDecl.toExpr;
-  minorType ← withExistingLocalDecls lhs.fvarDecls do {
-    args ← lhs.patterns.toArray.mapM Pattern.toExpr;
-    let minorType := mkAppN motive args;
+  let xs := lhs.fvarDecls.toArray.map LocalDecl.toExpr
+  let minorType ← withExistingLocalDecls lhs.fvarDecls do
+    let args ← lhs.patterns.toArray.mapM Pattern.toExpr
+    let minorType := mkAppN motive args
     mkForallFVars xs minorType
-  };
-  let (minorType, minorNumParams) := if !xs.isEmpty then (minorType, xs.size) else (mkSimpleThunkType minorType, 1);
-  let idx       := alts.length;
-  let minorName := (`h).appendIndexAfter (idx+1);
-  trace! `Meta.Match.debug ("minor premise " ++ minorName ++ " : " ++ minorType);
+  let (minorType, minorNumParams) := if !xs.isEmpty then (minorType, xs.size) else (mkSimpleThunkType minorType, 1)
+  let idx       := alts.length
+  let minorName := (`h).appendIndexAfter (idx+1)
+  trace! `Meta.Match.debug ("minor premise " ++ minorName ++ " : " ++ minorType)
   withLocalDeclD minorName minorType fun minor => do
-    let rhs    := if xs.isEmpty then mkApp minor (mkConst `Unit.unit) else mkAppN minor xs;
-    let minors := minors.push (minor, minorNumParams);
-    fvarDecls ← lhs.fvarDecls.mapM instantiateLocalDeclMVars;
-    let alts   := { ref := lhs.ref, idx := idx, rhs := rhs, fvarDecls := fvarDecls, patterns := lhs.patterns : Alt } :: alts;
-    withAltsAux lhss alts minors k
+    let rhs    := if xs.isEmpty then mkApp minor (mkConst `Unit.unit) else mkAppN minor xs
+    let minors := minors.push (minor, minorNumParams)
+    let fvarDecls ← lhs.fvarDecls.mapM instantiateLocalDeclMVars
+    let alts   := { ref := lhs.ref, idx := idx, rhs := rhs, fvarDecls := fvarDecls, patterns := lhs.patterns : Alt } :: alts
+    withAltsAux motive lhss alts minors k
 
 /- Given a list of `AltLHS`, create a minor premise for each one, convert them into `Alt`, and then execute `k` -/
 private partial def withAlts {α} (motive : Expr) (lhss : List AltLHS) (k : List Alt → Array (Expr × Nat) → MetaM α) : MetaM α :=
@@ -358,41 +356,41 @@ match p.vars with
 | x :: xs => do
   let alts := p.alts.map fun alt => match alt.patterns with
     | Pattern.inaccessible _ :: ps => { alt with patterns := ps }
-    | _       => unreachable!;
+    | _       => unreachable!
   { p with alts := alts, vars := xs }
 
 private def processLeaf (p : Problem) : StateRefT State MetaM Unit :=
 match p.alts with
 | []       => do
-  liftM $ admit p.mvarId;
+  liftM $ admit p.mvarId
   modify fun s => { s with counterExamples := p.examples :: s.counterExamples }
 | alt :: _ => do
   -- TODO: check whether we have unassigned metavars in rhs
-  liftM $ assignGoalOf p alt.rhs;
+  liftM $ assignGoalOf p alt.rhs
   modify fun s => { s with used := s.used.insert alt.idx }
 
 private def processAsPattern (p : Problem) : MetaM Problem :=
 match p.vars with
 | []      => unreachable!
 | x :: xs => withGoalOf p do
-  alts ← p.alts.mapM fun alt => match alt.patterns with
+  let alts ← p.alts.mapM fun alt => match alt.patterns with
     | Pattern.as fvarId p :: ps => { alt with patterns := p :: ps }.checkAndReplaceFVarId fvarId x
-    | _                         => pure alt;
+    | _                         => pure alt
   pure { p with alts := alts }
 
 private def processVariable (p : Problem) : MetaM Problem :=
 match p.vars with
 | []      => unreachable!
 | x :: xs => withGoalOf p do
-  alts ← p.alts.mapM fun alt => match alt.patterns with
+  let alts ← p.alts.mapM fun alt => match alt.patterns with
     | Pattern.inaccessible _ :: ps => pure { alt with patterns := ps }
     | Pattern.var fvarId :: ps     => { alt with patterns := ps }.checkAndReplaceFVarId fvarId x
-    | _                            => unreachable!;
+    | _                            => unreachable!
   pure { p with alts := alts, vars := xs }
 
 private def throwInductiveTypeExpected {α} (e : Expr) : MetaM α := do
-t ← inferType e;
-throwError ("failed to compile pattern matching, inductive type expected" ++ indentExpr e ++ Format.line ++ "has type" ++ indentExpr t)
+let t ← inferType e
+throwError! "failed to compile pattern matching, inductive type expected{indentExpr e}\nhas type{indentExpr t}"
 
 private def inLocalDecls (localDecls : List LocalDecl) (fvarId : FVarId) : Bool :=
 localDecls.any fun d => d.fvarId == fvarId
@@ -408,39 +406,39 @@ structure State :=
 abbrev M := ReaderT Context $ StateRefT State MetaM
 
 def isAltVar (fvarId : FVarId) : M Bool := do
-ctx ← read;
+let ctx ← read
 pure $ inLocalDecls ctx.altFVarDecls fvarId
 
 def expandIfVar (e : Expr) : M Expr := do
 match e with
-| Expr.fvar _ _ => do s ← get; pure $ s.fvarSubst.apply e
-| _             => pure e
+| Expr.fvar _ _ => return (← get).fvarSubst.apply e
+| _             => return e
 
 def occurs (fvarId : FVarId) (v : Expr) : Bool :=
 (v.find? fun e => match e with
    | Expr.fvar fvarId' _ => fvarId == fvarId'
    | _=> false).isSome
 
-def assign (fvarId : FVarId) (v : Expr) : M Bool :=
-if occurs fvarId v then do
-  trace! `Meta.Match.unify ("assign occurs check failed, " ++ mkFVar fvarId ++ " := " ++ v);
+def assign (fvarId : FVarId) (v : Expr) : M Bool := do
+if occurs fvarId v then
+  trace[Meta.Match.unify]! "assign occurs check failed, {mkFVar fvarId} := {v}"
   pure false
-else do
-  ctx ← read;
-  condM (isAltVar fvarId)
-    (do
-      trace! `Meta.Match.unify (mkFVar fvarId ++ " := " ++ v);
-      modify fun s => { s with fvarSubst := s.fvarSubst.insert fvarId v }; pure true)
-    (do
-      trace! `Meta.Match.unify ("assign failed variable is not local, " ++ mkFVar fvarId ++ " := " ++ v);
-      pure false)
+else
+  let ctx ← read
+  if (← isAltVar fvarId) then
+    trace[Meta.Match.unify]! "{mkFVar fvarId} := {v}"
+    modify fun s => { s with fvarSubst := s.fvarSubst.insert fvarId v }
+    pure true
+  else
+    trace! `Meta.Match.unify ("assign failed variable is not local, " ++ mkFVar fvarId ++ " := " ++ v)
+    pure false
 
 partial def unify : Expr → Expr → M Bool
 | a, b => do
-  trace! `Meta.Match.unify (a ++ " =?= " ++ b);
+  trace! `Meta.Match.unify (a ++ " =?= " ++ b)
   condM (isDefEq a b) (pure true) do
-  a' ← expandIfVar a;
-  b' ← expandIfVar b;
+  let a' ← expandIfVar a
+  let b' ← expandIfVar b
   if a != a' || b != b' then unify a' b'
   else match a, b with
     | Expr.mdata _ a _, b                      => unify a b
@@ -450,57 +448,57 @@ partial def unify : Expr → Expr → M Bool
     | a, Expr.fvar bFVarId _ => assign bFVarId a
     | Expr.app aFn aArg _, Expr.app bFn bArg _ => unify aFn bFn <&&> unify aArg bArg
     | _, _ => do
-      trace! `Meta.Match.unify ("unify failed @" ++ a ++ " =?= " ++ b);
+      trace! `Meta.Match.unify ("unify failed @" ++ a ++ " =?= " ++ b)
       pure false
 
 end Unify
 
 private def unify? (altFVarDecls : List LocalDecl) (a b : Expr) : MetaM (Option FVarSubst) := do
-a ← instantiateMVars a;
-b ← instantiateMVars b;
-(b, s) ← (Unify.unify a b { altFVarDecls := altFVarDecls}).run {};
+let a ← instantiateMVars a
+let b ← instantiateMVars b
+let (b, s) ← (Unify.unify a b { altFVarDecls := altFVarDecls}).run {}
 if b then pure s.fvarSubst else pure none
 
 private def expandVarIntoCtor? (alt : Alt) (fvarId : FVarId) (ctorName : Name) : MetaM (Option Alt) :=
 withExistingLocalDecls alt.fvarDecls do
-  env ← getEnv;
-  ldecl ← getLocalDecl fvarId;
-  expectedType ← inferType (mkFVar fvarId);
-  expectedType ← whnfD expectedType;
-  (ctorLevels, ctorParams) ← getInductiveUniverseAndParams expectedType;
-  let ctor := mkAppN (mkConst ctorName ctorLevels) ctorParams;
-  ctorType ← inferType ctor;
+  let env ← getEnv
+  let ldecl ← getLocalDecl fvarId
+  let expectedType ← inferType (mkFVar fvarId)
+  let expectedType ← whnfD expectedType
+  let (ctorLevels, ctorParams) ← getInductiveUniverseAndParams expectedType
+  let ctor := mkAppN (mkConst ctorName ctorLevels) ctorParams
+  let ctorType ← inferType ctor
   forallTelescopeReducing ctorType fun ctorFields resultType => do
-    let ctor := mkAppN ctor ctorFields;
-    let alt  := alt.replaceFVarId fvarId ctor;
-    ctorFieldDecls ← ctorFields.mapM fun ctorField => getLocalDecl ctorField.fvarId!;
-    let newAltDecls := ctorFieldDecls.toList ++ alt.fvarDecls;
-    subst? ← unify? newAltDecls resultType expectedType;
+    let ctor := mkAppN ctor ctorFields
+    let alt  := alt.replaceFVarId fvarId ctor
+    let ctorFieldDecls ← ctorFields.mapM fun ctorField => getLocalDecl ctorField.fvarId!
+    let newAltDecls := ctorFieldDecls.toList ++ alt.fvarDecls
+    let subst? ← unify? newAltDecls resultType expectedType
     match subst? with
     | none       => pure none
     | some subst => do
-      let newAltDecls := newAltDecls.filter fun d => !subst.contains d.fvarId; -- remove declarations that were assigned
-      let newAltDecls := newAltDecls.map fun d => d.applyFVarSubst subst; -- apply substitution to remaining declaration types
-      let patterns    := alt.patterns.map fun p => p.applyFVarSubst subst;
-      let rhs         := subst.apply alt.rhs;
+      let newAltDecls := newAltDecls.filter fun d => !subst.contains d.fvarId -- remove declarations that were assigned
+      let newAltDecls := newAltDecls.map fun d => d.applyFVarSubst subst -- apply substitution to remaining declaration types
+      let patterns    := alt.patterns.map fun p => p.applyFVarSubst subst
+      let rhs         := subst.apply alt.rhs
       let ctorFieldPatterns := ctorFields.toList.map fun ctorField => match subst.get ctorField.fvarId! with
         | e@(Expr.fvar fvarId _) => if inLocalDecls newAltDecls fvarId then Pattern.var fvarId else Pattern.inaccessible e
-        | e                      => Pattern.inaccessible e;
+        | e                      => Pattern.inaccessible e
       pure $ some { alt with fvarDecls := newAltDecls, rhs := rhs, patterns := ctorFieldPatterns ++ patterns }
 
 private def getInductiveVal? (x : Expr) : MetaM (Option InductiveVal) := do
-xType ← inferType x;
-xType ← whnfD xType;
+let xType ← inferType x
+let xType ← whnfD xType
 match xType.getAppFn with
 | Expr.const constName _ _ => do
-  cinfo ← getConstInfo constName;
+  let cinfo ← getConstInfo constName
   match cinfo with
   | ConstantInfo.inductInfo val => pure (some val)
   | _ => pure none
 | _ => pure none
 
 private def hasRecursiveType (x : Expr) : MetaM Bool := do
-val? ← getInductiveVal? x;
+let val? ← getInductiveVal? x
 match val? with
 | some val => pure val.isRec
 | _        => pure false
@@ -512,102 +510,96 @@ match val? with
    update the next patterns with the fields of the constructor.
    Otherwise, return none. -/
 def processInaccessibleAsCtor (alt : Alt) (ctorName : Name) : MetaM (Option Alt) := do
-env ← getEnv;
+let env ← getEnv
 match alt.patterns with
 | p@(Pattern.inaccessible e) :: ps => do
-  trace! `Meta.Match.match ("inaccessible in ctor step " ++ e);
+  trace! `Meta.Match.match ("inaccessible in ctor step " ++ e)
   withExistingLocalDecls alt.fvarDecls do
     -- Try to push inaccessible annotations.
-    e ← whnfD e;
+    let e ← whnfD e
     match e.constructorApp? env with
     | some (ctorVal, ctorArgs) => do
       if ctorVal.name == ctorName then
-        let fields := ctorArgs.extract ctorVal.nparams ctorArgs.size;
-        let fields := fields.toList.map Pattern.inaccessible;
+        let fields := ctorArgs.extract ctorVal.nparams ctorArgs.size
+        let fields := fields.toList.map Pattern.inaccessible
         pure $ some { alt with patterns := fields ++ ps }
       else
         pure none
-    | _ => throwErrorAt alt.ref $
-      "dependent match elimination failed, inaccessible pattern found " ++ indentD p.toMessageData ++
-      Format.line ++ "constructor expected"
+    | _ => throwErrorAt! alt.ref "dependent match elimination failed, inaccessible pattern found{indentD p.toMessageData}\nconstructor expected"
 | _ => unreachable!
 
 private def processConstructor (p : Problem) : MetaM (Array Problem) := do
-trace! `Meta.Match.match ("constructor step");
-env ← getEnv;
+trace! `Meta.Match.match ("constructor step")
+let env ← getEnv
 match p.vars with
 | []      => unreachable!
 | x :: xs => do
-  subgoals? ← commitWhenSome? do {
-     subgoals ← cases p.mvarId x.fvarId!;
+  let subgoals? ← commitWhenSome? do
+     let subgoals ← cases p.mvarId x.fvarId!
      if subgoals.isEmpty then
        /- Easy case: we have solved problem `p` since there are no subgoals -/
        pure (some #[])
      else if !p.alts.isEmpty then
        pure (some subgoals)
      else do
-       isRec ← withGoalOf p $ hasRecursiveType x;
+       let isRec ← withGoalOf p $ hasRecursiveType x
         /- If there are no alternatives and the type of the current variable is recursive, we do NOT consider
           a constructor-transition to avoid nontermination.
           TODO: implement a more general approach if this is not sufficient in practice -/
        if isRec then pure none
        else pure (some subgoals)
-  };
   match subgoals? with
   | none          => pure #[{ p with vars := xs }]
-  | some subgoals => do
+  | some subgoals =>
     subgoals.mapM fun subgoal => withMVarContext subgoal.mvarId do
-      let subst    := subgoal.subst;
-      let fields   := subgoal.fields.toList;
-      let newVars  := fields ++ xs;
-      let newVars  := newVars.map fun x => x.applyFVarSubst subst;
+      let subst    := subgoal.subst
+      let fields   := subgoal.fields.toList
+      let newVars  := fields ++ xs
+      let newVars  := newVars.map fun x => x.applyFVarSubst subst
       let subex    := Example.ctor subgoal.ctorName $ fields.map fun field => match field with
         | Expr.fvar fvarId _ => Example.var fvarId
-        | _                  => Example.underscore; -- This case can happen due to dependent elimination
-      let examples := p.examples.map $ Example.replaceFVarId x.fvarId! subex;
-      let examples := examples.map $ Example.applyFVarSubst subst;
+        | _                  => Example.underscore -- This case can happen due to dependent elimination
+      let examples := p.examples.map $ Example.replaceFVarId x.fvarId! subex
+      let examples := examples.map $ Example.applyFVarSubst subst
       let newAlts  := p.alts.filter fun alt => match alt.patterns with
         | Pattern.ctor n _ _ _ :: _    => n == subgoal.ctorName
         | Pattern.var _ :: _           => true
         | Pattern.inaccessible _ :: _  => true
-        | _                            => false;
-      let newAlts  := newAlts.map fun alt => alt.applyFVarSubst subst;
-      newAlts ← newAlts.filterMapM fun alt => match alt.patterns with
+        | _                            => false
+      let newAlts  := newAlts.map fun alt => alt.applyFVarSubst subst
+      let newAlts ← newAlts.filterMapM fun alt => match alt.patterns with
         | Pattern.ctor _ _ _ fields :: ps  => pure $ some { alt with patterns := fields ++ ps }
         | Pattern.var fvarId :: ps         => expandVarIntoCtor? { alt with patterns := ps } fvarId subgoal.ctorName
         | Pattern.inaccessible _ :: _      => processInaccessibleAsCtor alt subgoal.ctorName
-        | _                                => unreachable!;
+        | _                                => unreachable!
       pure { mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
 
 private def processNonVariable (p : Problem) : MetaM Problem :=
 match p.vars with
 | []      => unreachable!
 | x :: xs => withGoalOf p do
-  x ← whnfD x;
-  env ← getEnv;
+  let x ← whnfD x
+  let env ← getEnv
   match x.constructorApp? env with
   | some (ctorVal, xArgs) => do
-    alts ← p.alts.filterMapM fun alt => match alt.patterns with
+    let alts ← p.alts.filterMapM fun alt => match alt.patterns with
       | Pattern.ctor n _ _ fields :: ps   =>
         if n != ctorVal.name then
           pure none
         else
           pure $ some { alt with patterns := fields ++ ps }
       | Pattern.inaccessible _ :: _ => processInaccessibleAsCtor alt ctorVal.name
-      | p :: _  => throwError ("failed to compile pattern matching, inaccessible pattern or constructor expected" ++ indentD p.toMessageData)
-      | _       => unreachable!;
-    let xFields := xArgs.extract ctorVal.nparams xArgs.size;
+      | p :: _  => throwError! "failed to compile pattern matching, inaccessible pattern or constructor expected{indentD p.toMessageData}"
+      | _       => unreachable!
+    let xFields := xArgs.extract ctorVal.nparams xArgs.size
     pure { p with alts := alts, vars := xFields.toList ++ xs }
-  | none =>
-    throwError ("failed to compile pattern matching, constructor expected" ++ indentExpr x)
+  | none => throwError! "failed to compile pattern matching, constructor expected{indentExpr x}"
 
 private def collectValues (p : Problem) : Array Expr :=
-p.alts.foldl
-  (fun (values : Array Expr) alt =>
-    match alt.patterns with
-    | Pattern.val v :: _ => if values.contains v then values else values.push v
-    | _                  => values)
-  #[]
+p.alts.foldl (init := #[]) fun values alt =>
+  match alt.patterns with
+  | Pattern.val v :: _ => if values.contains v then values else values.push v
+  | _                  => values
 
 private def isFirstPatternVar (alt : Alt) : Bool :=
 match alt.patterns with
@@ -615,98 +607,96 @@ match alt.patterns with
 | _                  => false
 
 private def processValue (p : Problem) : MetaM (Array Problem) := do
-trace! `Meta.Match.match ("value step");
+trace[Meta.Match.match]! "value step"
 match p.vars with
 | []      => unreachable!
 | x :: xs => do
-  let values := collectValues p;
-  subgoals ← caseValues p.mvarId x.fvarId! values;
+  let values := collectValues p
+  let subgoals ← caseValues p.mvarId x.fvarId! values
   subgoals.mapIdxM fun i subgoal =>
     if h : i < values.size then do
-      let value := values.get ⟨i, h⟩;
+      let value := values.get ⟨i, h⟩
       -- (x = value) branch
-      let subst := subgoal.subst;
-      let examples := p.examples.map $ Example.replaceFVarId x.fvarId! (Example.val value);
-      let examples := examples.map $ Example.applyFVarSubst subst;
+      let subst := subgoal.subst
+      let examples := p.examples.map $ Example.replaceFVarId x.fvarId! (Example.val value)
+      let examples := examples.map $ Example.applyFVarSubst subst
       let newAlts  := p.alts.filter fun alt => match alt.patterns with
         | Pattern.val v :: _ => v == value
         | Pattern.var _ :: _ => true
-        | _                  => false;
-      let newAlts := newAlts.map fun alt => alt.applyFVarSubst subst;
+        | _                  => false
+      let newAlts := newAlts.map fun alt => alt.applyFVarSubst subst
       let newAlts := newAlts.map fun alt => match alt.patterns with
         | Pattern.val _ :: ps      => { alt with patterns := ps }
         | Pattern.var fvarId :: ps => do
-          let alt := { alt with patterns := ps };
+          let alt := { alt with patterns := ps }
           alt.replaceFVarId fvarId value
-        | _  => unreachable!;
-      let newVars := xs.map fun x => x.applyFVarSubst subst;
+        | _  => unreachable!
+      let newVars := xs.map fun x => x.applyFVarSubst subst
       pure { mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
     else do
       -- else branch
-      let newAlts := p.alts.filter isFirstPatternVar;
+      let newAlts := p.alts.filter isFirstPatternVar
       pure { p with mvarId := subgoal.mvarId, alts := newAlts, vars := x::xs }
 
 private def collectArraySizes (p : Problem) : Array Nat :=
-p.alts.foldl
-  (fun (sizes : Array Nat) alt =>
-    match alt.patterns with
-    | Pattern.arrayLit _ ps :: _ => let sz := ps.length; if sizes.contains sz then sizes else sizes.push sz
-    | _                          => sizes)
-  #[]
-
-private def expandVarIntoArrayLitAux (alt : Alt) (fvarId : FVarId) (arrayElemType : Expr) (varNamePrefix : Name) : Nat → Array Expr → MetaM Alt
-| n+1, newVars =>
-  withLocalDeclD (varNamePrefix.appendIndexAfter (n+1)) arrayElemType fun x =>
-    expandVarIntoArrayLitAux n (newVars.push x)
-| 0, newVars => do
-  arrayLit ← mkArrayLit arrayElemType newVars.toList;
-  let alt := alt.replaceFVarId fvarId arrayLit;
-  newDecls ← newVars.toList.mapM fun newVar => getLocalDecl newVar.fvarId!;
-  let newPatterns := newVars.toList.map fun newVar => Pattern.var newVar.fvarId!;
-  pure { alt with fvarDecls := newDecls ++ alt.fvarDecls, patterns := newPatterns ++ alt.patterns }
+p.alts.foldl (init := #[]) fun sizes alt =>
+  match alt.patterns with
+  | Pattern.arrayLit _ ps :: _ => let sz := ps.length; if sizes.contains sz then sizes else sizes.push sz
+  | _                          => sizes
 
 private def expandVarIntoArrayLit (alt : Alt) (fvarId : FVarId) (arrayElemType : Expr) (arraySize : Nat) : MetaM Alt :=
 withExistingLocalDecls alt.fvarDecls do
-  fvarDecl ← getLocalDecl fvarId;
-  expandVarIntoArrayLitAux alt fvarId arrayElemType fvarDecl.userName arraySize #[]
+  let fvarDecl ← getLocalDecl fvarId
+  let varNamePrefix := fvarDecl.userName
+  let rec loop
+  | n+1, newVars =>
+    withLocalDeclD (varNamePrefix.appendIndexAfter (n+1)) arrayElemType fun x =>
+      loop n (newVars.push x)
+  | 0, newVars => do
+    let arrayLit ← mkArrayLit arrayElemType newVars.toList
+    let alt := alt.replaceFVarId fvarId arrayLit
+    let newDecls ← newVars.toList.mapM fun newVar => getLocalDecl newVar.fvarId!
+    let newPatterns := newVars.toList.map fun newVar => Pattern.var newVar.fvarId!
+    pure { alt with fvarDecls := newDecls ++ alt.fvarDecls, patterns := newPatterns ++ alt.patterns }
+  loop arraySize #[]
 
 private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
-trace! `Meta.Match.match ("array literal step");
+trace! `Meta.Match.match ("array literal step")
 match p.vars with
 | []      => unreachable!
 | x :: xs => do
-  let sizes := collectArraySizes p;
-  subgoals ← caseArraySizes p.mvarId x.fvarId! sizes;
+  let sizes := collectArraySizes p
+  let subgoals ← caseArraySizes p.mvarId x.fvarId! sizes
   subgoals.mapIdxM fun i subgoal =>
     if h : i < sizes.size then do
-      let size     := sizes.get! i;
-      let subst    := subgoal.subst;
-      let elems    := subgoal.elems.toList;
-      let newVars  := elems.map mkFVar ++ xs;
-      let newVars  := newVars.map fun x => x.applyFVarSubst subst;
-      let subex    := Example.arrayLit $ elems.map Example.var;
-      let examples := p.examples.map $ Example.replaceFVarId x.fvarId! subex;
-      let examples := examples.map $ Example.applyFVarSubst subst;
+      let size     := sizes.get! i
+      let subst    := subgoal.subst
+      let elems    := subgoal.elems.toList
+      let newVars  := elems.map mkFVar ++ xs
+      let newVars  := newVars.map fun x => x.applyFVarSubst subst
+      let subex    := Example.arrayLit $ elems.map Example.var
+      let examples := p.examples.map $ Example.replaceFVarId x.fvarId! subex
+      let examples := examples.map $ Example.applyFVarSubst subst
       let newAlts  := p.alts.filter fun alt => match alt.patterns with
         | Pattern.arrayLit _ ps :: _ => ps.length == size
         | Pattern.var _ :: _         => true
-        | _                          => false;
-      let newAlts := newAlts.map fun alt => alt.applyFVarSubst subst;
+        | _                          => false
+      let newAlts := newAlts.map fun alt => alt.applyFVarSubst subst
       newAlts ← newAlts.mapM fun alt => match alt.patterns with
         | Pattern.arrayLit _ pats :: ps => pure { alt with patterns := pats ++ ps }
-        | Pattern.var fvarId :: ps      => do α ← getArrayArgType x; expandVarIntoArrayLit { alt with patterns := ps } fvarId α size
-        | _  => unreachable!;
+        | Pattern.var fvarId :: ps      => do let α ← getArrayArgType x; expandVarIntoArrayLit { alt with patterns := ps } fvarId α size
+        | _  => unreachable!
       pure { mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
     else do
       -- else branch
-      let newAlts := p.alts.filter isFirstPatternVar;
+      let newAlts := p.alts.filter isFirstPatternVar
       pure { p with mvarId := subgoal.mvarId, alts := newAlts, vars := x::xs }
 
 private def expandNatValuePattern (p : Problem) : Problem := do
 let alts := p.alts.map fun alt => match alt.patterns with
   | Pattern.val (Expr.lit (Literal.natVal 0) _) :: ps     => { alt with patterns := Pattern.ctor `Nat.zero [] [] [] :: ps }
   | Pattern.val (Expr.lit (Literal.natVal (n+1)) _) :: ps => { alt with patterns := Pattern.ctor `Nat.succ [] [] [Pattern.val (mkNatLit n)] :: ps }
-  | _                                                     => alt;
+  | _                                                     => alt
 { p with alts := alts }
 
 private def traceStep (msg : String) : StateRefT State MetaM Unit :=
@@ -717,45 +707,45 @@ withGoalOf p (traceM `Meta.Match.match p.toMessageData)
 
 private def throwNonSupported (p : Problem) : MetaM Unit :=
 withGoalOf p do
-  msg ← p.toMessageData;
-  throwError ("failed to compile pattern matching, stuck at" ++ (indentD msg))
+  let msg ← p.toMessageData
+  throwError! "failed to compile pattern matching, stuck at{indentD msg}"
 
 def isCurrVarInductive (p : Problem) : MetaM Bool := do
 match p.vars with
 | []   => pure false
 | x::_ => withGoalOf p do
-  val? ← getInductiveVal? x;
+  let val? ← getInductiveVal? x
   pure val?.isSome
 
 private partial def process : Problem → StateRefT State MetaM Unit
 | p => withIncRecDepth do
-  liftM $ traceState p;
-  isInductive ← liftM $ isCurrVarInductive p;
+  liftM $ traceState p
+  let isInductive ← liftM $ isCurrVarInductive p
   if isDone p then
     processLeaf p
   else if hasAsPattern p then do
-    traceStep ("as-pattern");
-    p ← liftM $ processAsPattern p;
+    traceStep ("as-pattern")
+    let p ← liftM $ processAsPattern p
     process p
   else if isNatValueTransition p then do
-    traceStep ("nat value to constructor");
+    traceStep ("nat value to constructor")
     process (expandNatValuePattern p)
   else if !isNextVar p then do
-    traceStep ("non variable");
-    p ← liftM $ processNonVariable p;
+    traceStep ("non variable")
+    let p ← liftM $ processNonVariable p
     process p
   else if isInductive && isConstructorTransition p then do
-    ps ← liftM $ processConstructor p;
+    let ps ← liftM $ processConstructor p
     ps.forM process
   else if isVariableTransition p then do
-    traceStep ("variable");
-    p ← liftM $ processVariable p;
+    traceStep ("variable")
+    let p ← liftM $ processVariable p
     process p
   else if isValueTransition p then do
-    ps ← liftM $ processValue p;
+    let ps ← liftM $ processValue p
     ps.forM process
   else if isArrayLitTransition p then do
-    ps ← liftM $ processArrayLit p;
+    let ps ← liftM $ processArrayLit p
     ps.forM process
   else
     liftM $ throwNonSupported p
@@ -829,36 +819,36 @@ where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition.
 -/
 def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss : List AltLHS) : MetaM MatcherResult :=
 forallBoundedTelescope matchType numDiscrs fun majors matchTypeBody => do
-checkNumPatterns majors lhss;
+checkNumPatterns majors lhss
 /- We generate an matcher that can eliminate using different motives with different universe levels.
    `uElim` is the universe level the caller wants to eliminate to.
    If it is not levelZero, we create a matcher that can eliminate in any universe level.
    This is useful for implementing `MatcherApp.addArg` because it may have to change the universe level. -/
-uElim ← getLevel matchTypeBody;
-uElimGen ← if uElim == levelZero then pure levelZero else mkFreshLevelMVar;
-motiveType ← mkForallFVars majors (mkSort uElimGen);
+let uElim ← getLevel matchTypeBody
+let uElimGen ← if uElim == levelZero then pure levelZero else mkFreshLevelMVar
+let motiveType ← mkForallFVars majors (mkSort uElimGen)
 withLocalDeclD `motive motiveType fun motive => do
-trace! `Meta.Match.debug ("motiveType: " ++ motiveType);
-let mvarType  := mkAppN motive majors;
-trace! `Meta.Match.debug ("target: " ++ mvarType);
+trace! `Meta.Match.debug ("motiveType: " ++ motiveType)
+let mvarType  := mkAppN motive majors
+trace! `Meta.Match.debug ("target: " ++ mvarType)
 withAlts motive lhss fun alts minors => do
-  mvar ← mkFreshExprMVar mvarType;
-  let examples := majors.toList.map fun major => Example.var major.fvarId!;
-  (_, s) ← (process { mvarId := mvar.mvarId!, vars := majors.toList, alts := alts, examples := examples }).run {};
-  let args := #[motive] ++ majors ++ minors.map Prod.fst;
-  type ← mkForallFVars args mvarType;
-  val  ← mkLambdaFVars args mvar;
-  trace! `Meta.Match.debug ("matcher value: " ++ val ++ "\ntype: " ++ type);
-  matcher ← mkAuxDefinition matcherName type val;
-  trace! `Meta.Match.debug ("matcher levels: " ++ toString matcher.getAppFn.constLevels! ++ ", uElim: " ++ toString uElimGen);
-  uElimPos? ← getUElimPos? matcher.getAppFn.constLevels! uElimGen;
-  isLevelDefEq uElimGen uElim;
-  addMatcherInfo matcherName { numParams := matcher.getAppNumArgs, numDiscrs := numDiscrs, altNumParams := minors.map Prod.snd, uElimPos? := uElimPos? };
-  setInlineAttribute matcherName;
-  trace! `Meta.Match.debug ("matcher: " ++ matcher);
+  let mvar ← mkFreshExprMVar mvarType
+  let examples := majors.toList.map fun major => Example.var major.fvarId!
+  let (_, s) ← (process { mvarId := mvar.mvarId!, vars := majors.toList, alts := alts, examples := examples }).run {}
+  let args := #[motive] ++ majors ++ minors.map Prod.fst
+  let type ← mkForallFVars args mvarType
+  let val  ← mkLambdaFVars args mvar
+  trace! `Meta.Match.debug ("matcher value: " ++ val ++ "\ntype: " ++ type)
+  let matcher ← mkAuxDefinition matcherName type val
+  trace! `Meta.Match.debug ("matcher levels: " ++ toString matcher.getAppFn.constLevels! ++ ", uElim: " ++ toString uElimGen)
+  let uElimPos? ← getUElimPos? matcher.getAppFn.constLevels! uElimGen
+  isLevelDefEq uElimGen uElim
+  addMatcherInfo matcherName { numParams := matcher.getAppNumArgs, numDiscrs := numDiscrs, altNumParams := minors.map Prod.snd, uElimPos? := uElimPos? }
+  setInlineAttribute matcherName
+  trace! `Meta.Match.debug ("matcher: " ++ matcher)
   let unusedAltIdxs : List Nat := lhss.length.fold
     (fun i r => if s.used.contains i then r else i::r)
-    [];
+    []
   pure { matcher := matcher, counterExamples := s.counterExamples, unusedAltIdxs := unusedAltIdxs.reverse }
 
 end Match
@@ -866,11 +856,11 @@ end Match
 export Match (MatcherInfo)
 
 def getMatcherInfo? (declName : Name) : MetaM (Option MatcherInfo) := do
-env ← getEnv;
+let env ← getEnv
 pure $ Match.Extension.getMatcherInfo? env declName
 
 def isMatcher (declName : Name) : MetaM Bool := do
-info? ← getMatcherInfo? declName;
+let info? ← getMatcherInfo? declName
 pure info?.isSome
 
 structure MatcherApp :=
@@ -887,8 +877,8 @@ structure MatcherApp :=
 def matchMatcherApp? (e : Expr) : MetaM (Option MatcherApp) :=
 match e.getAppFn with
 | Expr.const declName declLevels _ => do
-  some info ← getMatcherInfo? declName | pure none;
-  let args := e.getAppArgs;
+  let some info ← getMatcherInfo? declName | pure none
+  let args := e.getAppArgs
   if args.size < info.numParams + 1 + info.numDiscrs + info.numAlts then pure none
   else
     pure $ some {
@@ -905,28 +895,27 @@ match e.getAppFn with
 | _ => pure none
 
 def MatcherApp.toExpr (matcherApp : MatcherApp) : Expr :=
-let result := mkAppN (mkConst matcherApp.matcherName matcherApp.matcherLevels.toList) matcherApp.params;
-let result := mkApp result matcherApp.motive;
-let result := mkAppN result matcherApp.discrs;
-let result := mkAppN result matcherApp.alts;
+let result := mkAppN (mkConst matcherApp.matcherName matcherApp.matcherLevels.toList) matcherApp.params
+let result := mkApp result matcherApp.motive
+let result := mkAppN result matcherApp.discrs
+let result := mkAppN result matcherApp.alts
 mkAppN result matcherApp.remaining
 
 /- Auxiliary function for MatcherApp.addArg -/
 private partial def updateAlts : Expr → Array Nat → Array Expr → Nat → MetaM (Array Nat × Array Expr)
 | typeNew, altNumParams, alts, i =>
   if h : i < alts.size then do
-    let alt       := alts.get ⟨i, h⟩;
-    let numParams := altNumParams.get! i;
-    typeNew ← whnfD typeNew;
+    let alt       := alts.get ⟨i, h⟩
+    let numParams := altNumParams.get! i
+    let typeNew ← whnfD typeNew
     match typeNew with
     | Expr.forallE n d b _ => do
-      alt ← forallBoundedTelescope d (some numParams) fun xs d => do {
-        alt ← catch (instantiateLambda alt xs) (fun _ => throwError "unexpected matcher application, insufficient number of parameters in alternative");
+      let alt ← forallBoundedTelescope d (some numParams) fun xs d => do
+        let alt ← try instantiateLambda alt xs catch _ => throwError "unexpected matcher application, insufficient number of parameters in alternative"
         forallBoundedTelescope d (some 1) fun x d => do
-          alt ← mkLambdaFVars x alt; -- x is the new argument we are adding to the alternative
-          alt ← mkLambdaFVars xs alt;
+          let alt ← mkLambdaFVars x alt -- x is the new argument we are adding to the alternative
+          let alt ← mkLambdaFVars xs alt
           pure alt
-      };
       updateAlts (b.instantiate1 alt) (altNumParams.set! i (numParams+1)) (alts.set ⟨i, h⟩ alt) (i+1)
     | _ => throwError "unexpected type at MatcherApp.addArg"
   else
@@ -944,36 +933,35 @@ private partial def updateAlts : Expr → Array Nat → Array Expr → Nat → M
 -/
 def MatcherApp.addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp :=
 lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do
-  unless (motiveArgs.size == matcherApp.discrs.size) $
+  unless motiveArgs.size == matcherApp.discrs.size do
     -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`.
-    throwError ("unexpected matcher application, motive must be lambda expression with #" ++ toString matcherApp.discrs.size ++ " arguments");
-  eType ← inferType e;
-  eTypeAbst ← matcherApp.discrs.size.foldRevM
+    throwError! "unexpected matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments"
+  let eType ← inferType e
+  let eTypeAbst ← matcherApp.discrs.size.foldRevM
     (fun i eTypeAbst => do
-      let motiveArg := motiveArgs.get! i;
-      let discr     := matcherApp.discrs.get! i;
-      eTypeAbst ← kabstract eTypeAbst discr;
+      let motiveArg := motiveArgs.get! i
+      let discr     := matcherApp.discrs.get! i
+      eTypeAbst ← kabstract eTypeAbst discr
       pure $ eTypeAbst.instantiate1 motiveArg)
-    eType;
-  motiveBody ← mkArrow eTypeAbst motiveBody;
-  matcherLevels ← match matcherApp.uElimPos? with
+    eType
+  let motiveBody ← mkArrow eTypeAbst motiveBody
+  let matcherLevels ← match matcherApp.uElimPos? with
     | none     => pure matcherApp.matcherLevels
-    | some pos => do {
-      uElim ← getLevel motiveBody;
+    | some pos => do
+      let uElim ← getLevel motiveBody
       pure $ matcherApp.matcherLevels.set! pos uElim
-    };
-  motive ← mkLambdaFVars motiveArgs motiveBody;
+  let motive ← mkLambdaFVars motiveArgs motiveBody
   -- Construct `aux` `match_i As (fun xs => B[xs] → motive[xs]) discrs`, and infer its type `auxType`.
   -- We use `auxType` to infer the type `B[C_i[ys_i]]` of the new argument in each alternative.
-  let aux := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) matcherApp.params;
-  let aux := mkApp aux motive;
-  let aux := mkAppN aux matcherApp.discrs;
-  trace! `Meta.debug aux;
-  check aux;
-  unlessM (isTypeCorrect aux) $
-    throwError "failed to add argument to matcher application, type error when constructing the new motive";
-  auxType ← inferType aux;
-  (altNumParams, alts) ← updateAlts auxType matcherApp.altNumParams matcherApp.alts 0;
+  let aux := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) matcherApp.params
+  let aux := mkApp aux motive
+  let aux := mkAppN aux matcherApp.discrs
+  trace! `Meta.debug aux
+  check aux
+  unless (← isTypeCorrect aux) do
+    throwError "failed to add argument to matcher application, type error when constructing the new motive"
+  let auxType ← inferType aux
+  let (altNumParams, alts) ← updateAlts auxType matcherApp.altNumParams matcherApp.alts 0
   pure { matcherApp with
          matcherLevels := matcherLevels,
          motive        := motive,
@@ -981,11 +969,9 @@ lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do
          altNumParams  := altNumParams,
          remaining     := #[e] ++ matcherApp.remaining }
 
-@[init] private def regTraceClasses : IO Unit := do
-registerTraceClass `Meta.Match.match;
-registerTraceClass `Meta.Match.debug;
-registerTraceClass `Meta.Match.unify;
-pure ()
+initialize
+  registerTraceClass `Meta.Match.match
+  registerTraceClass `Meta.Match.debug
+  registerTraceClass `Meta.Match.unify
 
-end Meta
-end Lean
+end Lean.Meta

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

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -7,12 +8,9 @@ import Lean.Attributes
 
 namespace Lean
 
-def mkMatchPatternAttr : IO TagAttribute :=
+initialize matchPatternAttr : TagAttribute ←
 registerTagAttribute `matchPattern "mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)"
 
-@[init mkMatchPatternAttr]
-constant matchPatternAttr : TagAttribute := arbitrary _
-
 @[export lean_has_match_pattern_attribute]
 def hasMatchPatternAttribute (env : Environment) (n : Name) : Bool :=
 matchPatternAttr.hasTag env n

stage0/stdlib/Lean/Elab/Declaration.c

@@ -243,7 +243,6 @@ extern lean_object* l_Lean_nullKind___closed__2;
 lean_object* l_Lean_Elab_Command_expandInitialize___closed__19;
 lean_object* l_Lean_Elab_Command_expandMutualElement(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Command_expandMutualElement(lean_object*);
-extern lean_object* l___private_Lean_Meta_Match_Match_40__process___main___closed__1;
 lean_object* l_Lean_Elab_Command_expandInitialize___closed__36;
 lean_object* l_Lean_Elab_Term_resetMessageLog(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_expandMutualPreamble___closed__2;
@@ -338,6 +337,7 @@ lean_object* l_Lean_Elab_Command_elabAttr(lean_object*, lean_object*, lean_objec
 lean_object* l_Lean_Elab_Command_expandInitialize___closed__20;
 lean_object* l_Lean_Elab_Command_elabDeclaration___closed__1;
 lean_object* l_Lean_Elab_Command_expandDeclIdNamespace_x3f_match__2(lean_object*);
+extern lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process___closed__1;
 lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Command_elabAttr___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabDeclaration___closed__3;
 lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_expandMutualNamespace___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
@@ -3955,7 +3955,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Elab_elabModifiers___rarg___lambda__3___closed__2;
-x_2 = l___private_Lean_Meta_Match_Match_40__process___main___closed__1;
+x_2 = l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }

stage0/stdlib/Lean/Elab/Do.c

@@ -136,7 +136,6 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTermCore___closed__11;
 lean_object* l_Lean_Elab_Term_Do_extendUpdatedVarsAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Do_ToTerm_run(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Do_ToTerm_continueToTermCore___closed__23;
-extern lean_object* l___private_Lean_Meta_Match_CaseArraySizes_2__introArrayLitAux___main___closed__3;
 lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39;
 uint8_t l_Lean_Elab_Term_Do_hasTerminalAction(lean_object*);
 lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -333,6 +332,7 @@ lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode___closed__11;
 lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTermCore___closed__13;
 extern lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDone___closed__1;
 lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Meta_caseValueAux___lambda__4___closed__8;
 lean_object* l_Std_RBNode_setBlack___rarg(lean_object*);
 lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__4___closed__1;
 lean_object* l_Lean_Elab_Term_Do_getLetDeclVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -341,7 +341,6 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTermCore___closed__21;
 lean_object* l_Lean_throwError___at_Lean_Elab_Term_Do_ToCodeBlock_checkReassignable___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Do_concat_match__2___rarg(lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_Do_convertTerminalActionIntoJmp_loop___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_Meta_Match_processInaccessibleAsCtor___closed__1;
 lean_object* l_Lean_Elab_Term_elabTermEnsuringType(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Do_CodeBlocl_toMessageData_loop___closed__9;
@@ -359,6 +358,7 @@ uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_ensureInsideFor___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Do_CodeBlocl_toMessageData_loop___closed__4;
 lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__4___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*, lean_object*, lean_object*);
+extern lean_object* l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_introArrayLit_loop___closed__3;
 lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTermCore_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_Do_mkDoSeq___spec__1(lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__1___closed__5;
@@ -368,7 +368,6 @@ lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__4(lean_object
 lean_object* l_Lean_Elab_Term_Do_attachJPs(lean_object*, lean_object*);
 extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_301____closed__5;
 lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doReturnToCode(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_Elab_Term_elabLetDeclAux___closed__4;
 lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doReassignArrowToCode___closed__2;
 lean_object* l_Lean_Elab_Term_Do_ToTerm_declToTerm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_st_ref_take(lean_object*, lean_object*);
@@ -742,7 +741,6 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_seqToTermCore___closed__1;
 lean_object* l_Lean_Elab_Term_Do_ToTerm_reassignToTerm(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Expr_isMVar(lean_object*);
 lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___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*);
-extern lean_object* l_Lean_Meta_caseValueAux___lambda__5___closed__8;
 lean_object* l_Lean_Elab_Term_Do_ToTerm_mkUVarTuple(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Macros___hyg_464____closed__10;
 lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkMonadAlias___closed__2;
@@ -899,6 +897,7 @@ lean_object* l_Lean_Elab_Term_Do_getLetPatDeclVars(lean_object*, lean_object*, l
 lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_ToCodeBlock_mkForInBody___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_Do_mkReassignCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Do_getLetDeclVars___closed__1;
+extern lean_object* l_Lean_Meta_Match_processInaccessibleAsCtor___closed__3;
 lean_object* l_Lean_Elab_Term_Do_getLetDeclVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTerm___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Do_ToTerm_declToTermCore_match__1___rarg(lean_object*, lean_object*, lean_object*);
@@ -1007,6 +1006,7 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTermCore___boxed(lean_object*, le
 lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTermCore_match__1(lean_object*);
 lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__1___closed__11;
 extern lean_object* l___regBuiltin_Lean_Elab_Term_elabSyntheticHole___closed__2;
+extern lean_object* l_Lean_Meta_Match_Unify_assign___closed__6;
 extern lean_object* l_Lean_Elab_Term_expandFunBinders_loop___closed__8;
 lean_object* l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_myMacro____x40_Init_Data_ToString_Macro___hyg_39____closed__8;
@@ -2925,7 +2925,7 @@ lean_dec(x_37);
 x_39 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_39, 0, x_33);
 lean_ctor_set(x_39, 1, x_38);
-x_40 = l_Lean_Elab_Term_elabLetDeclAux___closed__4;
+x_40 = l_Lean_Meta_Match_Unify_assign___closed__6;
 x_41 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_41, 0, x_39);
 lean_ctor_set(x_41, 1, x_40);
@@ -25023,7 +25023,7 @@ lean_ctor_set(x_19, 0, x_12);
 lean_ctor_set(x_19, 1, x_18);
 x_20 = l_ULift_HasRepr___rarg___closed__2;
 x_21 = l_Lean_mkAtomFrom(x_1, x_20);
-x_22 = l_Lean_Meta_caseValueAux___lambda__5___closed__8;
+x_22 = l_Lean_Meta_caseValueAux___lambda__4___closed__8;
 x_23 = lean_array_push(x_22, x_15);
 x_24 = lean_array_push(x_23, x_19);
 x_25 = lean_array_push(x_24, x_13);
@@ -25888,7 +25888,7 @@ lean_dec(x_10);
 x_20 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__16;
 x_21 = l_Lean_mkAtomFrom(x_11, x_20);
 lean_dec(x_11);
-x_22 = l___private_Lean_Meta_Match_CaseArraySizes_2__introArrayLitAux___main___closed__3;
+x_22 = l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_introArrayLit_loop___closed__3;
 x_23 = lean_array_push(x_22, x_19);
 x_24 = lean_array_push(x_23, x_21);
 x_25 = lean_array_push(x_24, x_17);
@@ -25939,7 +25939,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_mkAppStx___closed__6;
-x_2 = l_Lean_Meta_Match_processInaccessibleAsCtor___closed__1;
+x_2 = l_Lean_Meta_Match_processInaccessibleAsCtor___closed__3;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@@ -26385,12 +26385,12 @@ x_113 = l_Lean_Elab_Term_expandFunBinders_loop___closed__11;
 x_114 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_114, 0, x_113);
 lean_ctor_set(x_114, 1, x_112);
-x_115 = l_Lean_Meta_Match_processInaccessibleAsCtor___closed__1;
+x_115 = l_Lean_Meta_Match_processInaccessibleAsCtor___closed__3;
 x_116 = l_Lean_mkAtomFrom(x_87, x_115);
 x_117 = l_Lean_Elab_Term_expandFunBinders_loop___closed__8;
 x_118 = l_Lean_mkAtomFrom(x_87, x_117);
 lean_dec(x_87);
-x_119 = l_Lean_Meta_caseValueAux___lambda__5___closed__8;
+x_119 = l_Lean_Meta_caseValueAux___lambda__4___closed__8;
 x_120 = lean_array_push(x_119, x_116);
 x_121 = lean_array_push(x_120, x_88);
 x_122 = lean_array_push(x_121, x_89);
@@ -26435,12 +26435,12 @@ x_144 = l_Lean_Elab_Term_expandFunBinders_loop___closed__11;
 x_145 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_145, 0, x_144);
 lean_ctor_set(x_145, 1, x_143);
-x_146 = l_Lean_Meta_Match_processInaccessibleAsCtor___closed__1;
+x_146 = l_Lean_Meta_Match_processInaccessibleAsCtor___closed__3;
 x_147 = l_Lean_mkAtomFrom(x_87, x_146);
 x_148 = l_Lean_Elab_Term_expandFunBinders_loop___closed__8;
 x_149 = l_Lean_mkAtomFrom(x_87, x_148);
 lean_dec(x_87);
-x_150 = l_Lean_Meta_caseValueAux___lambda__5___closed__8;
+x_150 = l_Lean_Meta_caseValueAux___lambda__4___closed__8;
 x_151 = lean_array_push(x_150, x_147);
 x_152 = lean_array_push(x_151, x_88);
 x_153 = lean_array_push(x_152, x_89);
@@ -27119,7 +27119,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_SourceInfo_inhabited___closed__1;
-x_2 = l_Lean_Meta_Match_processInaccessibleAsCtor___closed__1;
+x_2 = l_Lean_Meta_Match_processInaccessibleAsCtor___closed__3;
 x_3 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);

stage0/stdlib/Lean/Elab/MutualDef.c

@@ -383,7 +383,6 @@ lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_checkModifiers___
 lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_MutualClosure_main___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getLocalDecl___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkClosureForAux___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 size_t l_USize_mod(size_t, size_t);
-extern lean_object* l_Lean_Elab_elabAttr___rarg___lambda__3___closed__3;
 lean_object* l_Lean_Elab_Term_MutualClosure_ClosureState_localDecls___default;
 lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_FixPoint_getUsedFVarsMap(lean_object*);
 lean_object* l_List_foldl___main___at_Lean_Elab_Term_MutualClosure_pushLetRecs___spec__1(uint8_t, lean_object*, lean_object*, lean_object*);
@@ -482,6 +481,7 @@ lean_object* l_Lean_Elab_elabModifiers___at_Lean_Elab_Command_elabMutualDef___sp
 lean_object* l_Lean_Elab_Term_elabMutualDef___lambda__2___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_List_forInAux___main___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkFreeVarMap___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_expr_update_lambda(lean_object*, uint8_t, lean_object*, lean_object*);
+extern lean_object* l_Lean_Meta_Match_Pattern_toMessageData___closed__6;
 lean_object* l_Lean_Meta_getZetaFVarIds___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkClosureForAux___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_FindImpl_findM_x3f___main___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_typeHasRecFun___spec__2(lean_object*, lean_object*, size_t, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_FixPoint_isModified___rarg(lean_object*);
@@ -14771,7 +14771,7 @@ x_12 = l_Lean_Elab_elabAttr___rarg___lambda__3___closed__2;
 x_13 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_13, 0, x_12);
 lean_ctor_set(x_13, 1, x_11);
-x_14 = l_Lean_Elab_elabAttr___rarg___lambda__3___closed__3;
+x_14 = l_Lean_Meta_Match_Pattern_toMessageData___closed__6;
 x_15 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_15, 0, x_13);
 lean_ctor_set(x_15, 1, x_14);

stage0/stdlib/Lean/Elab/PreDefinition/Structural.c

@@ -15,6 +15,7 @@ extern "C" {
 #endif
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_hasBadIndexDep_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_fmt___at_Lean_Position_Lean_HasFormat___spec__1(lean_object*);
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___closed__2;
 extern lean_object* l_Lean_Meta_binductionOnSuffix;
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_mkBRecOn___lambda__3___closed__3;
 lean_object* lean_array_set(lean_object*, lean_object*, lean_object*);
@@ -47,7 +48,6 @@ lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRec
 lean_object* l___private_Lean_Util_Trace_3__checkTraceOptionM___at_Lean_Meta_substCore___spec__13(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop_match__3(lean_object*);
 lean_object* l_Array_indexOfAux___main___at___private_Lean_Meta_FunInfo_3__collectDepsAux___main___spec__1(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__3(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___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_hasBadIndexDep_x3f_match__1(lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___lambda__1(lean_object*);
 lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop___spec__3___closed__3;
@@ -64,12 +64,11 @@ lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_ensureN
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelowAux___closed__16;
 lean_object* lean_array_fswap(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_inferType___at___private_Lean_Elab_PreDefinition_MkInhabitant_0__Lean_Elab_findAssumption_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___closed__1;
 lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop_match__1___rarg(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_elimRecursion___lambda__2___closed__2;
 lean_object* l_Array_filterAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_mkBRecOn___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l___private_Lean_Meta_Match_Match_42__updateAlts___main___lambda__2___closed__1;
 extern lean_object* l_Array_empty___closed__1;
 lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___spec__3___lambda__2___closed__1;
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_hasBadParamDep_x3f_match__1(lean_object*);
@@ -126,6 +125,7 @@ lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwTypeMismatchError___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_mkBRecOn___lambda__2___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*);
 lean_object* l_Lean_Elab_structuralRecursion___closed__1;
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg(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___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop___rarg___closed__8;
 lean_object* l_Lean_ForEachExpr_visit___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_getFixedPrefix___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___spec__3___closed__1;
@@ -134,12 +134,11 @@ lean_object* l_Lean_Elab_structuralRecursion___boxed(lean_object*, lean_object*,
 lean_object* l_Lean_mkMData(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop___rarg___closed__9;
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_mkBRecOn___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*, lean_object*, lean_object*);
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__3(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_Expr_getAppNumArgsAux___main(lean_object*, lean_object*);
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg(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_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___spec__3___closed__2;
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_getFixedPrefix_match__1(lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop___rarg___closed__4;
-lean_object* l_Lean_Meta_whnfD___at_Lean_Meta_getInductiveUniverseAndParams___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_decLevel___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_mkBRecOn___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelowAux___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_getIndexMinPos_match__1___boxed(lean_object*, lean_object*);
@@ -155,6 +154,7 @@ lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelow
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Array_anyRangeMAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2(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_st_ref_take(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_hasBadParamDep_x3f_match__4___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___spec__6___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -196,20 +196,23 @@ lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelow
 lean_object* l_Lean_Elab_structuralRecursion___closed__3;
 lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_getIndexMinPos___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop___rarg___closed__5;
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2___closed__2;
 lean_object* l_Lean_throwError___at_Lean_Elab_mkInhabitantFor___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2___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_Array_umapMAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___spec__8___lambda__2___closed__8;
 lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_hasBadIndexDep_x3f___spec__3___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___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelowAux___closed__14;
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop___rarg___closed__15;
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___closed__1;
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_throwToBelowFailed___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_st_mk_ref(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop___rarg___closed__6;
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2___closed__1;
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___lambda__3___boxed(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_withLocalDecl___at_Lean_Meta_forallTelescopeCompatibleAux___spec__4___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_forEachExpr_x27___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_ensureNoRecFn___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1(lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___spec__3___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* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___spec__3___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -230,11 +233,10 @@ lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelow
 lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___spec__8___lambda__2___closed__1;
 lean_object* l___private_Lean_CoreM_1__mkFreshNameImp(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_hasBadIndexDep_x3f___closed__1;
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2___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___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop_match__2(lean_object*);
 uint8_t l___private_Init_Data_Array_Basic_9__allDiffAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop___spec__4(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2___closed__1;
+lean_object* l_Lean_Meta_whnfD___at_Lean_Meta_getArrayArgType___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_ensureNoRecFn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_PreDefinition_Structural___hyg_3364_(lean_object*);
 uint8_t l_Lean_Expr_isConstOf(lean_object*, lean_object*);
@@ -253,7 +255,6 @@ size_t lean_usize_of_nat(lean_object*);
 lean_object* l___private_Lean_Meta_LevelDefEq_2__decLevelImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_mkBRecOn___lambda__3___closed__2;
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Lean_Meta_Basic_21__forallBoundedTelescopeImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelowAux___closed__6;
 lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -262,7 +263,6 @@ lean_object* l_Lean_throwError___at_Lean_Meta_mkWHNFRef___spec__1___rarg(lean_ob
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_mkBRecOn___lambda__3___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*, lean_object*);
 lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___spec__8___lambda__2___closed__2;
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelowAux___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2___closed__2;
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelowAux___closed__4;
 size_t l_USize_mod(size_t, size_t);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_mkBRecOn___lambda__3___closed__4;
@@ -294,9 +294,8 @@ lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Str
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelowAux___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_expr_eqv(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_elimRecursion___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* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop_match__2___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__3___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_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1(lean_object*);
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop_match__1(lean_object*);
 lean_object* l_Lean_mkApp(lean_object*, lean_object*);
@@ -335,7 +334,6 @@ lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_throwTo
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_hasBadParamDep_x3f_match__2___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_toList___rarg(lean_object*);
 extern lean_object* l_Lean_Expr_Inhabited;
-lean_object* l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkAppM___at___private_Lean_Elab_PreDefinition_MkInhabitant_0__Lean_Elab_mkInhabitant_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_hasBadParamDep_x3f___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_mk_array(lean_object*, lean_object*);
@@ -348,17 +346,17 @@ lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_elimRec
 extern lean_object* l_Lean_Meta_decLevel___rarg___lambda__1___closed__3;
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_ensureNoRecFn___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_HashMapImp_find_x3f___at_Lean_Meta_ForEachExpr_visit___main___spec__10(lean_object*, lean_object*);
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___closed__2;
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop_match__2___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_mkBRecOn___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_indentD(lean_object*);
 lean_object* l_Lean_Expr_FindImpl_findM_x3f___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_containsRecFn___spec__1(lean_object*, size_t, lean_object*, lean_object*);
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__3___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_forallBoundedTelescope___at___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_mkBRecOn___lambda__3___closed__5;
 extern lean_object* l_Lean_mkOptionalNode___closed__2;
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelowAux_match__2___rarg___closed__2;
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_hasBadParamDep_x3f_match__3(lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_getFixedPrefix_match__1___rarg(lean_object*, lean_object*);
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2(lean_object*);
 lean_object* l_Lean_hasConst___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_map___main___at_Lean_MessageData_hasCoeOfListExpr___spec__1(lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_hasBadIndexDep_x3f_match__1___rarg(lean_object*, lean_object*);
@@ -366,7 +364,6 @@ extern lean_object* l_Nat_Inhabited;
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop_match__2(lean_object*);
 lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2(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___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop(lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_mkBRecOn___lambda__2(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*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_ensureNoRecFn___lambda__1___closed__2;
@@ -403,6 +400,7 @@ uint8_t lean_string_dec_eq(lean_object*, lean_object*);
 uint8_t l_Lean_LocalDecl_isLet(lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelowAux_match__3(lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
+extern lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1;
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop_match__1___boxed(lean_object*, lean_object*);
 lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_hasBadIndexDep_x3f___spec__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___closed__1;
@@ -3810,7 +3808,7 @@ lean_inc(x_8);
 lean_inc(x_7);
 lean_inc(x_6);
 lean_inc(x_5);
-x_19 = l_Lean_Meta_whnfD___at_Lean_Meta_getInductiveUniverseAndParams___spec__1(x_18, x_5, x_6, x_7, x_8, x_16);
+x_19 = l_Lean_Meta_whnfD___at_Lean_Meta_getArrayArgType___spec__2(x_18, x_5, x_6, x_7, x_8, x_16);
 if (lean_obj_tag(x_19) == 0)
 {
 lean_object* x_20; lean_object* x_21; lean_object* x_22; 
@@ -7582,66 +7580,7 @@ lean_dec(x_3);
 return x_11;
 }
 }
-lean_object* l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___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* x_7, lean_object* x_8) {
-_start:
-{
-lean_object* x_9; 
-x_9 = l___private_Lean_Meta_Basic_21__forallBoundedTelescopeImp___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
-if (lean_obj_tag(x_9) == 0)
-{
-uint8_t x_10; 
-x_10 = !lean_is_exclusive(x_9);
-if (x_10 == 0)
-{
-return x_9;
-}
-else
-{
-lean_object* x_11; lean_object* x_12; lean_object* x_13; 
-x_11 = lean_ctor_get(x_9, 0);
-x_12 = lean_ctor_get(x_9, 1);
-lean_inc(x_12);
-lean_inc(x_11);
-lean_dec(x_9);
-x_13 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_13, 0, x_11);
-lean_ctor_set(x_13, 1, x_12);
-return x_13;
-}
-}
-else
-{
-uint8_t x_14; 
-x_14 = !lean_is_exclusive(x_9);
-if (x_14 == 0)
-{
-return x_9;
-}
-else
-{
-lean_object* x_15; lean_object* x_16; lean_object* x_17; 
-x_15 = lean_ctor_get(x_9, 0);
-x_16 = lean_ctor_get(x_9, 1);
-lean_inc(x_16);
-lean_inc(x_15);
-lean_dec(x_9);
-x_17 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_17, 0, x_15);
-lean_ctor_set(x_17, 1, x_16);
-return x_17;
-}
-}
-}
-}
-lean_object* l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg), 8, 0);
-return x_2;
-}
-}
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__1(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, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__1(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, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
 _start:
 {
 lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
@@ -7656,7 +7595,7 @@ x_16 = lean_apply_7(x_4, x_5, x_15, x_6, x_7, x_8, x_9, x_10);
 return x_16;
 }
 }
-static lean_object* _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2___closed__1() {
+static lean_object* _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2___closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -7664,17 +7603,17 @@ x_1 = lean_mk_string("C");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2___closed__2() {
+static lean_object* _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2___closed__1;
+x_2 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2(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, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2(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, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
 _start:
 {
 lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
@@ -7694,14 +7633,14 @@ lean_inc(x_16);
 x_17 = lean_ctor_get(x_15, 1);
 lean_inc(x_17);
 lean_dec(x_15);
-x_18 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2___closed__2;
+x_18 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2___closed__2;
 x_19 = l___private_Lean_CoreM_1__mkFreshNameImp(x_18, x_9, x_10, x_17);
 x_20 = lean_ctor_get(x_19, 0);
 lean_inc(x_20);
 x_21 = lean_ctor_get(x_19, 1);
 lean_inc(x_21);
 lean_dec(x_19);
-x_22 = lean_alloc_closure((void*)(l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__1), 10, 4);
+x_22 = lean_alloc_closure((void*)(l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__1), 10, 4);
 lean_closure_set(x_22, 0, x_1);
 lean_closure_set(x_22, 1, x_2);
 lean_closure_set(x_22, 2, x_3);
@@ -7742,7 +7681,7 @@ return x_28;
 }
 }
 }
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__3(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, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__3(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, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
 _start:
 {
 lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
@@ -7765,13 +7704,13 @@ lean_inc(x_16);
 x_17 = lean_ctor_get(x_15, 1);
 lean_inc(x_17);
 lean_dec(x_15);
-x_18 = lean_alloc_closure((void*)(l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2___boxed), 11, 4);
+x_18 = lean_alloc_closure((void*)(l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2___boxed), 11, 4);
 lean_closure_set(x_18, 0, x_14);
 lean_closure_set(x_18, 1, x_1);
 lean_closure_set(x_18, 2, x_4);
 lean_closure_set(x_18, 3, x_5);
-x_19 = l___private_Lean_Meta_Match_Match_42__updateAlts___main___lambda__2___closed__1;
-x_20 = l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg(x_16, x_19, x_18, x_7, x_8, x_9, x_10, x_17);
+x_19 = l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1;
+x_20 = l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___spec__1___rarg(x_16, x_19, x_18, x_7, x_8, x_9, x_10, x_17);
 return x_20;
 }
 else
@@ -7806,7 +7745,7 @@ return x_24;
 }
 }
 }
-static lean_object* _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___closed__1() {
+static lean_object* _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -7814,16 +7753,16 @@ x_1 = lean_mk_string("unexpected 'below' type");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___closed__2() {
+static lean_object* _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___closed__1;
+x_1 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___closed__1;
 x_2 = l_Lean_stringToMessageData(x_1);
 return x_2;
 }
 }
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___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* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___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* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
 _start:
 {
 if (lean_obj_tag(x_4) == 5)
@@ -7861,7 +7800,7 @@ lean_dec(x_4);
 lean_dec(x_2);
 lean_dec(x_1);
 x_22 = l_Lean_indentExpr(x_3);
-x_23 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___closed__2;
+x_23 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___closed__2;
 x_24 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_24, 0, x_23);
 lean_ctor_set(x_24, 1, x_22);
@@ -7898,17 +7837,17 @@ else
 lean_object* x_32; lean_object* x_33; 
 lean_dec(x_3);
 x_32 = lean_box(0);
-x_33 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__3(x_5, x_1, x_4, x_19, x_2, x_32, x_7, x_8, x_9, x_10, x_11);
+x_33 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__3(x_5, x_1, x_4, x_19, x_2, x_32, x_7, x_8, x_9, x_10, x_11);
 return x_33;
 }
 }
 }
 }
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2(lean_object* x_1) {
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg), 11, 0);
+x_2 = lean_alloc_closure((void*)(l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg), 11, 0);
 return x_2;
 }
 }
@@ -7996,7 +7935,7 @@ x_17 = lean_unsigned_to_nat(1u);
 x_18 = lean_nat_sub(x_14, x_17);
 lean_dec(x_14);
 lean_inc(x_10);
-x_19 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg(x_2, x_3, x_10, x_10, x_16, x_18, x_4, x_5, x_6, x_7, x_12);
+x_19 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg(x_2, x_3, x_10, x_10, x_16, x_18, x_4, x_5, x_6, x_7, x_12);
 return x_19;
 }
 block_31:
@@ -8068,21 +8007,21 @@ x_2 = lean_alloc_closure((void*)(l___private_Lean_Elab_PreDefinition_Structural_
 return x_2;
 }
 }
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2___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, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2___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, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
 _start:
 {
 lean_object* x_12; 
-x_12 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
+x_12 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
 lean_dec(x_6);
 lean_dec(x_5);
 return x_12;
 }
 }
-lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__3___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, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
+lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__3___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, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
 _start:
 {
 lean_object* x_12; 
-x_12 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__3(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
+x_12 = l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__3(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
 lean_dec(x_6);
 return x_12;
 }
@@ -11576,7 +11515,7 @@ lean_closure_set(x_28, 5, x_2);
 lean_closure_set(x_28, 6, x_5);
 lean_closure_set(x_28, 7, x_6);
 lean_closure_set(x_28, 8, x_7);
-x_29 = l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg(x_19, x_27, x_28, x_10, x_11, x_12, x_13, x_20);
+x_29 = l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___spec__1___rarg(x_19, x_27, x_28, x_10, x_11, x_12, x_13, x_20);
 return x_29;
 }
 else
@@ -11845,8 +11784,8 @@ lean_closure_set(x_36, 3, x_2);
 lean_closure_set(x_36, 4, x_6);
 lean_closure_set(x_36, 5, x_1);
 lean_closure_set(x_36, 6, x_28);
-x_37 = l___private_Lean_Meta_Match_Match_42__updateAlts___main___lambda__2___closed__1;
-x_38 = l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg(x_32, x_37, x_36, x_11, x_12, x_13, x_14, x_35);
+x_37 = l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1;
+x_38 = l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___spec__1___rarg(x_32, x_37, x_36, x_11, x_12, x_13, x_14, x_35);
 return x_38;
 }
 else
@@ -11875,8 +11814,8 @@ lean_closure_set(x_46, 3, x_2);
 lean_closure_set(x_46, 4, x_6);
 lean_closure_set(x_46, 5, x_1);
 lean_closure_set(x_46, 6, x_28);
-x_47 = l___private_Lean_Meta_Match_Match_42__updateAlts___main___lambda__2___closed__1;
-x_48 = l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg(x_32, x_47, x_46, x_11, x_12, x_13, x_14, x_45);
+x_47 = l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1;
+x_48 = l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___spec__1___rarg(x_32, x_47, x_46, x_11, x_12, x_13, x_14, x_45);
 return x_48;
 }
 }
@@ -13380,14 +13319,14 @@ l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelowAux___closed_
 lean_mark_persistent(l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelowAux___closed__15);
 l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelowAux___closed__16 = _init_l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelowAux___closed__16();
 lean_mark_persistent(l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelowAux___closed__16);
-l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2___closed__1 = _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2___closed__1();
-lean_mark_persistent(l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2___closed__1);
-l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2___closed__2 = _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2___closed__2();
-lean_mark_persistent(l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___lambda__2___closed__2);
-l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___closed__1 = _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___closed__1();
-lean_mark_persistent(l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___closed__1);
-l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___closed__2 = _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___closed__2();
-lean_mark_persistent(l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__2___rarg___closed__2);
+l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2___closed__1 = _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2___closed__1();
+lean_mark_persistent(l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2___closed__1);
+l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2___closed__2 = _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2___closed__2();
+lean_mark_persistent(l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___lambda__2___closed__2);
+l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___closed__1 = _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___closed__1();
+lean_mark_persistent(l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___closed__1);
+l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___closed__2 = _init_l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___closed__2();
+lean_mark_persistent(l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___spec__1___rarg___closed__2);
 l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___rarg___closed__1 = _init_l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___rarg___closed__1();
 lean_mark_persistent(l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___rarg___closed__1);
 l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___rarg___closed__2 = _init_l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_withBelowDict___rarg___closed__2();

stage0/stdlib/Lean/Meta/Match.c

@@ -14,13 +14,13 @@
 extern "C" {
 #endif
 lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
+extern lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAltsAux___rarg___closed__2;
 lean_object* l___private_Lean_Meta_Match_1__regTraceClasses(lean_object*);
-extern lean_object* l___private_Lean_Meta_Match_Match_2__withAltsAux___main___rarg___closed__2;
 lean_object* l___private_Lean_Meta_Match_1__regTraceClasses(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
-x_2 = l___private_Lean_Meta_Match_Match_2__withAltsAux___main___rarg___closed__2;
+x_2 = l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAltsAux___rarg___closed__2;
 x_3 = l_Lean_registerTraceClass(x_2, x_1);
 return x_3;
 }

stage0/stdlib/Lean/Meta/Match/MVarRenaming.c

@@ -28,9 +28,13 @@ lean_object* l_Lean_Meta_MVarRenaming_insert(lean_object*, lean_object*, lean_ob
 extern lean_object* l_Lean_Name_inhabited;
 uint8_t l_Lean_Meta_MVarRenaming_isEmpty(lean_object*);
 lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_MVarRenaming_apply___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_MVarRenaming_apply_match__2___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_MVarRenaming_map___default;
+lean_object* l_Lean_Meta_MVarRenaming_apply_match__1(lean_object*);
 lean_object* l_Std_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_MVarRenaming_find_x21___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_MVarRenaming_apply___spec__1(lean_object*, size_t, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_MVarRenaming_apply_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_find___main___at_Lean_Meta_MVarRenaming_find_x3f___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_MVarRenaming_find_x3f___boxed(lean_object*, lean_object*);
 lean_object* lean_expr_update_let(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -44,10 +48,19 @@ size_t lean_ptr_addr(lean_object*);
 lean_object* l_Lean_Meta_MVarRenaming_find_x21(lean_object*, lean_object*);
 uint8_t l_Lean_Expr_hasMVar(lean_object*);
 lean_object* lean_panic_fn(lean_object*, lean_object*);
+lean_object* l_Lean_Meta_MVarRenaming_apply_match__2(lean_object*);
 lean_object* lean_expr_update_lambda(lean_object*, uint8_t, lean_object*, lean_object*);
 extern lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___closed__1;
 lean_object* lean_expr_update_app(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Expr_ReplaceImpl_initCache;
+static lean_object* _init_l_Lean_Meta_MVarRenaming_map___default() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_box(0);
+return x_1;
+}
+}
 uint8_t l_Lean_Meta_MVarRenaming_isEmpty(lean_object* x_1) {
 _start:
 {
@@ -187,6 +200,69 @@ x_4 = l_Std_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_1, x_2, x_
 return x_4;
 }
 }
+lean_object* l_Lean_Meta_MVarRenaming_apply_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_dec(x_3);
+x_4 = lean_box(0);
+x_5 = lean_apply_1(x_2, x_4);
+return x_5;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_2);
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = lean_apply_1(x_3, x_6);
+return x_7;
+}
+}
+}
+lean_object* l_Lean_Meta_MVarRenaming_apply_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Meta_MVarRenaming_apply_match__1___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_Meta_MVarRenaming_apply_match__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 2)
+{
+lean_object* x_4; uint64_t x_5; lean_object* x_6; lean_object* x_7; 
+lean_dec(x_3);
+x_4 = lean_ctor_get(x_1, 0);
+lean_inc(x_4);
+x_5 = lean_ctor_get_uint64(x_1, sizeof(void*)*1);
+lean_dec(x_1);
+x_6 = lean_box_uint64(x_5);
+x_7 = lean_apply_2(x_2, x_4, x_6);
+return x_7;
+}
+else
+{
+lean_object* x_8; 
+lean_dec(x_2);
+x_8 = lean_apply_1(x_3, x_1);
+return x_8;
+}
+}
+}
+lean_object* l_Lean_Meta_MVarRenaming_apply_match__2(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Meta_MVarRenaming_apply_match__2___rarg), 3, 0);
+return x_2;
+}
+}
 lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_MVarRenaming_apply___spec__1(lean_object* x_1, size_t x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
@@ -675,28 +751,63 @@ return x_165;
 lean_object* l_Lean_Meta_MVarRenaming_apply(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-uint8_t x_3; 
-x_3 = l_Lean_Expr_hasMVar(x_2);
+uint8_t x_3; uint8_t x_13; 
+x_13 = l_Lean_Expr_hasMVar(x_2);
+if (x_13 == 0)
+{
+uint8_t x_14; 
+x_14 = 1;
+x_3 = x_14;
+goto block_12;
+}
+else
+{
+uint8_t x_15; 
+x_15 = 0;
+x_3 = x_15;
+goto block_12;
+}
+block_12:
+{
 if (x_3 == 0)
 {
-return x_2;
-}
-else
-{
+uint8_t x_4; 
 if (lean_obj_tag(x_1) == 0)
 {
-return x_2;
+uint8_t x_10; 
+x_10 = 1;
+x_4 = x_10;
+goto block_9;
 }
 else
 {
-size_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
-x_4 = 8192;
-x_5 = l_Lean_Expr_ReplaceImpl_initCache;
-x_6 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_MVarRenaming_apply___spec__1(x_1, x_4, x_2, x_5);
-x_7 = lean_ctor_get(x_6, 0);
-lean_inc(x_7);
-lean_dec(x_6);
-return x_7;
+uint8_t x_11; 
+x_11 = 0;
+x_4 = x_11;
+goto block_9;
+}
+block_9:
+{
+if (x_4 == 0)
+{
+size_t x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; 
+x_5 = 8192;
+x_6 = l_Lean_Expr_ReplaceImpl_initCache;
+x_7 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_MVarRenaming_apply___spec__1(x_1, x_5, x_2, x_6);
+x_8 = lean_ctor_get(x_7, 0);
+lean_inc(x_8);
+lean_dec(x_7);
+return x_8;
+}
+else
+{
+return x_2;
+}
+}
+}
+else
+{
+return x_2;
 }
 }
 }
@@ -734,6 +845,8 @@ lean_dec_ref(res);
 res = initialize_Lean_Util_ReplaceExpr(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l_Lean_Meta_MVarRenaming_map___default = _init_l_Lean_Meta_MVarRenaming_map___default();
+lean_mark_persistent(l_Lean_Meta_MVarRenaming_map___default);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Lean/Meta/Match/MatchPatternAttr.c

@@ -13,21 +13,21 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+lean_object* l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__2;
 lean_object* l_Lean_hasMatchPatternAttribute___boxed(lean_object*, lean_object*);
-lean_object* l_Lean_mkMatchPatternAttr(lean_object*);
-lean_object* l_Lean_mkMatchPatternAttr___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_mkMatchPatternAttr___closed__2;
-lean_object* l_Lean_mkMatchPatternAttr___closed__1;
+lean_object* l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3_(lean_object*);
 extern lean_object* l_Lean_TagAttribute_Inhabited___closed__1;
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
-lean_object* l_Lean_mkMatchPatternAttr___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_has_match_pattern_attribute(lean_object*, lean_object*);
 uint8_t l_Lean_TagAttribute_hasTag(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__1;
+lean_object* l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__4;
 lean_object* l_Lean_registerTagAttribute(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_mkMatchPatternAttr___closed__3;
-lean_object* l_Lean_mkMatchPatternAttr___closed__4;
+lean_object* l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__3;
 lean_object* l_Lean_matchPatternAttr;
-lean_object* l_Lean_mkMatchPatternAttr___lambda__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_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
 lean_object* x_6; lean_object* x_7; 
@@ -38,7 +38,7 @@ lean_ctor_set(x_7, 1, x_5);
 return x_7;
 }
 }
-static lean_object* _init_l_Lean_mkMatchPatternAttr___closed__1() {
+static lean_object* _init_l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -46,17 +46,17 @@ x_1 = lean_mk_string("matchPattern");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_mkMatchPatternAttr___closed__2() {
+static lean_object* _init_l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_mkMatchPatternAttr___closed__1;
+x_2 = l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_mkMatchPatternAttr___closed__3() {
+static lean_object* _init_l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -64,30 +64,30 @@ x_1 = lean_mk_string("mark that a definition can be used in a pattern (remark: t
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_mkMatchPatternAttr___closed__4() {
+static lean_object* _init_l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__4() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_mkMatchPatternAttr___lambda__1___boxed), 5, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____lambda__1___boxed), 5, 0);
 return x_1;
 }
 }
-lean_object* l_Lean_mkMatchPatternAttr(lean_object* x_1) {
+lean_object* l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
-x_2 = l_Lean_mkMatchPatternAttr___closed__2;
-x_3 = l_Lean_mkMatchPatternAttr___closed__3;
-x_4 = l_Lean_mkMatchPatternAttr___closed__4;
+x_2 = l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__2;
+x_3 = l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__3;
+x_4 = l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__4;
 x_5 = l_Lean_registerTagAttribute(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
-lean_object* l_Lean_mkMatchPatternAttr___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+lean_object* l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
 lean_object* x_6; 
-x_6 = l_Lean_mkMatchPatternAttr___lambda__1(x_1, x_2, x_3, x_4, x_5);
+x_6 = l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____lambda__1(x_1, x_2, x_3, x_4, x_5);
 lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
@@ -128,15 +128,15 @@ lean_dec_ref(res);
 res = initialize_Lean_Attributes(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-l_Lean_mkMatchPatternAttr___closed__1 = _init_l_Lean_mkMatchPatternAttr___closed__1();
-lean_mark_persistent(l_Lean_mkMatchPatternAttr___closed__1);
-l_Lean_mkMatchPatternAttr___closed__2 = _init_l_Lean_mkMatchPatternAttr___closed__2();
-lean_mark_persistent(l_Lean_mkMatchPatternAttr___closed__2);
-l_Lean_mkMatchPatternAttr___closed__3 = _init_l_Lean_mkMatchPatternAttr___closed__3();
-lean_mark_persistent(l_Lean_mkMatchPatternAttr___closed__3);
-l_Lean_mkMatchPatternAttr___closed__4 = _init_l_Lean_mkMatchPatternAttr___closed__4();
-lean_mark_persistent(l_Lean_mkMatchPatternAttr___closed__4);
-res = l_Lean_mkMatchPatternAttr(lean_io_mk_world());
+l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__1 = _init_l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__1();
+lean_mark_persistent(l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__1);
+l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__2 = _init_l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__2();
+lean_mark_persistent(l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__2);
+l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__3 = _init_l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__3();
+lean_mark_persistent(l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__3);
+l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__4 = _init_l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__4();
+lean_mark_persistent(l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3____closed__4);
+res = l_Lean_initFn____x40_Lean_Meta_Match_MatchPatternAttr___hyg_3_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 l_Lean_matchPatternAttr = lean_io_result_get_value(res);
 lean_mark_persistent(l_Lean_matchPatternAttr);