max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-02 15:57:22 -07:00
parent a0fdc2d050
commit a1d09f1ced
16 changed files with 1663 additions and 1128 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
stage0/src/Init/Data/Array/Basic.lean generated
View file

@ -39,13 +39,13 @@ def singleton (v : α) : Array α :=
`fget` may be slightly slower than `uget`. -/
@[extern "lean_array_uget"]
def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
a.get ⟨i.toNat, h⟩
a[i.toNat, h]
def back [Inhabited α] (a : Array α) : α :=
a.get! (a.size - 1)
def get? (a : Array α) (i : Nat) : Option α :=
if h : i < a.size then some (a.get ⟨i, h⟩) else none
if h : i < a.size then some a[i, h] else none
abbrev getOp? (self : Array α) (idx : Nat) : Option α :=
self.get? idx
@ -55,7 +55,7 @@ def back? (a : Array α) : Option α :=
-- auxiliary declaration used in the equation compiler when pattern matching array literals.
abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
a.get ⟨i, h₁.symm ▸ h₂⟩
a[i, h₁.symm ▸ h₂]
@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
List.length_set ..
@ -166,7 +166,7 @@ protected def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m
have h' : i < as.size := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
have : as.size - 1 < as.size := Nat.sub_lt (Nat.zero_lt_of_lt h') (by decide)
have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
match (← f (as.get ⟨as.size - 1 - i, this⟩) b) with
match (← f as[as.size - 1 - i, this] b) with
| ForInStep.done b => pure b
| ForInStep.yield b => loop i (Nat.le_of_lt h') b
loop as.size (Nat.le_refl _) b
@ -199,7 +199,7 @@ def foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β
match i with
| 0 => pure b
| i'+1 =>
loop i' (j+1) (← f b (as.get ⟨j, Nat.lt_of_lt_of_le hlt h⟩))
loop i' (j+1) (← f b as[j, Nat.lt_of_lt_of_le hlt h])
else
pure b
loop (stop - start) start init
@ -236,7 +236,7 @@ def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
| 0, _ => pure b
| i+1, h =>
have : i < as.size := Nat.lt_of_lt_of_le (Nat.lt_succ_self _) h
fold i (Nat.le_of_lt this) (← f (as.get ⟨i, this⟩) b)
fold i (Nat.le_of_lt this) (← f as[i, this] b)
if h : start ≤ as.size then
if stop < start then
fold start h init
@ -330,7 +330,7 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
let any (stop : Nat) (h : stop ≤ as.size) :=
let rec loop (j : Nat) : m Bool := do
if hlt : j < stop then
if (← p (as.get ⟨j, Nat.lt_of_lt_of_le hlt h⟩)) then
if (← p as[j, Nat.lt_of_lt_of_le hlt h]) then
pure true
else
loop (j+1)
@ -353,7 +353,7 @@ def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
| 0, _ => pure none
| i+1, h => do
have : i < as.size := Nat.lt_of_lt_of_le (Nat.lt_succ_self _) h
let r ← f (as.get ⟨i, this⟩)
let r ← f as[i, this]
match r with
| some _ => pure r
| none =>
@ -422,7 +422,7 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
rw [inv] at hlt
exact absurd hlt (Nat.lt_irrefl _)
| i+1, inv =>
if p (as.get ⟨j, hlt⟩) then
if p as[j, hlt] then
some j
else
have : i + (j+1) = as.size := by
@ -515,7 +515,7 @@ namespace Array
@[specialize]
def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
if h : i < a.size then
p (a.get ⟨i, h⟩) (b.get ⟨i, hsz ▸ h⟩) && isEqvAux a b hsz p (i+1)
p a[i, h] b[i, hsz ▸ h] && isEqvAux a b hsz p (i+1)
else
true
termination_by _ => a.size - i
@ -553,7 +553,7 @@ def filterMap (f : α → Option β) (as : Array α) (start := 0) (stop := as.si
@[specialize]
def getMax? (as : Array α) (lt : α → α → Bool) : Option α :=
if h : 0 < as.size then
let a0 := as.get ⟨0, h⟩
let a0 := as[0, h]
some <| as.foldl (init := a0) (start := 1) fun best a =>
if lt best a then a else best
else
@ -572,7 +572,7 @@ def partition (p : α → Bool) (as : Array α) : Array α × Array α := Id.run
theorem ext (a b : Array α)
(h₁ : a.size = b.size)
(h₂ : (i : Nat) → (hi₁ : i < a.size) → (hi₂ : i < b.size) → a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩)
(h₂ : (i : Nat) → (hi₁ : i < a.size) → (hi₂ : i < b.size) → a[i, hi₁] = b[i, hi₂])
: a = b := by
let rec extAux (a b : List α)
(h₁ : a.length = b.length)
@ -758,8 +758,8 @@ theorem toArrayLit_eq (a : Array α) (n : Nat) (hsz : a.size = n) : a = toArrayL
def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
if h : i < as.size then
let a := as.get ⟨i, h⟩;
let b := bs.get ⟨i, Nat.lt_of_lt_of_le h hle⟩;
let a := as[i, h]
let b := bs[i, Nat.lt_of_lt_of_le h hle]
if a == b then
isPrefixOfAux as bs hle (i+1)
else
@ -780,11 +780,11 @@ private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat),
| 0, _ => true
| i+1, h =>
have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
a != as.get ⟨i, this⟩ && allDiffAuxAux as a i this
a != as[i, this] && allDiffAuxAux as a i this
private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
if h : i < as.size then
allDiffAuxAux as (as.get ⟨i, h⟩) i h && allDiffAux as (i+1)
allDiffAuxAux as as[i, h] i h && allDiffAux as (i+1)
else
true
termination_by _ => as.size - i
@ -794,9 +794,9 @@ def allDiff [BEq α] (as : Array α) : Bool :=
@[specialize] def zipWithAux (f : α → β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) : Array γ :=
if h : i < as.size then
let a := as.get ⟨i, h⟩;
let a := as[i, h]
if h : i < bs.size then
let b := bs.get ⟨i, h⟩;
let b := bs[i, h]
zipWithAux f as bs (i+1) <| cs.push <| f a b
else
cs

2
stage0/src/Init/Data/Array/DecidableEq.lean generated
View file

@ -9,7 +9,7 @@ import Init.Classical
namespace Array
theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : Array.isEqvAux a b hsz (fun x y => x = y) i) (j : Nat) (low : i ≤ j) (high : j < a.size) : a.get ⟨j, high⟩ = b.get ⟨j, hsz ▸ high⟩ := by
theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : Array.isEqvAux a b hsz (fun x y => x = y) i) (j : Nat) (low : i ≤ j) (high : j < a.size) : a[j, high] = b[j, hsz ▸ high] := by
by_cases h : i < a.size
· unfold Array.isEqvAux at heqv
simp [h] at heqv

2
stage0/src/Init/Data/Array/InsertionSort.lean generated
View file

@ -22,7 +22,7 @@ where
| 0 => a
| j'+1 =>
have h' : j' < a.size := by subst j; exact Nat.lt_trans (Nat.lt_succ_self _) h
if lt (a.get ⟨j, h⟩) (a.get ⟨j', h'⟩) then
if lt a[j, h] a[j', h'] then
swapLoop (a.swap ⟨j, h⟩ ⟨j', h'⟩) j' (by rw [size_swap]; assumption done)
else
a

9
stage0/src/Init/Data/Array/Subarray.lean generated
View file

@ -27,15 +27,18 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
simp [size] at this
rw [Nat.add_comm]
exact Nat.add_lt_of_lt_sub this
s.as.get ⟨s.start + i.val, this⟩
s.as[s.start + i.val, this]
abbrev getOp (self : Subarray α) (idx : Fin self.size) : α :=
self.get idx
@[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
if h : i < s.size then s.get ⟨i, h⟩ else v₀
def get! [Inhabited α] (s : Subarray α) (i : Nat) : α :=
abbrev get! [Inhabited α] (s : Subarray α) (i : Nat) : α :=
getD s i default
def getOp [Inhabited α] (self : Subarray α) (idx : Nat) : α :=
abbrev getOp! [Inhabited α] (self : Subarray α) (idx : Nat) : α :=
self.get! idx
def popFront (s : Subarray α) : Subarray α :=

8
stage0/src/Init/Meta.lean generated
View file

@ -374,7 +374,7 @@ def unsetTrailing (stx : Syntax) : Syntax :=
@[specialize] private partial def updateFirst {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) :=
if h : i < a.size then
let v := a.get ⟨i, h⟩;
let v := a[i, h]
match f v with
| some v => some <| a.set ⟨i, h⟩ v
| none => updateFirst a f (i+1)
@ -954,13 +954,13 @@ open Lean
private partial def filterSepElemsMAux {m : Type → Type} [Monad m] (a : Array Syntax) (p : Syntax → m Bool) (i : Nat) (acc : Array Syntax) : m (Array Syntax) := do
if h : i < a.size then
let stx := a.get ⟨i, h⟩
let stx := a[i, h]
if (← p stx) then
if acc.isEmpty then
filterSepElemsMAux a p (i+2) (acc.push stx)
else if hz : i ≠ 0 then
have : i.pred < i := Nat.pred_lt hz
let sepStx := a.get ⟨i.pred, Nat.lt_trans this h⟩
let sepStx := a[i.pred, Nat.lt_trans this h]
filterSepElemsMAux a p (i+2) ((acc.push sepStx).push stx)
else
filterSepElemsMAux a p (i+2) (acc.push stx)
@ -977,7 +977,7 @@ def filterSepElems (a : Array Syntax) (p : Syntax → Bool) : Array Syntax :=
private partial def mapSepElemsMAux {m : Type → Type} [Monad m] (a : Array Syntax) (f : Syntax → m Syntax) (i : Nat) (acc : Array Syntax) : m (Array Syntax) := do
if h : i < a.size then
let stx := a.get ⟨i, h⟩
let stx := a[i, h]
if i % 2 == 0 then do
let stx ← f stx
mapSepElemsMAux a f (i+1) (acc.push stx)

2
stage0/src/Init/Notation.lean generated
View file

@ -237,3 +237,5 @@ declare_syntax_cat rawStx
instance : Coe Syntax (TSyntax `rawStx) where
coe stx := ⟨stx⟩
macro:max a:term noWs "[" i:term ", " h:term "]" : term => `($a[⟨$i, $h⟩])

2
stage0/src/Init/Prelude.lean generated
View file

@ -1255,7 +1255,7 @@ def Array.size {α : Type u} (a : @& Array α) : Nat :=
def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=
a.data.get i
@[inline] def Array.getD (a : Array α) (i : Nat) (v₀ : α) : α :=
@[inline] abbrev Array.getD (a : Array α) (i : Nat) (v₀ : α) : α :=
dite (LT.lt i a.size) (fun h => a.get ⟨i, h⟩) (fun _ => v₀)
/- "Comfortable" version of `fget`. It performs a bound check at runtime. -/

2
stage0/src/Lean/Meta/Match/MatchEqs.lean generated
View file

@ -633,7 +633,7 @@ private partial def mkEquationsFor (matchDeclName : Name) : MetaM MatchEqns :=
let altNonEqNumParams := altNumParams - numDiscrEqs
let thmName := baseName ++ ((`eq).appendIndexAfter idx)
eqnNames := eqnNames.push thmName
let (notAlt, splitterAltType, splitterAltNumParam, argMask) ← forallAltTelescope (← inferType alts[i]) altNonEqNumParams fun ys eqs rhsArgs argMask altResultType => do
let (notAlt, splitterAltType, splitterAltNumParam, argMask) ← forallAltTelescope (← inferType alts[i]!) altNonEqNumParams fun ys eqs rhsArgs argMask altResultType => do
let patterns := altResultType.getAppArgs
let mut hs := #[]
for notAlt in notAlts do

22
stage0/src/Std/Data/PersistentHashMap.lean generated
View file

@ -106,8 +106,8 @@ partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize
| ⟨Node.collision keys vals heq, _⟩ =>
let rec traverse (i : Nat) (entries : Node α β) : Node α β :=
if h : i < keys.size then
let k := keys.get ⟨i, h⟩
let v := vals.get ⟨i, heq ▸ h⟩
let k := keys[i, h]
let v := vals[i, heq ▸ h]
let h := hash k |>.toUSize
let h := div2Shift h (shift * (depth - 1))
traverse (i+1) (insertAux entries h depth k v)
@ -129,8 +129,8 @@ def insert {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α →
partial def findAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Option β :=
if h : i < keys.size then
let k' := keys.get ⟨i, h⟩
if k == k' then some (vals.get ⟨i, by rw [←heq]; assumption⟩)
let k' := keys[i, h]
if k == k' then some vals[i, by rw [←heq]; assumption]
else findAtAux keys vals heq (i+1) k
else none
@ -159,8 +159,8 @@ def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Op
partial def findEntryAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Option (α × β) :=
if h : i < keys.size then
let k' := keys.get ⟨i, h⟩
if k == k' then some (k', vals.get ⟨i, by rw [←heq]; assumption⟩)
let k' := keys[i, h]
if k == k' then some (k', vals[i, by rw [←heq]; assumption])
else findEntryAtAux keys vals heq (i+1) k
else none
@ -178,7 +178,7 @@ def findEntry? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α
partial def containsAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Bool :=
if h : i < keys.size then
let k' := keys.get ⟨i, h⟩
let k' := keys[i, h]
if k == k' then true
else containsAtAux keys vals heq (i+1) k
else false
@ -197,7 +197,7 @@ def contains [BEq α] [Hashable α] : PersistentHashMap α β → α → Bool
partial def isUnaryEntries (a : Array (Entry α β (Node α β))) (i : Nat) (acc : Option (α × β)) : Option (α × β) :=
if h : i < a.size then
match a.get ⟨i, h⟩ with
match a[i, h] with
| Entry.null => isUnaryEntries a (i+1) acc
| Entry.ref _ => none
| Entry.entry k v =>
@ -211,7 +211,7 @@ def isUnaryNode : Node α β → Option (α × β)
| Node.collision keys vals heq =>
if h : 1 = keys.size then
have : 0 < keys.size := by rw [←h]; decide
some (keys.get ⟨0, this⟩, vals.get ⟨0, by rw [←heq]; assumption⟩)
some (keys[0, this], vals[0, by rw [←heq]; assumption])
else
none
@ -253,8 +253,8 @@ variable {σ : Type w}
| Node.collision keys vals heq, acc =>
let rec traverse (i : Nat) (acc : σ) : m σ := do
if h : i < keys.size then
let k := keys.get ⟨i, h⟩
let v := vals.get ⟨i, heq ▸ h⟩
let k := keys[i, h]
let v := vals[i, heq ▸ h]
traverse (i+1) (← f acc k v)
else
pure acc

61
stage0/stdlib/Init/Data/Array/Subarray.c generated
View file

@ -50,6 +50,7 @@ static lean_object* l_Array_term_____x5b___x3a___x5d___closed__1;
static lean_object* l_instReprSubarray___rarg___closed__12;
size_t lean_usize_sub(size_t, size_t);
static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a_x5d__1___closed__22;
LEAN_EXPORT lean_object* l_Subarray_getOp_x21___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Subarray_anyM___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Subarray_foldr___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__16;
@ -134,7 +135,7 @@ LEAN_EXPORT lean_object* l_Subarray_all(lean_object*);
static lean_object* l_instReprSubarray___rarg___closed__6;
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Subarray_allM___spec__1___rarg___lambda__1(lean_object*, uint8_t);
LEAN_EXPORT lean_object* l_Subarray_foldr___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Subarray_getOp___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Subarray_getOp___rarg___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_ofSubarray(lean_object*);
static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a_x5d__1___closed__13;
static lean_object* l_Array_term_____x5b___x3a___x5d___closed__24;
@ -184,7 +185,7 @@ LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Subarray_allM___spec__1___r
LEAN_EXPORT lean_object* l_Subarray_instForInSubarray(lean_object*, lean_object*, lean_object*);
static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__4;
static lean_object* l_Array_term_____x5b_x3a___x5d___closed__6;
LEAN_EXPORT lean_object* l_Subarray_getOp___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Subarray_getOp___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Subarray_forInUnsafe___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instToStringSubarray___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Subarray_forRevM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -198,6 +199,7 @@ static lean_object* l_instReprSubarray___rarg___closed__10;
LEAN_EXPORT lean_object* l_Subarray_forM___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_ofSubarray___rarg(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Subarray_getOp_x21___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_instReprSubarray___rarg___closed__8;
LEAN_EXPORT uint8_t l_Subarray_all___rarg(lean_object*, lean_object*);
static lean_object* l_instReprSubarray___rarg___closed__4;
@ -231,6 +233,7 @@ static lean_object* l_instReprSubarray___rarg___closed__13;
static lean_object* l_Array_term_____x5b___x3a___x5d___closed__18;
static lean_object* l_Array_term_____x5b___x3a___x5d___closed__5;
static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__11;
LEAN_EXPORT lean_object* l_Subarray_getOp_x21(lean_object*);
LEAN_EXPORT lean_object* l_Subarray_size___rarg(lean_object*);
static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__12;
LEAN_EXPORT lean_object* l_Subarray_allM(lean_object*, lean_object*);
@ -303,6 +306,32 @@ lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Subarray_getOp___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Subarray_get___rarg(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Subarray_getOp(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Subarray_getOp___rarg___boxed), 2, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Subarray_getOp___rarg___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Subarray_getOp___rarg(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Subarray_getD___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -381,27 +410,39 @@ lean_dec(x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Subarray_getOp___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
LEAN_EXPORT lean_object* l_Subarray_getOp_x21___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Subarray_get_x21___rarg(x_1, x_2, x_3);
return x_4;
lean_object* x_4; uint8_t x_5;
x_4 = l_Subarray_size___rarg(x_2);
x_5 = lean_nat_dec_lt(x_3, x_4);
lean_dec(x_4);
if (x_5 == 0)
{
lean_inc(x_1);
return x_1;
}
else
{
lean_object* x_6;
x_6 = l_Subarray_get___rarg(x_2, x_3);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Subarray_getOp(lean_object* x_1) {
}
LEAN_EXPORT lean_object* l_Subarray_getOp_x21(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Subarray_getOp___rarg___boxed), 3, 0);
x_2 = lean_alloc_closure((void*)(l_Subarray_getOp_x21___rarg___boxed), 3, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Subarray_getOp___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
LEAN_EXPORT lean_object* l_Subarray_getOp_x21___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Subarray_getOp___rarg(x_1, x_2, x_3);
x_4 = l_Subarray_getOp_x21___rarg(x_1, x_2, x_3);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);

1912
stage0/stdlib/Init/Meta.c generated
View file

File diff suppressed because it is too large Load diff

443
stage0/stdlib/Init/Notation.c generated
View file

@ -226,6 +226,7 @@ static lean_object* l_term___x2d_____closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___x3e_x3e_x3d____1___closed__7;
static lean_object* l_term___x3c_x2a_____closed__1;
static lean_object* l_prioMid___closed__2;
static lean_object* l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__6;
static lean_object* l_precLead___closed__5;
static lean_object* l_term___x3e_x3d_____closed__6;
static lean_object* l_termIfLet___x3a_x3d__Then__Else_____closed__12;
@ -258,6 +259,7 @@ static lean_object* l_term_x7b___x3a___x2f_x2f___x7d___closed__15;
static lean_object* l___aux__Init__Notation______macroRules__term___x3a_x3a____1___closed__5;
lean_object* lean_array_get_size(lean_object*);
LEAN_EXPORT lean_object* l_termDepIfThenElse;
static lean_object* l_Lean_term_____x5b___x2c___x5d___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term_xac____1___closed__1;
static lean_object* l_precLead___closed__3;
static lean_object* l_termDepIfThenElse___closed__24;
@ -285,6 +287,7 @@ static lean_object* l___aux__Init__Notation______unexpand__Function__comp__1___c
LEAN_EXPORT lean_object* l_term___x3c_x7c__;
static lean_object* l___aux__Init__Notation______macroRules__term___x5e____1___closed__8;
static lean_object* l___aux__Init__Notation______macroRules__term___x3e____1___closed__6;
static lean_object* l_Lean_term_____x5b___x2c___x5d___closed__6;
LEAN_EXPORT lean_object* l_term___x2b_x2b__;
static lean_object* l___aux__Init__Notation______macroRules__term___x2a_x3e____1___closed__7;
static lean_object* l___aux__Init__Notation______macroRules__term___x3e_x3e_x3e____1___closed__2;
@ -337,8 +340,10 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x2a____1___c
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__HOr__hOr__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_termIfThenElse___closed__11;
static lean_object* l___aux__Init__Notation______macroRules__stx___x3c_x7c_x3e____1___closed__5;
static lean_object* l_Lean_term_____x5b___x2c___x5d___closed__2;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a_x3e____1___closed__11;
static lean_object* l_termIfLet___x3a_x3d__Then__Else_____closed__14;
static lean_object* l_Lean_term_____x5b___x2c___x5d___closed__10;
static lean_object* l_prec_x28___x29___closed__2;
static lean_object* l_boolIfThenElse___closed__10;
static lean_object* l___aux__Init__Notation______macroRules__term___x2b____1___closed__6;
@ -353,6 +358,7 @@ static lean_object* l_precMin___closed__1;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__List__cons__1(lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Notation______macroRules__term___x3e_x3e_x3d____1___closed__2;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a____1___closed__9;
static lean_object* l_Lean_term_____x5b___x2c___x5d___closed__13;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__Complement__complement__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_term___x3c_x7c_x3e_____closed__2;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x26_x26____1(lean_object*, lean_object*, lean_object*);
@ -463,6 +469,7 @@ static lean_object* l_termDepIfThenElse___closed__10;
static lean_object* l_Lean___aux__Init__Notation______macroRules__term_x5b___x5d__1___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__termWithout__expected__type____1___closed__2;
static lean_object* l_term___x3e_x3e_____closed__1;
static lean_object* l_Lean_term_____x5b___x2c___x5d___closed__9;
LEAN_EXPORT lean_object* l_term___x3c_x2a__;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x24_x3e____1___closed__8;
static lean_object* l___aux__Init__Notation______macroRules__term___x25____1___closed__9;
@ -527,6 +534,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a_x3e_
LEAN_EXPORT lean_object* l_precMin;
static lean_object* l_term___x2a_x3e_____closed__5;
static lean_object* l___aux__Init__Notation______macroRules__term___x5e_x5e_x5e____1___closed__1;
static lean_object* l_Lean_term_____x5b___x2c___x5d___closed__8;
static lean_object* l___aux__Init__Notation______macroRules__term___x5e_x5e_x5e____1___closed__2;
static lean_object* l_prioLow___closed__1;
lean_object* l_Lean_Syntax_getHeadInfo(lean_object*);
@ -656,6 +664,7 @@ LEAN_EXPORT lean_object* l_Lean_instCoeSyntaxTSyntaxConsSyntaxNodeKindMkStrAnony
static lean_object* l_Lean_Parser_Syntax_addPrio___closed__5;
static lean_object* l___aux__Init__Notation______macroRules__term___x3a_x3a____1___closed__8;
static lean_object* l___aux__Init__Notation______macroRules__precMax__1___closed__2;
static lean_object* l_Lean_term_____x5b___x2c___x5d___closed__14;
static lean_object* l_prioDefault___closed__1;
static lean_object* l_term_x25_x5b___x7c___x5d___closed__5;
static lean_object* l___aux__Init__Notation______macroRules__stx___x2a__1___closed__4;
@ -666,6 +675,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a_x3e_
LEAN_EXPORT lean_object* l_term___x3c_x2a_x3e__;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c____1___closed__6;
static lean_object* l_term___x2d_____closed__3;
static lean_object* l_Lean_term_____x5b___x2c___x5d___closed__5;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___u2228____1(lean_object*, lean_object*, lean_object*);
static lean_object* l_term___x3c_x24_x3e_____closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___x3a_x3a____1___closed__2;
@ -678,8 +688,10 @@ LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__termDepIfThenE
static lean_object* l___aux__Init__Notation______macroRules__term_x2d____1___closed__2;
static lean_object* l_term___xd7_____closed__3;
static lean_object* l_prio_x28___x29___closed__3;
static lean_object* l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__2;
static lean_object* l___aux__Init__Notation______macroRules__term_x7e_x7e_x7e____1___closed__6;
static lean_object* l___aux__Init__Notation______macroRules__term___x26_x26_x26____1___closed__5;
static lean_object* l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__1;
static lean_object* l_prioLow___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___x3a_x3a____1___closed__4;
static lean_object* l_term_x7e_x7e_x7e_____closed__5;
@ -769,6 +781,7 @@ static lean_object* l_term___x26_x26_x26_____closed__2;
static lean_object* l___aux__Init__Notation______macroRules__termIfThenElse__1___closed__2;
static lean_object* l_term___x3c_____closed__4;
static lean_object* l_termDepIfThenElse___closed__30;
static lean_object* l_Lean_term_____x5b___x2c___x5d___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___x26_x26____1___closed__6;
static lean_object* l___aux__Init__Notation______macroRules__term___x25____1___closed__4;
static lean_object* l_Lean_Parser_Syntax_addPrec___closed__10;
@ -957,6 +970,7 @@ static lean_object* l_stx___x2c_x2b___closed__1;
static lean_object* l_term___x7c_x3e_____closed__7;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x3c____1(lean_object*, lean_object*, lean_object*);
static lean_object* l_precMin___closed__5;
LEAN_EXPORT lean_object* l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArgs(lean_object*);
static lean_object* l_term___u2209_____closed__3;
static lean_object* l_term___x2f_____closed__2;
@ -972,6 +986,7 @@ static lean_object* l_term___u2264_____closed__2;
static lean_object* l___aux__Init__Notation______macroRules__term_x7e_x7e_x7e____1___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___x5e_x5e_x5e____1___closed__3;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x7c_x7c_x7c____1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_term_____x5b___x2c___x5d___closed__12;
LEAN_EXPORT lean_object* l_Lean_termThis;
static lean_object* l___aux__Init__Notation______macroRules__term___x26_x26____1___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___xd7____1___closed__1;
@ -1011,6 +1026,7 @@ static lean_object* l_term___x3c_x2a_____closed__5;
static lean_object* l_term___x2b_x2b_____closed__5;
static lean_object* l_term___x24_______closed__11;
static lean_object* l_term___u2227_____closed__2;
static lean_object* l_Lean_term_____x5b___x2c___x5d___closed__1;
static lean_object* l_precMin___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term___x7c_x7c____1___closed__4;
LEAN_EXPORT lean_object* l_Lean_instCoeTSyntaxSyntax(lean_object*);
@ -1060,6 +1076,7 @@ LEAN_EXPORT lean_object* l_stx___x2c_x2b;
static lean_object* l_term_x7e_x7e_x7e_____closed__1;
static lean_object* l___aux__Init__Notation______macroRules__termDepIfThenElse__1___closed__13;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__SeqLeft__seqLeft__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__5;
static lean_object* l_term___x3a_x3a_____closed__7;
static lean_object* l_term___x3d_x3d_____closed__3;
static lean_object* l_termDepIfThenElse___closed__8;
@ -1112,6 +1129,7 @@ LEAN_EXPORT lean_object* l_term___x2f__;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a_x3e____1___closed__19;
static lean_object* l_term___u2265_____closed__6;
static lean_object* l_termDepIfThenElse___closed__4;
static lean_object* l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__3;
static lean_object* l_termIfThenElse___closed__2;
static lean_object* l_term___u2228_____closed__5;
static lean_object* l_stx___x2c_x2b_x2c_x3f___closed__5;
@ -1197,6 +1215,7 @@ static lean_object* l_term___x26_x26_____closed__2;
LEAN_EXPORT lean_object* l_precMax;
static lean_object* l___aux__Init__Notation______macroRules__term___x3e_x3d____1___closed__9;
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_term_____x5b___x2c___x5d;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x3c_x3c_x3c____1(lean_object*, lean_object*, lean_object*);
static lean_object* l_prioHigh___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__stx___x3f__1___closed__4;
@ -1290,6 +1309,7 @@ static lean_object* l_term___u2209_____closed__7;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x3d_x3d____2(lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a_x3e____1___closed__8;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__HAdd__hAdd__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___x3d____1___closed__6;
static lean_object* l_term___x3d_____closed__3;
static lean_object* l_Lean_rawStx_quot___closed__12;
@ -1314,6 +1334,7 @@ LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x3c____
static lean_object* l_precArg___closed__4;
static lean_object* l_termWithout__expected__type_____closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term___x3e____1___closed__7;
static lean_object* l_Lean_term_____x5b___x2c___x5d___closed__7;
static lean_object* l_stx___x2c_x2b___closed__5;
static lean_object* l_term___u2209_____closed__1;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x25____1(lean_object*, lean_object*, lean_object*);
@ -1323,6 +1344,7 @@ LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x2a_x3e
static lean_object* l_term___x3e_x3e_____closed__2;
static lean_object* l_Lean_Parser_Syntax_subPrec___closed__1;
LEAN_EXPORT lean_object* l_Lean___aux__Init__Notation______macroRules__term_x5b___x5d__1_expandListLit___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_term_____x5b___x2c___x5d___closed__11;
static lean_object* l___aux__Init__Notation______macroRules__term_xac____1___closed__6;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a_x3e____1___closed__12;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___u2208____1(lean_object*, lean_object*, lean_object*);
@ -30922,6 +30944,385 @@ lean_dec(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_term_____x5b___x2c___x5d___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("term__[_,_]", 11);
return x_1;
}
}
static lean_object* _init_l_Lean_term_____x5b___x2c___x5d___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__2;
x_2 = l_Lean_term_____x5b___x2c___x5d___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_term_____x5b___x2c___x5d___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("group", 5);
return x_1;
}
}
static lean_object* _init_l_Lean_term_____x5b___x2c___x5d___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_term_____x5b___x2c___x5d___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_term_____x5b___x2c___x5d___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("noWs", 4);
return x_1;
}
}
static lean_object* _init_l_Lean_term_____x5b___x2c___x5d___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_term_____x5b___x2c___x5d___closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_term_____x5b___x2c___x5d___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_term_____x5b___x2c___x5d___closed__6;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_term_____x5b___x2c___x5d___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_term_____x5b___x2c___x5d___closed__4;
x_2 = l_Lean_term_____x5b___x2c___x5d___closed__7;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_term_____x5b___x2c___x5d___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_term_____x5b___x2c___x5d___closed__8;
x_3 = l_term_x5b___x5d___closed__4;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_term_____x5b___x2c___x5d___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_term_____x5b___x2c___x5d___closed__9;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_term_____x5b___x2c___x5d___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_term_____x5b___x2c___x5d___closed__10;
x_3 = l_term_x5b___x5d___closed__6;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_term_____x5b___x2c___x5d___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_term_____x5b___x2c___x5d___closed__11;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_term_____x5b___x2c___x5d___closed__13() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_term_____x5b___x2c___x5d___closed__12;
x_3 = l_term_x5b___x5d___closed__10;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_term_____x5b___x2c___x5d___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_term_____x5b___x2c___x5d___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = lean_unsigned_to_nat(0u);
x_4 = l_Lean_term_____x5b___x2c___x5d___closed__13;
x_5 = lean_alloc_ctor(4, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
lean_ctor_set(x_5, 2, x_3);
lean_ctor_set(x_5, 3, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_term_____x5b___x2c___x5d() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_term_____x5b___x2c___x5d___closed__14;
return x_1;
}
}
static lean_object* _init_l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("arrayRef", 8);
return x_1;
}
}
static lean_object* _init_l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___aux__Init__Notation______macroRules__term___u2218____1___closed__2;
x_2 = l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("anonymousCtor", 13);
return x_1;
}
}
static lean_object* _init_l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___aux__Init__Notation______macroRules__term___u2218____1___closed__2;
x_2 = l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("⟨", 3);
return x_1;
}
}
static lean_object* _init_l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__6() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("⟩", 3);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = l_Lean_term_____x5b___x2c___x5d___closed__2;
lean_inc(x_1);
x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7;
lean_dec(x_2);
lean_dec(x_1);
x_6 = lean_box(1);
x_7 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_3);
return x_7;
}
else
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; uint8_t x_15;
x_8 = lean_unsigned_to_nat(0u);
x_9 = l_Lean_Syntax_getArg(x_1, x_8);
x_10 = lean_unsigned_to_nat(3u);
x_11 = l_Lean_Syntax_getArg(x_1, x_10);
x_12 = lean_unsigned_to_nat(5u);
x_13 = l_Lean_Syntax_getArg(x_1, x_12);
lean_dec(x_1);
x_14 = l_Lean_MonadRef_mkInfoFromRefPos___at___aux__Init__Notation______macroRules__precMax__1___spec__1(x_2, x_3);
x_15 = !lean_is_exclusive(x_14);
if (x_15 == 0)
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45;
x_16 = lean_ctor_get(x_14, 0);
x_17 = l_term_x5b___x5d___closed__3;
lean_inc(x_16);
x_18 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_18, 0, x_16);
lean_ctor_set(x_18, 1, x_17);
x_19 = l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__5;
lean_inc(x_16);
x_20 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_20, 0, x_16);
lean_ctor_set(x_20, 1, x_19);
x_21 = l___aux__Init__Notation______macroRules__stx___x3c_x7c_x3e____1___closed__7;
lean_inc(x_16);
x_22 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_22, 0, x_16);
lean_ctor_set(x_22, 1, x_21);
x_23 = l___aux__Init__Notation______unexpand__Function__comp__1___closed__3;
x_24 = lean_array_push(x_23, x_11);
x_25 = lean_array_push(x_24, x_22);
x_26 = lean_array_push(x_25, x_13);
x_27 = lean_box(2);
x_28 = l___aux__Init__Notation______macroRules__stx___x2b__1___closed__8;
x_29 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
lean_ctor_set(x_29, 2, x_26);
x_30 = l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__6;
lean_inc(x_16);
x_31 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_31, 0, x_16);
lean_ctor_set(x_31, 1, x_30);
x_32 = lean_array_push(x_23, x_20);
x_33 = lean_array_push(x_32, x_29);
x_34 = lean_array_push(x_33, x_31);
x_35 = l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__4;
x_36 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_36, 0, x_27);
lean_ctor_set(x_36, 1, x_35);
lean_ctor_set(x_36, 2, x_34);
x_37 = l_term_x5b___x5d___closed__9;
x_38 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_38, 0, x_16);
lean_ctor_set(x_38, 1, x_37);
x_39 = l___aux__Init__Notation______macroRules__stx___x2b__1___closed__9;
x_40 = lean_array_push(x_39, x_9);
x_41 = lean_array_push(x_40, x_18);
x_42 = lean_array_push(x_41, x_36);
x_43 = lean_array_push(x_42, x_38);
x_44 = l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__2;
x_45 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_45, 0, x_27);
lean_ctor_set(x_45, 1, x_44);
lean_ctor_set(x_45, 2, x_43);
lean_ctor_set(x_14, 0, x_45);
return x_14;
}
else
{
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77;
x_46 = lean_ctor_get(x_14, 0);
x_47 = lean_ctor_get(x_14, 1);
lean_inc(x_47);
lean_inc(x_46);
lean_dec(x_14);
x_48 = l_term_x5b___x5d___closed__3;
lean_inc(x_46);
x_49 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_49, 0, x_46);
lean_ctor_set(x_49, 1, x_48);
x_50 = l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__5;
lean_inc(x_46);
x_51 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_51, 0, x_46);
lean_ctor_set(x_51, 1, x_50);
x_52 = l___aux__Init__Notation______macroRules__stx___x3c_x7c_x3e____1___closed__7;
lean_inc(x_46);
x_53 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_53, 0, x_46);
lean_ctor_set(x_53, 1, x_52);
x_54 = l___aux__Init__Notation______unexpand__Function__comp__1___closed__3;
x_55 = lean_array_push(x_54, x_11);
x_56 = lean_array_push(x_55, x_53);
x_57 = lean_array_push(x_56, x_13);
x_58 = lean_box(2);
x_59 = l___aux__Init__Notation______macroRules__stx___x2b__1___closed__8;
x_60 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_60, 0, x_58);
lean_ctor_set(x_60, 1, x_59);
lean_ctor_set(x_60, 2, x_57);
x_61 = l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__6;
lean_inc(x_46);
x_62 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_62, 0, x_46);
lean_ctor_set(x_62, 1, x_61);
x_63 = lean_array_push(x_54, x_51);
x_64 = lean_array_push(x_63, x_60);
x_65 = lean_array_push(x_64, x_62);
x_66 = l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__4;
x_67 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_67, 0, x_58);
lean_ctor_set(x_67, 1, x_66);
lean_ctor_set(x_67, 2, x_65);
x_68 = l_term_x5b___x5d___closed__9;
x_69 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_69, 0, x_46);
lean_ctor_set(x_69, 1, x_68);
x_70 = l___aux__Init__Notation______macroRules__stx___x2b__1___closed__9;
x_71 = lean_array_push(x_70, x_9);
x_72 = lean_array_push(x_71, x_49);
x_73 = lean_array_push(x_72, x_67);
x_74 = lean_array_push(x_73, x_69);
x_75 = l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__2;
x_76 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_76, 0, x_58);
lean_ctor_set(x_76, 1, x_75);
lean_ctor_set(x_76, 2, x_74);
x_77 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_77, 0, x_76);
lean_ctor_set(x_77, 1, x_47);
return x_77;
}
}
}
}
lean_object* initialize_Init_Prelude(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Coe(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
@ -33245,6 +33646,48 @@ l_Lean_rawStx_quot___closed__12 = _init_l_Lean_rawStx_quot___closed__12();
lean_mark_persistent(l_Lean_rawStx_quot___closed__12);
l_Lean_rawStx_quot = _init_l_Lean_rawStx_quot();
lean_mark_persistent(l_Lean_rawStx_quot);
l_Lean_term_____x5b___x2c___x5d___closed__1 = _init_l_Lean_term_____x5b___x2c___x5d___closed__1();
lean_mark_persistent(l_Lean_term_____x5b___x2c___x5d___closed__1);
l_Lean_term_____x5b___x2c___x5d___closed__2 = _init_l_Lean_term_____x5b___x2c___x5d___closed__2();
lean_mark_persistent(l_Lean_term_____x5b___x2c___x5d___closed__2);
l_Lean_term_____x5b___x2c___x5d___closed__3 = _init_l_Lean_term_____x5b___x2c___x5d___closed__3();
lean_mark_persistent(l_Lean_term_____x5b___x2c___x5d___closed__3);
l_Lean_term_____x5b___x2c___x5d___closed__4 = _init_l_Lean_term_____x5b___x2c___x5d___closed__4();
lean_mark_persistent(l_Lean_term_____x5b___x2c___x5d___closed__4);
l_Lean_term_____x5b___x2c___x5d___closed__5 = _init_l_Lean_term_____x5b___x2c___x5d___closed__5();
lean_mark_persistent(l_Lean_term_____x5b___x2c___x5d___closed__5);
l_Lean_term_____x5b___x2c___x5d___closed__6 = _init_l_Lean_term_____x5b___x2c___x5d___closed__6();
lean_mark_persistent(l_Lean_term_____x5b___x2c___x5d___closed__6);
l_Lean_term_____x5b___x2c___x5d___closed__7 = _init_l_Lean_term_____x5b___x2c___x5d___closed__7();
lean_mark_persistent(l_Lean_term_____x5b___x2c___x5d___closed__7);
l_Lean_term_____x5b___x2c___x5d___closed__8 = _init_l_Lean_term_____x5b___x2c___x5d___closed__8();
lean_mark_persistent(l_Lean_term_____x5b___x2c___x5d___closed__8);
l_Lean_term_____x5b___x2c___x5d___closed__9 = _init_l_Lean_term_____x5b___x2c___x5d___closed__9();
lean_mark_persistent(l_Lean_term_____x5b___x2c___x5d___closed__9);
l_Lean_term_____x5b___x2c___x5d___closed__10 = _init_l_Lean_term_____x5b___x2c___x5d___closed__10();
lean_mark_persistent(l_Lean_term_____x5b___x2c___x5d___closed__10);
l_Lean_term_____x5b___x2c___x5d___closed__11 = _init_l_Lean_term_____x5b___x2c___x5d___closed__11();
lean_mark_persistent(l_Lean_term_____x5b___x2c___x5d___closed__11);
l_Lean_term_____x5b___x2c___x5d___closed__12 = _init_l_Lean_term_____x5b___x2c___x5d___closed__12();
lean_mark_persistent(l_Lean_term_____x5b___x2c___x5d___closed__12);
l_Lean_term_____x5b___x2c___x5d___closed__13 = _init_l_Lean_term_____x5b___x2c___x5d___closed__13();
lean_mark_persistent(l_Lean_term_____x5b___x2c___x5d___closed__13);
l_Lean_term_____x5b___x2c___x5d___closed__14 = _init_l_Lean_term_____x5b___x2c___x5d___closed__14();
lean_mark_persistent(l_Lean_term_____x5b___x2c___x5d___closed__14);
l_Lean_term_____x5b___x2c___x5d = _init_l_Lean_term_____x5b___x2c___x5d();
lean_mark_persistent(l_Lean_term_____x5b___x2c___x5d);
l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__1 = _init_l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__1();
lean_mark_persistent(l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__1);
l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__2 = _init_l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__2();
lean_mark_persistent(l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__2);
l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__3 = _init_l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__3();
lean_mark_persistent(l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__3);
l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__4 = _init_l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__4();
lean_mark_persistent(l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__4);
l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__5 = _init_l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__5();
lean_mark_persistent(l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__5);
l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__6 = _init_l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__6();
lean_mark_persistent(l_Lean___aux__Init__Notation______macroRules__Lean__term_____x5b___x2c___x5d__1___closed__6);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

12
stage0/stdlib/Lean/Meta/Basic.c generated
View file

@ -251,7 +251,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_forallMetaBoundedTelescope(lean_object*, le
LEAN_EXPORT lean_object* l_Lean_Meta_instMonadEnvMetaM___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux_process___rarg___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_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassExpensive_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9544_(uint8_t, uint8_t);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9552_(uint8_t, uint8_t);
static lean_object* l_Lean_Meta_instAlternativeMetaM___closed__2;
LEAN_EXPORT lean_object* l_Lean_Meta_setInlineAttribute___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withConfig___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1444,7 +1444,7 @@ x_5 = lean_ctor_get(x_1, 1);
x_6 = lean_ctor_get_uint8(x_2, sizeof(void*)*2);
x_7 = lean_ctor_get(x_2, 0);
x_8 = lean_ctor_get(x_2, 1);
x_9 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9544_(x_3, x_6);
x_9 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9552_(x_3, x_6);
if (x_9 == 0)
{
uint8_t x_10;
@ -7122,7 +7122,7 @@ x_8 = lean_ctor_get(x_6, 0);
x_9 = 0;
x_10 = lean_unbox(x_8);
lean_dec(x_8);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9544_(x_10, x_9);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9552_(x_10, x_9);
x_12 = lean_box(x_11);
lean_ctor_set(x_6, 0, x_12);
return x_6;
@ -7138,7 +7138,7 @@ lean_dec(x_6);
x_15 = 0;
x_16 = lean_unbox(x_13);
lean_dec(x_13);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9544_(x_16, x_15);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9552_(x_16, x_15);
x_18 = lean_box(x_17);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_18);
@ -7172,7 +7172,7 @@ x_8 = lean_ctor_get(x_6, 0);
x_9 = 2;
x_10 = lean_unbox(x_8);
lean_dec(x_8);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9544_(x_10, x_9);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9552_(x_10, x_9);
x_12 = lean_box(x_11);
lean_ctor_set(x_6, 0, x_12);
return x_6;
@ -7188,7 +7188,7 @@ lean_dec(x_6);
x_15 = 2;
x_16 = lean_unbox(x_13);
lean_dec(x_13);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9544_(x_16, x_15);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9552_(x_16, x_15);
x_18 = lean_box(x_17);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_18);

6
stage0/stdlib/Lean/Meta/GetConst.c generated
View file

@ -21,7 +21,7 @@ lean_object* lean_st_ref_get(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_getConstNoEx_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_isReducible___at___private_Lean_Meta_GetConst_0__Lean_Meta_canUnfoldDefault___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_getConst_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9544_(uint8_t, uint8_t);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9552_(uint8_t, uint8_t);
lean_object* l_Lean_ConstantInfo_name(lean_object*);
LEAN_EXPORT lean_object* l_Lean_getReducibilityStatus___at___private_Lean_Meta_GetConst_0__Lean_Meta_canUnfoldDefault___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_GetConst_0__Lean_Meta_canUnfoldDefault(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -315,7 +315,7 @@ x_39 = lean_ctor_get(x_38, 0);
lean_inc(x_39);
lean_dec(x_38);
x_40 = 3;
x_41 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9544_(x_6, x_40);
x_41 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9552_(x_6, x_40);
if (x_41 == 0)
{
uint8_t x_42; lean_object* x_43;
@ -360,7 +360,7 @@ x_51 = lean_ctor_get(x_49, 0);
lean_inc(x_51);
lean_dec(x_49);
x_52 = 3;
x_53 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9544_(x_6, x_52);
x_53 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9552_(x_6, x_52);
if (x_53 == 0)
{
uint8_t x_54; lean_object* x_55; lean_object* x_56;

264
stage0/stdlib/Lean/Meta/Match/MatchEqs.c generated
View file

@ -66,6 +66,7 @@ lean_object* lean_array_uget(lean_object*, size_t);
LEAN_EXPORT lean_object* l_Std_RBNode_find___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_isCastEqRec___spec__1(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_casesOnStuckLHS___lambda__1___closed__2;
LEAN_EXPORT lean_object* l_Std_RBNode_insert___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_mkMap___spec__1(lean_object*, lean_object*, lean_object*);
uint64_t lean_uint64_of_nat(lean_object*);
static lean_object* l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_simpH_x3f___lambda__3___closed__7;
lean_object* lean_expr_update_mdata(lean_object*, lean_object*);
lean_object* l_Array_append___rarg(lean_object*, lean_object*);
@ -106,6 +107,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match
static lean_object* l_Lean_Meta_Match_proveCondEqThm___closed__3;
lean_object* l_Lean_getConstInfo___at_Lean_Meta_mkConstWithFreshMVarLevels___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__6;
LEAN_EXPORT lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_convertCastEqRec___spec__8___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*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_convertTemplate___lambda__2___closed__3;
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAux___at_Lean_Meta_Match_getEquationsForImpl___spec__2(lean_object*, size_t, lean_object*);
@ -467,7 +469,7 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_Match
static lean_object* l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_simpH_x3f___closed__1;
static lean_object* l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___lambda__4___closed__3;
lean_object* l_Lean_Meta_matchEq_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5(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*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5(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*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_convertTemplate___spec__12___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Meta_forallTelescope___at___private_Lean_Meta_InferType_0__Lean_Meta_inferForallType___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_convertCastEqRec_go___spec__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*);
@ -528,7 +530,6 @@ LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_MatchEqs
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_convertCastEqRec(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Match_proveCondEqThm_go___lambda__2___closed__14;
static lean_object* l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_SimpH_processNextEq___lambda__2___closed__1;
lean_object* l_Subarray_get_x21___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_withSplitterAlts_go___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentArray_forIn___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_injectionAny___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -548,6 +549,7 @@ lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_instantiateForallAux(lean_
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_withNewAlts_go___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*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAtAux___at_Lean_Meta_Match_getEquationsForImpl___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_withNewAlts_go(lean_object*);
lean_object* l_Subarray_get___rarg(lean_object*, lean_object*);
lean_object* l_List_erase___at_Lean_Meta_getNondepPropHyps_removeDeps___spec__3(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_convertTemplate___spec__13___rarg___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*);
static lean_object* l_Lean_Meta_Match_unfoldNamedPattern___closed__2;
@ -632,6 +634,7 @@ lean_object* lean_mk_array(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkEqHEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_transform_visit___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_convertTemplate___spec__7___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*);
static lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__3;
static uint64_t l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__5;
lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_GeneralizeTelescope_generalizeTelescopeAux___spec__1___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_convertCastEqRec___spec__8___lambda__2___closed__1;
static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_convertCastEqRec___spec__8___lambda__11___closed__1;
@ -32195,65 +32198,102 @@ x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5(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* x_12, lean_object* x_13, lean_object* x_14, lean_object* x_15, lean_object* x_16, lean_object* x_17, lean_object* x_18, lean_object* x_19, lean_object* x_20, lean_object* x_21, lean_object* x_22, lean_object* x_23, lean_object* x_24, lean_object* x_25) {
static uint64_t _init_l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__5() {
_start:
{
uint8_t x_26;
x_26 = lean_nat_dec_le(x_18, x_17);
if (x_26 == 0)
lean_object* x_1; uint64_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_uint64_of_nat(x_1);
return x_2;
}
}
static lean_object* _init_l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__6() {
_start:
{
lean_object* x_27; uint8_t x_28;
x_27 = lean_unsigned_to_nat(0u);
x_28 = lean_nat_dec_eq(x_16, x_27);
if (x_28 == 0)
lean_object* x_1; uint64_t x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(0u);
x_2 = l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__5;
x_3 = lean_alloc_ctor(0, 1, 8);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint64(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5(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* x_12, lean_object* x_13, lean_object* x_14, lean_object* x_15, lean_object* x_16, lean_object* x_17, lean_object* x_18, lean_object* x_19, lean_object* x_20, lean_object* x_21, lean_object* x_22, lean_object* x_23, lean_object* x_24, lean_object* x_25, lean_object* x_26) {
_start:
{
lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51;
x_29 = lean_unsigned_to_nat(1u);
x_30 = lean_nat_sub(x_16, x_29);
lean_dec(x_16);
x_31 = lean_ctor_get(x_20, 0);
lean_inc(x_31);
x_32 = lean_ctor_get(x_20, 1);
uint8_t x_27;
x_27 = lean_nat_dec_le(x_19, x_18);
if (x_27 == 0)
{
lean_object* x_28; uint8_t x_29;
x_28 = lean_unsigned_to_nat(0u);
x_29 = lean_nat_dec_eq(x_17, x_28);
if (x_29 == 0)
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; uint8_t x_112;
x_30 = lean_unsigned_to_nat(1u);
x_31 = lean_nat_sub(x_17, x_30);
lean_dec(x_17);
x_32 = lean_ctor_get(x_21, 0);
lean_inc(x_32);
lean_dec(x_20);
x_33 = lean_ctor_get(x_32, 0);
x_33 = lean_ctor_get(x_21, 1);
lean_inc(x_33);
x_34 = lean_ctor_get(x_32, 1);
lean_dec(x_21);
x_34 = lean_ctor_get(x_33, 0);
lean_inc(x_34);
lean_dec(x_32);
x_35 = lean_ctor_get(x_34, 0);
x_35 = lean_ctor_get(x_33, 1);
lean_inc(x_35);
x_36 = lean_ctor_get(x_34, 1);
lean_dec(x_33);
x_36 = lean_ctor_get(x_35, 0);
lean_inc(x_36);
lean_dec(x_34);
x_37 = lean_ctor_get(x_36, 0);
x_37 = lean_ctor_get(x_35, 1);
lean_inc(x_37);
x_38 = lean_ctor_get(x_36, 1);
lean_dec(x_35);
x_38 = lean_ctor_get(x_37, 0);
lean_inc(x_38);
lean_dec(x_36);
x_39 = lean_ctor_get(x_38, 0);
x_39 = lean_ctor_get(x_37, 1);
lean_inc(x_39);
x_40 = lean_ctor_get(x_38, 1);
lean_dec(x_37);
x_40 = lean_ctor_get(x_39, 0);
lean_inc(x_40);
lean_dec(x_38);
x_41 = lean_ctor_get(x_8, 2);
x_42 = l_instInhabitedNat;
x_43 = lean_array_get(x_42, x_41, x_17);
x_44 = lean_nat_sub(x_43, x_9);
lean_dec(x_43);
x_45 = l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__2;
lean_inc(x_35);
x_46 = lean_name_append_index_after(x_45, x_35);
x_47 = l_Lean_Name_append(x_3, x_46);
lean_inc(x_47);
x_48 = lean_array_push(x_33, x_47);
x_49 = l_Lean_instInhabitedExpr;
x_50 = l_Subarray_get_x21___rarg(x_49, x_13, x_17);
x_41 = lean_ctor_get(x_39, 1);
lean_inc(x_41);
lean_dec(x_39);
x_42 = lean_ctor_get(x_8, 2);
x_43 = l_instInhabitedNat;
x_44 = lean_array_get(x_43, x_42, x_18);
x_45 = lean_nat_sub(x_44, x_9);
lean_dec(x_44);
x_46 = l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__2;
lean_inc(x_36);
x_47 = lean_name_append_index_after(x_46, x_36);
x_48 = l_Lean_Name_append(x_3, x_47);
lean_inc(x_48);
x_49 = lean_array_push(x_34, x_48);
x_112 = lean_nat_dec_lt(x_18, x_16);
if (x_112 == 0)
{
lean_object* x_113;
x_113 = l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__6;
x_50 = x_113;
goto block_111;
}
else
{
lean_object* x_114;
x_114 = l_Subarray_get___rarg(x_13, x_18);
x_50 = x_114;
goto block_111;
}
block_111:
{
lean_object* x_51;
lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_inc(x_22);
lean_inc(x_21);
x_51 = lean_infer_type(x_50, x_21, x_22, x_23, x_24, x_25);
x_51 = lean_infer_type(x_50, x_22, x_23, x_24, x_25, x_26);
if (lean_obj_tag(x_51) == 0)
{
lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55;
@ -32271,34 +32311,34 @@ lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_7);
lean_inc(x_4);
lean_inc(x_17);
lean_inc(x_18);
lean_inc(x_13);
lean_inc(x_14);
lean_inc(x_6);
lean_inc(x_15);
lean_inc(x_37);
lean_inc(x_38);
x_54 = lean_alloc_closure((void*)(l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___lambda__3___boxed), 26, 16);
lean_closure_set(x_54, 0, x_37);
lean_closure_set(x_54, 0, x_38);
lean_closure_set(x_54, 1, x_15);
lean_closure_set(x_54, 2, x_6);
lean_closure_set(x_54, 3, x_14);
lean_closure_set(x_54, 4, x_13);
lean_closure_set(x_54, 5, x_17);
lean_closure_set(x_54, 5, x_18);
lean_closure_set(x_54, 6, x_4);
lean_closure_set(x_54, 7, x_7);
lean_closure_set(x_54, 8, x_11);
lean_closure_set(x_54, 9, x_12);
lean_closure_set(x_54, 10, x_1);
lean_closure_set(x_54, 11, x_47);
lean_closure_set(x_54, 11, x_48);
lean_closure_set(x_54, 12, x_5);
lean_closure_set(x_54, 13, x_10);
lean_closure_set(x_54, 14, x_9);
lean_closure_set(x_54, 15, x_2);
lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_inc(x_22);
lean_inc(x_21);
x_55 = l_Lean_Meta_Match_forallAltTelescope___rarg(x_52, x_44, x_54, x_21, x_22, x_23, x_24, x_53);
x_55 = l_Lean_Meta_Match_forallAltTelescope___rarg(x_52, x_45, x_54, x_22, x_23, x_24, x_25, x_53);
if (lean_obj_tag(x_55) == 0)
{
lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; uint8_t x_68; lean_object* x_69; lean_object* x_92; lean_object* x_93; lean_object* x_94; uint8_t x_95;
@ -32322,12 +32362,12 @@ lean_inc(x_62);
x_63 = lean_ctor_get(x_58, 1);
lean_inc(x_63);
lean_dec(x_58);
x_64 = lean_array_push(x_37, x_60);
x_64 = lean_array_push(x_38, x_60);
lean_inc(x_61);
x_65 = lean_array_push(x_40, x_61);
x_66 = lean_array_push(x_39, x_62);
x_67 = lean_array_push(x_31, x_63);
x_92 = lean_st_ref_get(x_24, x_59);
x_65 = lean_array_push(x_41, x_61);
x_66 = lean_array_push(x_40, x_62);
x_67 = lean_array_push(x_32, x_63);
x_92 = lean_st_ref_get(x_25, x_59);
x_93 = lean_ctor_get(x_92, 0);
lean_inc(x_93);
x_94 = lean_ctor_get(x_93, 3);
@ -32353,7 +32393,7 @@ x_98 = lean_ctor_get(x_92, 1);
lean_inc(x_98);
lean_dec(x_92);
lean_inc(x_2);
x_99 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___spec__14(x_2, x_21, x_22, x_23, x_24, x_98);
x_99 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___spec__14(x_2, x_22, x_23, x_24, x_25, x_98);
x_100 = lean_ctor_get(x_99, 0);
lean_inc(x_100);
x_101 = lean_ctor_get(x_99, 1);
@ -32372,8 +32412,8 @@ if (x_68 == 0)
lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75;
lean_dec(x_61);
x_70 = lean_box(0);
x_71 = l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___lambda__4(x_66, x_65, x_64, x_48, x_67, x_35, x_70, x_21, x_22, x_23, x_24, x_69);
lean_dec(x_35);
x_71 = l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___lambda__4(x_66, x_65, x_64, x_49, x_67, x_36, x_70, x_22, x_23, x_24, x_25, x_69);
lean_dec(x_36);
x_72 = lean_ctor_get(x_71, 0);
lean_inc(x_72);
x_73 = lean_ctor_get(x_71, 1);
@ -32382,12 +32422,12 @@ lean_dec(x_71);
x_74 = lean_ctor_get(x_72, 0);
lean_inc(x_74);
lean_dec(x_72);
x_75 = lean_nat_add(x_17, x_19);
lean_dec(x_17);
x_16 = x_30;
x_17 = x_75;
x_20 = x_74;
x_25 = x_73;
x_75 = lean_nat_add(x_18, x_20);
lean_dec(x_18);
x_17 = x_31;
x_18 = x_75;
x_21 = x_74;
x_26 = x_73;
goto _start;
}
else
@ -32404,15 +32444,15 @@ x_81 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_81, 0, x_79);
lean_ctor_set(x_81, 1, x_80);
lean_inc(x_2);
x_82 = l_Lean_addTrace___at_Lean_Meta_processPostponed_loop___spec__1(x_2, x_81, x_21, x_22, x_23, x_24, x_69);
x_82 = l_Lean_addTrace___at_Lean_Meta_processPostponed_loop___spec__1(x_2, x_81, x_22, x_23, x_24, x_25, x_69);
x_83 = lean_ctor_get(x_82, 0);
lean_inc(x_83);
x_84 = lean_ctor_get(x_82, 1);
lean_inc(x_84);
lean_dec(x_82);
x_85 = l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___lambda__4(x_66, x_65, x_64, x_48, x_67, x_35, x_83, x_21, x_22, x_23, x_24, x_84);
x_85 = l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___lambda__4(x_66, x_65, x_64, x_49, x_67, x_36, x_83, x_22, x_23, x_24, x_25, x_84);
lean_dec(x_83);
lean_dec(x_35);
lean_dec(x_36);
x_86 = lean_ctor_get(x_85, 0);
lean_inc(x_86);
x_87 = lean_ctor_get(x_85, 1);
@ -32421,12 +32461,12 @@ lean_dec(x_85);
x_88 = lean_ctor_get(x_86, 0);
lean_inc(x_88);
lean_dec(x_86);
x_89 = lean_nat_add(x_17, x_19);
lean_dec(x_17);
x_16 = x_30;
x_17 = x_89;
x_20 = x_88;
x_25 = x_87;
x_89 = lean_nat_add(x_18, x_20);
lean_dec(x_18);
x_17 = x_31;
x_18 = x_89;
x_21 = x_88;
x_26 = x_87;
goto _start;
}
}
@ -32434,18 +32474,18 @@ goto _start;
else
{
uint8_t x_103;
lean_dec(x_48);
lean_dec(x_49);
lean_dec(x_41);
lean_dec(x_40);
lean_dec(x_39);
lean_dec(x_37);
lean_dec(x_35);
lean_dec(x_38);
lean_dec(x_36);
lean_dec(x_32);
lean_dec(x_31);
lean_dec(x_30);
lean_dec(x_25);
lean_dec(x_24);
lean_dec(x_23);
lean_dec(x_22);
lean_dec(x_21);
lean_dec(x_17);
lean_dec(x_18);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
@ -32482,20 +32522,20 @@ return x_106;
else
{
uint8_t x_107;
lean_dec(x_49);
lean_dec(x_48);
lean_dec(x_47);
lean_dec(x_44);
lean_dec(x_45);
lean_dec(x_41);
lean_dec(x_40);
lean_dec(x_39);
lean_dec(x_37);
lean_dec(x_35);
lean_dec(x_38);
lean_dec(x_36);
lean_dec(x_32);
lean_dec(x_31);
lean_dec(x_30);
lean_dec(x_25);
lean_dec(x_24);
lean_dec(x_23);
lean_dec(x_22);
lean_dec(x_21);
lean_dec(x_17);
lean_dec(x_18);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
@ -32529,15 +32569,16 @@ return x_110;
}
}
}
}
else
{
lean_object* x_111;
lean_object* x_115;
lean_dec(x_25);
lean_dec(x_24);
lean_dec(x_23);
lean_dec(x_22);
lean_dec(x_21);
lean_dec(x_18);
lean_dec(x_17);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
@ -32551,21 +32592,21 @@ lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_111 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_111, 0, x_20);
lean_ctor_set(x_111, 1, x_25);
return x_111;
x_115 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_115, 0, x_21);
lean_ctor_set(x_115, 1, x_26);
return x_115;
}
}
else
{
lean_object* x_112;
lean_object* x_116;
lean_dec(x_25);
lean_dec(x_24);
lean_dec(x_23);
lean_dec(x_22);
lean_dec(x_21);
lean_dec(x_18);
lean_dec(x_17);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
@ -32579,10 +32620,10 @@ lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_112 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_112, 0, x_20);
lean_ctor_set(x_112, 1, x_25);
return x_112;
x_116 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_116, 0, x_21);
lean_ctor_set(x_116, 1, x_26);
return x_116;
}
}
}
@ -33166,7 +33207,7 @@ lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_4);
lean_inc(x_3);
x_39 = l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5(x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_1, x_10, x_8, x_20, x_22, x_27, x_32, x_2, x_33, x_19, x_33, x_28, x_38, x_13, x_14, x_15, x_16, x_17);
x_39 = l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5(x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_1, x_10, x_8, x_20, x_22, x_27, x_32, x_2, x_33, x_33, x_19, x_33, x_28, x_38, x_13, x_14, x_15, x_16, x_17);
lean_dec(x_33);
lean_dec(x_1);
if (lean_obj_tag(x_39) == 0)
@ -34274,15 +34315,17 @@ lean_object* x_22 = _args[21];
lean_object* x_23 = _args[22];
lean_object* x_24 = _args[23];
lean_object* x_25 = _args[24];
lean_object* x_26 = _args[25];
_start:
{
lean_object* x_26;
x_26 = l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_17, x_18, x_19, x_20, x_21, x_22, x_23, x_24, x_25);
lean_object* x_27;
x_27 = l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_17, x_18, x_19, x_20, x_21, x_22, x_23, x_24, x_25, x_26);
lean_dec(x_20);
lean_dec(x_19);
lean_dec(x_18);
lean_dec(x_16);
lean_dec(x_8);
lean_dec(x_3);
return x_26;
return x_27;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___lambda__1___boxed(lean_object** _args) {
@ -35083,6 +35126,9 @@ l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Matc
lean_mark_persistent(l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__3);
l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__4 = _init_l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__4();
lean_mark_persistent(l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__4);
l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__5 = _init_l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__5();
l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__6 = _init_l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__6();
lean_mark_persistent(l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___spec__5___closed__6);
l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___lambda__1___closed__1 = _init_l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___lambda__1___closed__1();
lean_mark_persistent(l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___lambda__1___closed__1);
l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___lambda__1___closed__2 = _init_l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkEquationsFor___lambda__1___closed__2();

8
stage0/stdlib/Lean/Meta/WHNF.c generated
View file

@ -128,7 +128,7 @@ size_t lean_usize_shift_right(size_t, size_t);
static lean_object* l_Lean_Meta_reduceNative_x3f___closed__14;
LEAN_EXPORT lean_object* l_Lean_Meta_smartUnfoldingMatch_x3f(lean_object*);
lean_object* l_Lean_Expr_getRevArg_x21(lean_object*, lean_object*);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9544_(uint8_t, uint8_t);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9552_(uint8_t, uint8_t);
static lean_object* l_Lean_Meta_toCtorIfLit___closed__16;
static lean_object* l_Lean_Meta_canUnfoldAtMatcher___closed__10;
uint8_t lean_usize_dec_lt(size_t, size_t);
@ -10029,7 +10029,7 @@ lean_inc(x_9);
lean_dec(x_7);
x_10 = 2;
x_11 = lean_unbox(x_8);
x_12 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9544_(x_11, x_10);
x_12 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9552_(x_11, x_10);
if (x_12 == 0)
{
lean_object* x_13; uint8_t x_14; lean_object* x_15;
@ -20494,7 +20494,7 @@ x_10 = lean_ctor_get(x_7, 1);
x_11 = 3;
x_12 = lean_unbox(x_9);
lean_dec(x_9);
x_13 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9544_(x_12, x_11);
x_13 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9552_(x_12, x_11);
if (x_13 == 0)
{
lean_object* x_14;
@ -20526,7 +20526,7 @@ lean_dec(x_7);
x_18 = 3;
x_19 = lean_unbox(x_16);
lean_dec(x_16);
x_20 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9544_(x_19, x_18);
x_20 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9552_(x_19, x_18);
if (x_20 == 0)
{
lean_object* x_21; lean_object* x_22;