chore: update stage0

2021-01-27 18:35:34 -08:00 · 2021-01-27 18:35:34 -08:00 · 7f047a95f4
commit 7f047a95f4
parent 4a19a5d2a4
5 changed files with 4770 additions and 2663 deletions
--- a/stage0/src/Init/Core.lean
+++ b/stage0/src/Init/Core.lean
@ -46,9 +46,6 @@ infix:20 " ↔ "   => Iff

 /- Eq basic support -/

-theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
-  h₂ ▸ h₁
-
 inductive Sum (α : Type u) (β : Type v) where
  | inl (val : α) : Sum α β
  | inr (val : β) : Sum α β
--- a/stage0/src/Init/Prelude.lean
+++ b/stage0/src/Init/Prelude.lean
@ -83,6 +83,9 @@ theorem Eq.subst {α : Sort u} {motive : α → Prop} {a b : α} (h₁ : Eq a b)
 theorem Eq.symm {α : Sort u} {a b : α} (h : Eq a b) : Eq b a :=
  h ▸ rfl

+theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : Eq a b) (h₂ : Eq b c) : Eq a c :=
+  h₂ ▸ h₁
+
@[macroInline] def cast {α β : Sort u} (h : Eq α β) (a : α) : β :=
  Eq.rec (motive := fun α _ => α) a h

--- a/stage0/src/Lean/Meta/SizeOf.lean
+++ b/stage0/src/Lean/Meta/SizeOf.lean
@ -158,6 +158,20 @@ def mkSizeOfFns (typeName : Name) : MetaM (Array Name × NameMap Name) := do
    i := i + 1
  return (result, recMap)

+def mkSizeOfSpecLemmaName (ctorName : Name) : Name :=
+  ctorName ++ `sizeOf_spec
+
+def mkSizeOfSpecLemmaInstance (ctorApp : Expr) : MetaM Expr :=
+  matchConstCtor ctorApp.getAppFn (fun _ => throwError! "failed to apply 'sizeOf' spec, constructor expected{indentExpr ctorApp}") fun ctorInfo ctorLevels => do
+    let ctorArgs     := ctorApp.getAppArgs
+    let ctorFields   := ctorArgs[ctorArgs.size - ctorInfo.numFields:]
+    let lemmaName  := mkSizeOfSpecLemmaName ctorInfo.name
+    let lemmaInfo  ← getConstInfo lemmaName
+    let lemmaArity ← forallTelescopeReducing lemmaInfo.type fun xs _ => return xs.size
+    let lemmaArgMask := mkArray (lemmaArity - ctorInfo.numFields) (none (α := Expr))
+    let lemmaArgMask := lemmaArgMask ++ ctorFields.toArray.map some
+    mkAppOptM lemmaName lemmaArgMask
+
 /- SizeOf spec theorem for nested inductive types -/
 namespace SizeOfSpecNested

@ -188,111 +202,161 @@ private def recToSizeOf (e : Expr) : M Expr := do
      let major   := args[info.getMajorIdx]
      return mkAppN (mkConst sizeOfName us.tail!) ((← read).params ++ (← read).localInsts ++ indices ++ #[major])

-/-- Construct proof of auxiliary lemma. See `mkSizeOfAuxLemma` -/
-private def mkSizeOfAuxLemmaProof (info : InductiveVal) (lhs rhs : Expr) : M Expr := do
-  let lhsArgs := lhs.getAppArgs
-  let sizeOfBaseArgs := lhsArgs[:lhsArgs.size - info.numIndices - 1]
-  let indicesMajor := lhsArgs[lhsArgs.size - info.numIndices - 1:]
-  let sizeOfLevels := lhs.getAppFn.constLevels!
-  /- Auxiliary function for constructing an `_sizeOf_<idx>` for `ys`,
-     where `ys` are the indices + major.
-     Recall that if `info.name` is part of a mutually inductive declaration, then the resulting application
-     is not necessarily a `lhs.getAppFn` application.
-     The result is an application of one of the `(← read),sizeOfFns` functions.
-     We use this auxiliary function to builtin the motive of the recursor. -/
-  let rec mkSizeOf (ys : Array Expr) : M Expr := do
-    for sizeOfFn in (← read).sizeOfFns do
-      let candidate := mkAppN (mkAppN (mkConst sizeOfFn sizeOfLevels) sizeOfBaseArgs) ys
-      if (← isTypeCorrect candidate) then
-        return candidate
-    throwFailed
-  let major := lhs.appArg!
-  let majorType ← whnf (← inferType major)
-  let majorTypeArgs := majorType.getAppArgs
-  match majorType.getAppFn.const? with
-  | none => throwFailed
-  | some (_, us) =>
-    let recName := mkRecName info.name
-    let recInfo ← getConstInfoRec recName
-    let r := mkConst recName (levelZero :: us)
-    let r := mkAppN r majorTypeArgs[:info.numParams]
-    forallBoundedTelescope (← inferType r) recInfo.numMotives fun motiveFVars _ => do
-      let mut r := r
-      -- Add motives
-      for motiveFVar in motiveFVars do
-        let motive ← forallTelescopeReducing (← inferType motiveFVar) fun ys _ => do
-          let lhs ← mkSizeOf ys
-          let rhs ← mkAppM ``SizeOf.sizeOf #[ys.back]
-          mkLambdaFVars ys (← mkEq lhs rhs)
-        r := mkApp r motive
-      forallBoundedTelescope (← inferType r) recInfo.numMinors fun minorFVars _ => do
-        let mut r := r
-        -- Add minors
-        for minorFVar in minorFVars do
-          let minor ← forallTelescopeReducing (← inferType minorFVar) fun ys target => do
-            let target ← whnf target
-            let proof ← mkSorry target true -- TODO
-            mkLambdaFVars ys proof
-          r := mkApp r minor
-        -- Add indices and major
-        return mkAppN r indicesMajor
-
-/--
-  Generate proof for `C._sizeOf_<idx> t = sizeOf t` where `C._sizeOf_<idx>` is a auxiliary function
-  generated for a nested inductive type in `C`.
-  For example, given
-  ```lean
-  inductive Expr where
-    | app (f : String) (args : List Expr)
-  ```
-  We generate the auxiliary function `Expr._sizeOf_1 : List Expr → Nat`.
-  To generate the `sizeOf` spec lemma
-  ```
-  sizeOf (Expr.app f args) = 1 + sizeOf f + sizeOf args
-  ```
-  we need an auxiliary lemma for showing `Expr._sizeOf_1 args = sizeOf args`.
-  Recall that `sizeOf (Expr.app f args)` is definitionally equal to `1 + sizeOf f + Expr._sizeOf_1 args`, but
-  `Expr._sizeOf_1 args` is **not** definitionally equal to `sizeOf args`. We need a proof by induction.
-/
-private def mkSizeOfAuxLemma (lhs rhs : Expr) : M Expr := do
-  trace[Meta.sizeOf.aux]! "{lhs} =?= {rhs}"
-  match lhs.getAppFn.const? with
-  | none => throwFailed
-  | some (fName, us) =>
-    let thmLevelParams ← us.mapM fun
-      | Level.param n _ => return n
-      | _ => throwFailed
-    let thmName  := fName.appendAfter "_eq"
-    if (← getEnv).contains thmName then
-      -- Auxiliary lemma has already been defined
-      return mkAppN (mkConst thmName us) lhs.getAppArgs
+mutual
+  /-- Construct minor premise proof for `mkSizeOfAuxLemmaProof`. `ys` contains fields and inductive hypotheses for the minor premise. -/
+  private partial def mkMinorProof (ys : Array Expr) (lhs rhs : Expr) : M Expr := do
+    trace[Meta.sizeOf.minor]! "{lhs} =?= {rhs}"
+    if (← isDefEq lhs rhs) then
+      mkEqRefl rhs
    else
-      -- Define auxiliary lemma
-      -- First, generalize indices
-      let x := lhs.appArg!
-      let xType ← whnf (← inferType x)
-      matchConstInduct xType.getAppFn (fun _ => throwFailed) fun info _ => do
-        let params := xType.getAppArgs[:info.numParams]
-        forallTelescopeReducing (← inferType (mkAppN xType.getAppFn params)) fun indices _ => do
-          let majorType := mkAppN (mkAppN xType.getAppFn params) indices
-          withLocalDeclD `x majorType fun major => do
-            let lhsArgs := lhs.getAppArgs
-            let lhsArgsNew := lhsArgs[:lhsArgs.size - 1 - indices.size] ++ indices ++ #[major]
-            let lhsNew := mkAppN lhs.getAppFn lhsArgsNew
-            let rhsNew ← mkAppM ``SizeOf.sizeOf #[major]
-            let eq ← mkEq lhsNew rhsNew
-            let thmParams := lhsArgsNew
-            let thmType ← mkForallFVars thmParams eq
-            let thmValue ← mkSizeOfAuxLemmaProof info lhsNew rhsNew
-            let thmValue ← mkLambdaFVars thmParams thmValue
-            trace[Meta.sizeOf]! "thmValue: {thmValue}"
-            addDecl <| Declaration.thmDecl {
-              name        := thmName
-              levelParams := thmLevelParams
-              type        := thmType
-              value       := thmValue
-            }
-            return mkAppN (mkConst thmName us) lhs.getAppArgs
+      match (← whnfI lhs).natAdd?, (← whnfI rhs).natAdd? with
+      | some (a₁, b₁), some (a₂, b₂) =>
+        let p₁ ← mkMinorProof ys a₁ a₂
+        let p₂ ← mkMinorProofStep ys b₁ b₂
+        mkCongr (← mkCongrArg (mkConst ``Nat.add) p₁) p₂
+      | _, _ =>
+        throwUnexpected m!"expected 'Nat.add' application, lhs is {indentExpr lhs}\nrhs is{indentExpr rhs}"
+
+  /--
+    Helper method for `mkMinorProof`. The proof step is one of the following
+    - Reflexivity
+    - Assumption (i.e., using an inductive hypotheses from `ys`)
+    - `mkSizeOfAuxLemma` application. This case happens when we have multiple levels of nesting
+  -/
+  private partial def mkMinorProofStep (ys : Array Expr) (lhs rhs : Expr) : M Expr := do
+    if (← isDefEq lhs rhs) then
+      mkEqRefl rhs
+    else
+      let lhs ← recToSizeOf lhs
+      trace[Meta.sizeOf.minor.step]! "{lhs} =?= {rhs}"
+      let target ← mkEq lhs rhs
+      for y in ys do
+        if (← isDefEq (← inferType y) target) then
+          return y
+      mkSizeOfAuxLemma lhs rhs
+
+  /-- Construct proof of auxiliary lemma. See `mkSizeOfAuxLemma` -/
+  private partial def mkSizeOfAuxLemmaProof (info : InductiveVal) (lhs rhs : Expr) : M Expr := do
+    let lhsArgs := lhs.getAppArgs
+    let sizeOfBaseArgs := lhsArgs[:lhsArgs.size - info.numIndices - 1]
+    let indicesMajor := lhsArgs[lhsArgs.size - info.numIndices - 1:]
+    let sizeOfLevels := lhs.getAppFn.constLevels!
+    /- Auxiliary function for constructing an `_sizeOf_<idx>` for `ys`,
+       where `ys` are the indices + major.
+       Recall that if `info.name` is part of a mutually inductive declaration, then the resulting application
+       is not necessarily a `lhs.getAppFn` application.
+       The result is an application of one of the `(← read),sizeOfFns` functions.
+       We use this auxiliary function to builtin the motive of the recursor. -/
+    let rec mkSizeOf (ys : Array Expr) : M Expr := do
+      for sizeOfFn in (← read).sizeOfFns do
+        let candidate := mkAppN (mkAppN (mkConst sizeOfFn sizeOfLevels) sizeOfBaseArgs) ys
+        if (← isTypeCorrect candidate) then
+          return candidate
+      throwFailed
+    let major := lhs.appArg!
+    let majorType ← whnf (← inferType major)
+    let majorTypeArgs := majorType.getAppArgs
+    match majorType.getAppFn.const? with
+    | none => throwFailed
+    | some (_, us) =>
+      let recName := mkRecName info.name
+      let recInfo ← getConstInfoRec recName
+      let r := mkConst recName (levelZero :: us)
+      let r := mkAppN r majorTypeArgs[:info.numParams]
+      forallBoundedTelescope (← inferType r) recInfo.numMotives fun motiveFVars _ => do
+        let mut r := r
+        -- Add motives
+        for motiveFVar in motiveFVars do
+          let motive ← forallTelescopeReducing (← inferType motiveFVar) fun ys _ => do
+            let lhs ← mkSizeOf ys
+            let rhs ← mkAppM ``SizeOf.sizeOf #[ys.back]
+            mkLambdaFVars ys (← mkEq lhs rhs)
+          r := mkApp r motive
+        forallBoundedTelescope (← inferType r) recInfo.numMinors fun minorFVars _ => do
+          let mut r := r
+          -- Add minors
+          for minorFVar in minorFVars do
+            let minor ← forallTelescopeReducing (← inferType minorFVar) fun ys target => do
+              let target ← whnf target
+              match target.eq? with
+              | none => throwFailed
+              | some (_, lhs, rhs) =>
+                if (← isDefEq lhs rhs) then
+                  mkLambdaFVars ys (← mkEqRefl rhs)
+                else
+                  let lhs ← unfoldDefinition lhs -- Unfold `_sizeOf_<idx>`
+                  -- rhs is of the form `sizeOf (ctor ...)`
+                  let ctorApp := rhs.appArg!
+                  let specLemma ← mkSizeOfSpecLemmaInstance ctorApp
+                  let specEq ← whnf (← inferType specLemma)
+                  match specEq.eq? with
+                  | none => throwFailed
+                  | some (_, rhs, rhsExpanded) =>
+                    let lhs_eq_rhsExpanded ← mkMinorProof ys lhs rhsExpanded
+                    let rhsExpanded_eq_rhs ← mkEqSymm specLemma
+                    mkLambdaFVars ys (← mkEqTrans lhs_eq_rhsExpanded rhsExpanded_eq_rhs)
+            r := mkApp r minor
+          -- Add indices and major
+          return mkAppN r indicesMajor
+
+  /--
+    Generate proof for `C._sizeOf_<idx> t = sizeOf t` where `C._sizeOf_<idx>` is a auxiliary function
+    generated for a nested inductive type in `C`.
+    For example, given
+    ```lean
+    inductive Expr where
+      | app (f : String) (args : List Expr)
+    ```
+    We generate the auxiliary function `Expr._sizeOf_1 : List Expr → Nat`.
+    To generate the `sizeOf` spec lemma
+    ```
+    sizeOf (Expr.app f args) = 1 + sizeOf f + sizeOf args
+    ```
+    we need an auxiliary lemma for showing `Expr._sizeOf_1 args = sizeOf args`.
+    Recall that `sizeOf (Expr.app f args)` is definitionally equal to `1 + sizeOf f + Expr._sizeOf_1 args`, but
+    `Expr._sizeOf_1 args` is **not** definitionally equal to `sizeOf args`. We need a proof by induction.
+  -/
+  private partial def mkSizeOfAuxLemma (lhs rhs : Expr) : M Expr := do
+    trace[Meta.sizeOf.aux]! "{lhs} =?= {rhs}"
+    match lhs.getAppFn.const? with
+    | none => throwFailed
+    | some (fName, us) =>
+      let thmLevelParams ← us.mapM fun
+        | Level.param n _ => return n
+        | _ => throwFailed
+      let thmName  := fName.appendAfter "_eq"
+      if (← getEnv).contains thmName then
+        -- Auxiliary lemma has already been defined
+        return mkAppN (mkConst thmName us) lhs.getAppArgs
+      else
+        -- Define auxiliary lemma
+        -- First, generalize indices
+        let x := lhs.appArg!
+        let xType ← whnf (← inferType x)
+        matchConstInduct xType.getAppFn (fun _ => throwFailed) fun info _ => do
+          let params := xType.getAppArgs[:info.numParams]
+          forallTelescopeReducing (← inferType (mkAppN xType.getAppFn params)) fun indices _ => do
+            let majorType := mkAppN (mkAppN xType.getAppFn params) indices
+            withLocalDeclD `x majorType fun major => do
+              let lhsArgs := lhs.getAppArgs
+              let lhsArgsNew := lhsArgs[:lhsArgs.size - 1 - indices.size] ++ indices ++ #[major]
+              let lhsNew := mkAppN lhs.getAppFn lhsArgsNew
+              let rhsNew ← mkAppM ``SizeOf.sizeOf #[major]
+              let eq ← mkEq lhsNew rhsNew
+              let thmParams := lhsArgsNew
+              let thmType ← mkForallFVars thmParams eq
+              let thmValue ← mkSizeOfAuxLemmaProof info lhsNew rhsNew
+              let thmValue ← mkLambdaFVars thmParams thmValue
+              trace[Meta.sizeOf]! "thmValue: {thmValue}"
+              addDecl <| Declaration.thmDecl {
+                name        := thmName
+                levelParams := thmLevelParams
+                type        := thmType
+                value       := thmValue
+              }
+              return mkAppN (mkConst thmName us) lhs.getAppArgs
+
+end

 /- Prove SizeOf spec lemma of the form `sizeOf <ctor-application> = 1 + sizeOf <field_1> + ... + sizeOf <field_n> -/
 partial def main (lhs rhs : Expr) : M Expr := do
@ -340,7 +404,7 @@ private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name
        unless (← whnf (← inferType field)).isForall do
          rhs ← mkAdd rhs (← mkAppM ``SizeOf.sizeOf #[field])
      let target ← mkEq lhs rhs
-      let thmName := ctorName ++ `sizeOf_spec
+      let thmName   := mkSizeOfSpecLemmaName ctorName
      let thmParams := params ++ localInsts ++ fields
      let thmType ← mkForallFVars thmParams target
      let thmValue ←
--- a/stage0/stdlib/Init/Core.c
+++ b/stage0/stdlib/Init/Core.c
@ -17,6 +17,7 @@ lean_object* l_instDecidableIte___rarg___boxed(lean_object*, lean_object*, lean_
 lean_object* l_strictAnd___boxed(lean_object*, lean_object*);
 lean_object* lean_thunk_map(lean_object*, lean_object*);
 lean_object* l_instDecidableArrow___rarg___boxed(lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_Core___hyg_1346____closed__1;
 lean_object* l_Quotient_hrecOn___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Quotient_lift(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_reduceBool(uint8_t);
@ -24,13 +25,13 @@ lean_object* l_inline(lean_object*);
 lean_object* l_instDecidableDite(lean_object*, lean_object*, lean_object*);
 lean_object* l_Quotient_lift_u2082(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_term___u2260_____closed__2;
+lean_object* l_myMacro____x40_Init_Core___hyg_1767____closed__4;
 lean_object* l_instBEqProd_match__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Quotient_rec___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_bne(lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Quotient_liftOn(lean_object*, lean_object*, lean_object*);
 lean_object* l_Quotient_recOn(lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_960____closed__7;
 lean_object* l_Thunk_map___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_term___x3c_x2d_x3e__;
 lean_object* l_instDecidableEqProd_match__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -47,14 +48,14 @@ lean_object* l_instDecidableIff___rarg___boxed(lean_object*, lean_object*);
 extern lean_object* l_term___u2218_____closed__6;
 uint8_t l_decidableOfDecidableOfEq___rarg(uint8_t, lean_object*);
 lean_object* l_term___x21_x3d_____closed__5;
-lean_object* l_myMacro____x40_Init_Core___hyg_960____closed__3;
+lean_object* l_myMacro____x40_Init_Core___hyg_1767____closed__2;
 lean_object* l_Quot_indep(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Array_empty___closed__1;
 lean_object* l_Eq_ndrecOn___rarg(lean_object*);
 lean_object* l_term___x21_x3d_____closed__2;
 lean_object* l_instHasLessProd(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_1792____closed__2;
 lean_object* l_term___u2260_____closed__1;
+lean_object* l_myMacro____x40_Init_Core___hyg_935____closed__7;
 lean_object* l_Quot_liftOn___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_instDecidableEqProd_match__2(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Eq_mpr___rarg___boxed(lean_object*);
@ -76,54 +77,54 @@ lean_object* l_term___u2260_____closed__5;
 lean_object* l_term___x21_x3d_____closed__3;
 lean_object* l_term___u2260_____closed__3;
 lean_object* l_prodHasDecidableLt___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_1792____closed__4;
+lean_object* l_myMacro____x40_Init_Core___hyg_935____closed__3;
+lean_object* l_myMacro____x40_Init_Core___hyg_1346____closed__4;
 lean_object* lean_string_utf8_byte_size(lean_object*);
+lean_object* l_myMacro____x40_Init_Core___hyg_1767____closed__1;
 lean_object* l_Quotient_recOnSubsingleton___rarg(lean_object*, lean_object*);
 lean_object* l_Task_get___boxed(lean_object*, lean_object*);
 lean_object* l_myMacro____x40_Init_Core___hyg_172____closed__1;
 lean_object* l_Task_map___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_1792____closed__1;
 lean_object* l_instDecidableEqProd_match__2___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Decidable_byCases___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_term___u2248__;
 uint8_t l_toBoolUsing___rarg(uint8_t);
 lean_object* l_Eq_ndrecOn___rarg___boxed(lean_object*);
+lean_object* l_myMacro____x40_Init_Core___hyg_1346____closed__6;
 lean_object* l_Quotient_mk(lean_object*, lean_object*);
 lean_object* l_Quotient_liftOn___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_instDecidableEqProd_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_term___u2194_____closed__1;
 lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_myMacro____x40_Init_Notation___hyg_109____spec__1(lean_object*, lean_object*);
 lean_object* l_Quot_rec___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_Core___hyg_935____closed__1;
 lean_object* l_instHasEquiv(lean_object*, lean_object*);
 lean_object* l_Quotient_lift_u2082___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_term___u2194_____closed__2;
 lean_object* l_Task_bind___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_1371____closed__3;
-lean_object* l_myMacro____x40_Init_Core___hyg_960____closed__8;
+lean_object* l_myMacro____x40_Init_Core___hyg_1767____closed__6;
 lean_object* lean_thunk_pure(lean_object*);
 lean_object* l_term___u2260__;
 lean_object* l_myMacro____x40_Init_Core___hyg_172____closed__6;
 lean_object* l_instDecidableDite_match__1(lean_object*, lean_object*);
 lean_object* l_decidableOfDecidableOfEq___rarg___boxed(lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_960____closed__9;
 lean_object* l_toBoolUsing___rarg___boxed(lean_object*);
 lean_object* l_strictOr___boxed(lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_960____closed__4;
 lean_object* l_Quotient_recOnSubsingleton_u2082___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Subtype_instDecidableEqSubtype___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_term___x3c_x2d_x3e_____closed__6;
 lean_object* l_Quotient_mk___boxed(lean_object*, lean_object*);
 lean_object* l_instDecidableEqQuotient___boxed(lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_1792____closed__6;
 lean_object* l_instDecidableDite___rarg(uint8_t, lean_object*, lean_object*);
 lean_object* l_term___u2260_____closed__6;
 lean_object* l_Eq_mpr(lean_object*, lean_object*, lean_object*);
 lean_object* l_Quot_recOn___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Thunk_get___boxed(lean_object*, lean_object*);
 lean_object* l_term___u2194_____closed__4;
+lean_object* l_myMacro____x40_Init_Core___hyg_1767____closed__3;
 lean_object* l_Quot_recOnSubsingleton(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_myMacro____x40_Init_Core___hyg_172____closed__2;
-lean_object* l_myMacro____x40_Init_Core___hyg_960____closed__6;
+lean_object* l_myMacro____x40_Init_Core___hyg_1346____closed__2;
 lean_object* l_Lean_reduceNat(lean_object*);
 lean_object* l_instBEqProd_match__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_instDecidableEqProd_match__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -132,13 +133,15 @@ uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l_Sum_inhabitedLeft___rarg(lean_object*);
 lean_object* l_Quotient_lift_u2082___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_instDecidableIte___rarg(uint8_t, uint8_t, uint8_t);
+lean_object* l_myMacro____x40_Init_Core___hyg_935____closed__2;
 lean_object* l_instDecidableEqQuotient_match__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Quot_hrecOn(lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_960_(lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_Core___hyg_935_(lean_object*, lean_object*, lean_object*);
 lean_object* l_myMacro____x40_Init_Core___hyg_428_(lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_1792_(lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_1371_(lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_Core___hyg_1767_(lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_Core___hyg_1346_(lean_object*, lean_object*, lean_object*);
 lean_object* l_myMacro____x40_Init_Core___hyg_172_(lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_Core___hyg_935____closed__4;
 lean_object* l_Task_Priority_dedicated;
 lean_object* l_instDecidableEqProd_match__3___rarg(lean_object*, lean_object*);
 lean_object* l_myMacro____x40_Init_Core___hyg_172____closed__4;
@ -146,12 +149,15 @@ lean_object* l_Sum_inhabitedRight___rarg(lean_object*);
 lean_object* l_Quotient_lift___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Quotient_recOnSubsingleton_u2082___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_instInhabitedProd(lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_Core___hyg_935____closed__6;
 lean_object* l_instDecidableEqProd_match__1___rarg(uint8_t, lean_object*, lean_object*);
 lean_object* l_instInhabitedForInStep___rarg(lean_object*);
+lean_object* l_myMacro____x40_Init_Core___hyg_935____closed__8;
+lean_object* l_myMacro____x40_Init_Core___hyg_1346____closed__5;
 lean_object* l_instDecidableDite_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_instInhabitedPNonScalar;
 lean_object* l_instDecidableEqQuotient(lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_960____closed__2;
+lean_object* l_myMacro____x40_Init_Core___hyg_935____closed__9;
 lean_object* lean_task_map(lean_object*, lean_object*, lean_object*);
 lean_object* l_instDecidableEqProd_match__2___rarg(uint8_t, lean_object*, lean_object*);
 lean_object* l_instInhabitedProp;
@ -159,14 +165,13 @@ lean_object* l_flip___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Quotient_hrecOn___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Quotient_rec(lean_object*, lean_object*, lean_object*);
 lean_object* l_Quotient_liftOn_u2082___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_960____closed__1;
 lean_object* l_instInhabitedNonScalar;
 lean_object* l_instDecidableIte_match__1___rarg(uint8_t, lean_object*, lean_object*);
-lean_object* l_unexpand____x40_Init_Core___hyg_941_(lean_object*, lean_object*);
-lean_object* l_unexpand____x40_Init_Core___hyg_1352_(lean_object*, lean_object*);
+lean_object* l_unexpand____x40_Init_Core___hyg_916_(lean_object*, lean_object*);
+lean_object* l_unexpand____x40_Init_Core___hyg_1327_(lean_object*, lean_object*);
 lean_object* l_unexpand____x40_Init_Core___hyg_409_(lean_object*, lean_object*);
 lean_object* l_unexpand____x40_Init_Core___hyg_153_(lean_object*, lean_object*);
-lean_object* l_unexpand____x40_Init_Core___hyg_1773_(lean_object*, lean_object*);
+lean_object* l_unexpand____x40_Init_Core___hyg_1748_(lean_object*, lean_object*);
 lean_object* l_instDecidableIff(lean_object*, lean_object*);
 uint8_t l_instDecidableIff___rarg(uint8_t, uint8_t);
 lean_object* l_term___x3c_x2d_x3e_____closed__5;
@ -178,7 +183,6 @@ lean_object* l_Eq_mpr___rarg(lean_object*);
 lean_object* l_term___x3c_x2d_x3e_____closed__4;
 lean_object* l_decidableOfDecidableOfEq(lean_object*, lean_object*);
 lean_object* l_instDecidableEqProd___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_1371____closed__5;
 lean_object* l_Squash_mk(lean_object*);
 lean_object* lean_mk_thunk(lean_object*);
 lean_object* l_Thunk_bind___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -192,6 +196,7 @@ lean_object* l_instDecidableEqQuotient___rarg(lean_object*, lean_object*, lean_o
 lean_object* l_term___u2248_____closed__4;
 lean_object* l_instBEqProd___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_Core___hyg_1346____closed__3;
 extern lean_object* l_Lean_nullKind___closed__2;
 lean_object* l_Squash_lift(lean_object*, lean_object*, lean_object*);
 lean_object* l_term___x3c_x2d_x3e_____closed__3;
@ -205,7 +210,6 @@ lean_object* l_Subtype_instDecidableEqSubtype_match__1(lean_object*, lean_object
 lean_object* l_Subtype_instInhabitedSubtype___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Decidable_byCases_match__1___rarg(uint8_t, lean_object*, lean_object*);
 lean_object* l_instInhabitedProd___rarg(lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_1371____closed__6;
 uint8_t l_instInhabitedBool;
 uint8_t l_instDecidableFalse;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_2191____closed__4;
@ -215,10 +219,9 @@ lean_object* l_prodHasDecidableLt___boxed(lean_object*, lean_object*, lean_objec
 lean_object* l_Quotient_mk___rarg(lean_object*);
 lean_object* l_Prod_map___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* lean_task_bind(lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_1792____closed__3;
 lean_object* l_instDecidableEqProd_match__4___rarg(lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_1792____closed__5;
 uint8_t l_bne___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_Core___hyg_1767____closed__5;
 lean_object* l_Lean_Syntax_getArgs(lean_object*);
 lean_object* l_instDecidableEqSum(lean_object*, lean_object*);
 lean_object* l_Subtype_instInhabitedSubtype(lean_object*, lean_object*);
@ -244,14 +247,13 @@ lean_object* l_Task_Priority_max;
 lean_object* l_instDecidableEqSum_match__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Decidable_byCases_match__1(lean_object*, lean_object*);
 lean_object* l_Lean_reduceNat___boxed(lean_object*);
+lean_object* l_myMacro____x40_Init_Core___hyg_935____closed__5;
 lean_object* l_Eq_ndrecOn___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_1371____closed__1;
 lean_object* l_Quotient_rec___rarg(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
 lean_object* l_term___x3c_x2d_x3e_____closed__1;
 lean_object* l_Task_pure___boxed(lean_object*, lean_object*);
 lean_object* l_instDecidableEqQuotient_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_1371____closed__2;
 lean_object* l_Quotient_liftOn_u2082(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Prod_map(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_term___x21_x3d_____closed__4;
@ -269,7 +271,6 @@ lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 lean_object* l_Quotient_recOnSubsingleton_u2082(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Decidable_byCases(lean_object*, lean_object*);
 lean_object* l_inline___rarg(lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_1371____closed__4;
 lean_object* l_instDecidableEqSum_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Core_0__funSetoid(lean_object*, lean_object*);
 lean_object* l_Sum_inhabitedRight(lean_object*, lean_object*);
@ -280,7 +281,6 @@ lean_object* l_term___u2248_____closed__2;
 uint8_t l_instDecidableArrow___rarg(uint8_t, uint8_t);
 lean_object* l_Squash_mk___rarg(lean_object*);
 lean_object* l_instDecidableIte(lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_Core___hyg_960____closed__5;
 lean_object* l_Thunk_pure___boxed(lean_object*, lean_object*);
 lean_object* l_decidableOfDecidableOfIff(lean_object*, lean_object*);
 lean_object* l___private_Init_Core_0__extfunApp(lean_object*, lean_object*);
@ -1150,7 +1150,7 @@ x_1 = l_term___u2248_____closed__6;
 return x_1;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_960____closed__1() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_935____closed__1() {
 _start:
 {
 lean_object* x_1; 
@ -1158,22 +1158,22 @@ x_1 = lean_mk_string("HasEquiv.Equiv");
 return x_1;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_960____closed__2() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_935____closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_myMacro____x40_Init_Core___hyg_960____closed__1;
+x_1 = l_myMacro____x40_Init_Core___hyg_935____closed__1;
 x_2 = lean_string_utf8_byte_size(x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_960____closed__3() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_935____closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_myMacro____x40_Init_Core___hyg_960____closed__1;
+x_1 = l_myMacro____x40_Init_Core___hyg_935____closed__1;
 x_2 = lean_unsigned_to_nat(0u);
-x_3 = l_myMacro____x40_Init_Core___hyg_960____closed__2;
+x_3 = l_myMacro____x40_Init_Core___hyg_935____closed__2;
 x_4 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@ -1181,7 +1181,7 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_960____closed__4() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_935____closed__4() {
 _start:
 {
 lean_object* x_1; 
@ -1189,17 +1189,17 @@ x_1 = lean_mk_string("HasEquiv");
 return x_1;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_960____closed__5() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_935____closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_Core___hyg_960____closed__4;
+x_2 = l_myMacro____x40_Init_Core___hyg_935____closed__4;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_960____closed__6() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_935____closed__6() {
 _start:
 {
 lean_object* x_1; 
@ -1207,41 +1207,41 @@ x_1 = lean_mk_string("Equiv");
 return x_1;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_960____closed__7() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_935____closed__7() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_myMacro____x40_Init_Core___hyg_960____closed__5;
-x_2 = l_myMacro____x40_Init_Core___hyg_960____closed__6;
+x_1 = l_myMacro____x40_Init_Core___hyg_935____closed__5;
+x_2 = l_myMacro____x40_Init_Core___hyg_935____closed__6;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_960____closed__8() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_935____closed__8() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_Core___hyg_960____closed__7;
+x_2 = l_myMacro____x40_Init_Core___hyg_935____closed__7;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_960____closed__9() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_935____closed__9() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_Core___hyg_960____closed__8;
+x_2 = l_myMacro____x40_Init_Core___hyg_935____closed__8;
 x_3 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-lean_object* l_myMacro____x40_Init_Core___hyg_960_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_myMacro____x40_Init_Core___hyg_935_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; uint8_t x_5; 
@ -1278,10 +1278,10 @@ lean_inc(x_15);
 x_16 = lean_ctor_get(x_2, 1);
 lean_inc(x_16);
 lean_dec(x_2);
-x_17 = l_myMacro____x40_Init_Core___hyg_960____closed__7;
+x_17 = l_myMacro____x40_Init_Core___hyg_935____closed__7;
 x_18 = l_Lean_addMacroScope(x_16, x_17, x_15);
-x_19 = l_myMacro____x40_Init_Core___hyg_960____closed__3;
-x_20 = l_myMacro____x40_Init_Core___hyg_960____closed__9;
+x_19 = l_myMacro____x40_Init_Core___hyg_935____closed__3;
+x_20 = l_myMacro____x40_Init_Core___hyg_935____closed__9;
 x_21 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_21, 0, x_14);
 lean_ctor_set(x_21, 1, x_19);
@ -1316,10 +1316,10 @@ lean_inc(x_33);
 x_34 = lean_ctor_get(x_2, 1);
 lean_inc(x_34);
 lean_dec(x_2);
-x_35 = l_myMacro____x40_Init_Core___hyg_960____closed__7;
+x_35 = l_myMacro____x40_Init_Core___hyg_935____closed__7;
 x_36 = l_Lean_addMacroScope(x_34, x_35, x_33);
-x_37 = l_myMacro____x40_Init_Core___hyg_960____closed__3;
-x_38 = l_myMacro____x40_Init_Core___hyg_960____closed__9;
+x_37 = l_myMacro____x40_Init_Core___hyg_935____closed__3;
+x_38 = l_myMacro____x40_Init_Core___hyg_935____closed__9;
 x_39 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_39, 0, x_31);
 lean_ctor_set(x_39, 1, x_37);
@ -1346,7 +1346,7 @@ return x_49;
 }
 }
 }
-lean_object* l_unexpand____x40_Init_Core___hyg_941_(lean_object* x_1, lean_object* x_2) {
+lean_object* l_unexpand____x40_Init_Core___hyg_916_(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; uint8_t x_4; 
@ -1659,7 +1659,7 @@ x_1 = l_term___x21_x3d_____closed__6;
 return x_1;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1371____closed__1() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1346____closed__1() {
 _start:
 {
 lean_object* x_1; 
@ -1667,22 +1667,22 @@ x_1 = lean_mk_string("bne");
 return x_1;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1371____closed__2() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1346____closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_myMacro____x40_Init_Core___hyg_1371____closed__1;
+x_1 = l_myMacro____x40_Init_Core___hyg_1346____closed__1;
 x_2 = lean_string_utf8_byte_size(x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1371____closed__3() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1346____closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_myMacro____x40_Init_Core___hyg_1371____closed__1;
+x_1 = l_myMacro____x40_Init_Core___hyg_1346____closed__1;
 x_2 = lean_unsigned_to_nat(0u);
-x_3 = l_myMacro____x40_Init_Core___hyg_1371____closed__2;
+x_3 = l_myMacro____x40_Init_Core___hyg_1346____closed__2;
 x_4 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@ -1690,41 +1690,41 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1371____closed__4() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1346____closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_Core___hyg_1371____closed__1;
+x_2 = l_myMacro____x40_Init_Core___hyg_1346____closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1371____closed__5() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1346____closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_Core___hyg_1371____closed__4;
+x_2 = l_myMacro____x40_Init_Core___hyg_1346____closed__4;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1371____closed__6() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1346____closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_Core___hyg_1371____closed__5;
+x_2 = l_myMacro____x40_Init_Core___hyg_1346____closed__5;
 x_3 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-lean_object* l_myMacro____x40_Init_Core___hyg_1371_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_myMacro____x40_Init_Core___hyg_1346_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; uint8_t x_5; 
@ -1761,10 +1761,10 @@ lean_inc(x_15);
 x_16 = lean_ctor_get(x_2, 1);
 lean_inc(x_16);
 lean_dec(x_2);
-x_17 = l_myMacro____x40_Init_Core___hyg_1371____closed__4;
+x_17 = l_myMacro____x40_Init_Core___hyg_1346____closed__4;
 x_18 = l_Lean_addMacroScope(x_16, x_17, x_15);
-x_19 = l_myMacro____x40_Init_Core___hyg_1371____closed__3;
-x_20 = l_myMacro____x40_Init_Core___hyg_1371____closed__6;
+x_19 = l_myMacro____x40_Init_Core___hyg_1346____closed__3;
+x_20 = l_myMacro____x40_Init_Core___hyg_1346____closed__6;
 x_21 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_21, 0, x_14);
 lean_ctor_set(x_21, 1, x_19);
@ -1799,10 +1799,10 @@ lean_inc(x_33);
 x_34 = lean_ctor_get(x_2, 1);
 lean_inc(x_34);
 lean_dec(x_2);
-x_35 = l_myMacro____x40_Init_Core___hyg_1371____closed__4;
+x_35 = l_myMacro____x40_Init_Core___hyg_1346____closed__4;
 x_36 = l_Lean_addMacroScope(x_34, x_35, x_33);
-x_37 = l_myMacro____x40_Init_Core___hyg_1371____closed__3;
-x_38 = l_myMacro____x40_Init_Core___hyg_1371____closed__6;
+x_37 = l_myMacro____x40_Init_Core___hyg_1346____closed__3;
+x_38 = l_myMacro____x40_Init_Core___hyg_1346____closed__6;
 x_39 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_39, 0, x_31);
 lean_ctor_set(x_39, 1, x_37);
@ -1829,7 +1829,7 @@ return x_49;
 }
 }
 }
-lean_object* l_unexpand____x40_Init_Core___hyg_1352_(lean_object* x_1, lean_object* x_2) {
+lean_object* l_unexpand____x40_Init_Core___hyg_1327_(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; uint8_t x_4; 
@ -2062,7 +2062,7 @@ x_1 = l_term___u2260_____closed__6;
 return x_1;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1792____closed__1() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1767____closed__1() {
 _start:
 {
 lean_object* x_1; 
@ -2070,22 +2070,22 @@ x_1 = lean_mk_string("Ne");
 return x_1;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1792____closed__2() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1767____closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_myMacro____x40_Init_Core___hyg_1792____closed__1;
+x_1 = l_myMacro____x40_Init_Core___hyg_1767____closed__1;
 x_2 = lean_string_utf8_byte_size(x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1792____closed__3() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1767____closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_myMacro____x40_Init_Core___hyg_1792____closed__1;
+x_1 = l_myMacro____x40_Init_Core___hyg_1767____closed__1;
 x_2 = lean_unsigned_to_nat(0u);
-x_3 = l_myMacro____x40_Init_Core___hyg_1792____closed__2;
+x_3 = l_myMacro____x40_Init_Core___hyg_1767____closed__2;
 x_4 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@ -2093,41 +2093,41 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1792____closed__4() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1767____closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_Core___hyg_1792____closed__1;
+x_2 = l_myMacro____x40_Init_Core___hyg_1767____closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1792____closed__5() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1767____closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_Core___hyg_1792____closed__4;
+x_2 = l_myMacro____x40_Init_Core___hyg_1767____closed__4;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1792____closed__6() {
+static lean_object* _init_l_myMacro____x40_Init_Core___hyg_1767____closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_Core___hyg_1792____closed__5;
+x_2 = l_myMacro____x40_Init_Core___hyg_1767____closed__5;
 x_3 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-lean_object* l_myMacro____x40_Init_Core___hyg_1792_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_myMacro____x40_Init_Core___hyg_1767_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; uint8_t x_5; 
@ -2164,10 +2164,10 @@ lean_inc(x_15);
 x_16 = lean_ctor_get(x_2, 1);
 lean_inc(x_16);
 lean_dec(x_2);
-x_17 = l_myMacro____x40_Init_Core___hyg_1792____closed__4;
+x_17 = l_myMacro____x40_Init_Core___hyg_1767____closed__4;
 x_18 = l_Lean_addMacroScope(x_16, x_17, x_15);
-x_19 = l_myMacro____x40_Init_Core___hyg_1792____closed__3;
-x_20 = l_myMacro____x40_Init_Core___hyg_1792____closed__6;
+x_19 = l_myMacro____x40_Init_Core___hyg_1767____closed__3;
+x_20 = l_myMacro____x40_Init_Core___hyg_1767____closed__6;
 x_21 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_21, 0, x_14);
 lean_ctor_set(x_21, 1, x_19);
@ -2202,10 +2202,10 @@ lean_inc(x_33);
 x_34 = lean_ctor_get(x_2, 1);
 lean_inc(x_34);
 lean_dec(x_2);
-x_35 = l_myMacro____x40_Init_Core___hyg_1792____closed__4;
+x_35 = l_myMacro____x40_Init_Core___hyg_1767____closed__4;
 x_36 = l_Lean_addMacroScope(x_34, x_35, x_33);
-x_37 = l_myMacro____x40_Init_Core___hyg_1792____closed__3;
-x_38 = l_myMacro____x40_Init_Core___hyg_1792____closed__6;
+x_37 = l_myMacro____x40_Init_Core___hyg_1767____closed__3;
+x_38 = l_myMacro____x40_Init_Core___hyg_1767____closed__6;
 x_39 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_39, 0, x_31);
 lean_ctor_set(x_39, 1, x_37);
@ -2232,7 +2232,7 @@ return x_49;
 }
 }
 }
-lean_object* l_unexpand____x40_Init_Core___hyg_1773_(lean_object* x_1, lean_object* x_2) {
+lean_object* l_unexpand____x40_Init_Core___hyg_1748_(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; uint8_t x_4; 
@ -4127,24 +4127,24 @@ l_term___u2248_____closed__6 = _init_l_term___u2248_____closed__6();
 lean_mark_persistent(l_term___u2248_____closed__6);
 l_term___u2248__ = _init_l_term___u2248__();
 lean_mark_persistent(l_term___u2248__);
-l_myMacro____x40_Init_Core___hyg_960____closed__1 = _init_l_myMacro____x40_Init_Core___hyg_960____closed__1();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_960____closed__1);
-l_myMacro____x40_Init_Core___hyg_960____closed__2 = _init_l_myMacro____x40_Init_Core___hyg_960____closed__2();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_960____closed__2);
-l_myMacro____x40_Init_Core___hyg_960____closed__3 = _init_l_myMacro____x40_Init_Core___hyg_960____closed__3();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_960____closed__3);
-l_myMacro____x40_Init_Core___hyg_960____closed__4 = _init_l_myMacro____x40_Init_Core___hyg_960____closed__4();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_960____closed__4);
-l_myMacro____x40_Init_Core___hyg_960____closed__5 = _init_l_myMacro____x40_Init_Core___hyg_960____closed__5();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_960____closed__5);
-l_myMacro____x40_Init_Core___hyg_960____closed__6 = _init_l_myMacro____x40_Init_Core___hyg_960____closed__6();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_960____closed__6);
-l_myMacro____x40_Init_Core___hyg_960____closed__7 = _init_l_myMacro____x40_Init_Core___hyg_960____closed__7();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_960____closed__7);
-l_myMacro____x40_Init_Core___hyg_960____closed__8 = _init_l_myMacro____x40_Init_Core___hyg_960____closed__8();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_960____closed__8);
-l_myMacro____x40_Init_Core___hyg_960____closed__9 = _init_l_myMacro____x40_Init_Core___hyg_960____closed__9();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_960____closed__9);
+l_myMacro____x40_Init_Core___hyg_935____closed__1 = _init_l_myMacro____x40_Init_Core___hyg_935____closed__1();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_935____closed__1);
+l_myMacro____x40_Init_Core___hyg_935____closed__2 = _init_l_myMacro____x40_Init_Core___hyg_935____closed__2();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_935____closed__2);
+l_myMacro____x40_Init_Core___hyg_935____closed__3 = _init_l_myMacro____x40_Init_Core___hyg_935____closed__3();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_935____closed__3);
+l_myMacro____x40_Init_Core___hyg_935____closed__4 = _init_l_myMacro____x40_Init_Core___hyg_935____closed__4();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_935____closed__4);
+l_myMacro____x40_Init_Core___hyg_935____closed__5 = _init_l_myMacro____x40_Init_Core___hyg_935____closed__5();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_935____closed__5);
+l_myMacro____x40_Init_Core___hyg_935____closed__6 = _init_l_myMacro____x40_Init_Core___hyg_935____closed__6();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_935____closed__6);
+l_myMacro____x40_Init_Core___hyg_935____closed__7 = _init_l_myMacro____x40_Init_Core___hyg_935____closed__7();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_935____closed__7);
+l_myMacro____x40_Init_Core___hyg_935____closed__8 = _init_l_myMacro____x40_Init_Core___hyg_935____closed__8();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_935____closed__8);
+l_myMacro____x40_Init_Core___hyg_935____closed__9 = _init_l_myMacro____x40_Init_Core___hyg_935____closed__9();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_935____closed__9);
 l_Task_Priority_default = _init_l_Task_Priority_default();
 lean_mark_persistent(l_Task_Priority_default);
 l_Task_Priority_max = _init_l_Task_Priority_max();
@ -4165,18 +4165,18 @@ l_term___x21_x3d_____closed__6 = _init_l_term___x21_x3d_____closed__6();
 lean_mark_persistent(l_term___x21_x3d_____closed__6);
 l_term___x21_x3d__ = _init_l_term___x21_x3d__();
 lean_mark_persistent(l_term___x21_x3d__);
-l_myMacro____x40_Init_Core___hyg_1371____closed__1 = _init_l_myMacro____x40_Init_Core___hyg_1371____closed__1();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1371____closed__1);
-l_myMacro____x40_Init_Core___hyg_1371____closed__2 = _init_l_myMacro____x40_Init_Core___hyg_1371____closed__2();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1371____closed__2);
-l_myMacro____x40_Init_Core___hyg_1371____closed__3 = _init_l_myMacro____x40_Init_Core___hyg_1371____closed__3();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1371____closed__3);
-l_myMacro____x40_Init_Core___hyg_1371____closed__4 = _init_l_myMacro____x40_Init_Core___hyg_1371____closed__4();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1371____closed__4);
-l_myMacro____x40_Init_Core___hyg_1371____closed__5 = _init_l_myMacro____x40_Init_Core___hyg_1371____closed__5();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1371____closed__5);
-l_myMacro____x40_Init_Core___hyg_1371____closed__6 = _init_l_myMacro____x40_Init_Core___hyg_1371____closed__6();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1371____closed__6);
+l_myMacro____x40_Init_Core___hyg_1346____closed__1 = _init_l_myMacro____x40_Init_Core___hyg_1346____closed__1();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1346____closed__1);
+l_myMacro____x40_Init_Core___hyg_1346____closed__2 = _init_l_myMacro____x40_Init_Core___hyg_1346____closed__2();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1346____closed__2);
+l_myMacro____x40_Init_Core___hyg_1346____closed__3 = _init_l_myMacro____x40_Init_Core___hyg_1346____closed__3();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1346____closed__3);
+l_myMacro____x40_Init_Core___hyg_1346____closed__4 = _init_l_myMacro____x40_Init_Core___hyg_1346____closed__4();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1346____closed__4);
+l_myMacro____x40_Init_Core___hyg_1346____closed__5 = _init_l_myMacro____x40_Init_Core___hyg_1346____closed__5();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1346____closed__5);
+l_myMacro____x40_Init_Core___hyg_1346____closed__6 = _init_l_myMacro____x40_Init_Core___hyg_1346____closed__6();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1346____closed__6);
 l_term___u2260_____closed__1 = _init_l_term___u2260_____closed__1();
 lean_mark_persistent(l_term___u2260_____closed__1);
 l_term___u2260_____closed__2 = _init_l_term___u2260_____closed__2();
@ -4191,18 +4191,18 @@ l_term___u2260_____closed__6 = _init_l_term___u2260_____closed__6();
 lean_mark_persistent(l_term___u2260_____closed__6);
 l_term___u2260__ = _init_l_term___u2260__();
 lean_mark_persistent(l_term___u2260__);
-l_myMacro____x40_Init_Core___hyg_1792____closed__1 = _init_l_myMacro____x40_Init_Core___hyg_1792____closed__1();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1792____closed__1);
-l_myMacro____x40_Init_Core___hyg_1792____closed__2 = _init_l_myMacro____x40_Init_Core___hyg_1792____closed__2();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1792____closed__2);
-l_myMacro____x40_Init_Core___hyg_1792____closed__3 = _init_l_myMacro____x40_Init_Core___hyg_1792____closed__3();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1792____closed__3);
-l_myMacro____x40_Init_Core___hyg_1792____closed__4 = _init_l_myMacro____x40_Init_Core___hyg_1792____closed__4();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1792____closed__4);
-l_myMacro____x40_Init_Core___hyg_1792____closed__5 = _init_l_myMacro____x40_Init_Core___hyg_1792____closed__5();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1792____closed__5);
-l_myMacro____x40_Init_Core___hyg_1792____closed__6 = _init_l_myMacro____x40_Init_Core___hyg_1792____closed__6();
-lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1792____closed__6);
+l_myMacro____x40_Init_Core___hyg_1767____closed__1 = _init_l_myMacro____x40_Init_Core___hyg_1767____closed__1();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1767____closed__1);
+l_myMacro____x40_Init_Core___hyg_1767____closed__2 = _init_l_myMacro____x40_Init_Core___hyg_1767____closed__2();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1767____closed__2);
+l_myMacro____x40_Init_Core___hyg_1767____closed__3 = _init_l_myMacro____x40_Init_Core___hyg_1767____closed__3();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1767____closed__3);
+l_myMacro____x40_Init_Core___hyg_1767____closed__4 = _init_l_myMacro____x40_Init_Core___hyg_1767____closed__4();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1767____closed__4);
+l_myMacro____x40_Init_Core___hyg_1767____closed__5 = _init_l_myMacro____x40_Init_Core___hyg_1767____closed__5();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1767____closed__5);
+l_myMacro____x40_Init_Core___hyg_1767____closed__6 = _init_l_myMacro____x40_Init_Core___hyg_1767____closed__6();
+lean_mark_persistent(l_myMacro____x40_Init_Core___hyg_1767____closed__6);
 l_instDecidableTrue = _init_l_instDecidableTrue();
 l_instDecidableFalse = _init_l_instDecidableFalse();
 l_instInhabitedProp = _init_l_instInhabitedProp();
--- a/stage0/stdlib/Lean/Meta/SizeOf.c
+++ b/stage0/stdlib/Lean/Meta/SizeOf.c