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-03-01 09:03:20 -08:00
parent da55789c26
commit 0158c2eeb7
191 changed files with 2161 additions and 1358 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
stage0/src/Init/Core.lean generated
View file

@ -178,21 +178,22 @@ infix:50 " != " => bne
class LawfulBEq (α : Type u) [BEq α] : Prop where
eq_of_beq : (a b : α) → (a == b) = true → a = b
rfl : (a : α) → (a == a) = true
theorem eq_of_beq [BEq α] [LawfulBEq α] {a b : α} (h : (a == b) = true) : a = b :=
LawfulBEq.eq_of_beq a b h
instance : LawfulBEq Bool where
eq_of_beq a b h := by cases a <;> cases b <;> first | rfl | contradiction
instance : LawfulBEq Nat where
eq_of_beq _ _ h := of_decide_eq_true h
rfl a := by cases a <;> decide
instance : LawfulBEq Char where
eq_of_beq _ _ h := of_decide_eq_true h
rfl a := of_decide_eq_self_eq_true a
instance : LawfulBEq String where
eq_of_beq _ _ h := of_decide_eq_true h
rfl a := of_decide_eq_self_eq_true a
/- Logical connectives an equality -/

4
stage0/src/Init/Data/List/Basic.lean generated
View file

@ -483,5 +483,9 @@ instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where
simp [BEq.beq, List.beq]
intro ⟨h₁, h₂⟩
exact ⟨eq_of_beq h₁, ih _ h₂⟩
rfl as := by
induction as with
| nil => rfl
| cons a as ih => simp [BEq.beq, List.beq, LawfulBEq.rfl]; exact ih
end List

12
stage0/src/Init/Data/Nat/Basic.lean generated
View file

@ -60,6 +60,18 @@ def blt (a b : Nat) : Bool :=
@[simp] theorem ble_eq : (Nat.ble x y = true) = (x ≤ y) := propext <| Iff.intro Nat.le_of_ble_eq_true Nat.ble_eq_true_of_le
@[simp] theorem blt_eq : (Nat.blt x y = true) = (x < y) := propext <| Iff.intro Nat.le_of_ble_eq_true Nat.ble_eq_true_of_le
instance : LawfulBEq Nat where
eq_of_beq _ _ h := Nat.eq_of_beq_eq_true h
rfl a := by simp [BEq.beq]
@[simp] theorem beq_eq_true_eq (a b : Nat) : ((a == b) = true) = (a = b) := propext <| Iff.intro eq_of_beq (fun h => by subst h; apply LawfulBEq.rfl)
@[simp] theorem not_beq_eq_true_eq (a b : Nat) : ((!(a == b)) = true) = ¬(a = b) :=
propext <| Iff.intro
(fun h₁ h₂ => by subst h₂; rw [LawfulBEq.rfl] at h₁; contradiction)
(fun h =>
have : ¬ ((a == b) = true) := fun h' => absurd (eq_of_beq h') h
by simp [this])
/- Nat.add theorems -/
@[simp] protected theorem zero_add : ∀ (n : Nat), 0 + n = n

4
stage0/src/Init/Data/Nat/Linear.lean generated
View file

@ -179,6 +179,10 @@ instance : LawfulBEq PolyCnstr where
simp at h
have ⟨⟨h₁, h₂⟩, h₃⟩ := h
rw [h₁, eq_of_beq h₂, eq_of_beq h₃]
rfl a := by
cases a; rename_i eq lhs rhs
show (eq == eq && lhs == lhs && rhs == rhs) = true
simp [LawfulBEq.rfl]
def PolyCnstr.mul (k : Nat) (c : PolyCnstr) : PolyCnstr :=
{ c with lhs := c.lhs.mul k, rhs := c.rhs.mul k }

1
stage0/src/Init/Data/Prod.lean generated
View file

@ -8,3 +8,4 @@ import Init.SimpLemmas
instance [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β) where
eq_of_beq a b h := by cases a; cases b; simp [BEq.beq] at h; have ⟨h₁, h₂⟩ := h; rw [eq_of_beq h₁, eq_of_beq h₂]
rfl a := by cases a; simp [BEq.beq, LawfulBEq.rfl]

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

@ -300,6 +300,11 @@ theorem of_decide_eq_false [s : Decidable p] : Eq (decide p) false → Not p :=
| isTrue h₁ => absurd h (ne_false_of_eq_true (decide_eq_true h₁))
| isFalse h₁ => h₁
theorem of_decide_eq_self_eq_true [s : DecidableEq α] (a : α) : Eq (decide (Eq a a)) true :=
match (generalizing := false) s a a with
| isTrue h₁ => rfl
| isFalse h₁ => absurd rfl h₁
@[inline] instance : DecidableEq Bool :=
fun a b => match a, b with
| false, false => isTrue rfl
@ -600,6 +605,9 @@ def Nat.beq : (@& Nat) → (@& Nat) → Bool
| succ n, zero => false
| succ n, succ m => beq n m
instance : BEq Nat where
beq := Nat.beq
theorem Nat.eq_of_beq_eq_true : {n m : Nat} → Eq (beq n m) true → Eq n m
| zero, zero, h => rfl
| zero, succ m, h => Bool.noConfusion h

5
stage0/src/Init/SimpLemmas.lean generated
View file

@ -150,10 +150,9 @@ theorem Bool.of_not_eq_false {b : Bool} : ¬ (b = false) → b = true := by case
@[simp] theorem decide_not [h : Decidable p] : decide (¬ p) = !decide p := by cases h <;> rfl
@[simp] theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by cases h <;> simp [decide, *]
@[simp] theorem Nat.beq_to_eq (a b : Nat) : ((a == b) = true) = (a = b) := by simp [BEq.beq]
@[simp] theorem Nat.not_beq_to_not_eq (a b : Nat) : ((!(a == b)) = true) = ¬(a = b) := by simp [BEq.beq]
@[simp] theorem heq_eq_eq {α : Sort u} (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq
@[simp] theorem cond_true (a b : α) : cond true a b = a := rfl
@[simp] theorem cond_false (a b : α) : cond false a b = b := rfl
@[simp] theorem beq_self_eq_true [BEq α] [LawfulBEq α] (a : α) : (a == a) = true := LawfulBEq.rfl a

19
stage0/src/Lean/Compiler/ConstFolding.lean generated
View file

@ -125,6 +125,19 @@ def foldNatDecEq := foldNatBinPred mkNatEq (fun a b => a = b)
def foldNatDecLt := foldNatBinPred mkNatLt (fun a b => a < b)
def foldNatDecLe := foldNatBinPred mkNatLe (fun a b => a ≤ b)
def foldNatBinBoolPred (fn : Nat → Nat → Bool) (a₁ a₂ : Expr) : Option Expr :=
OptionM.run do
let n₁ ← getNumLit a₁
let n₂ ← getNumLit a₂
if fn n₁ n₂ then
return mkConst ``Bool.true
else
return mkConst ``Bool.false
def foldNatBeq := fun _ : Bool => foldNatBinBoolPred (fun a b => a == b)
def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b)
def foldNatBlt := fun _ : Bool => foldNatBinBoolPred (fun a b => a ≤ b)
def natFoldFns : List (Name × BinFoldFn) :=
[(``Nat.add, foldNatAdd),
(``Nat.mul, foldNatMul),
@ -133,7 +146,11 @@ def natFoldFns : List (Name × BinFoldFn) :=
(``Nat.pow, foldNatPow),
(``Nat.decEq, foldNatDecEq),
(``Nat.decLt, foldNatDecLt),
(``Nat.decLe, foldNatDecLe)]
(``Nat.decLe, foldNatDecLe),
(``Nat.beq, foldNatBeq),
(``Nat.blt, foldNatBlt),
(``Nat.ble, foldNatBle)
]
def getBoolLit : Expr → Option Bool
| Expr.const ``Bool.true _ _ => some true

5
stage0/src/Lean/Compiler/IR/SimpCase.lean generated
View file

@ -43,8 +43,11 @@ private def addDefault (alts : Array Alt) : Array Alt :=
let alts := alts.filter fun alt => alt.body != max.body
alts.push (Alt.default max.body)
private def filterUnreachable (alts : Array Alt) : Array Alt :=
alts.filter fun alt => alt.body != FnBody.unreachable
private def mkSimpCase (tid : Name) (x : VarId) (xType : IRType) (alts : Array Alt) : FnBody :=
let alts := alts.filter (fun alt => alt.body != FnBody.unreachable);
let alts := filterUnreachable alts
let alts := addDefault alts;
if alts.size == 0 then
FnBody.unreachable

2
stage0/src/kernel/inductive.h generated
View file

@ -67,6 +67,8 @@ inline expr to_cnstr_when_structure(environment const & env, name const & induct
expr e_type = whnf(infer_type(e));
if (!is_constant(get_app_fn(e_type), induct_name))
return e;
if (whnf(infer_type(e_type)) == mk_Prop())
return e;
return expand_eta_struct(env, e_type, e);
}

10
stage0/src/kernel/type_checker.cpp generated
View file

@ -252,18 +252,22 @@ expr type_checker::infer_proj(expr const & e, bool infer_only) {
if (!is_pi(r)) throw invalid_proj_exception(env(), m_lctx, e);
r = instantiate(binding_body(r), args[i]);
}
bool is_prop_type = is_prop(type);
for (unsigned i = 0; i < idx; i++) {
r = whnf(r);
if (!is_pi(r)) throw invalid_proj_exception(env(), m_lctx, e);
if (has_loose_bvars(binding_body(r)))
if (has_loose_bvars(binding_body(r))) {
if (is_prop_type && !is_prop(binding_domain(r)))
throw invalid_proj_exception(env(), m_lctx, e);
r = instantiate(binding_body(r), mk_proj(I_name, i, proj_expr(e)));
else
} else {
r = binding_body(r);
}
}
r = whnf(r);
if (!is_pi(r)) throw invalid_proj_exception(env(), m_lctx, e);
r = binding_domain(r);
if (is_prop(type) && !is_prop(r))
if (is_prop_type && !is_prop(r))
throw invalid_proj_exception(env(), m_lctx, e);
return r;
}

1
stage0/stdlib/Init/Data/Array/Basic.c generated
View file

@ -453,6 +453,7 @@ LEAN_EXPORT lean_object* l_Array_findSomeRevM_x3f_find___at_Array_findSomeRev_x3
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Array_filterM___spec__1___rarg___lambda__2(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_popWhile(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Array_append___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_modifyMUnsafe___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_concatMapM___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapIdx___rarg___boxed(lean_object*, lean_object*);

2
stage0/stdlib/Init/Data/Array/BinSearch.c generated
View file

@ -34,7 +34,6 @@ LEAN_EXPORT lean_object* l_Array_binInsertM___rarg___lambda__2(lean_object*, lea
LEAN_EXPORT lean_object* l_Array_binSearchAux___at_Array_binSearchContains___spec__1(lean_object*);
LEAN_EXPORT uint8_t l_Array_binSearchAux___at_Array_binSearchContains___spec__1___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_BinSearch_0__Array_binInsertAux___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Array_binSearchContains___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -59,6 +58,7 @@ LEAN_EXPORT lean_object* l_Array_binInsertM___rarg(lean_object*, lean_object*, l
LEAN_EXPORT lean_object* l_Array_binSearchAux___at_Array_binSearch___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_binSearchAux___at_Array_binSearch___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_BinSearch_0__Array_binInsertAux___at_Array_binInsert___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_binSearchContains___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_binSearchContains(lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_BinSearch_0__Array_binInsertAux___at_Array_binInsert___spec__2(lean_object*);

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

@ -87,7 +87,6 @@ LEAN_EXPORT lean_object* l_Subarray_popFront___rarg(lean_object*);
static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b_x3a___x5d__1___closed__2;
LEAN_EXPORT lean_object* l_Subarray_anyM(lean_object*, lean_object*);
static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__6;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Subarray_all___rarg___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Subarray_toArray___rarg(lean_object*);
LEAN_EXPORT uint8_t l_Subarray_any___rarg(lean_object*, lean_object*);
@ -183,6 +182,7 @@ LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Subarray_foldr___spec__1
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*);
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;

1
stage0/stdlib/Init/Data/ByteArray/Basic.c generated
View file

@ -97,6 +97,7 @@ static lean_object* l_ByteArray_toUInt64LE_x21___closed__2;
uint64_t lean_uint64_shift_left(uint64_t, uint64_t);
LEAN_EXPORT lean_object* l_ByteArray_forIn_loop___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint64_t lean_uint64_lor(uint64_t, uint64_t);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* lean_byte_array_copy_slice(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
LEAN_EXPORT lean_object* l_ByteArray_foldlMUnsafe_fold___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_ByteArray_forIn_loop(lean_object*, lean_object*);

1
stage0/stdlib/Init/Data/FloatArray/Basic.c generated
View file

@ -80,6 +80,7 @@ lean_object* lean_float_array_set(lean_object*, lean_object*, double);
LEAN_EXPORT lean_object* l_List_toString___at_instToStringFloatArray___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_instToStringFloatArray(lean_object*);
LEAN_EXPORT lean_object* l_FloatArray_foldlMUnsafe_fold___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_FloatArray_foldlMUnsafe_fold___at_FloatArray_foldl___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_FloatArray_foldlMUnsafe_fold___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_empty_float_array(lean_object*);

2
stage0/stdlib/Init/Data/Format/Basic.c generated
View file

@ -62,7 +62,6 @@ LEAN_EXPORT lean_object* l_Std_Format_joinSuffix___rarg(lean_object*, lean_objec
LEAN_EXPORT lean_object* l_Std_Format_FlattenBehavior_noConfusion___rarg(uint8_t, uint8_t, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Format_Basic_0__Std_Format_SpaceResult_space___default;
LEAN_EXPORT lean_object* l___private_Init_Data_Format_Basic_0__Std_Format_pushGroup___at_Std_Format_pretty___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_instToFormatString(lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Format_Basic_0__Std_Format_State_out___default;
lean_object* lean_nat_sub(lean_object*, lean_object*);
@ -136,6 +135,7 @@ LEAN_EXPORT lean_object* l_panic___at___private_Init_Data_Format_Basic_0__Std_Fo
LEAN_EXPORT lean_object* l_Std_Format_instCoeStringFormat(lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Format_Basic_0__Std_Format_be___rarg___lambda__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Format_isEmpty___closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_foldl___at_Std_Format_join___spec__1(lean_object*, lean_object*);
lean_object* lean_panic_fn(lean_object*, lean_object*);
lean_object* l_StateT_instMonadStateT___rarg(lean_object*);

1
stage0/stdlib/Init/Data/Nat/Linear.c generated
View file

@ -69,6 +69,7 @@ LEAN_EXPORT lean_object* l_Nat_Linear_Poly_isNum_x3f___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Certificate_combineHyps(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Nat_Linear_Poly_isNonZero(lean_object*);
lean_object* lean_nat_mul(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Nat_Linear_Certificate_combine___closed__1;
LEAN_EXPORT lean_object* l_Nat_Linear_ExprCnstr_toPoly___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Nat_Linear_Poly_norm(lean_object*);

1
stage0/stdlib/Init/Data/Ord.c generated
View file

@ -62,6 +62,7 @@ LEAN_EXPORT uint8_t l_compareOfLessAndEq___rarg(lean_object*, lean_object*, lean
LEAN_EXPORT uint8_t l_instOrdUInt32(uint32_t, uint32_t);
uint8_t lean_int_dec_lt(lean_object*, lean_object*);
uint8_t lean_uint16_dec_lt(uint16_t, uint16_t);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_instOrdUSize(size_t, size_t);
LEAN_EXPORT lean_object* l_Ordering_noConfusion___rarg___lambda__1___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Ordering_toCtorIdx(uint8_t);

1
stage0/stdlib/Init/Data/String/Basic.c generated
View file

@ -247,6 +247,7 @@ LEAN_EXPORT lean_object* l_Substring_dropRight(lean_object*, lean_object*);
lean_object* lean_nat_mul(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Substring_splitOn_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_String_anyAux(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_toLower(lean_object*);
LEAN_EXPORT lean_object* l_String_foldlAux(lean_object*);
LEAN_EXPORT uint8_t l_String_startsWith(lean_object*, lean_object*);

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

@ -693,6 +693,7 @@ static lean_object* l_List_foldr___at_Lean_Syntax_decodeNameLit___spec__1___clos
LEAN_EXPORT lean_object* l_Lean_Syntax_decodeQuotedChar___boxed__const__1;
static lean_object* l_Lean_Parser_Tactic___aux__Init__Meta______macroRules__Lean__Parser__Tactic__tacticErw______1___closed__5;
LEAN_EXPORT lean_object* l_Lean_Syntax_getTailInfo_x3f(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_instBEqConfig;
static lean_object* l_Lean_termEval__prec_____closed__2;
LEAN_EXPORT uint8_t l_Lean_Meta_Simp_Config_iota___default;

1
stage0/stdlib/Init/NotationExtra.c generated
View file

@ -543,6 +543,7 @@ static lean_object* l_command__ClassAbbrev_____x3a___x3a_x3d_____x2c___closed__9
static lean_object* l_calc___closed__5;
static lean_object* l_solve___closed__14;
static lean_object* l___aux__Init__NotationExtra______macroRules__term_x25_x5b___x7c___x5d__1___closed__6;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l___aux__Init__NotationExtra______macroRules__tacticFunext______1___closed__2;
LEAN_EXPORT lean_object* l_unexpandUnit___boxed(lean_object*);
static lean_object* l_solve___closed__5;

22
stage0/stdlib/Init/Prelude.c generated
View file

@ -248,6 +248,7 @@ LEAN_EXPORT lean_object* l_inferInstance___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Macro_instInhabitedMethods___lambda__3___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_getThe___rarg(lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Prelude_0__Lean_extractMacroScopesAux(lean_object*, lean_object*);
static lean_object* l_instBEqNat___closed__1;
LEAN_EXPORT uint8_t l_Lean_Name_hasMacroScopes(lean_object*);
LEAN_EXPORT uint8_t l_instDecidableEqChar(uint32_t, uint32_t);
LEAN_EXPORT lean_object* l_ReaderT_instMonadReaderT___rarg___lambda__7___boxed(lean_object*, lean_object*, lean_object*);
@ -728,6 +729,7 @@ LEAN_EXPORT lean_object* lean_simp_macro_scopes(lean_object*);
LEAN_EXPORT lean_object* l_max___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_PrettyPrinter_instMonadQuotationUnexpandM___closed__3;
LEAN_EXPORT lean_object* l_EStateM_bind(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instBEqNat;
LEAN_EXPORT lean_object* l_UInt32_val___boxed(lean_object*);
LEAN_EXPORT lean_object* l_dite___rarg(uint8_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_unsafeCast(lean_object*, lean_object*);
@ -1983,6 +1985,22 @@ x_4 = lean_box(x_3);
return x_4;
}
}
static lean_object* _init_l_instBEqNat___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Nat_beq___boxed), 2, 0);
return x_1;
}
}
static lean_object* _init_l_instBEqNat() {
_start:
{
lean_object* x_1;
x_1 = l_instBEqNat___closed__1;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Nat_decEq___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -10537,6 +10555,10 @@ l_instPowNat___closed__1 = _init_l_instPowNat___closed__1();
lean_mark_persistent(l_instPowNat___closed__1);
l_instPowNat = _init_l_instPowNat();
lean_mark_persistent(l_instPowNat);
l_instBEqNat___closed__1 = _init_l_instBEqNat___closed__1();
lean_mark_persistent(l_instBEqNat___closed__1);
l_instBEqNat = _init_l_instBEqNat();
lean_mark_persistent(l_instBEqNat);
l_instLENat = _init_l_instLENat();
lean_mark_persistent(l_instLENat);
l_instLTNat = _init_l_instLTNat();

1
stage0/stdlib/Init/System/FilePath.c generated
View file

@ -101,6 +101,7 @@ lean_object* l_Char_toLower(uint32_t);
LEAN_EXPORT uint8_t l_List_elem___at_System_FilePath_normalize___spec__1(uint32_t, lean_object*);
LEAN_EXPORT lean_object* l_System_instHashableFilePath;
LEAN_EXPORT uint32_t l_System_SearchPath_separator;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_System_FilePath_pathSeparators___closed__2;
LEAN_EXPORT lean_object* l_System_SearchPath_parse(lean_object*);
uint64_t lean_uint64_mix_hash(uint64_t, uint64_t);

2
stage0/stdlib/Init/System/IO.c generated
View file

@ -206,7 +206,6 @@ LEAN_EXPORT lean_object* l_EIO_toIO___rarg(lean_object*, lean_object*, lean_obje
static uint32_t l_IO_AccessRight_flags___closed__1;
static uint32_t l_IO_AccessRight_flags___closed__9;
LEAN_EXPORT lean_object* l_IO_FS_Handle_readBinToEnd(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_sleep___lambda__1(lean_object*, lean_object*);
static uint32_t l_IO_AccessRight_flags___closed__2;
LEAN_EXPORT lean_object* l_IO_FS_readBinFile___boxed(lean_object*, lean_object*);
@ -474,6 +473,7 @@ lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Init_System_IO_0__IO_FS_reprSystemTime____x40_Init_System_IO___hyg_2117____closed__2;
LEAN_EXPORT lean_object* l_IO_toEIO___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Handle_putStrLn(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_createDirAll___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_termPrintln_x21_______closed__11;
static lean_object* l___private_Init_System_IO_0__IO_FS_reprDirEntry____x40_Init_System_IO___hyg_1886____closed__2;

2
stage0/stdlib/Lean/Attributes.c generated
View file

@ -161,7 +161,6 @@ LEAN_EXPORT lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_getBuiltinAt
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_updateEnvAttributesImpl___spec__3(lean_object*, size_t, size_t, lean_object*);
static lean_object* l_Lean_instToStringAttributeKind___closed__3;
LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_registerEnumAttributes___spec__3___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_128_(uint8_t, uint8_t);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_foldlMAux___at_Lean_getBuiltinAttributeNames___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
@ -371,6 +370,7 @@ static lean_object* l_Lean_registerBuiltinAttribute___lambda__2___closed__1;
LEAN_EXPORT lean_object* l_Std_RBNode_find___at_Lean_ParametricAttribute_getParam___spec__1(lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_registerBuiltinAttribute___closed__2;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeApplicationTime____x40_Lean_Attributes___hyg_13_(uint8_t, uint8_t);
extern lean_object* l_Lean_instInhabitedName;
static lean_object* l_Lean_Attribute_Builtin_getIdent___closed__2;

457
stage0/stdlib/Lean/Compiler/ConstFolding.c generated
View file

@ -40,9 +40,11 @@ lean_object* l_Nat_div___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_NumScalarTypeInfo_size___default___boxed(lean_object*);
static lean_object* l_Lean_Compiler_foldCharOfNat___closed__1;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldUIntSub___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Nat_beq___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_natFoldFns___closed__15;
static lean_object* l_Lean_Compiler_toDecidableExpr___closed__6;
static lean_object* l_Lean_Compiler_foldCharOfNat___closed__2;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBeq(uint8_t);
LEAN_EXPORT lean_object* l_Lean_Compiler_NumScalarTypeInfo_ofNatFn___default(lean_object*);
extern lean_object* l_System_Platform_numBits;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatPow___boxed(lean_object*);
@ -59,6 +61,7 @@ static lean_object* l_Lean_Compiler_foldNatMul___rarg___closed__1;
static lean_object* l_Lean_Compiler_getBoolLit___closed__2;
LEAN_EXPORT lean_object* l_Lean_Compiler_preUIntBinFoldFns;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldStrictAnd___boxed(lean_object*);
static lean_object* l_Lean_Compiler_natFoldFns___closed__51;
LEAN_EXPORT lean_object* l_Lean_Compiler_natFoldFns;
static lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__25;
static lean_object* l_Lean_Compiler_boolFoldFns___closed__5;
@ -81,6 +84,7 @@ lean_object* lean_nat_pow(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatMod(uint8_t);
static lean_object* l_Lean_Compiler_natFoldFns___closed__27;
static lean_object* l_Lean_Compiler_natFoldFns___closed__9;
static lean_object* l_Lean_Compiler_natFoldFns___closed__40;
static lean_object* l_Lean_Compiler_natFoldFns___closed__4;
static lean_object* l_Lean_Compiler_numScalarTypes___closed__20;
static lean_object* l_List_foldl___at_Lean_Compiler_uintFoldToNatFns___spec__1___closed__1;
@ -97,14 +101,17 @@ static lean_object* l_Lean_Compiler_foldNatDecLe___closed__1;
uint32_t lean_uint32_of_nat(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatAdd___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatDecLe___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_natFoldFns___closed__45;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatDiv(uint8_t);
extern lean_object* l_Lean_levelZero;
lean_object* lean_nat_add(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__19;
LEAN_EXPORT lean_object* l_Lean_Compiler_mkUInt32Lit(lean_object*);
static lean_object* l_Lean_Compiler_numScalarTypes___closed__17;
static lean_object* l_Lean_Compiler_natFoldFns___closed__37;
static lean_object* l_Lean_Compiler_toDecidableExpr___closed__4;
static lean_object* l_Lean_Compiler_numScalarTypes___closed__27;
static lean_object* l_Lean_Compiler_foldNatBinBoolPred___closed__2;
static lean_object* l_Lean_Compiler_numScalarTypes___closed__4;
static lean_object* l_Lean_Compiler_natFoldFns___closed__16;
lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
@ -112,21 +119,25 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_binFoldFns;
static lean_object* l_Lean_Compiler_mkNatLe___closed__2;
lean_object* l_Lean_mkDecIsTrue(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_foldStrictOr___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBle___rarg(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_natFoldFns___closed__7;
static lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__21;
LEAN_EXPORT lean_object* l_List_lookup___at_Lean_Compiler_findUnFoldFn___spec__1(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_foldNatBinBoolPred___closed__1;
static lean_object* l_Lean_Compiler_numScalarTypes___closed__8;
static lean_object* l_Lean_Compiler_binFoldFns___closed__1;
static lean_object* l_Lean_Compiler_mkNatEq___closed__3;
static lean_object* l_Lean_Compiler_toDecidableExpr___closed__8;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldUIntDiv___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_natFoldFns___closed__21;
static lean_object* l_Lean_Compiler_natFoldFns___closed__38;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatDecEq(uint8_t, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_foldUIntDiv___closed__1;
static lean_object* l_Lean_Compiler_mkNatEq___closed__8;
LEAN_EXPORT lean_object* l_Lean_Compiler_toDecidableExpr___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* lean_fold_un_op(uint8_t, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_toDecidableExpr___closed__1;
static lean_object* l_Lean_Compiler_natFoldFns___closed__42;
static lean_object* l_Lean_Compiler_boolFoldFns___closed__6;
static lean_object* l_Lean_Compiler_unFoldFns___closed__6;
lean_object* lean_nat_sub(lean_object*, lean_object*);
@ -149,6 +160,7 @@ static lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__17;
static lean_object* l_Lean_Compiler_numScalarTypes___closed__3;
static lean_object* l_Lean_Compiler_unFoldFns___closed__4;
static lean_object* l_Lean_Compiler_numScalarTypes___closed__5;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBle(uint8_t);
static lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__4;
static lean_object* l_Lean_Compiler_unFoldFns___closed__9;
static lean_object* l_Lean_Compiler_numScalarTypes___closed__18;
@ -159,6 +171,7 @@ LEAN_EXPORT lean_object* l_List_lookup___at_Lean_Compiler_findUnFoldFn___spec__1
static lean_object* l_Lean_Compiler_numScalarTypes___closed__14;
static lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__12;
static lean_object* l_Lean_Compiler_numScalarTypes___closed__28;
static lean_object* l_Lean_Compiler_natFoldFns___closed__47;
static lean_object* l_Lean_Compiler_boolFoldFns___closed__8;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldUIntMod___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_getInfoFromFn(lean_object*, lean_object*);
@ -166,6 +179,7 @@ static lean_object* l_Lean_Compiler_mkNatEq___closed__4;
LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Compiler_uintBinFoldFns___spec__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_unFoldFns___closed__8;
static lean_object* l_Lean_Compiler_mkNatLe___closed__8;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBlt(uint8_t);
static lean_object* l_Lean_Compiler_natFoldFns___closed__12;
lean_object* l_Nat_repr(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_findUnFoldFn(lean_object*);
@ -189,6 +203,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_mkUIntTypeName(lean_object*);
LEAN_EXPORT lean_object* l_List_lookup___at_Lean_Compiler_findBinFoldFn___spec__1(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_unFoldFns___closed__2;
static lean_object* l_Lean_Compiler_boolFoldFns___closed__2;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBle___boxed(lean_object*);
static lean_object* l_Lean_Compiler_boolFoldFns___closed__4;
static lean_object* l_Lean_Compiler_numScalarTypes___closed__26;
static lean_object* l_Lean_Compiler_mkUIntTypeName___closed__1;
@ -206,7 +221,9 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_foldUIntMul___boxed(lean_object*, lean_
static lean_object* l_Lean_Compiler_natFoldFns___closed__2;
LEAN_EXPORT lean_object* l_Lean_Compiler_getInfoFromFn___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_foldUIntMul___closed__1;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBeq___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_foldBinOp___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_natFoldFns___closed__48;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatDecLe(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_mkDecIsFalse(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__11;
@ -218,6 +235,9 @@ static lean_object* l_Lean_Compiler_boolFoldFns___closed__1;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBinPred(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_mkNatLt___closed__2;
LEAN_EXPORT lean_object* l_List_foldl___at_Lean_Compiler_uintFoldToNatFns___spec__1(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_natFoldFns___closed__50;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBlt___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBlt___boxed(lean_object*);
static lean_object* l_Lean_Compiler_unFoldFns___closed__7;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatDiv___boxed(lean_object*);
static lean_object* l_Lean_Compiler_natFoldFns___closed__34;
@ -251,7 +271,9 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_mkNatLt(lean_object*, lean_object*);
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_mkUIntLit(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_foldBinUInt___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBeq___boxed(lean_object*);
static lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__24;
static lean_object* l_Lean_Compiler_foldNatBeq___rarg___closed__1;
lean_object* l_Lean_Name_append(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_mkNatLe___closed__1;
static lean_object* l_Lean_Compiler_numScalarTypes___closed__2;
@ -261,6 +283,7 @@ static lean_object* l_Lean_Compiler_mkNatLt___closed__6;
lean_object* l_Nat_mul___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_NumScalarTypeInfo_toNatFn___default(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatAdd(uint8_t);
static lean_object* l_Lean_Compiler_natFoldFns___closed__49;
static lean_object* l_Lean_Compiler_natFoldFns___closed__24;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldStrictOr(uint8_t);
static lean_object* l_Lean_Compiler_mkNatLt___closed__4;
@ -268,6 +291,7 @@ lean_object* lean_nat_mul(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_natFoldFns___closed__36;
static lean_object* l_Lean_Compiler_numScalarTypes___closed__10;
static lean_object* l_Lean_Compiler_natFoldFns___closed__35;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBinBoolPred(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_findBinFoldFn___boxed(lean_object*);
static lean_object* l_Lean_Compiler_natFoldFns___closed__17;
static lean_object* l_Lean_Compiler_foldNatMod___rarg___closed__1;
@ -298,6 +322,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_foldBinUInt(lean_object*, uint8_t, lean
LEAN_EXPORT lean_object* l_Lean_Compiler_foldUIntAdd(uint8_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_foldr___at_Lean_Compiler_isOfNat___spec__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_mkNatLe___closed__7;
static lean_object* l_Lean_Compiler_natFoldFns___closed__39;
lean_object* lean_nat_mod(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_numScalarTypes___closed__7;
static lean_object* l_Lean_Compiler_natFoldFns___closed__1;
@ -306,17 +331,20 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_getInfoFromVal___boxed(lean_object*);
static lean_object* l_Lean_Compiler_natFoldFns___closed__23;
static lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__16;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldUIntMul___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_natFoldFns___closed__41;
static lean_object* l_Lean_Compiler_numScalarTypes___closed__11;
static lean_object* l_Lean_Compiler_mkNatLt___closed__8;
extern lean_object* l_Lean_levelOne;
LEAN_EXPORT lean_object* l_Lean_Compiler_foldUIntMul(uint8_t, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_foldNatDecEq___closed__2;
static lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__6;
static lean_object* l_Lean_Compiler_natFoldFns___closed__43;
LEAN_EXPORT lean_object* lean_get_num_lit(lean_object*);
static lean_object* l_Lean_Compiler_foldNatDecLt___closed__1;
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_boolFoldFns;
static lean_object* l_Lean_Compiler_unFoldFns___closed__10;
static lean_object* l_Lean_Compiler_natFoldFns___closed__46;
static lean_object* l_Lean_Compiler_getBoolLit___closed__1;
LEAN_EXPORT lean_object* l_Lean_Compiler_findUnFoldFn___boxed(lean_object*);
lean_object* l_List_appendTR___rarg(lean_object*, lean_object*);
@ -334,6 +362,7 @@ static lean_object* l_Lean_Compiler_mkNatLt___closed__9;
lean_object* l_Nat_decEq___boxed(lean_object*, lean_object*);
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatDecEq___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_natFoldFns___closed__44;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_boolFoldFns___closed__10;
static lean_object* l_Lean_Compiler_toDecidableExpr___closed__2;
@ -2749,6 +2778,168 @@ x_5 = l_Lean_Compiler_foldNatDecLe(x_4, x_2, x_3);
return x_5;
}
}
static lean_object* _init_l_Lean_Compiler_foldNatBinBoolPred___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Compiler_toDecidableExpr___closed__5;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Compiler_foldNatBinBoolPred___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Compiler_toDecidableExpr___closed__8;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBinBoolPred(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_get_num_lit(x_2);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5;
lean_dec(x_3);
lean_dec(x_1);
x_5 = lean_box(0);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7;
x_6 = lean_ctor_get(x_4, 0);
lean_inc(x_6);
lean_dec(x_4);
x_7 = lean_get_num_lit(x_3);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8;
lean_dec(x_6);
lean_dec(x_1);
x_8 = lean_box(0);
return x_8;
}
else
{
lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_9 = lean_ctor_get(x_7, 0);
lean_inc(x_9);
lean_dec(x_7);
x_10 = lean_apply_2(x_1, x_6, x_9);
x_11 = lean_unbox(x_10);
lean_dec(x_10);
if (x_11 == 0)
{
lean_object* x_12;
x_12 = l_Lean_Compiler_foldNatBinBoolPred___closed__1;
return x_12;
}
else
{
lean_object* x_13;
x_13 = l_Lean_Compiler_foldNatBinBoolPred___closed__2;
return x_13;
}
}
}
}
}
static lean_object* _init_l_Lean_Compiler_foldNatBeq___rarg___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Nat_beq___boxed), 2, 0);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBeq___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = l_Lean_Compiler_foldNatBeq___rarg___closed__1;
x_4 = l_Lean_Compiler_foldNatBinBoolPred(x_3, x_1, x_2);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBeq(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Compiler_foldNatBeq___rarg), 2, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBeq___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_Lean_Compiler_foldNatBeq(x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBle___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = l_Lean_Compiler_foldNatDecLt___closed__2;
x_4 = l_Lean_Compiler_foldNatBinBoolPred(x_3, x_1, x_2);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBle(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Compiler_foldNatBle___rarg), 2, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBle___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_Lean_Compiler_foldNatBle(x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBlt___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = l_Lean_Compiler_foldNatDecLe___closed__2;
x_4 = l_Lean_Compiler_foldNatBinBoolPred(x_3, x_1, x_2);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBlt(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Compiler_foldNatBlt___rarg), 2, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_foldNatBlt___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_Lean_Compiler_foldNatBlt(x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Compiler_natFoldFns___closed__1() {
_start:
{
@ -3024,46 +3215,36 @@ return x_3;
static lean_object* _init_l_Lean_Compiler_natFoldFns___closed__29() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Compiler_natFoldFns___closed__28;
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* x_1;
x_1 = lean_mk_string("beq");
return x_1;
}
}
static lean_object* _init_l_Lean_Compiler_natFoldFns___closed__30() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__24;
x_1 = l_Lean_Compiler_mkNatEq___closed__6;
x_2 = l_Lean_Compiler_natFoldFns___closed__29;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Compiler_natFoldFns___closed__31() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__20;
x_2 = l_Lean_Compiler_natFoldFns___closed__30;
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;
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Compiler_foldNatBeq___boxed), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Compiler_natFoldFns___closed__32() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__16;
x_1 = l_Lean_Compiler_natFoldFns___closed__30;
x_2 = l_Lean_Compiler_natFoldFns___closed__31;
x_3 = lean_alloc_ctor(1, 2, 0);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
@ -3072,45 +3253,205 @@ return x_3;
static lean_object* _init_l_Lean_Compiler_natFoldFns___closed__33() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__12;
x_2 = l_Lean_Compiler_natFoldFns___closed__32;
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;
lean_object* x_1;
x_1 = lean_mk_string("blt");
return x_1;
}
}
static lean_object* _init_l_Lean_Compiler_natFoldFns___closed__34() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__9;
x_1 = l_Lean_Compiler_mkNatEq___closed__6;
x_2 = l_Lean_Compiler_natFoldFns___closed__33;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Compiler_natFoldFns___closed__35() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__6;
x_2 = l_Lean_Compiler_natFoldFns___closed__34;
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;
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Compiler_foldNatBlt___boxed), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Compiler_natFoldFns___closed__36() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__3;
x_1 = l_Lean_Compiler_natFoldFns___closed__34;
x_2 = l_Lean_Compiler_natFoldFns___closed__35;
x_3 = lean_alloc_ctor(0, 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_Compiler_natFoldFns___closed__37() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("ble");
return x_1;
}
}
static lean_object* _init_l_Lean_Compiler_natFoldFns___closed__38() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_mkNatEq___closed__6;
x_2 = l_Lean_Compiler_natFoldFns___closed__37;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Compiler_natFoldFns___closed__39() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Compiler_foldNatBle___boxed), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Compiler_natFoldFns___closed__40() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__38;
x_2 = l_Lean_Compiler_natFoldFns___closed__39;
x_3 = lean_alloc_ctor(0, 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_Compiler_natFoldFns___closed__41() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Compiler_natFoldFns___closed__40;
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;
}
}
static lean_object* _init_l_Lean_Compiler_natFoldFns___closed__42() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__36;
x_2 = l_Lean_Compiler_natFoldFns___closed__41;
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_Compiler_natFoldFns___closed__43() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__32;
x_2 = l_Lean_Compiler_natFoldFns___closed__42;
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_Compiler_natFoldFns___closed__44() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__28;
x_2 = l_Lean_Compiler_natFoldFns___closed__43;
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_Compiler_natFoldFns___closed__45() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__24;
x_2 = l_Lean_Compiler_natFoldFns___closed__44;
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_Compiler_natFoldFns___closed__46() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__20;
x_2 = l_Lean_Compiler_natFoldFns___closed__45;
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_Compiler_natFoldFns___closed__47() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__16;
x_2 = l_Lean_Compiler_natFoldFns___closed__46;
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_Compiler_natFoldFns___closed__48() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__12;
x_2 = l_Lean_Compiler_natFoldFns___closed__47;
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_Compiler_natFoldFns___closed__49() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__9;
x_2 = l_Lean_Compiler_natFoldFns___closed__48;
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_Compiler_natFoldFns___closed__50() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__6;
x_2 = l_Lean_Compiler_natFoldFns___closed__49;
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_Compiler_natFoldFns___closed__51() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_natFoldFns___closed__3;
x_2 = l_Lean_Compiler_natFoldFns___closed__50;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -3121,7 +3462,7 @@ static lean_object* _init_l_Lean_Compiler_natFoldFns() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Compiler_natFoldFns___closed__36;
x_1 = l_Lean_Compiler_natFoldFns___closed__51;
return x_1;
}
}
@ -4594,6 +4935,12 @@ l_Lean_Compiler_foldNatDecLe___closed__1 = _init_l_Lean_Compiler_foldNatDecLe___
lean_mark_persistent(l_Lean_Compiler_foldNatDecLe___closed__1);
l_Lean_Compiler_foldNatDecLe___closed__2 = _init_l_Lean_Compiler_foldNatDecLe___closed__2();
lean_mark_persistent(l_Lean_Compiler_foldNatDecLe___closed__2);
l_Lean_Compiler_foldNatBinBoolPred___closed__1 = _init_l_Lean_Compiler_foldNatBinBoolPred___closed__1();
lean_mark_persistent(l_Lean_Compiler_foldNatBinBoolPred___closed__1);
l_Lean_Compiler_foldNatBinBoolPred___closed__2 = _init_l_Lean_Compiler_foldNatBinBoolPred___closed__2();
lean_mark_persistent(l_Lean_Compiler_foldNatBinBoolPred___closed__2);
l_Lean_Compiler_foldNatBeq___rarg___closed__1 = _init_l_Lean_Compiler_foldNatBeq___rarg___closed__1();
lean_mark_persistent(l_Lean_Compiler_foldNatBeq___rarg___closed__1);
l_Lean_Compiler_natFoldFns___closed__1 = _init_l_Lean_Compiler_natFoldFns___closed__1();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__1);
l_Lean_Compiler_natFoldFns___closed__2 = _init_l_Lean_Compiler_natFoldFns___closed__2();
@ -4666,6 +5013,36 @@ l_Lean_Compiler_natFoldFns___closed__35 = _init_l_Lean_Compiler_natFoldFns___clo
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__35);
l_Lean_Compiler_natFoldFns___closed__36 = _init_l_Lean_Compiler_natFoldFns___closed__36();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__36);
l_Lean_Compiler_natFoldFns___closed__37 = _init_l_Lean_Compiler_natFoldFns___closed__37();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__37);
l_Lean_Compiler_natFoldFns___closed__38 = _init_l_Lean_Compiler_natFoldFns___closed__38();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__38);
l_Lean_Compiler_natFoldFns___closed__39 = _init_l_Lean_Compiler_natFoldFns___closed__39();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__39);
l_Lean_Compiler_natFoldFns___closed__40 = _init_l_Lean_Compiler_natFoldFns___closed__40();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__40);
l_Lean_Compiler_natFoldFns___closed__41 = _init_l_Lean_Compiler_natFoldFns___closed__41();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__41);
l_Lean_Compiler_natFoldFns___closed__42 = _init_l_Lean_Compiler_natFoldFns___closed__42();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__42);
l_Lean_Compiler_natFoldFns___closed__43 = _init_l_Lean_Compiler_natFoldFns___closed__43();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__43);
l_Lean_Compiler_natFoldFns___closed__44 = _init_l_Lean_Compiler_natFoldFns___closed__44();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__44);
l_Lean_Compiler_natFoldFns___closed__45 = _init_l_Lean_Compiler_natFoldFns___closed__45();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__45);
l_Lean_Compiler_natFoldFns___closed__46 = _init_l_Lean_Compiler_natFoldFns___closed__46();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__46);
l_Lean_Compiler_natFoldFns___closed__47 = _init_l_Lean_Compiler_natFoldFns___closed__47();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__47);
l_Lean_Compiler_natFoldFns___closed__48 = _init_l_Lean_Compiler_natFoldFns___closed__48();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__48);
l_Lean_Compiler_natFoldFns___closed__49 = _init_l_Lean_Compiler_natFoldFns___closed__49();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__49);
l_Lean_Compiler_natFoldFns___closed__50 = _init_l_Lean_Compiler_natFoldFns___closed__50();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__50);
l_Lean_Compiler_natFoldFns___closed__51 = _init_l_Lean_Compiler_natFoldFns___closed__51();
lean_mark_persistent(l_Lean_Compiler_natFoldFns___closed__51);
l_Lean_Compiler_natFoldFns = _init_l_Lean_Compiler_natFoldFns();
lean_mark_persistent(l_Lean_Compiler_natFoldFns);
l_Lean_Compiler_getBoolLit___closed__1 = _init_l_Lean_Compiler_getBoolLit___closed__1();

1
stage0/stdlib/Lean/Compiler/ExternAttr.c generated
View file

@ -145,6 +145,7 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Compiler_E
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Compiler_ExternAttr_0__Lean_syntaxToExternAttrData___spec__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_mul(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Compiler_ExternAttr_0__Lean_getExternConstArity___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_expandExternPatternAux(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_getExternEntryForAux___boxed(lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNone(lean_object*);

1
stage0/stdlib/Lean/Compiler/IR/Basic.c generated
View file

@ -245,6 +245,7 @@ LEAN_EXPORT uint8_t l_Lean_IR_CtorInfo_beq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_instToFormatJoinPointId(lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_IRType_isStruct___boxed(lean_object*);
static lean_object* l___private_Lean_Compiler_IR_Basic_0__Lean_IR_reprCtorInfo____x40_Lean_Compiler_IR_Basic___hyg_748____closed__2;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_IRType_instBEqIRType;
LEAN_EXPORT lean_object* l_Lean_IR_Decl_updateBody_x21(lean_object*, lean_object*);
LEAN_EXPORT lean_object* lean_ir_mk_uset(lean_object*, lean_object*, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Compiler/IR/Borrow.c generated
View file

@ -177,6 +177,7 @@ lean_object* lean_nat_mul(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_Borrow_isOwned___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_Borrow_ApplyParamMap_visitFnBody___spec__4(lean_object*, lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_Borrow_ApplyParamMap_visitDecls(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Std_AssocList_foldlM___at_Lean_IR_Borrow_ParamMap_fmt___spec__1___closed__3;
LEAN_EXPORT lean_object* l_Lean_IR_Borrow_ownArgsIfParam(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_Borrow_ownArgsUsingParams(lean_object*, lean_object*, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Compiler/IR/Boxing.c generated
View file

@ -123,6 +123,7 @@ LEAN_EXPORT lean_object* l_Lean_IR_ExplicitBoxing_mkBoxedVersion(lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_ExplicitBoxing_unboxResultIfNeeded___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_LocalContext_addLocal(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_ExplicitBoxing_eqvTypes___boxed(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_ExplicitBoxing_getResultType(lean_object*, lean_object*);
lean_object* l_Lean_IR_Decl_updateBody_x21(lean_object*, lean_object*);
static lean_object* l_Lean_IR_ExplicitBoxing_getDecl___closed__1;

1
stage0/stdlib/Lean/Compiler/IR/Checker.c generated
View file

@ -121,6 +121,7 @@ LEAN_EXPORT lean_object* l_Lean_IR_Checker_checkPartialApp___boxed(lean_object*,
lean_object* l_Lean_IR_LocalContext_addLocal(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_mul(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_Checker_getUSizeSize(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_IR_Checker_checkFullApp___closed__1;
LEAN_EXPORT lean_object* l_Lean_IR_Checker_getMaxCtorFields(lean_object*);
static lean_object* l_Lean_IR_Checker_checkJP___closed__2;

1
stage0/stdlib/Lean/Compiler/IR/ElimDeadBranches.c generated
View file

@ -292,6 +292,7 @@ LEAN_EXPORT lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_IR_Unreacha
lean_object* l_Lean_Name_getPrefix(lean_object*);
static lean_object* l___private_Lean_Compiler_IR_ElimDeadBranches_0__Lean_IR_UnreachableBranches_reprValue____x40_Lean_Compiler_IR_ElimDeadBranches___hyg_40____closed__8;
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_IR_UnreachableBranches_initFn____x40_Lean_Compiler_IR_ElimDeadBranches___hyg_950____spec__4(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l___private_Lean_Compiler_IR_ElimDeadBranches_0__Lean_IR_UnreachableBranches_reprValue____x40_Lean_Compiler_IR_ElimDeadBranches___hyg_40____closed__17;
LEAN_EXPORT lean_object* l_Lean_IR_elimDeadBranches___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashMapImp_expand___at_Lean_IR_UnreachableBranches_initFn____x40_Lean_Compiler_IR_ElimDeadBranches___hyg_950____spec__8(lean_object*, lean_object*);

1
stage0/stdlib/Lean/Compiler/IR/EmitC.c generated
View file

@ -472,6 +472,7 @@ LEAN_EXPORT lean_object* l_Nat_forM_loop___at_Lean_IR_EmitC_emitArgs___spec__1__
LEAN_EXPORT lean_object* l_Nat_foldM_loop___at_Lean_IR_EmitC_emitSimpleExternalCall___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_foldM_loop___at_Lean_IR_EmitC_emitSimpleExternalCall___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_EmitC_emitTag(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_IR_EmitC_emitInitFn___closed__11;
LEAN_EXPORT lean_object* l_Lean_IR_EmitC_emitDecl(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_EmitC_throwUnknownVar(lean_object*);

2
stage0/stdlib/Lean/Compiler/IR/EmitUtil.c generated
View file

@ -42,7 +42,6 @@ size_t lean_uint64_to_usize(uint64_t);
lean_object* l_Lean_IR_AltCore_body(lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* lean_get_init_fn_name_for(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_IR_mkVarJPMaps___spec__2(lean_object*);
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_mkHashMapImp___rarg(lean_object*);
@ -71,6 +70,7 @@ LEAN_EXPORT lean_object* l_Lean_IR_CollectUsedDecls_collectInitDecl(lean_object*
LEAN_EXPORT lean_object* l_Std_HashMapImp_moveEntries___at_Lean_IR_CollectMaps_collectJP___spec__4(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_AssocList_contains___at_Lean_IR_CollectMaps_collectVar___spec__2___boxed(lean_object*, lean_object*);
lean_object* lean_nat_mul(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_AssocList_contains___at_Lean_IR_CollectMaps_collectJP___spec__2___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_foldr___at_Lean_IR_usesModuleFrom___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Environment_allImportedModuleNames(lean_object*);

1
stage0/stdlib/Lean/Compiler/IR/ExpandResetReuse.c generated
View file

@ -101,6 +101,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_ExpandResetReuse_re
lean_object* lean_nat_mul(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_ExpandResetReuse_reuseToCtor___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_ExpandResetReuse_reuseToCtor___boxed(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_IR_Decl_updateBody_x21(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_ExpandResetReuse_mkFresh___rarg(lean_object*);
lean_object* lean_array_pop(lean_object*);

2
stage0/stdlib/Lean/Compiler/IR/Format.c generated
View file

@ -87,7 +87,6 @@ static lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatParam__
static lean_object* l_Lean_IR_formatFnBody_loop___closed__6;
static lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatCtorInfo___closed__6;
static lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed__23;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType___closed__14;
static lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType___closed__25;
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_formatFnBody_loop___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*);
@ -191,6 +190,7 @@ static lean_object* l_Lean_IR_formatFnBodyHead___closed__28;
static lean_object* l_Lean_IR_formatFnBodyHead___closed__14;
static lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType___closed__3;
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatCtorInfo(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatCtorInfo___lambda__2___closed__4;
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatParam(lean_object*);
static lean_object* l_Lean_IR_formatDecl___closed__4;

1
stage0/stdlib/Lean/Compiler/IR/FreeVars.c generated
View file

@ -97,6 +97,7 @@ LEAN_EXPORT uint8_t l_Lean_IR_HasIndex_visitArgs(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_IR_HasIndex_visitFnBody(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Compiler_IR_FreeVars_0__Lean_IR_FreeIndices_collectArray___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_FreeVars_0__Lean_IR_MaxIndex_collectArgs(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_FnBody_maxIndex(lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_MaxIndex_instAndThenCollector(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_FreeVars_0__Lean_IR_MaxIndex_collectAlts(lean_object*, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Compiler/IR/LiveVars.c generated
View file

@ -79,6 +79,7 @@ uint8_t l_Lean_IR_HasIndex_visitArgs(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_LiveVars_collectFnBody___lambda__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_mkLiveVarSet(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindParams(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindParams___spec__1(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_IR_LocalContext_getJPBody(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_RBNode_fold___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_accumulate___spec__1___boxed(lean_object*, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Compiler/IR/NormIds.c generated
View file

@ -62,6 +62,7 @@ LEAN_EXPORT lean_object* l_Lean_IR_UniqueIds_checkId(lean_object*, lean_object*)
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_NormalizeIds_normJP(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_NormalizeIds_instMonadLiftMN___rarg(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_IR_UniqueIds_checkFnBody___spec__1(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_IR_Decl_updateBody_x21(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_NormalizeIds_normFnBody___spec__1(lean_object*, size_t, size_t, lean_object*);

418
stage0/stdlib/Lean/Compiler/IR/RC.c generated
View file

@ -59,6 +59,7 @@ LEAN_EXPORT lean_object* l_Lean_IR_explicitRC(lean_object*, lean_object*, lean_o
static lean_object* l_Lean_IR_ExplicitRC_getDecl___closed__3;
LEAN_EXPORT lean_object* l_Lean_IR_ExplicitRC_Context_localCtx___default;
uint8_t lean_usize_dec_lt(size_t, size_t);
static uint8_t l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_processVDecl___closed__1;
uint8_t l_Lean_IR_IRType_isObj(lean_object*);
LEAN_EXPORT lean_object* l_Nat_foldAux___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeAux___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
@ -126,6 +127,7 @@ LEAN_EXPORT uint8_t l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_consum
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_isPersistent___boxed(lean_object*);
LEAN_EXPORT uint8_t l_Lean_IR_ExplicitRC_mustConsume(lean_object*, lean_object*);
lean_object* l_Lean_IR_mkLiveVarSet(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_RBNode_insert___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_updateRefUsingCtorInfo___spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_RBNode_ins___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_updateRefUsingCtorInfo___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_Decl_updateBody_x21(lean_object*, lean_object*);
@ -4641,6 +4643,16 @@ lean_dec(x_4);
return x_5;
}
}
static uint8_t _init_l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_processVDecl___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3;
x_1 = lean_unsigned_to_nat(1u);
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_nat_dec_eq(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_processVDecl(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
@ -4724,186 +4736,208 @@ return x_26;
}
else
{
lean_object* x_27; uint8_t x_28; lean_object* x_29; uint8_t x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34;
x_27 = l_Lean_IR_ExplicitRC_getVarInfo(x_1, x_2);
x_28 = lean_ctor_get_uint8(x_27, 1);
lean_dec(x_27);
x_29 = lean_unsigned_to_nat(1u);
x_30 = 1;
uint8_t x_27;
x_27 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_processVDecl___closed__1;
if (x_27 == 0)
{
lean_object* x_28; uint8_t x_29; lean_object* x_30; uint8_t x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_28 = l_Lean_IR_ExplicitRC_getVarInfo(x_1, x_2);
x_29 = lean_ctor_get_uint8(x_28, 1);
lean_dec(x_28);
x_30 = lean_unsigned_to_nat(1u);
x_31 = 1;
lean_inc(x_2);
x_31 = lean_alloc_ctor(6, 3, 2);
lean_ctor_set(x_31, 0, x_2);
lean_ctor_set(x_31, 1, x_29);
lean_ctor_set(x_31, 2, x_21);
lean_ctor_set_uint8(x_31, sizeof(void*)*3, x_30);
lean_ctor_set_uint8(x_31, sizeof(void*)*3 + 1, x_28);
lean_inc(x_2);
x_32 = lean_alloc_ctor(0, 4, 0);
x_32 = lean_alloc_ctor(6, 3, 2);
lean_ctor_set(x_32, 0, x_2);
lean_ctor_set(x_32, 1, x_3);
lean_ctor_set(x_32, 2, x_4);
lean_ctor_set(x_32, 3, x_31);
x_33 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
lean_ctor_set(x_32, 1, x_30);
lean_ctor_set(x_32, 2, x_21);
lean_ctor_set_uint8(x_32, sizeof(void*)*3, x_31);
lean_ctor_set_uint8(x_32, sizeof(void*)*3 + 1, x_29);
lean_inc(x_2);
x_33 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_33, 0, x_2);
lean_ctor_set(x_33, 1, x_3);
lean_ctor_set(x_33, 2, x_4);
lean_ctor_set(x_33, 3, x_32);
x_34 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
lean_dec(x_2);
x_34 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_34, 0, x_32);
lean_ctor_set(x_34, 1, x_33);
return x_34;
x_35 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_35, 0, x_33);
lean_ctor_set(x_35, 1, x_34);
return x_35;
}
else
{
lean_object* x_36; lean_object* x_37; lean_object* x_38;
lean_dec(x_1);
lean_inc(x_2);
x_36 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_36, 0, x_2);
lean_ctor_set(x_36, 1, x_3);
lean_ctor_set(x_36, 2, x_4);
lean_ctor_set(x_36, 3, x_21);
x_37 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
lean_dec(x_2);
x_38 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_38, 0, x_36);
lean_ctor_set(x_38, 1, x_37);
return x_38;
}
}
}
case 4:
{
lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_35 = lean_ctor_get(x_4, 1);
lean_inc(x_35);
x_36 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addDecIfNeeded(x_1, x_35, x_5, x_6);
lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_39 = lean_ctor_get(x_4, 1);
lean_inc(x_39);
x_40 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addDecIfNeeded(x_1, x_39, x_5, x_6);
lean_dec(x_6);
lean_inc(x_2);
x_37 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_37, 0, x_2);
lean_ctor_set(x_37, 1, x_3);
lean_ctor_set(x_37, 2, x_4);
lean_ctor_set(x_37, 3, x_36);
x_38 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
x_41 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_41, 0, x_2);
lean_ctor_set(x_41, 1, x_3);
lean_ctor_set(x_41, 2, x_4);
lean_ctor_set(x_41, 3, x_40);
x_42 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
lean_dec(x_2);
x_39 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_39, 0, x_37);
lean_ctor_set(x_39, 1, x_38);
return x_39;
x_43 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_43, 0, x_41);
lean_ctor_set(x_43, 1, x_42);
return x_43;
}
case 5:
{
lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44;
x_40 = lean_ctor_get(x_4, 2);
lean_inc(x_40);
x_41 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addDecIfNeeded(x_1, x_40, x_5, x_6);
lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48;
x_44 = lean_ctor_get(x_4, 2);
lean_inc(x_44);
x_45 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addDecIfNeeded(x_1, x_44, x_5, x_6);
lean_dec(x_6);
lean_inc(x_2);
x_42 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_42, 0, x_2);
lean_ctor_set(x_42, 1, x_3);
lean_ctor_set(x_42, 2, x_4);
lean_ctor_set(x_42, 3, x_41);
x_43 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
x_46 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_46, 0, x_2);
lean_ctor_set(x_46, 1, x_3);
lean_ctor_set(x_46, 2, x_4);
lean_ctor_set(x_46, 3, x_45);
x_47 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
lean_dec(x_2);
x_44 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_44, 0, x_42);
lean_ctor_set(x_44, 1, x_43);
return x_44;
x_48 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_48, 0, x_46);
lean_ctor_set(x_48, 1, x_47);
return x_48;
}
case 6:
{
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; lean_object* x_52; lean_object* x_53;
x_45 = lean_ctor_get(x_4, 0);
lean_inc(x_45);
x_46 = lean_ctor_get(x_4, 1);
lean_inc(x_46);
x_47 = l_Lean_IR_ExplicitRC_getDecl(x_1, x_45);
x_48 = l_Lean_IR_Decl_params(x_47);
lean_dec(x_47);
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;
x_49 = lean_ctor_get(x_4, 0);
lean_inc(x_49);
x_50 = lean_ctor_get(x_4, 1);
lean_inc(x_50);
x_51 = l_Lean_IR_ExplicitRC_getDecl(x_1, x_49);
x_52 = l_Lean_IR_Decl_params(x_51);
lean_dec(x_51);
lean_inc(x_6);
lean_inc(x_48);
lean_inc(x_52);
lean_inc(x_1);
x_49 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addDecAfterFullApp(x_1, x_46, x_48, x_5, x_6);
x_53 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addDecAfterFullApp(x_1, x_50, x_52, x_5, x_6);
lean_inc(x_2);
x_50 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_50, 0, x_2);
lean_ctor_set(x_50, 1, x_3);
lean_ctor_set(x_50, 2, x_4);
lean_ctor_set(x_50, 3, x_49);
x_51 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBefore(x_1, x_46, x_48, x_50, x_6);
lean_dec(x_46);
x_52 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
x_54 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_54, 0, x_2);
lean_ctor_set(x_54, 1, x_3);
lean_ctor_set(x_54, 2, x_4);
lean_ctor_set(x_54, 3, x_53);
x_55 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBefore(x_1, x_50, x_52, x_54, x_6);
lean_dec(x_50);
x_56 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
lean_dec(x_2);
x_53 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_53, 0, x_51);
lean_ctor_set(x_53, 1, x_52);
return x_53;
x_57 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_57, 0, x_55);
lean_ctor_set(x_57, 1, x_56);
return x_57;
}
case 7:
{
lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59;
x_54 = lean_ctor_get(x_4, 1);
lean_inc(x_54);
lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63;
x_58 = lean_ctor_get(x_4, 1);
lean_inc(x_58);
lean_inc(x_2);
x_55 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_55, 0, x_2);
lean_ctor_set(x_55, 1, x_3);
lean_ctor_set(x_55, 2, x_4);
lean_ctor_set(x_55, 3, x_5);
x_56 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeConsumeAll___closed__1;
x_57 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeAux(x_1, x_54, x_56, x_55, x_6);
lean_dec(x_54);
x_58 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
x_59 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_59, 0, x_2);
lean_ctor_set(x_59, 1, x_3);
lean_ctor_set(x_59, 2, x_4);
lean_ctor_set(x_59, 3, x_5);
x_60 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeConsumeAll___closed__1;
x_61 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeAux(x_1, x_58, x_60, x_59, x_6);
lean_dec(x_58);
x_62 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
lean_dec(x_2);
x_59 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_59, 0, x_57);
lean_ctor_set(x_59, 1, x_58);
return x_59;
x_63 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_63, 0, x_61);
lean_ctor_set(x_63, 1, x_62);
return x_63;
}
case 8:
{
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;
x_60 = lean_ctor_get(x_4, 0);
lean_inc(x_60);
x_61 = lean_ctor_get(x_4, 1);
lean_inc(x_61);
x_62 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_62, 0, x_60);
x_63 = lean_array_push(x_61, x_62);
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;
x_64 = lean_ctor_get(x_4, 0);
lean_inc(x_64);
x_65 = lean_ctor_get(x_4, 1);
lean_inc(x_65);
x_66 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_66, 0, x_64);
x_67 = lean_array_push(x_65, x_66);
lean_inc(x_2);
x_64 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_64, 0, x_2);
lean_ctor_set(x_64, 1, x_3);
lean_ctor_set(x_64, 2, x_4);
lean_ctor_set(x_64, 3, x_5);
x_65 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeConsumeAll___closed__1;
x_66 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeAux(x_1, x_63, x_65, x_64, x_6);
lean_dec(x_63);
x_67 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
x_68 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_68, 0, x_2);
lean_ctor_set(x_68, 1, x_3);
lean_ctor_set(x_68, 2, x_4);
lean_ctor_set(x_68, 3, x_5);
x_69 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeConsumeAll___closed__1;
x_70 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeAux(x_1, x_67, x_69, x_68, x_6);
lean_dec(x_67);
x_71 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
lean_dec(x_2);
x_68 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_68, 0, x_66);
lean_ctor_set(x_68, 1, x_67);
return x_68;
x_72 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_72, 0, x_70);
lean_ctor_set(x_72, 1, x_71);
return x_72;
}
case 10:
{
lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73;
x_69 = lean_ctor_get(x_4, 0);
lean_inc(x_69);
x_70 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addDecIfNeeded(x_1, x_69, x_5, x_6);
lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77;
x_73 = lean_ctor_get(x_4, 0);
lean_inc(x_73);
x_74 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addDecIfNeeded(x_1, x_73, x_5, x_6);
lean_dec(x_6);
lean_inc(x_2);
x_71 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_71, 0, x_2);
lean_ctor_set(x_71, 1, x_3);
lean_ctor_set(x_71, 2, x_4);
lean_ctor_set(x_71, 3, x_70);
x_72 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
x_75 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_75, 0, x_2);
lean_ctor_set(x_75, 1, x_3);
lean_ctor_set(x_75, 2, x_4);
lean_ctor_set(x_75, 3, x_74);
x_76 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
lean_dec(x_2);
x_73 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_73, 0, x_71);
lean_ctor_set(x_73, 1, x_72);
return x_73;
x_77 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_77, 0, x_75);
lean_ctor_set(x_77, 1, x_76);
return x_77;
}
default:
{
lean_object* x_74; lean_object* x_75; lean_object* x_76;
lean_object* x_78; lean_object* x_79; lean_object* x_80;
lean_dec(x_6);
lean_dec(x_1);
lean_inc(x_2);
x_74 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_74, 0, x_2);
lean_ctor_set(x_74, 1, x_3);
lean_ctor_set(x_74, 2, x_4);
lean_ctor_set(x_74, 3, x_5);
x_75 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
x_78 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_78, 0, x_2);
lean_ctor_set(x_78, 1, x_3);
lean_ctor_set(x_78, 2, x_4);
lean_ctor_set(x_78, 3, x_5);
x_79 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
lean_dec(x_2);
x_76 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_76, 0, x_74);
lean_ctor_set(x_76, 1, x_75);
return x_76;
x_80 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_80, 0, x_78);
lean_ctor_set(x_80, 1, x_79);
return x_80;
}
}
}
@ -5793,88 +5827,103 @@ uint8_t x_169;
x_169 = lean_ctor_get_uint8(x_165, 2);
if (x_169 == 0)
{
uint8_t x_170; lean_object* x_171; uint8_t x_172; lean_object* x_173; lean_object* x_174; lean_object* x_175;
x_170 = lean_ctor_get_uint8(x_165, 1);
lean_dec(x_165);
x_171 = lean_unsigned_to_nat(1u);
x_172 = 1;
lean_object* x_170; uint8_t x_171;
lean_inc(x_164);
x_173 = lean_alloc_ctor(6, 3, 2);
lean_ctor_set(x_173, 0, x_164);
lean_ctor_set(x_173, 1, x_171);
lean_ctor_set(x_173, 2, x_1);
lean_ctor_set_uint8(x_173, sizeof(void*)*3, x_172);
lean_ctor_set_uint8(x_173, sizeof(void*)*3 + 1, x_170);
x_174 = l_Lean_IR_mkLiveVarSet(x_164);
x_175 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_175, 0, x_173);
lean_ctor_set(x_175, 1, x_174);
return x_175;
x_170 = l_Lean_IR_mkLiveVarSet(x_164);
x_171 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_processVDecl___closed__1;
if (x_171 == 0)
{
uint8_t x_172; lean_object* x_173; uint8_t x_174; lean_object* x_175; lean_object* x_176;
x_172 = lean_ctor_get_uint8(x_165, 1);
lean_dec(x_165);
x_173 = lean_unsigned_to_nat(1u);
x_174 = 1;
x_175 = lean_alloc_ctor(6, 3, 2);
lean_ctor_set(x_175, 0, x_164);
lean_ctor_set(x_175, 1, x_173);
lean_ctor_set(x_175, 2, x_1);
lean_ctor_set_uint8(x_175, sizeof(void*)*3, x_174);
lean_ctor_set_uint8(x_175, sizeof(void*)*3 + 1, x_172);
x_176 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_176, 0, x_175);
lean_ctor_set(x_176, 1, x_170);
return x_176;
}
else
{
lean_object* x_176; lean_object* x_177;
lean_object* x_177;
lean_dec(x_165);
x_176 = l_Lean_IR_mkLiveVarSet(x_164);
lean_dec(x_164);
x_177 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_177, 0, x_1);
lean_ctor_set(x_177, 1, x_176);
lean_ctor_set(x_177, 1, x_170);
return x_177;
}
}
}
else
{
lean_object* x_178; lean_object* x_179;
lean_dec(x_2);
x_178 = lean_box(0);
lean_dec(x_165);
x_178 = l_Lean_IR_mkLiveVarSet(x_164);
x_179 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_179, 0, x_1);
lean_ctor_set(x_179, 1, x_178);
return x_179;
}
}
}
else
{
lean_object* x_180; lean_object* x_181;
lean_dec(x_2);
x_180 = lean_box(0);
x_181 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_181, 0, x_1);
lean_ctor_set(x_181, 1, x_180);
return x_181;
}
}
case 12:
{
lean_object* x_180; lean_object* x_181; lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_185; lean_object* x_186; lean_object* x_187; lean_object* x_188;
x_180 = lean_ctor_get(x_1, 0);
lean_inc(x_180);
x_181 = lean_ctor_get(x_1, 1);
lean_inc(x_181);
x_182 = l_Lean_IR_ExplicitRC_getJPLiveVars(x_2, x_180);
lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_185; lean_object* x_186; lean_object* x_187; lean_object* x_188; lean_object* x_189; lean_object* x_190;
x_182 = lean_ctor_get(x_1, 0);
lean_inc(x_182);
x_183 = lean_ctor_get(x_1, 1);
lean_inc(x_183);
x_184 = l_Lean_IR_ExplicitRC_getJPLiveVars(x_2, x_182);
lean_inc(x_2);
x_183 = l_Lean_IR_ExplicitRC_getJPParams(x_2, x_180);
lean_dec(x_180);
x_185 = l_Lean_IR_ExplicitRC_getJPParams(x_2, x_182);
lean_dec(x_182);
lean_inc(x_2);
x_184 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBefore(x_2, x_181, x_183, x_1, x_182);
lean_dec(x_181);
x_185 = lean_ctor_get(x_2, 3);
lean_inc(x_185);
x_186 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBefore(x_2, x_183, x_185, x_1, x_184);
lean_dec(x_183);
x_187 = lean_ctor_get(x_2, 3);
lean_inc(x_187);
lean_dec(x_2);
x_186 = lean_box(0);
lean_inc(x_184);
x_187 = l_Lean_IR_LiveVars_collectFnBody(x_184, x_185, x_186);
x_188 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_188, 0, x_184);
lean_ctor_set(x_188, 1, x_187);
return x_188;
x_188 = lean_box(0);
lean_inc(x_186);
x_189 = l_Lean_IR_LiveVars_collectFnBody(x_186, x_187, x_188);
x_190 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_190, 0, x_186);
lean_ctor_set(x_190, 1, x_189);
return x_190;
}
case 13:
{
lean_object* x_189;
lean_object* x_191;
lean_dec(x_2);
x_189 = l_Lean_IR_ExplicitRC_visitFnBody___closed__1;
return x_189;
x_191 = l_Lean_IR_ExplicitRC_visitFnBody___closed__1;
return x_191;
}
default:
{
lean_object* x_190; lean_object* x_191;
lean_object* x_192; lean_object* x_193;
lean_dec(x_2);
x_190 = lean_box(0);
x_191 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_191, 0, x_1);
lean_ctor_set(x_191, 1, x_190);
return x_191;
x_192 = lean_box(0);
x_193 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_193, 0, x_1);
lean_ctor_set(x_193, 1, x_192);
return x_193;
}
}
}
@ -6075,6 +6124,7 @@ l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addDecForAlt___closed__1 =
lean_mark_persistent(l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addDecForAlt___closed__1);
l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeConsumeAll___closed__1 = _init_l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeConsumeAll___closed__1();
lean_mark_persistent(l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeConsumeAll___closed__1);
l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_processVDecl___closed__1 = _init_l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_processVDecl___closed__1();
l_Lean_IR_ExplicitRC_visitFnBody___closed__1 = _init_l_Lean_IR_ExplicitRC_visitFnBody___closed__1();
lean_mark_persistent(l_Lean_IR_ExplicitRC_visitFnBody___closed__1);
return lean_io_result_mk_ok(lean_box(0));

2
stage0/stdlib/Lean/Compiler/IR/ResetReuse.c generated
View file

@ -30,7 +30,6 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_ResetReuse_R___spec
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_ResetReuse_0__Lean_IR_ResetReuse_Dmain___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_Decl_insertResetReuse(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_ResetReuse_0__Lean_IR_ResetReuse_isCtorUsing___boxed(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_IR_LocalContext_addJP(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_ResetReuse_0__Lean_IR_ResetReuse_Dmain(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_IR_FnBody_isTerminal(lean_object*);
@ -56,6 +55,7 @@ LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Compiler_IR_Reset
lean_object* l_Lean_IR_FnBody_hasLiveVar(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_IR_HasIndex_visitFnBody(lean_object*, lean_object*);
lean_object* l_Lean_Name_getPrefix(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_IR_Decl_updateBody_x21(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Compiler_IR_ResetReuse_0__Lean_IR_ResetReuse_Dmain___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_ResetReuse_R(lean_object*, lean_object*, lean_object*);

124
stage0/stdlib/Lean/Compiler/IR/SimpCase.c generated
View file

@ -14,6 +14,7 @@
extern "C" {
#endif
size_t lean_usize_add(size_t, size_t);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_filterUnreachable(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_mkSimpCase___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_addDefault___boxed(lean_object*);
@ -23,17 +24,17 @@ lean_object* lean_array_uget(lean_object*, size_t);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_getOccsOf___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_addDefault___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_filterUnreachable___boxed(lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_filterUnreachable___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_usize_dec_lt(size_t, size_t);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_mkSimpCase___spec__1(lean_object*, size_t, size_t, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_maxOccs___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_AltCore_body(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_getOccsOf___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_mkSimpCase___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_FnBody_simpCase___spec__2(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_maxOccs(lean_object*);
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_IR_ensureHasDefault___spec__1(lean_object*, size_t, size_t);
@ -49,12 +50,14 @@ LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_mkSimp
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_FnBody_simpCase___spec__2___boxed(lean_object*, lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_ensureHasDefault(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_filterUnreachable___spec__1(lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_FnBody_simpCase(lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_Decl_simpCase(lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_IR_FnBody_flatten(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_addDefault(lean_object*);
lean_object* l_Lean_IR_reshape(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_FnBody_simpCase___spec__1(size_t, size_t, lean_object*);
lean_object* l_Lean_IR_Decl_updateBody_x21(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_getOccsOf___boxed(lean_object*, lean_object*);
@ -657,7 +660,7 @@ lean_dec(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_mkSimpCase___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_filterUnreachable___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
@ -692,48 +695,71 @@ return x_4;
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_filterUnreachable(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = lean_array_get_size(x_1);
x_3 = lean_unsigned_to_nat(0u);
x_4 = lean_nat_dec_lt(x_3, x_2);
if (x_4 == 0)
{
lean_object* x_5;
lean_dec(x_2);
x_5 = l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_addDefault___closed__1;
return x_5;
}
else
{
uint8_t x_6;
x_6 = lean_nat_dec_le(x_2, x_2);
if (x_6 == 0)
{
lean_object* x_7;
lean_dec(x_2);
x_7 = l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_addDefault___closed__1;
return x_7;
}
else
{
size_t x_8; size_t x_9; lean_object* x_10; lean_object* x_11;
x_8 = 0;
x_9 = lean_usize_of_nat(x_2);
lean_dec(x_2);
x_10 = l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_addDefault___closed__1;
x_11 = l_Array_foldlMUnsafe_fold___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_filterUnreachable___spec__1(x_1, x_8, x_9, x_10);
return x_11;
}
}
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_filterUnreachable___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7;
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = lean_unbox_usize(x_3);
lean_dec(x_3);
x_7 = l_Array_foldlMUnsafe_fold___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_filterUnreachable___spec__1(x_1, x_5, x_6, x_4);
lean_dec(x_1);
return x_7;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_filterUnreachable___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_filterUnreachable(x_1);
lean_dec(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_mkSimpCase(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_18; lean_object* x_19; uint8_t x_20;
x_18 = lean_array_get_size(x_4);
x_19 = lean_unsigned_to_nat(0u);
x_20 = lean_nat_dec_lt(x_19, x_18);
if (x_20 == 0)
{
lean_object* x_21;
lean_dec(x_18);
x_21 = l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_addDefault___closed__1;
x_5 = x_21;
goto block_17;
}
else
{
uint8_t x_22;
x_22 = lean_nat_dec_le(x_18, x_18);
if (x_22 == 0)
{
lean_object* x_23;
lean_dec(x_18);
x_23 = l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_addDefault___closed__1;
x_5 = x_23;
goto block_17;
}
else
{
size_t x_24; size_t x_25; lean_object* x_26; lean_object* x_27;
x_24 = 0;
x_25 = lean_usize_of_nat(x_18);
lean_dec(x_18);
x_26 = l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_addDefault___closed__1;
x_27 = l_Array_foldlMUnsafe_fold___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_mkSimpCase___spec__1(x_4, x_24, x_25, x_26);
x_5 = x_27;
goto block_17;
}
}
block_17:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9;
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_5 = l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_filterUnreachable(x_4);
x_6 = l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_addDefault(x_5);
lean_dec(x_5);
x_7 = lean_array_get_size(x_6);
@ -782,20 +808,6 @@ return x_16;
}
}
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_mkSimpCase___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7;
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = lean_unbox_usize(x_3);
lean_dec(x_3);
x_7 = l_Array_foldlMUnsafe_fold___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_mkSimpCase___spec__1(x_1, x_5, x_6, x_4);
lean_dec(x_1);
return x_7;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_mkSimpCase___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{

2
stage0/stdlib/Lean/Compiler/InlineAttrs.c generated
View file

@ -45,7 +45,6 @@ uint8_t lean_is_eager_lambda_lifting_name(lean_object*);
static lean_object* l_Lean_Compiler_initFn____x40_Lean_Compiler_InlineAttrs___hyg_30____closed__22;
LEAN_EXPORT lean_object* l_Lean_Compiler_inlineAttrs;
LEAN_EXPORT lean_object* l_Lean_Compiler_InlineAttributeKind_noConfusion___rarg___lambda__1___boxed(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_initFn____x40_Lean_Compiler_InlineAttrs___hyg_30____closed__25;
LEAN_EXPORT lean_object* l_Lean_Compiler_hasInlineAttribute___boxed(lean_object*, lean_object*);
uint8_t l_Lean_Name_isInternal(lean_object*);
@ -68,6 +67,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_setInlineAttribute___boxed(lean_object*
static lean_object* l_Lean_Compiler_initFn____x40_Lean_Compiler_InlineAttrs___hyg_30____closed__11;
static lean_object* l_Lean_Compiler_initFn____x40_Lean_Compiler_InlineAttrs___hyg_30____closed__19;
lean_object* l_Lean_Name_getPrefix(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT uint8_t lean_has_inline_if_reduce_attribute(lean_object*, lean_object*);
lean_object* l_Lean_EnumAttributes_getValue___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_initFn____x40_Lean_Compiler_InlineAttrs___hyg_30____closed__26;

2
stage0/stdlib/Lean/Compiler/Specialize.c generated
View file

@ -73,7 +73,6 @@ lean_object* lean_array_fget(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashMapImp_moveEntries___at_Lean_Compiler_SpecState_addEntry___spec__20(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_specExtension;
LEAN_EXPORT lean_object* l_Std_HashMapImp_expand___at_Lean_Compiler_SpecState_addEntry___spec__19(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Compiler_getCachedSpecialization___spec__2(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_initFn____x40_Lean_Compiler_Specialize___hyg_30____closed__2;
LEAN_EXPORT uint8_t l_Lean_Compiler_instInhabitedSpecializeAttributeKind;
@ -151,6 +150,7 @@ lean_object* lean_nat_mul(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_initFn____x40_Lean_Compiler_Specialize___hyg_30____lambda__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_getPrefix(lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAux___at_Lean_Compiler_getCachedSpecialization___spec__3(lean_object*, size_t, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAux___at_Lean_Compiler_getSpecializationInfo___spec__3___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_initFn____x40_Lean_Compiler_Specialize___hyg_30____closed__13;
LEAN_EXPORT lean_object* lean_get_cached_specialization(lean_object*, lean_object*);

2
stage0/stdlib/Lean/CoreM.c generated
View file

@ -89,7 +89,6 @@ static lean_object* l_Lean_Core_instMonadCoreM___closed__1;
LEAN_EXPORT lean_object* l___private_Lean_CoreM_0__Lean_Core_mkFreshNameImp(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Core_instMonadResolveNameCoreM___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Core_State_traceState___default___closed__4;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Core_instInhabitedCoreM___rarg(lean_object*);
static lean_object* l_Lean_Core_State_traceState___default___closed__3;
lean_object* l_Lean_MessageData_toString(lean_object*, lean_object*);
@ -202,6 +201,7 @@ LEAN_EXPORT lean_object* l_Lean_Core_CoreM_toIO(lean_object*);
lean_object* lean_nat_mul(lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Core_instMonadNameGeneratorCoreM___lambda__1(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Core_instInhabitedState___closed__9;
lean_object* l_IO_println___at_Lean_instEval__1___spec__1(lean_object*, lean_object*);
static lean_object* l_Lean_Core_instInhabitedState___closed__4;

1
stage0/stdlib/Lean/Data/Json/Basic.c generated
View file

@ -143,6 +143,7 @@ lean_object* lean_nat_mul(lean_object*, lean_object*);
lean_object* lean_nat_abs(lean_object*);
LEAN_EXPORT uint8_t l_Lean_JsonNumber_lt(lean_object*, lean_object*);
lean_object* lean_int_div(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_JsonNumber_toString___closed__4;
static lean_object* l_Lean_Json_getObjVal_x3f___closed__1;
LEAN_EXPORT lean_object* l_Lean_JsonNumber_instOrdJsonNumber___boxed(lean_object*, lean_object*);

1
stage0/stdlib/Lean/Data/Json/FromToJson.c generated
View file

@ -112,6 +112,7 @@ lean_object* l_Lean_Json_getBool_x3f___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_instToJsonJsonNumber(lean_object*);
LEAN_EXPORT lean_object* l_Lean_instFromJsonUSize___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Json_pretty(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
extern lean_object* l_USize_size;
LEAN_EXPORT lean_object* l_Lean_instFromJsonArray(lean_object*);
lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*);

1
stage0/stdlib/Lean/Data/JsonRpc.c generated
View file

@ -172,6 +172,7 @@ static lean_object* l_Lean_JsonRpc_instToJsonMessage___closed__8;
lean_object* l_Lean_Json_pretty(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_JsonRpc_instInhabitedRequest___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Lean_JsonRpc_instFromJsonNotification(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_JsonRpc_instFromJsonMessage(lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_writeNotification(lean_object*);
static lean_object* l_IO_FS_Stream_readRequestAs___closed__1;

2
stage0/stdlib/Lean/Data/KVMap.c generated
View file

@ -92,7 +92,6 @@ LEAN_EXPORT lean_object* l_Lean_KVMap_getSyntax___boxed(lean_object*, lean_objec
static lean_object* l_Lean_KVMap_instValueNat___closed__3;
static lean_object* l_Lean_instInhabitedDataValue___closed__2;
static lean_object* l_Lean_instReprDataValue___closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_KVMap_instValueString___closed__3;
LEAN_EXPORT lean_object* l_Lean_KVMap_getBool___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_instCoeNameDataValue(lean_object*);
@ -205,6 +204,7 @@ lean_object* lean_nat_abs(lean_object*);
static lean_object* l___private_Lean_Data_KVMap_0__Lean_reprDataValue____x40_Lean_Data_KVMap___hyg_255____closed__16;
LEAN_EXPORT lean_object* l_Lean_KVMap_instValueSyntax;
LEAN_EXPORT lean_object* l_Lean_KVMap_instValueName___lambda__1(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_KVMap_instValueInt___closed__1;
LEAN_EXPORT uint8_t lean_data_value_beq(lean_object*, lean_object*);
static lean_object* l___private_Lean_Data_KVMap_0__Lean_reprKVMap____x40_Lean_Data_KVMap___hyg_844____closed__9;

2
stage0/stdlib/Lean/Data/LBool.c generated
View file

@ -24,7 +24,6 @@ LEAN_EXPORT lean_object* l_Lean_LBool_toString___boxed(lean_object*);
static lean_object* l_Lean_LBool_toString___closed__2;
LEAN_EXPORT lean_object* l_toLBoolM(lean_object*);
LEAN_EXPORT lean_object* l_Lean_LBool_noConfusion___rarg___lambda__1___boxed(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_LBool_noConfusion___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_LBool_and(uint8_t, uint8_t);
static lean_object* l_Lean_LBool_toString___closed__3;
@ -40,6 +39,7 @@ LEAN_EXPORT lean_object* l_Lean_instBEqLBool;
LEAN_EXPORT uint8_t l_Lean_LBool_neg(uint8_t);
LEAN_EXPORT uint8_t l_Bool_toLBool(uint8_t);
static lean_object* l_Lean_LBool_toString___closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Data_LBool_0__Lean_beqLBool____x40_Lean_Data_LBool___hyg_13____boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_LBool_noConfusion___rarg(uint8_t, uint8_t, lean_object*);
LEAN_EXPORT lean_object* l_toLBoolM___rarg(lean_object*, lean_object*);

1
stage0/stdlib/Lean/Data/Lsp/Basic.c generated
View file

@ -256,6 +256,7 @@ static lean_object* l_Lean_Lsp_instToJsonVersionedTextDocumentIdentifier___close
static lean_object* l_Lean_Lsp_instFromJsonCancelParams___closed__1;
LEAN_EXPORT lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_923____spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Json_pretty(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonDocumentFilter____x40_Lean_Data_Lsp_Basic___hyg_2051_(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonCommand____x40_Lean_Data_Lsp_Basic___hyg_1228____spec__2___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonVersionedTextDocumentIdentifier____x40_Lean_Data_Lsp_Basic___hyg_1561____boxed(lean_object*);

1
stage0/stdlib/Lean/Data/Lsp/Diagnostics.c generated
View file

@ -172,6 +172,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Data_Lsp_Diagnostics_0__Lean_Lsp_beqDi
LEAN_EXPORT lean_object* l_Lean_Lsp_instInhabitedDiagnosticWith(lean_object*);
lean_object* l_Lean_Json_pretty(lean_object*, lean_object*);
static lean_object* l___private_Lean_Data_Lsp_Diagnostics_0__Lean_Lsp_toJsonDiagnosticWith____x40_Lean_Data_Lsp_Diagnostics___hyg_918____rarg___closed__5;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Diagnostics_0__Lean_Lsp_toJsonDiagnosticWith____x40_Lean_Data_Lsp_Diagnostics___hyg_918____spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Lsp_instToJsonDiagnosticWith___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Lsp_DiagnosticWith_source_x3f___default;

1
stage0/stdlib/Lean/Data/Lsp/Extra.c generated
View file

@ -215,6 +215,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_Ext
LEAN_EXPORT lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcCallParams____x40_Lean_Data_Lsp_Extra___hyg_1252____spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Json_pretty(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Lsp_instToJsonLeanFileProgressProcessingInfo;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
extern lean_object* l_USize_size;
LEAN_EXPORT lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonRpcKeepAliveParams____x40_Lean_Data_Lsp_Extra___hyg_1647_(lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonRange____x40_Lean_Data_Lsp_Basic___hyg_651____spec__1(lean_object*, lean_object*);

1
stage0/stdlib/Lean/Data/Name.c generated
View file

@ -168,6 +168,7 @@ LEAN_EXPORT lean_object* l_Std_HashMapImp_expand___at_Lean_NameSSet_insert___spe
LEAN_EXPORT lean_object* l_Std_RBNode_find___at_Lean_NameMap_contains___spec__1___rarg(lean_object*, lean_object*);
lean_object* lean_nat_mul(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Name_getPrefix(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_RBNode_ins___at_Lean_NameMap_insert___spec__3___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_RBNode_ins___at_Lean_NameMap_insert___spec__3(lean_object*);

2
stage0/stdlib/Lean/Data/Occurrences.c generated
View file

@ -16,7 +16,6 @@ extern "C" {
static lean_object* l_Lean_instBEqOccurrences___closed__1;
LEAN_EXPORT lean_object* l_Lean_Occurrences_contains___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_elem___at_Lean_Occurrences_contains___spec__1___boxed(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_instBEqOccurrences;
LEAN_EXPORT uint8_t l_Lean_Occurrences_contains(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_instInhabitedOccurrences;
@ -25,6 +24,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Data_Occurrences_0__Lean_beqOccurrence
LEAN_EXPORT uint8_t l___private_Lean_Data_Occurrences_0__Lean_beqOccurrences____x40_Lean_Data_Occurrences___hyg_32_(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_List_beq___at___private_Lean_Data_Occurrences_0__Lean_beqOccurrences____x40_Lean_Data_Occurrences___hyg_32____spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_beq___at___private_Lean_Data_Occurrences_0__Lean_beqOccurrences____x40_Lean_Data_Occurrences___hyg_32____spec__1___boxed(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Occurrences_isAll___boxed(lean_object*);
LEAN_EXPORT uint8_t l_Lean_Occurrences_isAll(lean_object*);
static lean_object* _init_l_Lean_instInhabitedOccurrences() {

1
stage0/stdlib/Lean/Data/Position.c generated
View file

@ -82,6 +82,7 @@ static lean_object* l_Lean_instInhabitedFileMap___closed__3;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_instDecidableEqPosition___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_instInhabitedFileMap___closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Position_instToExprPosition___lambda__1___closed__8;
LEAN_EXPORT lean_object* l_Lean_Position_instToExprPosition___lambda__1(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Position_instToFormatPosition(lean_object*);

1
stage0/stdlib/Lean/Data/Rat.c generated
View file

@ -74,6 +74,7 @@ LEAN_EXPORT lean_object* l_Lean_Rat_neg(lean_object*);
lean_object* lean_nat_mul(lean_object*, lean_object*);
lean_object* lean_nat_abs(lean_object*);
lean_object* lean_int_div(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_mkRat___closed__1;
LEAN_EXPORT lean_object* l_Lean_Rat_instCoeIntRat(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Rat_instLERat;

2
stage0/stdlib/Lean/Declaration.c generated
View file

@ -77,7 +77,6 @@ LEAN_EXPORT lean_object* l_Lean_RecursorVal_getMajorIdx(lean_object*);
LEAN_EXPORT lean_object* l_Lean_ConstantInfo_instantiateTypeLevelParams___boxed(lean_object*, lean_object*);
static lean_object* l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_269____closed__7;
LEAN_EXPORT lean_object* l_Lean_instInhabitedAxiomVal;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_foldlM___at_Lean_Declaration_forExprM___spec__3___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_instInhabitedConstructorVal;
LEAN_EXPORT lean_object* l_List_foldlM___at_Lean_Declaration_forExprM___spec__4(lean_object*);
@ -170,6 +169,7 @@ static lean_object* l___private_Lean_Declaration_0__Lean_reprDefinitionSafety___
LEAN_EXPORT uint8_t lean_quot_val_kind(lean_object*);
lean_object* l_Lean_Name_getPrefix(lean_object*);
LEAN_EXPORT lean_object* l_List_foldlM___at_Lean_Declaration_forExprM___spec__4___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_instInhabitedQuotVal;
LEAN_EXPORT lean_object* l_Lean_mkInductiveDeclEs___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_269____closed__1;

1
stage0/stdlib/Lean/Elab/App.c generated
View file

@ -618,6 +618,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs
static lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_mkProjAndCheck___closed__7;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_App___hyg_12092_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_App___hyg_5_(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppAux(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_propagateExpectedTypeFor___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_mkProjAndCheck___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Elab/Binders.c generated
View file

@ -539,6 +539,7 @@ lean_object* l_Lean_Elab_Term_elabType(lean_object*, lean_object*, lean_object*,
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__41;
static lean_object* l___regBuiltin_Lean_Elab_Term_elabLetFunDecl_declRange___closed__2;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabLetDeclCore___closed__4;
static lean_object* l___regBuiltin_Lean_Elab_Term_expandFun___closed__3;
lean_object* l_Lean_mkForall(lean_object*, uint8_t, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Elab/BuiltinCommand.c generated
View file

@ -598,6 +598,7 @@ static lean_object* l_Lean_resolveGlobalConstNoOverloadCore___at_Lean_Elab_Comma
lean_object* l_Lean_Elab_Command_getRef(lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Command_elabNonComputableSection_declRange___closed__1;
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_elabNamespace___closed__2;
static lean_object* l_Lean_Elab_Command_elabCheckCore___lambda__1___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Command_elabEval_declRange___closed__5;

1
stage0/stdlib/Lean/Elab/BuiltinNotation.c generated
View file

@ -609,6 +609,7 @@ lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getRefPos___at___private_Lean_Elab_App_0__Lean_Elab_Term_toMessageData___spec__1___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabSubst___lambda__6(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*);
uint8_t l_Lean_Expr_isFVar(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_expandHave___closed__5;
static lean_object* l_Lean_Elab_Term_elabAnonymousCtor___lambda__3___closed__11;
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

2
stage0/stdlib/Lean/Elab/Command.c generated
View file

@ -248,7 +248,6 @@ LEAN_EXPORT lean_object* l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_li
lean_object* l_Lean_MapDeclarationExtension_insert___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_State_nextMacroScope___default___closed__1;
static lean_object* l_Lean_addMessageContextPartial___at_Lean_Elab_Command_instAddMessageContextCommandElabM___spec__1___closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static size_t l_Lean_Elab_Command_instInhabitedState___closed__8;
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_2155____closed__1;
LEAN_EXPORT lean_object* l_Lean_addDocString___at_Lean_Elab_Command_expandDeclId___spec__11___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -534,6 +533,7 @@ static lean_object* l_Lean_addTrace___at_Lean_Elab_Command_elabCommand___spec__4
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_instMonadResolveNameCommandElabM___lambda__2(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_State_ngen___default___closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentArray_forIn___at_Lean_Elab_Command_elabCommandTopLevel___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_liftCoreM(lean_object*);
uint8_t l_Lean_Syntax_isNone(lean_object*);

2
stage0/stdlib/Lean/Elab/Declaration.c generated
View file

@ -186,7 +186,6 @@ static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_expandMutual
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_MapDeclarationExtension_insert___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_expandInitCmd___lambda__1___closed__26;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_elabDeclaration___closed__10;
static lean_object* l___regBuiltin_Lean_Elab_Command_elabDeclaration___closed__5;
uint8_t l_Lean_isExtern(lean_object*, lean_object*);
@ -415,6 +414,7 @@ lean_object* l_Lean_Elab_expandDeclSig(lean_object*);
lean_object* l_Lean_Elab_Term_elabType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_expandInitCmd___lambda__1___closed__33;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__1___closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_isMutualDef___boxed(lean_object*);

2
stage0/stdlib/Lean/Elab/DefView.c generated
View file

@ -80,7 +80,6 @@ static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__16;
static lean_object* l_Lean_Elab_instBEqDefKind___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_mkInstanceName___spec__5(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_mkDefViewOfAbbrev___closed__3;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_expandMacroImpl_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkDefViewOfConstant___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
@ -178,6 +177,7 @@ lean_object* l_Lean_Elab_Command_getRef(lean_object*, lean_object*, lean_object*
lean_object* l_Lean_Elab_expandDeclSig(lean_object*);
lean_object* l_Lean_Elab_Term_elabType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__2;
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Command_mkDefView___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNone(lean_object*);

1
stage0/stdlib/Lean/Elab/Deriving/BEq.c generated
View file

@ -202,6 +202,7 @@ static lean_object* l___private_Lean_Elab_Deriving_BEq_0__Lean_Elab_Deriving_BEq
static lean_object* l___private_Lean_Elab_Deriving_BEq_0__Lean_Elab_Deriving_BEq_mkBEqEnumFun___closed__1;
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_BEq_mkMatch_mkElseAlt___spec__1___closed__7;
static lean_object* l___private_Lean_Elab_Deriving_BEq_0__Lean_Elab_Deriving_BEq_mkBEqEnumFun___closed__8;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_getConstInfoCtor___at_Lean_Elab_Deriving_BEq_mkMatch_mkAlts___spec__1___closed__2;
static lean_object* l_Lean_Elab_Deriving_BEq_mkMutualBlock___closed__1;
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Elab/Deriving/Basic.c generated
View file

@ -177,6 +177,7 @@ static lean_object* l___regBuiltin_Lean_Elab_elabDeriving_declRange___closed__6;
static lean_object* l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_elabDeriving___spec__16___closed__1;
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_elabDeriving___lambda__2(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedName;
LEAN_EXPORT lean_object* l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_elabDeriving___spec__16___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNone(lean_object*);

1
stage0/stdlib/Lean/Elab/Deriving/DecEq.c generated
View file

@ -309,6 +309,7 @@ lean_object* l_Lean_Elab_Command_getRef(lean_object*, lean_object*, lean_object*
static lean_object* l_Lean_Elab_Deriving_DecEq_mkMatch_mkSameCtorRhs___lambda__1___closed__28;
static lean_object* l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__2;
LEAN_EXPORT lean_object* l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__27;
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedName;

1
stage0/stdlib/Lean/Elab/Deriving/FromToJson.c generated
View file

@ -336,6 +336,7 @@ static lean_object* l_Array_mapIdxM_map___at_Lean_Elab_Deriving_FromToJson_mkToJ
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler_mkAlts___spec__3___closed__3;
LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler_mkAlts___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_qsort_sort___at_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler_mkAlts___spec__7___closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Array_mapIdxM_map___at_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler_mkAlts___spec__3___closed__1;
static lean_object* l_Array_mapIdxM_map___at_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___spec__4___closed__5;
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Elab/Deriving/Repr.c generated
View file

@ -234,6 +234,7 @@ LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Repr_mkM
static lean_object* l_Lean_Elab_Deriving_Repr_mkAuxFunction___lambda__1___closed__7;
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Repr_mkBodyForInduct_mkAlts___spec__2___closed__7;
LEAN_EXPORT lean_object* l_Lean_Elab_Deriving_Repr_mkReprHeader___boxed(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Deriving_Repr_mkBodyForStruct___rarg___lambda__1___closed__2;
extern lean_object* l_Lean_instInhabitedName;

1
stage0/stdlib/Lean/Elab/Do.c generated
View file

@ -1065,6 +1065,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_attachJP___boxed(lean_object*, lean
static lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkMonadAlias___closed__3;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_letDeclHasBinders___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_mkAuxDeclFor___at_Lean_Elab_Term_Do_pullExitPointsAux___spec__1___lambda__1(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_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__4;
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

2
stage0/stdlib/Lean/Elab/Exception.c generated
View file

@ -42,7 +42,6 @@ static lean_object* l_Lean_Elab_throwAbortCommand___rarg___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_throwAutoBoundImplicitLocal___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_mkMessageCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_throwAutoBoundImplicitLocal(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortTerm___rarg(lean_object*);
static lean_object* l_Lean_Elab_throwAutoBoundImplicitLocal___rarg___closed__3;
LEAN_EXPORT lean_object* l_Lean_Elab_mkMessageCore(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
@ -81,6 +80,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_throwIllFormedSyntax(lean_object*, lean_obj
static lean_object* l_Lean_Elab_throwAlreadyDeclaredUniverseLevel___rarg___closed__2;
lean_object* l_Lean_throwError___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_throwAlreadyDeclaredUniverseLevel___rarg___closed__4;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Exception___hyg_4____closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_unsupportedSyntaxExceptionId;
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Exception___hyg_18____closed__1;

246
stage0/stdlib/Lean/Elab/Inductive.c generated
View file

@ -408,6 +408,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_el
static lean_object* l_Lean_Elab_Command_instInhabitedElabHeaderResult___closed__9;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_eqvFirstTypeResult___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_mapM___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors___spec__1___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*);
static uint8_t l_Lean_Elab_Command_accLevelAtCtor___closed__3;
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4092_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_5_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_mkIBelow___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkAuxConstructions___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -450,6 +451,7 @@ lean_object* l_Lean_Elab_Term_elabType(lean_object*, lean_object*, lean_object*,
LEAN_EXPORT lean_object* l_Lean_Elab_Command_elabInductiveViews___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isFVar(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_instInhabitedElabHeaderResult___closed__1;
LEAN_EXPORT lean_object* l_Std_PersistentArray_mapMAux___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkInductiveDecl___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -7030,6 +7032,15 @@ x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static uint8_t _init_l_Lean_Elab_Command_accLevelAtCtor___closed__3() {
_start:
{
lean_object* x_1; uint8_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_nat_dec_eq(x_1, x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Command_accLevelAtCtor(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
@ -7071,7 +7082,7 @@ else
uint8_t x_32;
lean_dec(x_26);
lean_dec(x_3);
x_32 = lean_level_eq(x_1, x_2);
x_32 = l_Lean_Elab_Command_accLevelAtCtor___closed__3;
if (x_32 == 0)
{
uint8_t x_33;
@ -7115,72 +7126,69 @@ return x_39;
}
else
{
lean_object* x_40;
uint8_t x_40;
x_40 = lean_level_eq(x_1, x_2);
if (x_40 == 0)
{
uint8_t x_41;
x_41 = l_Lean_Level_occurs(x_2, x_1);
lean_dec(x_2);
if (x_41 == 0)
{
uint8_t x_42;
lean_dec(x_8);
lean_dec(x_5);
x_42 = l_Array_contains___at_Lean_Elab_Command_accLevelAtCtor___spec__1(x_4, x_1);
if (x_42 == 0)
{
lean_object* x_43; lean_object* x_44;
x_43 = lean_array_push(x_4, x_1);
x_44 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_44, 0, x_43);
lean_ctor_set(x_44, 1, x_11);
return x_44;
}
else
{
lean_object* x_45;
lean_dec(x_1);
x_45 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_45, 0, x_4);
lean_ctor_set(x_45, 1, x_11);
return x_45;
}
}
else
{
lean_object* x_46; lean_object* x_47;
lean_dec(x_4);
lean_dec(x_1);
x_46 = l_Lean_Elab_Command_accLevelAtCtor___closed__2;
x_47 = l_Lean_throwError___at_Lean_Elab_Command_accLevelAtCtor___spec__3(x_46, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
lean_dec(x_8);
return x_47;
}
}
else
{
lean_object* x_48;
lean_dec(x_8);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_40 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_40, 0, x_4);
lean_ctor_set(x_40, 1, x_11);
return x_40;
x_48 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_48, 0, x_4);
lean_ctor_set(x_48, 1, x_11);
return x_48;
}
}
}
}
case 4:
{
lean_object* x_41; uint8_t x_42;
x_41 = lean_unsigned_to_nat(0u);
x_42 = lean_nat_dec_eq(x_3, x_41);
if (x_42 == 0)
{
lean_object* x_43;
x_43 = lean_box(0);
x_12 = x_43;
goto block_24;
}
else
{
uint8_t x_44;
x_44 = lean_level_eq(x_1, x_2);
if (x_44 == 0)
{
lean_object* x_45;
x_45 = lean_box(0);
x_12 = x_45;
goto block_24;
}
else
{
lean_object* x_46;
lean_dec(x_8);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_46 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_46, 0, x_4);
lean_ctor_set(x_46, 1, x_11);
return x_46;
}
}
}
case 5:
{
lean_object* x_47; uint8_t x_48;
x_47 = lean_unsigned_to_nat(0u);
x_48 = lean_nat_dec_eq(x_3, x_47);
if (x_48 == 0)
{
lean_object* x_49;
x_49 = lean_box(0);
x_12 = x_49;
goto block_24;
}
else
{
uint8_t x_50;
x_50 = lean_level_eq(x_1, x_2);
lean_object* x_49; uint8_t x_50;
x_49 = lean_unsigned_to_nat(0u);
x_50 = lean_nat_dec_eq(x_3, x_49);
if (x_50 == 0)
{
lean_object* x_51;
@ -7190,70 +7198,119 @@ goto block_24;
}
else
{
lean_object* x_52;
uint8_t x_52;
x_52 = lean_level_eq(x_1, x_2);
if (x_52 == 0)
{
lean_object* x_53;
x_53 = lean_box(0);
x_12 = x_53;
goto block_24;
}
else
{
lean_object* x_54;
lean_dec(x_8);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_52 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_52, 0, x_4);
lean_ctor_set(x_52, 1, x_11);
return x_52;
x_54 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_54, 0, x_4);
lean_ctor_set(x_54, 1, x_11);
return x_54;
}
}
}
case 5:
{
lean_object* x_55; uint8_t x_56;
x_55 = lean_unsigned_to_nat(0u);
x_56 = lean_nat_dec_eq(x_3, x_55);
if (x_56 == 0)
{
lean_object* x_57;
x_57 = lean_box(0);
x_12 = x_57;
goto block_24;
}
else
{
uint8_t x_58;
x_58 = lean_level_eq(x_1, x_2);
if (x_58 == 0)
{
lean_object* x_59;
x_59 = lean_box(0);
x_12 = x_59;
goto block_24;
}
else
{
lean_object* x_60;
lean_dec(x_8);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_60 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_60, 0, x_4);
lean_ctor_set(x_60, 1, x_11);
return x_60;
}
}
}
default:
{
lean_object* x_53; lean_object* x_54; lean_object* x_55;
x_53 = lean_ctor_get(x_1, 0);
lean_inc(x_53);
x_54 = lean_ctor_get(x_1, 1);
lean_inc(x_54);
lean_object* x_61; lean_object* x_62; lean_object* x_63;
x_61 = lean_ctor_get(x_1, 0);
lean_inc(x_61);
x_62 = lean_ctor_get(x_1, 1);
lean_inc(x_62);
lean_dec(x_1);
lean_inc(x_8);
lean_inc(x_5);
lean_inc(x_3);
lean_inc(x_2);
x_55 = l_Lean_Elab_Command_accLevelAtCtor(x_53, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
if (lean_obj_tag(x_55) == 0)
x_63 = l_Lean_Elab_Command_accLevelAtCtor(x_61, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
if (lean_obj_tag(x_63) == 0)
{
lean_object* x_56; lean_object* x_57;
x_56 = lean_ctor_get(x_55, 0);
lean_inc(x_56);
x_57 = lean_ctor_get(x_55, 1);
lean_inc(x_57);
lean_dec(x_55);
x_1 = x_54;
x_4 = x_56;
x_11 = x_57;
lean_object* x_64; lean_object* x_65;
x_64 = lean_ctor_get(x_63, 0);
lean_inc(x_64);
x_65 = lean_ctor_get(x_63, 1);
lean_inc(x_65);
lean_dec(x_63);
x_1 = x_62;
x_4 = x_64;
x_11 = x_65;
goto _start;
}
else
{
uint8_t x_59;
lean_dec(x_54);
uint8_t x_67;
lean_dec(x_62);
lean_dec(x_8);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
x_59 = !lean_is_exclusive(x_55);
if (x_59 == 0)
x_67 = !lean_is_exclusive(x_63);
if (x_67 == 0)
{
return x_55;
return x_63;
}
else
{
lean_object* x_60; lean_object* x_61; lean_object* x_62;
x_60 = lean_ctor_get(x_55, 0);
x_61 = lean_ctor_get(x_55, 1);
lean_inc(x_61);
lean_inc(x_60);
lean_dec(x_55);
x_62 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_62, 0, x_60);
lean_ctor_set(x_62, 1, x_61);
return x_62;
lean_object* x_68; lean_object* x_69; lean_object* x_70;
x_68 = lean_ctor_get(x_63, 0);
x_69 = lean_ctor_get(x_63, 1);
lean_inc(x_69);
lean_inc(x_68);
lean_dec(x_63);
x_70 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_70, 0, x_68);
lean_ctor_set(x_70, 1, x_69);
return x_70;
}
}
}
@ -18373,6 +18430,7 @@ l_Lean_Elab_Command_accLevelAtCtor___closed__1 = _init_l_Lean_Elab_Command_accLe
lean_mark_persistent(l_Lean_Elab_Command_accLevelAtCtor___closed__1);
l_Lean_Elab_Command_accLevelAtCtor___closed__2 = _init_l_Lean_Elab_Command_accLevelAtCtor___closed__2();
lean_mark_persistent(l_Lean_Elab_Command_accLevelAtCtor___closed__2);
l_Lean_Elab_Command_accLevelAtCtor___closed__3 = _init_l_Lean_Elab_Command_accLevelAtCtor___closed__3();
l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___lambda__2___closed__1 = _init_l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___lambda__2___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___lambda__2___closed__1);
l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___lambda__2___closed__2 = _init_l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___lambda__2___closed__2();

2
stage0/stdlib/Lean/Elab/InfoTree.c generated
View file

@ -148,7 +148,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_enableInfoTree___rarg(lean_object*, uint8_t
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_withSaveInfoContext___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
static lean_object* l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__6;
static lean_object* l_Lean_Elab_TacticInfo_format___closed__2;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentArray_findSomeM_x3f___at_Lean_Elab_InfoTree_findInfo_x3f___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_findInfo_x3f(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Elab_resolveGlobalConstWithInfos___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*);
@ -341,6 +340,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_withSaveInfoContext___rarg(lean_object*, le
LEAN_EXPORT lean_object* l_Lean_Elab_instInhabitedContextInfo;
lean_object* l_Lean_Json_pretty(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_withSaveInfoContext___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static size_t l_Lean_Elab_instInhabitedTermInfo___closed__3;
lean_object* l_Lean_ppTerm(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange_fmtPos___closed__9;

2
stage0/stdlib/Lean/Elab/Macro.c generated
View file

@ -57,7 +57,6 @@ static lean_object* l_Lean_Elab_Command_expandMacro___lambda__2___closed__14;
lean_object* l_Array_mapMUnsafe_map___at___aux__Init__NotationExtra______macroRules__term_x25_x5b___x7c___x5d__1___spec__3(size_t, size_t, lean_object*);
static lean_object* l_Lean_Elab_Command_expandMacro___lambda__2___closed__28;
LEAN_EXPORT lean_object* l_Lean_Elab_Command_expandMacro(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
extern lean_object* l_Lean_numLitKind;
static lean_object* l___regBuiltin_Lean_Elab_Command_expandMacro_declRange___closed__1;
static lean_object* l_Lean_Elab_Command_expandMacro___lambda__2___closed__21;
@ -107,6 +106,7 @@ static lean_object* l_Lean_Elab_Command_expandMacro___lambda__2___closed__15;
static lean_object* l_Lean_Elab_Command_expandMacro___lambda__2___closed__18;
LEAN_EXPORT lean_object* l_Lean_Elab_Command_expandMacro___lambda__4(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_Lean_Elab_Command_expandMacro___lambda__2___closed__12;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_expandMacro___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNone(lean_object*);
static lean_object* l_Lean_Elab_Command_expandMacro___lambda__2___closed__11;

1
stage0/stdlib/Lean/Elab/Match.c generated
View file

@ -660,6 +660,7 @@ uint8_t l_Lean_Expr_isFVar(lean_object*);
static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__5___rarg___closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___lambda__3(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_Elab_Match_0__Lean_Elab_Term_elabMatchCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_containsFVar___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkForall(lean_object*, uint8_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_precheckMatch(lean_object*);

1
stage0/stdlib/Lean/Elab/MutualDef.c generated
View file

@ -620,6 +620,7 @@ lean_object* l_Lean_Elab_Term_elabType(lean_object*, lean_object*, lean_object*,
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereStructInst___spec__2___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereStructInst___spec__2___lambda__2___closed__3;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_MutualClosure_getModifiersForLetRecs___boxed(lean_object*);
static lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_isMultiConstant_x3f___spec__3___closed__8;
static lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereStructInst___closed__3;

2
stage0/stdlib/Lean/Elab/PatternVar.c generated
View file

@ -176,7 +176,6 @@ lean_object* lean_array_fget(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_processCtorAppCore___closed__1;
static lean_object* l_Lean_resolveGlobalConst___at___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_doubleQuotedNameToPattern___spec__3___closed__3;
LEAN_EXPORT lean_object* l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_isDone___boxed(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_processCtorApp(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_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Elab_Term_CollectPatternVars_main___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_processExplicitArg___closed__1;
@ -353,6 +352,7 @@ static lean_object* l_Lean_Elab_Term_CollectPatternVars_collect___closed__22;
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_panic___at_Lean_Elab_Term_CollectPatternVars_collect_pushNewArg___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapSepElemsM___at_Lean_Elab_Term_CollectPatternVars_collect___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapSepElemsM___at_Lean_Elab_Term_CollectPatternVars_collect___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_resolveGlobalName___at_Lean_Elab_Term_resolveName___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

2
stage0/stdlib/Lean/Elab/PreDefinition/Main.c generated
View file

@ -137,7 +137,6 @@ lean_object* l_Lean_Elab_mkInhabitantFor(lean_object*, lean_object*, lean_object
lean_object* lean_array_fget(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__1(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortCommand___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_ensureNoUnassignedMVarsAtPreDef___spec__1___rarg(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkSorry(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__26___lambda__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_betaReduceLetRecApps___spec__3___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -297,6 +296,7 @@ lean_object* l_Lean_Elab_WF_TerminationHint_ensureAllUsed(lean_object*, lean_obj
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_collectMVarsAtPreDef___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashMapImp_expand___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__14(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashMapImp_moveEntries___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__15(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_AssocList_replace___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__17(lean_object*, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Elab/PreDefinition/Structural/BRecOn.c generated
View file

@ -245,6 +245,7 @@ static lean_object* l_Lean_Elab_Structural_mkBRecOn___lambda__5___closed__1;
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Structural_mkBRecOn___spec__2(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_Structural_BRecOn_0__Lean_Elab_Structural_replaceRecApps_loop___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_lambdaTelescope___at___private_Lean_Elab_PreDefinition_Structural_BRecOn_0__Lean_Elab_Structural_replaceRecApps_loop___spec__16___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinition_Structural_BRecOn_0__Lean_Elab_Structural_replaceRecApps_loop___spec__17(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Elab/PreDefinition/Structural/FindRecArg.c generated
View file

@ -138,6 +138,7 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDe
LEAN_EXPORT uint8_t l___private_Init_Data_Array_Basic_0__Array_allDiffAuxAux___at_Lean_Elab_Structural_findRecArg_go___spec__7(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isFVar(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Structural_findRecArg_go___rarg___closed__1;

2
stage0/stdlib/Lean/Elab/PreDefinition/Structural/Main.c generated
View file

@ -55,7 +55,6 @@ static lean_object* l___private_Lean_Elab_PreDefinition_Structural_Main_0__Lean_
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*);
lean_object* l_List_mapTRAux___at_Lean_MessageData_instCoeListExprMessageData___spec__1(lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Structural_Main_0__Lean_Elab_Structural_elimRecursion___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
@ -98,6 +97,7 @@ static lean_object* l_Lean_Elab_Structural_structuralRecursion___closed__5;
static lean_object* l___private_Lean_Elab_PreDefinition_Structural_Main_0__Lean_Elab_Structural_elimRecursion___lambda__5___closed__2;
static lean_object* l_Lean_Elab_Structural_structuralRecursion___closed__4;
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Structural_structuralRecursion___closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Structural_Main_0__Lean_Elab_Structural_getFixedPrefix___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Structural_Main_0__Lean_Elab_Structural_elimRecursion___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

2
stage0/stdlib/Lean/Elab/PreDefinition/WF/Fix.c generated
View file

@ -100,7 +100,6 @@ lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean
static lean_object* l___private_Lean_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_processSumCasesOn___closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_replaceRecApps_loop___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkProj(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_replaceRecApps_loop___spec__14___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___private_Lean_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_processSumCasesOn___closed__2;
lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda_loop___spec__1___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -189,6 +188,7 @@ LEAN_EXPORT lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at___private_Lean_El
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_replaceRecApps_loop___spec__14(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_lambdaTelescope___at___private_Lean_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_replaceRecApps_loop___spec__12___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isFVar(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkArrow(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*);
lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Elab/PreDefinition/WF/Main.c generated
View file

@ -156,6 +156,7 @@ lean_object* l_Lean_Meta_lambdaTelescope___at___private_Lean_Elab_PreDefinition_
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_wfRecursion___lambda__2___closed__2;
static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs_mkSum___spec__1___closed__9;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_wfRecursion___lambda__2___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Elab/PreDefinition/WF/PackDomain.c generated
View file

@ -175,6 +175,7 @@ lean_object* l_Lean_mkApp4(lean_object*, lean_object*, lean_object*, lean_object
LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_WF_packDomain_packApplications_visit___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_WF_packDomain___spec__3___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_st_ref_set(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_panic___at___private_Lean_Elab_PreDefinition_WF_PackDomain_0__Lean_Elab_WF_mkPSigmaCasesOn_go___spec__1___closed__1;
lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_panic_fn(lean_object*, lean_object*);

1
stage0/stdlib/Lean/Elab/PreDefinition/WF/PackMutual.c generated
View file

@ -152,6 +152,7 @@ lean_object* l_Lean_Meta_getLevel(lean_object*, lean_object*, lean_object*, lean
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_WF_PackMutual_0__Lean_Elab_WF_getCodomainLevel___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_WF_packMutual___lambda__3(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_Elab_PreDefinition_WF_PackMutual_0__Lean_Elab_WF_getCodomainsLevel(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_PreDefinition_WF_PackMutual_0__Lean_Elab_WF_mkNewCoDomain_go___closed__6;
extern lean_object* l_Lean_instInhabitedName;
lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Elab/Quotation.c generated
View file

@ -889,6 +889,7 @@ LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Elab_Quotation_0__L
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__6___closed__25;
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_floatOutAntiquotTerms___lambda__2___closed__20;
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__6___lambda__2___closed__16;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_resolveGlobalName___at_Lean_Elab_Term_resolveName___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__2(lean_object*, lean_object*);
static lean_object* l___private_Init_Meta_0__Lean_quoteList___at_Lean_Elab_Term_Quotation_ArrayStxBuilder_build___spec__1___closed__7;

2
stage0/stdlib/Lean/Elab/Quotation/Precheck.c generated
View file

@ -88,7 +88,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Term_Quotation_withNewLocal(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Quotation_precheck___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ResolveName_resolveNamespace_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_precheckParen___closed__3;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_Quotation_precheck___lambda__1___closed__3;
static lean_object* l_Lean_addTrace___at_Lean_Elab_Term_Quotation_precheck___spec__3___closed__7;
static lean_object* l_List_forIn_loop___at_Lean_Elab_Term_Quotation_precheckIdent___spec__3___closed__3;
@ -194,6 +193,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Term_Quotation_pr
lean_object* l_Lean_Elab_Term_adaptExpander(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Quotation_precheck___spec__8___rarg___closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_precheckApp___closed__3;
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_forM___at_Lean_Elab_Term_Quotation_precheck___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Elab/StructInst.c generated
View file

@ -606,6 +606,7 @@ lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_getFieldIdx___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_panic___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1(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_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandNonAtomicExplicitSources_go___lambda__1___closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_StructInst_expandStructInstExpectedType_declRange___closed__6;
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStructInstAux___spec__1___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Elab/Syntax.c generated
View file

@ -578,6 +578,7 @@ lean_object* l_Lean_Name_getPrefix(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_checkLeftRec___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_addTrace___at_Lean_Elab_Term_checkLeftRec___spec__3___closed__6;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_elabSyntax(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__49;
static lean_object* l___regBuiltin_Lean_Elab_Command_elabSyntax___closed__3;

1
stage0/stdlib/Lean/Elab/SyntheticMVars.c generated
View file

@ -217,6 +217,7 @@ LEAN_EXPORT lean_object* l_List_forIn_loop___at___private_Lean_Elab_SyntheticMVa
LEAN_EXPORT lean_object* l_Lean_Elab_Term_runTactic___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVarsNoPostponing(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_getSomeSynthethicMVarsRef___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_withSynthesize___rarg(lean_object*, lean_object*, lean_object*, uint8_t);

2
stage0/stdlib/Lean/Elab/Tactic/Basic.c generated
View file

@ -127,7 +127,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ensureHasNoMVars___boxed(lean_object
static lean_object* l_Lean_Elab_goalsToMessageData___closed__2;
lean_object* l_Lean_ResolveName_resolveNamespace_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_instMonadTacticM___closed__5;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkSorry(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_expandMacroImpl_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_withInfoTreeContext___at_Lean_Elab_Tactic_withTacticInfoContext___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -300,6 +299,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_withMacroExpansion___rarg___lambda__
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_instAlternativeTacticM___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_st_ref_set(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalTacticAt(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___closed__1;
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_instAlternativeTacticM___spec__1___rarg(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_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

1
stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c generated
View file

@ -713,6 +713,7 @@ static lean_object* l_Lean_Elab_Tactic_evalIntro___closed__30;
LEAN_EXPORT lean_object* l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_Tactic_elabSetOption___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTraceMessage___closed__5;
static lean_object* l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_Tactic_elabSetOption___spec__3___closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalFailIfSuccess_declRange___closed__3;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalIntros_declRange___closed__5;

2
stage0/stdlib/Lean/Elab/Tactic/Conv/Congr.c generated
View file

@ -100,7 +100,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Conv_evalCongr___rarg(lean_object*,
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Conv_Congr_0__Lean_Elab_Tactic_Conv_ext___boxed(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_Elab_Tactic_Conv_evalLhs___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Conv_evalRhs___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRhs_declRange___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRhs_declRange___closed__1;
lean_object* l_Lean_Meta_applyRefl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -205,6 +204,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg_declRange___clo
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalLhs_declRange___closed__1;
static lean_object* l___private_Lean_Elab_Tactic_Conv_Congr_0__Lean_Elab_Tactic_Conv_extCore___lambda__2___closed__4;
static lean_object* l_Lean_Elab_Tactic_Conv_congr___lambda__2___closed__4;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_List_forIn_loop___at___private_Lean_Elab_Tactic_Conv_Congr_0__Lean_Elab_Tactic_Conv_selectIdx___spec__1___closed__3;
lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

2
stage0/stdlib/Lean/Elab/Tactic/Induction.c generated
View file

@ -188,7 +188,6 @@ static lean_object* l_Lean_Elab_Tactic_ElimApp_setMotiveArg___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInduction_declRange___closed__7;
static lean_object* l_Lean_Elab_Tactic_ElimApp_setMotiveArg___closed__4;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_addNewArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltVarNames___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getMVarType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeTargets___spec__1(size_t, size_t, lean_object*);
@ -425,6 +424,7 @@ uint8_t l_Lean_Expr_isFVar(lean_object*);
static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName___closed__2;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCases___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalTacticAt(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getAltNumFields___spec__1(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_ElimApp_evalAlts_go___spec__6(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

2
stage0/stdlib/Lean/Elab/Tactic/Match.c generated
View file

@ -86,7 +86,6 @@ static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_eva
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalMatch_declRange___closed__1;
lean_object* l_Lean_ResolveName_resolveNamespace_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Tactic_evalMatch___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalEraseAuxDiscrs_declRange___closed__6;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTermAux___spec__2(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_expandMacroImpl_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
@ -177,6 +176,7 @@ static lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Match
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalEraseAuxDiscrs___closed__9;
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Tactic_evalMatch___spec__1___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Lean_Elab_Tactic_evalEraseAuxDiscrs___spec__3(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_evalMatch___closed__5;

1
stage0/stdlib/Lean/Elab/Term.c generated
View file

@ -1056,6 +1056,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Term_Context_currMacroScope___default;
LEAN_EXPORT lean_object* l_ReaderT_pure___at_Lean_Elab_Term_addTermInfo___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_observing___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_instAddErrorMessageContextTermElabM___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___spec__15(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_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed__8;
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeApplicationTime____x40_Lean_Attributes___hyg_13_(uint8_t, uint8_t);

2
stage0/stdlib/Lean/Elab/Util.c generated
View file

@ -77,7 +77,6 @@ lean_object* l_Lean_ResolveName_resolveNamespace_x3f(lean_object*, lean_object*,
static lean_object* l_Lean_Elab_mkElabAttribute___rarg___lambda__3___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_mkElabAttribute___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_mkElabAttribute___rarg___lambda__2___closed__13;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_checkSyntaxNodeKindAtNamespaces(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_expandMacroImpl_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_Elab_getBetterRef___lambda__1(lean_object*);
@ -186,6 +185,7 @@ lean_object* l_Lean_throwError___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_getBetterRef___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_getBetterRef___boxed(lean_object*, lean_object*);
lean_object* l_Lean_findDeclarationRanges_x3f___at___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_List_foldl___at_Lean_MacroScopesView_review___spec__1(lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNone(lean_object*);
static lean_object* l_Lean_Elab_mkElabAttribute___rarg___lambda__3___closed__5;

1
stage0/stdlib/Lean/Environment.c generated
View file

@ -487,6 +487,7 @@ LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_4608_(lean_
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2055_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_instInhabitedPersistentEnvExtensionState___rarg(lean_object*);
static lean_object* l_Lean_instInhabitedEnvExtensionInterface___closed__5;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l___private_Lean_Environment_0__Lean_getEntriesFor___closed__1;
LEAN_EXPORT lean_object* l_Lean_EnvExtension_modifyState___rarg___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedName;

Some files were not shown because too many files have changed in this diff Show more