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:
Lean stage0 autoupdater 2024-11-29 21:32:14 +00:00
parent 39bffb6fda
commit 3752241edd
66 changed files with 72900 additions and 66246 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
stage0/src/include/lean/lean.h generated
View file

@ -1692,6 +1692,7 @@ static inline uint8_t lean_uint8_dec_le(uint8_t a1, uint8_t a2) { return a1 <= a
static inline uint16_t lean_uint8_to_uint16(uint8_t a) { return ((uint16_t)a); }
static inline uint32_t lean_uint8_to_uint32(uint8_t a) { return ((uint32_t)a); }
static inline uint64_t lean_uint8_to_uint64(uint8_t a) { return ((uint64_t)a); }
static inline size_t lean_uint8_to_usize(uint8_t a) { return ((size_t)a); }
/* UInt16 */
@ -1727,6 +1728,7 @@ static inline uint8_t lean_uint16_dec_le(uint16_t a1, uint16_t a2) { return a1 <
static inline uint8_t lean_uint16_to_uint8(uint16_t a) { return ((uint8_t)a); }
static inline uint32_t lean_uint16_to_uint32(uint16_t a) { return ((uint32_t)a); }
static inline uint64_t lean_uint16_to_uint64(uint16_t a) { return ((uint64_t)a); }
static inline size_t lean_uint16_to_usize(uint16_t a) { return ((size_t)a); }
/* UInt32 */
@ -1762,7 +1764,7 @@ static inline uint8_t lean_uint32_dec_le(uint32_t a1, uint32_t a2) { return a1 <
static inline uint8_t lean_uint32_to_uint8(uint32_t a) { return ((uint8_t)a); }
static inline uint16_t lean_uint32_to_uint16(uint32_t a) { return ((uint16_t)a); }
static inline uint64_t lean_uint32_to_uint64(uint32_t a) { return ((uint64_t)a); }
static inline size_t lean_uint32_to_usize(uint32_t a) { return a; }
static inline size_t lean_uint32_to_usize(uint32_t a) { return ((size_t)a); }
/* UInt64 */
@ -1834,6 +1836,8 @@ static inline uint8_t lean_usize_dec_le(size_t a1, size_t a2) { return a1 <= a2;
/* usize -> other */
static inline uint8_t lean_usize_to_uint8(size_t a) { return ((uint8_t)a); }
static inline uint16_t lean_usize_to_uint16(size_t a) { return ((uint16_t)a); }
static inline uint32_t lean_usize_to_uint32(size_t a) { return ((uint32_t)a); }
static inline uint64_t lean_usize_to_uint64(size_t a) { return ((uint64_t)a); }
@ -2801,16 +2805,6 @@ static inline lean_obj_res lean_nat_pred(b_lean_obj_arg n) {
return lean_nat_sub(n, lean_box(1));
}
static inline lean_obj_res lean_runtime_mark_multi_threaded(lean_obj_arg a) {
lean_mark_mt(a);
return a;
}
static inline lean_obj_res lean_runtime_mark_persistent(lean_obj_arg a) {
lean_mark_persistent(a);
return a;
}
#ifdef __cplusplus
}
#endif

12
stage0/src/runtime/io.cpp generated
View file

@ -692,7 +692,7 @@ extern "C" LEAN_EXPORT obj_res lean_windows_get_next_transition(b_obj_arg timezo
tm = (int64_t)(nextTransition / 1000.0);
}
int32_t dst_offset = ucal_get(cal, UCAL_DST_OFFSET, &status);
if (U_FAILURE(status)) {
@ -1450,6 +1450,16 @@ extern "C" LEAN_EXPORT obj_res lean_io_exit(uint8_t code, obj_arg /* w */) {
exit(code);
}
extern "C" LEAN_EXPORT obj_res lean_runtime_mark_multi_threaded(obj_arg a, obj_arg /* w */) {
lean_mark_mt(a);
return io_result_mk_ok(a);
}
extern "C" LEAN_EXPORT obj_res lean_runtime_mark_persistent(obj_arg a, obj_arg /* w */) {
lean_mark_persistent(a);
return io_result_mk_ok(a);
}
void initialize_io() {
g_io_error_nullptr_read = lean_mk_io_user_error(mk_ascii_string_unchecked("null reference read"));
mark_persistent(g_io_error_nullptr_read);

36
stage0/stdlib/Init/Data/Fin/Basic.c generated
View file

@ -209,6 +209,24 @@ lean_dec(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Fin_ofNat_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_nat_mod(x_3, x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Fin_ofNat_x27___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Fin_ofNat_x27(x_1, x_2, x_3);
lean_dec(x_3);
lean_dec(x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Fin_ofNat(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -230,24 +248,6 @@ lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Fin_ofNat_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_nat_mod(x_3, x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Fin_ofNat_x27___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Fin_ofNat_x27(x_1, x_2, x_3);
lean_dec(x_3);
lean_dec(x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Fin_add(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{

40
stage0/stdlib/Init/Data/List/Lemmas.c generated
View file

@ -24,6 +24,7 @@ LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_splitAt_go_ma
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_findSome_x3f_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_splitAt_go_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_filterMap__replicate_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__GetElem_x3f_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_partition_loop_match__1_splitter(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_foldlRecOn(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLastD_match__1_splitter(lean_object*, lean_object*);
@ -47,15 +48,54 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLast_x21_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_foldl_match__1_splitter(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_filterMap__replicate_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__GetElem_x3f_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_foldl__filterMap_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_foldl__filterMap_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_filter_match__1_splitter___rarg(uint8_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__Option_isSome_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__Option_isSome_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_partition_loop_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__GetElem_x3f_match__1_splitter(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLast_match__1_splitter(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_filterMap__replicate_match__1_splitter(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_foldl__filterMap_match__1_splitter(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__GetElem_x3f_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_dec(x_2);
lean_inc(x_3);
return x_3;
}
else
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_apply_1(x_2, x_4);
return x_5;
}
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__GetElem_x3f_match__1_splitter(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l___private_Init_Data_List_Lemmas_0__GetElem_x3f_match__1_splitter___rarg___boxed), 3, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__GetElem_x3f_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l___private_Init_Data_List_Lemmas_0__GetElem_x3f_match__1_splitter___rarg(x_1, x_2, x_3);
lean_dec(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_foldl_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{

52
stage0/stdlib/Init/Data/UInt/Basic.c generated
View file

@ -17,6 +17,7 @@ LEAN_EXPORT lean_object* l_UInt64_modn___boxed(lean_object*, lean_object*);
uint8_t lean_uint8_sub(uint8_t, uint8_t);
LEAN_EXPORT uint8_t l_instDecidableLtUInt16(uint16_t, uint16_t);
LEAN_EXPORT lean_object* l_instComplementUInt32;
LEAN_EXPORT lean_object* l_USize_toUInt16___boxed(lean_object*);
LEAN_EXPORT lean_object* l_USize_mul___boxed(lean_object*, lean_object*);
lean_object* lean_uint16_to_nat(uint16_t);
uint32_t lean_bool_to_uint32(uint8_t);
@ -60,6 +61,7 @@ size_t lean_uint64_to_usize(uint64_t);
uint64_t lean_uint64_lor(uint64_t, uint64_t);
LEAN_EXPORT lean_object* l_instMaxUInt64___boxed(lean_object*, lean_object*);
static lean_object* l_instShiftLeftUInt64___closed__1;
uint8_t lean_usize_to_uint8(size_t);
static lean_object* l_instHModUInt64Nat___closed__1;
LEAN_EXPORT lean_object* l_instAddUInt16;
uint32_t lean_uint32_complement(uint32_t);
@ -74,6 +76,7 @@ static lean_object* l_instDivUSize___closed__1;
LEAN_EXPORT lean_object* l_USize_div___boxed(lean_object*, lean_object*);
static lean_object* l_instShiftRightUInt8___closed__1;
LEAN_EXPORT lean_object* l_UInt64_decLt___boxed(lean_object*, lean_object*);
size_t lean_uint8_to_usize(uint8_t);
LEAN_EXPORT uint16_t l_instMaxUInt16(uint16_t, uint16_t);
uint16_t lean_uint16_complement(uint16_t);
LEAN_EXPORT lean_object* l_instOrOpUSize;
@ -101,6 +104,7 @@ LEAN_EXPORT lean_object* l_instMaxUInt8___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instAndOpUSize;
LEAN_EXPORT lean_object* l_Nat_cast___at_UInt8_modn___spec__1(lean_object*);
static lean_object* l_instAddUInt64___closed__1;
uint16_t lean_usize_to_uint16(size_t);
uint64_t lean_uint64_land(uint64_t, uint64_t);
static lean_object* l_instShiftRightUInt16___closed__1;
LEAN_EXPORT lean_object* l_UInt64_add___boxed(lean_object*, lean_object*);
@ -172,6 +176,7 @@ LEAN_EXPORT lean_object* l_UInt8_mod___boxed(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_instDecidableLeUInt64(uint64_t, uint64_t);
extern lean_object* l_System_Platform_numBits;
LEAN_EXPORT lean_object* l_instHModUInt16Nat;
size_t lean_uint16_to_usize(uint16_t);
lean_object* lean_usize_to_nat(size_t);
static lean_object* l_instAddUInt32___closed__1;
uint8_t lean_uint8_mul(uint8_t, uint8_t);
@ -260,11 +265,13 @@ uint32_t lean_uint32_lor(uint32_t, uint32_t);
LEAN_EXPORT lean_object* l_instAndOpUInt32;
LEAN_EXPORT lean_object* l_instXorUInt64;
uint32_t lean_uint32_shift_left(uint32_t, uint32_t);
LEAN_EXPORT lean_object* l_UInt8_toUSize___boxed(lean_object*);
uint8_t lean_uint64_dec_le(uint64_t, uint64_t);
uint8_t lean_uint8_dec_le(uint8_t, uint8_t);
uint64_t lean_uint64_shift_left(uint64_t, uint64_t);
static lean_object* l_instShiftLeftUInt8___closed__1;
uint8_t lean_uint8_shift_right(uint8_t, uint8_t);
LEAN_EXPORT lean_object* l_USize_toUInt8___boxed(lean_object*);
LEAN_EXPORT lean_object* l_USize_shiftLeft___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instMinUSize___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instMinUInt64___boxed(lean_object*, lean_object*);
@ -276,6 +283,7 @@ static lean_object* l_instXorUInt8___closed__1;
LEAN_EXPORT lean_object* l_instSubUInt16;
LEAN_EXPORT uint16_t l_instMinUInt16(uint16_t, uint16_t);
LEAN_EXPORT lean_object* l_UInt64_xor___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_UInt16_toUSize___boxed(lean_object*);
LEAN_EXPORT lean_object* l_UInt16_modn(uint16_t, lean_object*);
uint64_t lean_bool_to_uint64(uint8_t);
LEAN_EXPORT lean_object* l_UInt32_land___boxed(lean_object*, lean_object*);
@ -2465,6 +2473,50 @@ x_4 = lean_box_usize(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_UInt8_toUSize___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; size_t x_3; lean_object* x_4;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = lean_uint8_to_usize(x_2);
x_4 = lean_box_usize(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_USize_toUInt8___boxed(lean_object* x_1) {
_start:
{
size_t x_2; uint8_t x_3; lean_object* x_4;
x_2 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_3 = lean_usize_to_uint8(x_2);
x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_UInt16_toUSize___boxed(lean_object* x_1) {
_start:
{
uint16_t x_2; size_t x_3; lean_object* x_4;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = lean_uint16_to_usize(x_2);
x_4 = lean_box_usize(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_USize_toUInt16___boxed(lean_object* x_1) {
_start:
{
size_t x_2; uint16_t x_3; lean_object* x_4;
x_2 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_3 = lean_usize_to_uint16(x_2);
x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_UInt32_toUSize___boxed(lean_object* x_1) {
_start:
{

22071
stage0/stdlib/Init/Data/UInt/Lemmas.c generated
View file

File diff suppressed because one or more lines are too long

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

@ -75,6 +75,7 @@ static lean_object* l___private_Init_System_IO_0__IO_FS_reprDirEntry____x40_Init
LEAN_EXPORT lean_object* l_IO_println(lean_object*);
lean_object* lean_io_prim_handle_read(lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_readFile___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Runtime_markPersistent___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Init_System_IO_0__IO_reprTaskState____x40_Init_System_IO___hyg_1242____closed__17;
lean_object* lean_io_check_canceled(lean_object*);
static lean_object* l___private_Init_System_IO_0__IO_reprTaskState____x40_Init_System_IO___hyg_1242____closed__16;
@ -343,6 +344,7 @@ LEAN_EXPORT uint8_t l___private_Init_System_IO_0__IO_ordTaskState____x40_Init_Sy
lean_object* lean_st_mk_ref(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_ofBuffer___lambda__1___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Handle_mk___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Runtime_markMultiThreaded___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Handle_isTty___boxed(lean_object*, lean_object*);
static lean_object* l___auto____x40_Init_System_IO___hyg_1713____closed__38;
LEAN_EXPORT lean_object* l_IO_print(lean_object*);
@ -384,6 +386,7 @@ lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
static lean_object* l___auto____x40_Init_System_IO___hyg_1713____closed__30;
static lean_object* l___private_Init_System_IO_0__IO_FS_reprMetadata____x40_Init_System_IO___hyg_3089____closed__4;
LEAN_EXPORT lean_object* l_IO_instMaxTaskState___boxed(lean_object*, lean_object*);
lean_object* lean_runtime_mark_multi_threaded(lean_object*, lean_object*);
lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_withIsolatedStreams___rarg___lambda__4(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_withIsolatedStreams___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
@ -681,6 +684,7 @@ static lean_object* l___private_Init_System_IO_0__IO_reprTaskState____x40_Init_S
LEAN_EXPORT lean_object* l_IO_sleep___lambda__1___boxed(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instMonadLiftBaseIOEIO(lean_object*, lean_object*);
lean_object* lean_runtime_mark_persistent(lean_object*, lean_object*);
static lean_object* l___private_Init_System_IO_0__IO_FS_reprFileType____x40_Init_System_IO___hyg_2649____closed__7;
lean_object* lean_io_get_random_bytes(size_t, lean_object*);
lean_object* lean_io_process_get_pid(lean_object*);
@ -5821,12 +5825,12 @@ return x_1;
static lean_object* _init_l_IO_FS_instInhabitedSystemTime___closed__1() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = 0;
x_2 = l___private_Init_System_IO_0__IO_FS_reprSystemTime____x40_Init_System_IO___hyg_2835____closed__6;
lean_object* x_1; uint32_t x_2; lean_object* x_3;
x_1 = l___private_Init_System_IO_0__IO_FS_reprSystemTime____x40_Init_System_IO___hyg_2835____closed__6;
x_2 = l_IO_FS_instInhabitedStream___lambda__1___closed__1;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
@ -11588,6 +11592,22 @@ return x_89;
}
}
}
LEAN_EXPORT lean_object* l_Runtime_markMultiThreaded___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_runtime_mark_multi_threaded(x_2, x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Runtime_markPersistent___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_runtime_mark_persistent(x_2, x_3);
return x_4;
}
}
lean_object* initialize_Init_System_IOError(uint8_t builtin, lean_object*);
lean_object* initialize_Init_System_FilePath(uint8_t builtin, lean_object*);
lean_object* initialize_Init_System_ST(uint8_t builtin, lean_object*);

20
stage0/stdlib/Init/Util.c generated
View file

@ -14,7 +14,6 @@
extern "C" {
#endif
LEAN_EXPORT lean_object* l_dbgSleep___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Runtime_markPersistent___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Init_Util_0__mkPanicMessage___closed__3;
uint8_t lean_usize_dec_eq(size_t, size_t);
@ -37,12 +36,10 @@ uint8_t lean_is_exclusive_obj(lean_object*);
lean_object* l_panic___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_withPtrEqUnsafe___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ptrEq(lean_object*);
LEAN_EXPORT lean_object* l_Runtime_markMultiThreaded___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_isExclusiveUnsafe___boxed(lean_object*, lean_object*);
static lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl___closed__1;
LEAN_EXPORT lean_object* l_panicWithPosWithDecl___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ptrEqList(lean_object*);
lean_object* lean_runtime_mark_multi_threaded(lean_object*);
LEAN_EXPORT lean_object* l_dbgTraceVal___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Util_0__mkPanicMessage___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_dbgTrace___boxed(lean_object*, lean_object*, lean_object*);
@ -59,7 +56,6 @@ LEAN_EXPORT lean_object* l_dbgTraceIfShared___boxed(lean_object*, lean_object*,
LEAN_EXPORT lean_object* l_withPtrEqDecEq___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_withPtrAddrUnsafe(lean_object*, lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* lean_runtime_mark_persistent(lean_object*);
LEAN_EXPORT lean_object* l_dbgTraceVal___rarg___lambda__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ptrAddrUnsafe___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_withPtrEqDecEq(lean_object*);
@ -521,22 +517,6 @@ lean_dec(x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Runtime_markMultiThreaded___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_runtime_mark_multi_threaded(x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Runtime_markPersistent___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_runtime_mark_persistent(x_2);
return x_3;
}
}
lean_object* initialize_Init_Data_String_Basic(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_ToString_Basic(uint8_t builtin, lean_object*);
static bool _G_initialized = false;

2
stage0/stdlib/Lake/Load/Materialize.c generated
View file

@ -2916,7 +2916,7 @@ static lean_object* _init_l_Lake_Dependency_materialize___lambda__3___closed__8(
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("' (should be \"git#>rev>\")", 25, 25);
x_1 = lean_mk_string_unchecked("' (should be \"git#<rev>\")", 25, 25);
return x_1;
}
}

1987
stage0/stdlib/Lean/AddDecl.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/Class.c generated
View file

@ -2983,7 +2983,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_mkOutParamArgsImplicit_go___closed__1;
x_2 = l_Lean_mkOutParamArgsImplicit_go___closed__2;
x_3 = lean_unsigned_to_nat(1761u);
x_3 = lean_unsigned_to_nat(1765u);
x_4 = lean_unsigned_to_nat(24u);
x_5 = l_Lean_mkOutParamArgsImplicit_go___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -3004,7 +3004,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_mkOutParamArgsImplicit_go___closed__1;
x_2 = l_Lean_mkOutParamArgsImplicit_go___closed__5;
x_3 = lean_unsigned_to_nat(1750u);
x_3 = lean_unsigned_to_nat(1754u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_mkOutParamArgsImplicit_go___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

6
stage0/stdlib/Lean/Compiler/CSimpAttr.c generated
View file

@ -16,7 +16,6 @@ extern "C" {
LEAN_EXPORT lean_object* l_Lean_Compiler_CSimp_initFn____x40_Lean_Compiler_CSimpAttr___hyg_471_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_CSimp_initFn____x40_Lean_Compiler_CSimpAttr___hyg_471____lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_const___override(lean_object*, lean_object*);
lean_object* l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6569____spec__4(lean_object*);
static lean_object* l_Lean_Compiler_CSimp_instInhabitedEntry___closed__1;
static size_t l_Lean_PersistentHashMap_insertAux___at_Lean_Compiler_CSimp_initFn____x40_Lean_Compiler_CSimpAttr___hyg_137____spec__3___closed__1;
size_t lean_usize_shift_right(size_t, size_t);
@ -125,6 +124,7 @@ lean_object* l_Lean_PersistentHashMap_mkEmptyEntries(lean_object*, lean_object*)
uint64_t l_Lean_Name_hash___override(lean_object*);
static lean_object* l_Lean_Compiler_CSimp_initFn____x40_Lean_Compiler_CSimpAttr___hyg_137____closed__8;
uint64_t lean_uint64_xor(uint64_t, uint64_t);
lean_object* l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6597____spec__4(lean_object*);
lean_object* l_Lean_ScopedEnvExtension_getState___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insert___at_Lean_Compiler_CSimp_initFn____x40_Lean_Compiler_CSimpAttr___hyg_137____spec__2(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_CSimp_initFn____x40_Lean_Compiler_CSimpAttr___hyg_471____closed__12;
@ -330,7 +330,7 @@ lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get(x_1, 1);
x_5 = l_Lean_SMap_switch___at_Lean_Compiler_CSimp_State_switch___spec__1(x_3);
x_6 = l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6569____spec__4(x_4);
x_6 = l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6597____spec__4(x_4);
lean_ctor_set(x_1, 1, x_6);
lean_ctor_set(x_1, 0, x_5);
return x_1;
@ -344,7 +344,7 @@ lean_inc(x_8);
lean_inc(x_7);
lean_dec(x_1);
x_9 = l_Lean_SMap_switch___at_Lean_Compiler_CSimp_State_switch___spec__1(x_7);
x_10 = l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6569____spec__4(x_8);
x_10 = l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6597____spec__4(x_8);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_9);
lean_ctor_set(x_11, 1, x_10);

8
stage0/stdlib/Lean/Compiler/LCNF/FVarUtil.c generated
View file

@ -442,7 +442,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Compiler_LCNF_Expr_mapFVarM___rarg___lambda__1___closed__1;
x_2 = l_Lean_Compiler_LCNF_Expr_mapFVarM___rarg___lambda__1___closed__2;
x_3 = lean_unsigned_to_nat(1697u);
x_3 = lean_unsigned_to_nat(1701u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Compiler_LCNF_Expr_mapFVarM___rarg___lambda__1___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -521,7 +521,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Compiler_LCNF_Expr_mapFVarM___rarg___lambda__1___closed__1;
x_2 = l_Lean_Compiler_LCNF_Expr_mapFVarM___rarg___lambda__2___closed__1;
x_3 = lean_unsigned_to_nat(1686u);
x_3 = lean_unsigned_to_nat(1690u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l_Lean_Compiler_LCNF_Expr_mapFVarM___rarg___lambda__2___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -637,7 +637,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Compiler_LCNF_Expr_mapFVarM___rarg___lambda__1___closed__1;
x_2 = l_Lean_Compiler_LCNF_Expr_mapFVarM___rarg___lambda__4___closed__1;
x_3 = lean_unsigned_to_nat(1781u);
x_3 = lean_unsigned_to_nat(1785u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Compiler_LCNF_Expr_mapFVarM___rarg___lambda__4___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -775,7 +775,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Compiler_LCNF_Expr_mapFVarM___rarg___lambda__1___closed__1;
x_2 = l_Lean_Compiler_LCNF_Expr_mapFVarM___rarg___lambda__6___closed__1;
x_3 = lean_unsigned_to_nat(1761u);
x_3 = lean_unsigned_to_nat(1765u);
x_4 = lean_unsigned_to_nat(24u);
x_5 = l_Lean_Compiler_LCNF_Expr_mapFVarM___rarg___lambda__6___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

3970
stage0/stdlib/Lean/Compiler/LCNF/Main.c generated
View file

File diff suppressed because it is too large Load diff

16
stage0/stdlib/Lean/Compiler/LCNF/Simp/ConstantFold.c generated
View file

@ -196,6 +196,7 @@ static lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___c
lean_object* l_Nat_sub___boxed(lean_object*, lean_object*);
lean_object* l_UInt16_add___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_initFn____x40_Lean_Compiler_LCNF_Simp_ConstantFold___hyg_4833____closed__4;
extern uint32_t l_instInhabitedUInt32;
lean_object* l_Lean_Compiler_LCNF_getPhase(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_initFn____x40_Lean_Compiler_LCNF_Simp_ConstantFold___hyg_4833____closed__5;
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_Folder_leftAnnihilator___at_Lean_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___spec__29___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -308,6 +309,7 @@ static lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___c
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_Folder_mkBinaryDecisionProcedure___at_Lean_Compiler_LCNF_Simp_ConstantFold_relationFolders___spec__3___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_Lean_Compiler_LCNF_Simp_ConstantFold_Folder_leftNeutral___at_Lean_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___spec__16___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_Folder_mkBinaryDecisionProcedure___at_Lean_Compiler_LCNF_Simp_ConstantFold_relationFolders___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern uint64_t l_instInhabitedUInt64;
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkBoolLit___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_Folder_leftRightNeutral(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_Folder_rightAnnihilator___at_Lean_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___spec__30(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -393,7 +395,6 @@ static lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Compiler_LCNF_Simp_Co
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_Folder_mkBinary___at_Lean_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_Folder_leftRightNeutral___at_Lean_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___spec__11(uint16_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___closed__47;
extern uint16_t l_UInt16_instInhabited;
LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Compiler_LCNF_Simp_ConstantFold_initFn____x40_Lean_Compiler_LCNF_Simp_ConstantFold___hyg_4833____spec__3___boxed(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_Compiler_LCNF_Simp_ConstantFold_0__Lean_Compiler_LCNF_Simp_ConstantFold_getFolder___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_Folder_mkUnary___at_Lean_Compiler_LCNF_Simp_ConstantFold_stringFolders___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -488,10 +489,12 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_Folder_rightNeut
LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Compiler_LCNF_Simp_ConstantFold_initFn____x40_Lean_Compiler_LCNF_Simp_ConstantFold___hyg_4833____spec__2___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_Compiler_LCNF_Simp_ConstantFold_Folder_divShift___at_Lean_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___spec__56(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_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___closed__29;
extern uint16_t l_instInhabitedUInt16;
static lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_instLiteralString___closed__2;
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_Folder_rightNeutral___at_Lean_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___spec__13(uint16_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___closed__40;
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_Folder_first___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern uint8_t l_instInhabitedUInt8;
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_Folder_mulRhsShift___at_Lean_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___spec__34___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 lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___closed__20;
LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Compiler_LCNF_Simp_ConstantFold_0__Lean_Compiler_LCNF_Simp_ConstantFold_getFolder___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
@ -594,8 +597,6 @@ lean_object* lean_array_mk(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_Folder_leftNeutral___at_Lean_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_getBoolLit___closed__3;
static lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_instLiteralUInt8___closed__2;
extern uint32_t l_UInt32_instInhabited;
extern uint64_t l_UInt64_instInhabited;
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAtAux___at_Lean_Compiler_LCNF_Simp_ConstantFold_applyFolders___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_Folder_mkBinaryDecisionProcedure___at_Lean_Compiler_LCNF_Simp_ConstantFold_relationFolders___spec__4___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_Compiler_LCNF_Simp_ConstantFold_Folder_rightAnnihilator___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -669,7 +670,6 @@ uint8_t lean_nat_dec_le(lean_object*, lean_object*);
static lean_object* l___private_Lean_Compiler_LCNF_Simp_ConstantFold_0__Lean_Compiler_LCNF_Simp_ConstantFold_getFolderCoreUnsafe___closed__2;
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_mkAuxLetDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_usize_dec_lt(size_t, size_t);
extern uint8_t l_UInt8_instInhabited;
static lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_arithmeticFolders___closed__11;
static lean_object* l_Lean_Compiler_LCNF_Simp_ConstantFold_instLiteralUInt32___closed__4;
lean_object* l_UInt16_decLe___boxed(lean_object*, lean_object*);
@ -2574,7 +2574,7 @@ static lean_object* _init_l_Lean_Compiler_LCNF_Simp_ConstantFold_instLiteralUInt
_start:
{
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_UInt8_instInhabited;
x_1 = l_instInhabitedUInt8;
x_2 = l_Lean_Compiler_LCNF_Simp_ConstantFold_instLiteralUInt8___closed__4;
x_3 = l_Lean_Compiler_LCNF_Simp_ConstantFold_instLiteralUInt8___closed__3;
x_4 = l_Lean_Compiler_LCNF_Simp_ConstantFold_instLiteralUInt8___closed__5;
@ -2630,7 +2630,7 @@ static lean_object* _init_l_Lean_Compiler_LCNF_Simp_ConstantFold_instLiteralUInt
_start:
{
uint16_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_UInt16_instInhabited;
x_1 = l_instInhabitedUInt16;
x_2 = l_Lean_Compiler_LCNF_Simp_ConstantFold_instLiteralUInt16___closed__3;
x_3 = l_Lean_Compiler_LCNF_Simp_ConstantFold_instLiteralUInt16___closed__2;
x_4 = l_Lean_Compiler_LCNF_Simp_ConstantFold_instLiteralUInt16___closed__4;
@ -2686,7 +2686,7 @@ static lean_object* _init_l_Lean_Compiler_LCNF_Simp_ConstantFold_instLiteralUInt
_start:
{
uint32_t x_1; lean_object* x_2;
x_1 = l_UInt32_instInhabited;
x_1 = l_instInhabitedUInt32;
x_2 = lean_box_uint32(x_1);
return x_2;
}
@ -2749,7 +2749,7 @@ static lean_object* _init_l_Lean_Compiler_LCNF_Simp_ConstantFold_instLiteralUInt
_start:
{
uint64_t x_1; lean_object* x_2;
x_1 = l_UInt64_instInhabited;
x_1 = l_instInhabitedUInt64;
x_2 = lean_box_uint64(x_1);
return x_2;
}

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

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

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

@ -57,7 +57,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Command_mkDefView
LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_Command_mkDefViewOfInstance___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*, uint8_t);
LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_mkDefViewOfInstance___spec__10___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__6;
static uint64_t l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__6;
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Lean_stringToMessageData(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_instToSnapshotTreeDefsParsedSnapshot___spec__1___lambda__1(lean_object*);
@ -98,6 +98,7 @@ lean_object* l_Lean_ResolveName_resolveNamespace(lean_object*, lean_object*, lea
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_Elab_DefView_isInstance___spec__1(lean_object*, size_t, size_t);
static lean_object* l_Lean_Elab_Command_mkDefViewOfAbbrev___closed__1;
lean_object* l_Lean_SourceInfo_fromRef(lean_object*, uint8_t);
uint64_t lean_uint64_of_nat(lean_object*);
lean_object* l_Lean_MessageData_ofSyntax(lean_object*);
LEAN_EXPORT uint8_t l_Lean_Elab_DefKind_isTheorem(uint8_t);
static lean_object* l_Lean_Elab_instInhabitedDefView___closed__2;
@ -236,6 +237,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Command_mkDefView
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_mkStr4(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_addMacroStack___at_Lean_Elab_Command_instAddErrorMessageContextCommandElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__10;
LEAN_EXPORT lean_object* l_Lean_Elab_DefKind_noConfusion___rarg___lambda__1(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_DefKind_isTheorem___boxed(lean_object*);
lean_object* lean_array_get_size(lean_object*);
@ -626,11 +628,20 @@ lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__6() {
static uint64_t _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__6() {
_start:
{
lean_object* x_1; uint64_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_uint64_of_nat(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__7() {
_start:
{
uint64_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = 0;
x_1 = l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__6;
x_2 = l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__3;
x_3 = lean_alloc_ctor(0, 1, 8);
lean_ctor_set(x_3, 0, x_2);
@ -638,7 +649,7 @@ lean_ctor_set_uint64(x_3, sizeof(void*)*1, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__7() {
static lean_object* _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__8() {
_start:
{
lean_object* x_1;
@ -646,14 +657,14 @@ x_1 = lean_mk_string_unchecked("", 0, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__8() {
static lean_object* _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5; lean_object* x_6;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__7;
x_2 = l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__8;
x_3 = l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__5;
x_4 = l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__6;
x_4 = l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__7;
x_5 = 0;
x_6 = lean_alloc_ctor(0, 4, 1);
lean_ctor_set(x_6, 0, x_2);
@ -664,11 +675,11 @@ lean_ctor_set_uint8(x_6, sizeof(void*)*4, x_5);
return x_6;
}
}
static lean_object* _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__9() {
static lean_object* _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__8;
x_1 = l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__9;
x_2 = l_Lean_Elab_instInhabitedDefViewElabHeaderData___closed__1;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -682,7 +693,7 @@ _start:
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_2;
x_2 = l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__9;
x_2 = l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__10;
return x_2;
}
else
@ -836,7 +847,7 @@ _start:
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_2;
x_2 = l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__9;
x_2 = l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__10;
return x_2;
}
else
@ -3049,7 +3060,7 @@ static lean_object* _init_l_Lean_Elab_Command_mkDefViewOfInstance___closed__7()
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__7;
x_1 = l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__8;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
@ -5890,13 +5901,14 @@ lean_mark_persistent(l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lam
l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__5 = _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__5();
lean_mark_persistent(l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__5);
l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__6 = _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__6();
lean_mark_persistent(l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__6);
l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__7 = _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__7();
lean_mark_persistent(l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__7);
l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__8 = _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__8();
lean_mark_persistent(l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__8);
l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__9 = _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__9();
lean_mark_persistent(l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__9);
l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__10 = _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__10();
lean_mark_persistent(l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___lambda__1___closed__10);
l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___closed__1 = _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___closed__1();
lean_mark_persistent(l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___closed__1);
l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___closed__2 = _init_l_Lean_Elab_instToSnapshotTreeHeaderProcessedSnapshot___closed__2();

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

@ -260,7 +260,7 @@ LEAN_EXPORT lean_object* l_Lean_RBNode_fold___at___private_Lean_Elab_MutualDef_0
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_elabMutualDef_go___spec__17(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_forIn_x27Unsafe_loop___at_Lean_Elab_Term_elabMutualDef_processDeriving___spec__2(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*);
static lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_getPendingMVarErrorMessage___closed__2;
static lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__6;
static uint64_t l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__6;
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_MutualDef___hyg_6628____closed__5;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_MutualClosure_main___spec__1___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_Std_Range_forIn_x27_loop___at_Lean_Elab_Command_elabMutualDef___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*);
@ -474,6 +474,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_withH
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabFunValues___spec__18___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_EXPORT lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_checkModifiers(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__4___lambda__3___closed__4;
uint64_t lean_uint64_of_nat(lean_object*);
lean_object* l_List_findSome_x3f___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkLetRecClosures___spec__7___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkLetRecClosures___spec__8___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_EXPORT lean_object* l_Lean_Core_withRestoreOrSaveFull___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabFunValues___spec__14___boxed(lean_object**);
@ -1212,6 +1213,7 @@ LEAN_EXPORT lean_object* l_Lean_Language_withAlwaysResolvedPromises___at_Lean_El
LEAN_EXPORT lean_object* l_Lean_Elab_elabTerminationHints___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_declValToTerminationHint___spec__1___lambda__6(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_initFn____x40_Lean_Elab_MutualDef___hyg_6628____closed__1;
static lean_object* l_Lean_addDeclarationRanges___at_Lean_Elab_Term_elabMutualDef_go___spec__10___closed__2;
static lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__13;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_withRestoreOrSaveFull___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__4___boxed(lean_object**);
static lean_object* l_Nat_foldM_loop___at_Lean_Elab_Term_MutualClosure_pushMain___spec__1___closed__3;
uint8_t l_Lean_Exception_isRuntime(lean_object*);
@ -4079,11 +4081,20 @@ lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__6() {
static uint64_t _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__6() {
_start:
{
lean_object* x_1; uint64_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_uint64_of_nat(x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__7() {
_start:
{
uint64_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = 0;
x_1 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__6;
x_2 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__3;
x_3 = lean_alloc_ctor(0, 1, 8);
lean_ctor_set(x_3, 0, x_2);
@ -4091,14 +4102,14 @@ lean_ctor_set_uint64(x_3, sizeof(void*)*1, x_1);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__7() {
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5; lean_object* x_6;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_instantiateMVarsProfiling___closed__1;
x_3 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__5;
x_4 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__6;
x_4 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__7;
x_5 = 0;
x_6 = lean_alloc_ctor(0, 4, 1);
lean_ctor_set(x_6, 0, x_2);
@ -4109,47 +4120,47 @@ lean_ctor_set_uint8(x_6, sizeof(void*)*4, x_5);
return x_6;
}
}
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__8() {
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__7;
x_2 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__8;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__9() {
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__8;
x_1 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__9;
x_2 = lean_task_pure(x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__10() {
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__9;
x_2 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__10;
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___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__11() {
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__7;
x_2 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__8;
x_3 = lean_box(0);
x_4 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__10;
x_4 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__11;
x_5 = l_Lean_Elab_instInhabitedDefViewElabHeader___closed__1;
x_6 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_6, 0, x_2);
@ -4160,7 +4171,7 @@ lean_ctor_set(x_6, 4, x_5);
return x_6;
}
}
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__12() {
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__13() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -4175,7 +4186,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabH
_start:
{
lean_object* x_10; lean_object* x_11; uint8_t x_12;
x_10 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__11;
x_10 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__12;
x_11 = lean_io_promise_resolve(x_10, x_1, x_9);
x_12 = !lean_is_exclusive(x_11);
if (x_12 == 0)
@ -4183,7 +4194,7 @@ if (x_12 == 0)
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_11, 0);
lean_dec(x_13);
x_14 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__12;
x_14 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__13;
lean_ctor_set(x_11, 0, x_14);
return x_11;
}
@ -4193,7 +4204,7 @@ lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_ctor_get(x_11, 1);
lean_inc(x_15);
lean_dec(x_11);
x_16 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__12;
x_16 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__13;
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_15);
@ -53966,7 +53977,6 @@ lean_mark_persistent(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeade
l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__5 = _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__5();
lean_mark_persistent(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__5);
l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__6 = _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__6();
lean_mark_persistent(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__6);
l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__7 = _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__7();
lean_mark_persistent(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__7);
l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__8 = _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__8();
@ -53979,6 +53989,8 @@ l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda
lean_mark_persistent(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__11);
l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__12 = _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__12();
lean_mark_persistent(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__12);
l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__13 = _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__13();
lean_mark_persistent(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___lambda__1___closed__13);
l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___closed__1 = _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___closed__1();
lean_mark_persistent(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___closed__1);
l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___closed__2 = _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_mkTacTask___closed__2();

3978
stage0/stdlib/Lean/Elab/PreDefinition/Basic.c generated
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

4211
stage0/stdlib/Lean/Elab/PreDefinition/Structural/IndPred.c generated
View file

File diff suppressed because it is too large Load diff

10075
stage0/stdlib/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.c generated
View file

File diff suppressed because it is too large Load diff

9915
stage0/stdlib/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.c generated
View file

File diff suppressed because it is too large Load diff

2001
stage0/stdlib/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.c generated
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

6069
stage0/stdlib/Lean/Elab/Tactic/NormCast.c generated
View file

File diff suppressed because it is too large Load diff

4234
stage0/stdlib/Lean/Elab/Tactic/Omega/Frontend.c generated
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

26
stage0/stdlib/Lean/Expr.c generated
View file

@ -479,6 +479,7 @@ LEAN_EXPORT lean_object* l_Lean_Expr_instToString;
LEAN_EXPORT uint8_t lean_expr_has_level_mvar(lean_object*);
static lean_object* l_Lean_Nat_mkInstHMod___closed__4;
LEAN_EXPORT lean_object* l_Lean_Expr_projIdx_x21(lean_object*);
extern uint64_t l_instInhabitedUInt64;
lean_object* lean_expr_instantiate(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_Expr_isMVar(lean_object*);
static lean_object* l_Lean_Nat_mkInstAdd___closed__1;
@ -967,7 +968,6 @@ LEAN_EXPORT lean_object* l_Lean_mkEM(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Expr_isSemiOutParam___boxed(lean_object*);
LEAN_EXPORT uint8_t l_Lean_Expr_isTrue(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Expr_hasMVar___boxed(lean_object*);
extern uint64_t l_UInt64_instInhabited;
LEAN_EXPORT lean_object* l_Lean_mkApp(lean_object*, lean_object*);
lean_object* l_Std_HashSet_instEmptyCollection(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_RBNode_ins___at_Lean_MVarIdSet_insert___spec__2(lean_object*, lean_object*, lean_object*);
@ -2404,7 +2404,7 @@ static uint64_t _init_l_Lean_instInhabitedData__1() {
_start:
{
uint64_t x_1;
x_1 = l_UInt64_instInhabited;
x_1 = l_instInhabitedUInt64;
return x_1;
}
}
@ -28848,7 +28848,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__5;
x_2 = l___private_Lean_Expr_0__Lean_Expr_updateApp_x21Impl___closed__1;
x_3 = lean_unsigned_to_nat(1686u);
x_3 = lean_unsigned_to_nat(1690u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l_Lean_Expr_appFn_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -28927,7 +28927,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__5;
x_2 = l_Lean_Expr_updateFVar_x21___closed__1;
x_3 = lean_unsigned_to_nat(1697u);
x_3 = lean_unsigned_to_nat(1701u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_fvarId_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -28988,7 +28988,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__5;
x_2 = l___private_Lean_Expr_0__Lean_Expr_updateConst_x21Impl___closed__1;
x_3 = lean_unsigned_to_nat(1702u);
x_3 = lean_unsigned_to_nat(1706u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l_Lean_Expr_constName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -29054,7 +29054,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__5;
x_2 = l___private_Lean_Expr_0__Lean_Expr_updateSort_x21Impl___closed__1;
x_3 = lean_unsigned_to_nat(1713u);
x_3 = lean_unsigned_to_nat(1717u);
x_4 = lean_unsigned_to_nat(14u);
x_5 = l___private_Lean_Expr_0__Lean_Expr_updateSort_x21Impl___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -29125,7 +29125,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__5;
x_2 = l___private_Lean_Expr_0__Lean_Expr_updateMData_x21Impl___closed__1;
x_3 = lean_unsigned_to_nat(1724u);
x_3 = lean_unsigned_to_nat(1728u);
x_4 = lean_unsigned_to_nat(17u);
x_5 = l___private_Lean_Expr_0__Lean_Expr_updateMData_x21Impl___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -29193,7 +29193,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__5;
x_2 = l___private_Lean_Expr_0__Lean_Expr_updateProj_x21Impl___closed__1;
x_3 = lean_unsigned_to_nat(1735u);
x_3 = lean_unsigned_to_nat(1739u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l___private_Lean_Expr_0__Lean_Expr_updateProj_x21Impl___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -29264,7 +29264,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__5;
x_2 = l___private_Lean_Expr_0__Lean_Expr_updateForall_x21Impl___closed__1;
x_3 = lean_unsigned_to_nat(1750u);
x_3 = lean_unsigned_to_nat(1754u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l___private_Lean_Expr_0__Lean_Expr_updateForall_x21Impl___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -29367,7 +29367,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__5;
x_2 = l_Lean_Expr_updateForallE_x21___closed__1;
x_3 = lean_unsigned_to_nat(1761u);
x_3 = lean_unsigned_to_nat(1765u);
x_4 = lean_unsigned_to_nat(24u);
x_5 = l___private_Lean_Expr_0__Lean_Expr_updateForall_x21Impl___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -29473,7 +29473,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__5;
x_2 = l___private_Lean_Expr_0__Lean_Expr_updateLambda_x21Impl___closed__1;
x_3 = lean_unsigned_to_nat(1770u);
x_3 = lean_unsigned_to_nat(1774u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l___private_Lean_Expr_0__Lean_Expr_updateLambda_x21Impl___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -29576,7 +29576,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__5;
x_2 = l_Lean_Expr_updateLambdaE_x21___closed__1;
x_3 = lean_unsigned_to_nat(1781u);
x_3 = lean_unsigned_to_nat(1785u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l___private_Lean_Expr_0__Lean_Expr_updateLambda_x21Impl___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -29674,7 +29674,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__5;
x_2 = l___private_Lean_Expr_0__Lean_Expr_updateLet_x21Impl___closed__1;
x_3 = lean_unsigned_to_nat(1790u);
x_3 = lean_unsigned_to_nat(1794u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Expr_letName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

36
stage0/stdlib/Lean/Language/Basic.c generated
View file

@ -35,7 +35,7 @@ static lean_object* l_Lean_Language_diagnosticsOfHeaderError___closed__2;
LEAN_EXPORT lean_object* l_Lean_PersistentArray_forM___at_Lean_Language_reportMessages___spec__2(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Language_withAlwaysResolvedPromises___spec__1___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
static lean_object* l_Lean_Language_instInhabitedSnapshot___closed__1;
static uint64_t l_Lean_Language_instInhabitedSnapshot___closed__1;
LEAN_EXPORT lean_object* l_Lean_Language_reportMessages___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* lean_io_as_task(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_toString(lean_object*, uint8_t, lean_object*);
@ -73,6 +73,7 @@ LEAN_EXPORT lean_object* l_Lean_Language_SnapshotTree_getAll(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Language_SnapshotTree_forM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Language_reportMessages___lambda__1___closed__1;
LEAN_EXPORT uint8_t l_Lean_Language_instInhabitedDynamicSnapshot___lambda__1(lean_object*);
static lean_object* l_Lean_Language_instInhabitedSnapshot___closed__4;
lean_object* lean_string_utf8_byte_size(lean_object*);
LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Language_withAlwaysResolvedPromises___spec__2___rarg___lambda__2(lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Language_withHeaderExceptions___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -96,6 +97,7 @@ static lean_object* l_Lean_Language_instInhabitedSnapshotTree___closed__1;
static lean_object* l_Lean_Language_diagnosticsOfHeaderError___closed__1;
static lean_object* l_Lean_Language_instInhabitedDynamicSnapshot___closed__8;
LEAN_EXPORT lean_object* l_Lean_Language_SnapshotTree_waitAll(lean_object*, lean_object*);
uint64_t lean_uint64_of_nat(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Language_DynamicSnapshot_ofTyped___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Language_SnapshotTask_pure(lean_object*);
static lean_object* l___auto____x40_Lean_Language_Basic___hyg_62____closed__21;
@ -814,11 +816,20 @@ x_1 = l___auto____x40_Lean_Language_Basic___hyg_62____closed__41;
return x_1;
}
}
static lean_object* _init_l_Lean_Language_instInhabitedSnapshot___closed__1() {
static uint64_t _init_l_Lean_Language_instInhabitedSnapshot___closed__1() {
_start:
{
lean_object* x_1; uint64_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_uint64_of_nat(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Language_instInhabitedSnapshot___closed__2() {
_start:
{
uint64_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = 0;
x_1 = l_Lean_Language_instInhabitedSnapshot___closed__1;
x_2 = l_Lean_Language_Snapshot_instInhabitedDiagnostics___closed__4;
x_3 = lean_alloc_ctor(0, 1, 8);
lean_ctor_set(x_3, 0, x_2);
@ -826,7 +837,7 @@ lean_ctor_set_uint64(x_3, sizeof(void*)*1, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_Language_instInhabitedSnapshot___closed__2() {
static lean_object* _init_l_Lean_Language_instInhabitedSnapshot___closed__3() {
_start:
{
lean_object* x_1;
@ -834,14 +845,14 @@ x_1 = lean_mk_string_unchecked("", 0, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Language_instInhabitedSnapshot___closed__3() {
static lean_object* _init_l_Lean_Language_instInhabitedSnapshot___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5; lean_object* x_6;
x_1 = lean_box(0);
x_2 = l_Lean_Language_instInhabitedSnapshot___closed__2;
x_2 = l_Lean_Language_instInhabitedSnapshot___closed__3;
x_3 = l_Lean_Language_Snapshot_instInhabitedDiagnostics___closed__6;
x_4 = l_Lean_Language_instInhabitedSnapshot___closed__1;
x_4 = l_Lean_Language_instInhabitedSnapshot___closed__2;
x_5 = 0;
x_6 = lean_alloc_ctor(0, 4, 1);
lean_ctor_set(x_6, 0, x_2);
@ -856,7 +867,7 @@ static lean_object* _init_l_Lean_Language_instInhabitedSnapshot() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Language_instInhabitedSnapshot___closed__3;
x_1 = l_Lean_Language_instInhabitedSnapshot___closed__4;
return x_1;
}
}
@ -1808,7 +1819,7 @@ static lean_object* _init_l_Lean_Language_instInhabitedSnapshotTree___closed__1(
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Language_instInhabitedSnapshot___closed__3;
x_1 = l_Lean_Language_instInhabitedSnapshot___closed__4;
x_2 = l_Lean_Language_Snapshot_instInhabitedDiagnostics___closed__1;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2320,7 +2331,7 @@ _start:
{
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = 0;
x_2 = l_Lean_Language_instInhabitedSnapshot___closed__2;
x_2 = l_Lean_Language_instInhabitedSnapshot___closed__3;
x_3 = l_Lean_Language_initFn____x40_Lean_Language_Basic___hyg_1192____closed__3;
x_4 = lean_box(x_1);
x_5 = lean_alloc_ctor(0, 3, 0);
@ -3669,7 +3680,7 @@ x_11 = l_Lean_Language_diagnosticsOfHeaderError___closed__2;
x_12 = l_Lean_Language_diagnosticsOfHeaderError___closed__1;
x_13 = 0;
x_14 = 2;
x_15 = l_Lean_Language_instInhabitedSnapshot___closed__2;
x_15 = l_Lean_Language_instInhabitedSnapshot___closed__3;
x_16 = lean_alloc_ctor(0, 5, 2);
lean_ctor_set(x_16, 0, x_11);
lean_ctor_set(x_16, 1, x_12);
@ -4164,11 +4175,12 @@ lean_mark_persistent(l___auto____x40_Lean_Language_Basic___hyg_62____closed__41)
l___auto____x40_Lean_Language_Basic___hyg_62_ = _init_l___auto____x40_Lean_Language_Basic___hyg_62_();
lean_mark_persistent(l___auto____x40_Lean_Language_Basic___hyg_62_);
l_Lean_Language_instInhabitedSnapshot___closed__1 = _init_l_Lean_Language_instInhabitedSnapshot___closed__1();
lean_mark_persistent(l_Lean_Language_instInhabitedSnapshot___closed__1);
l_Lean_Language_instInhabitedSnapshot___closed__2 = _init_l_Lean_Language_instInhabitedSnapshot___closed__2();
lean_mark_persistent(l_Lean_Language_instInhabitedSnapshot___closed__2);
l_Lean_Language_instInhabitedSnapshot___closed__3 = _init_l_Lean_Language_instInhabitedSnapshot___closed__3();
lean_mark_persistent(l_Lean_Language_instInhabitedSnapshot___closed__3);
l_Lean_Language_instInhabitedSnapshot___closed__4 = _init_l_Lean_Language_instInhabitedSnapshot___closed__4();
lean_mark_persistent(l_Lean_Language_instInhabitedSnapshot___closed__4);
l_Lean_Language_instInhabitedSnapshot = _init_l_Lean_Language_instInhabitedSnapshot();
lean_mark_persistent(l_Lean_Language_instInhabitedSnapshot);
l_Lean_Language_withAlwaysResolvedPromise___rarg___lambda__3___closed__1 = _init_l_Lean_Language_withAlwaysResolvedPromise___rarg___lambda__3___closed__1();

1819
stage0/stdlib/Lean/Language/Lean.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/Level.c generated
View file

@ -171,6 +171,7 @@ static lean_object* l___private_Lean_Level_0__Lean_reprLevel____x40_Lean_Level__
static lean_object* l_Lean_Level_mvarId_x21___closed__2;
LEAN_EXPORT uint8_t l_Lean_Level_occurs(lean_object*, lean_object*);
static lean_object* l___private_Lean_Level_0__Lean_reprLevel____x40_Lean_Level___hyg_1013____closed__17;
extern uint64_t l_instInhabitedUInt64;
static lean_object* l_Lean_Level_mkData___closed__2;
LEAN_EXPORT lean_object* l_Nat_imax___boxed(lean_object*, lean_object*);
lean_object* lean_uint64_to_nat(uint64_t);
@ -321,7 +322,6 @@ LEAN_EXPORT lean_object* l_panic___at_Lean_Level_normalize___spec__1(lean_object
LEAN_EXPORT lean_object* l_Lean_Level_getOffset___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Level_getParamSubst(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Level_PP_Result_format___closed__1;
extern uint64_t l_UInt64_instInhabited;
LEAN_EXPORT lean_object* l_Lean_instBEqLevelMVarId;
LEAN_EXPORT lean_object* l_Lean_Level_mkNaryMax(lean_object*);
static lean_object* l___private_Lean_Level_0__Lean_reprLevel____x40_Lean_Level___hyg_1013____closed__22;
@ -448,7 +448,7 @@ static uint64_t _init_l_Lean_instInhabitedData() {
_start:
{
uint64_t x_1;
x_1 = l_UInt64_instInhabited;
x_1 = l_instInhabitedUInt64;
return x_1;
}
}

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

File diff suppressed because it is too large Load diff

2001
stage0/stdlib/Lean/Meta/Check.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -6462,7 +6462,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__2;
x_3 = lean_unsigned_to_nat(1724u);
x_3 = lean_unsigned_to_nat(1728u);
x_4 = lean_unsigned_to_nat(17u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -6491,7 +6491,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__5;
x_3 = lean_unsigned_to_nat(1735u);
x_3 = lean_unsigned_to_nat(1739u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__6;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -6520,7 +6520,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__8;
x_3 = lean_unsigned_to_nat(1686u);
x_3 = lean_unsigned_to_nat(1690u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__9;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -6549,7 +6549,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__11;
x_3 = lean_unsigned_to_nat(1781u);
x_3 = lean_unsigned_to_nat(1785u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__12;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -6578,7 +6578,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__14;
x_3 = lean_unsigned_to_nat(1761u);
x_3 = lean_unsigned_to_nat(1765u);
x_4 = lean_unsigned_to_nat(24u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__15;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -6607,7 +6607,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__17;
x_3 = lean_unsigned_to_nat(1790u);
x_3 = lean_unsigned_to_nat(1794u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__18;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2024
stage0/stdlib/Lean/Meta/ExprDefEq.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -417,7 +417,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Meta_ExprLens_0__Lean_Meta_lensCoord___rarg___lambda__3___closed__1;
x_2 = l___private_Lean_Meta_ExprLens_0__Lean_Meta_lensCoord___rarg___lambda__3___closed__2;
x_3 = lean_unsigned_to_nat(1686u);
x_3 = lean_unsigned_to_nat(1690u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l___private_Lean_Meta_ExprLens_0__Lean_Meta_lensCoord___rarg___lambda__3___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -603,7 +603,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Meta_ExprLens_0__Lean_Meta_lensCoord___rarg___lambda__3___closed__1;
x_2 = l___private_Lean_Meta_ExprLens_0__Lean_Meta_lensCoord___rarg___lambda__8___closed__1;
x_3 = lean_unsigned_to_nat(1790u);
x_3 = lean_unsigned_to_nat(1794u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l___private_Lean_Meta_ExprLens_0__Lean_Meta_lensCoord___rarg___lambda__8___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -804,7 +804,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Meta_ExprLens_0__Lean_Meta_lensCoord___rarg___lambda__3___closed__1;
x_2 = l___private_Lean_Meta_ExprLens_0__Lean_Meta_lensCoord___rarg___lambda__10___closed__1;
x_3 = lean_unsigned_to_nat(1781u);
x_3 = lean_unsigned_to_nat(1785u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l___private_Lean_Meta_ExprLens_0__Lean_Meta_lensCoord___rarg___lambda__10___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -928,7 +928,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Meta_ExprLens_0__Lean_Meta_lensCoord___rarg___lambda__3___closed__1;
x_2 = l___private_Lean_Meta_ExprLens_0__Lean_Meta_lensCoord___rarg___lambda__11___closed__1;
x_3 = lean_unsigned_to_nat(1761u);
x_3 = lean_unsigned_to_nat(1765u);
x_4 = lean_unsigned_to_nat(24u);
x_5 = l___private_Lean_Meta_ExprLens_0__Lean_Meta_lensCoord___rarg___lambda__11___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2001
stage0/stdlib/Lean/Meta/Injective.c generated
View file

File diff suppressed because it is too large Load diff

18
stage0/stdlib/Lean/Meta/LitValues.c generated
View file

@ -84,7 +84,6 @@ static lean_object* l_Lean_Meta_normLitValue___lambda__10___closed__3;
lean_object* l_Lean_Level_ofNat(lean_object*);
lean_object* l_Lean_Expr_appArg_x21(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_getCharValue_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Fin_ofNat(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_normLitValue___lambda__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_normLitValue___lambda__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_isLitValue___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -195,6 +194,7 @@ uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_mkApp3(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Loop_forIn_loop___at_Lean_Meta_getListLitOf_x3f___spec__1___rarg___closed__2;
static lean_object* l_Lean_Meta_getUInt64Value_x3f___closed__1;
lean_object* lean_nat_mod(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_litToCtor___lambda__1___closed__15;
lean_object* l_Lean_instantiateMVars___at___private_Lean_Meta_Basic_0__Lean_Meta_isClassApp_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_normLitValue___lambda__3___closed__1;
@ -1740,9 +1740,9 @@ x_39 = lean_unsigned_to_nat(1u);
x_40 = lean_nat_sub(x_36, x_39);
lean_dec(x_36);
x_41 = lean_nat_add(x_40, x_39);
x_42 = l_Fin_ofNat(x_40, x_19);
lean_dec(x_19);
lean_dec(x_40);
x_42 = lean_nat_mod(x_19, x_41);
lean_dec(x_19);
lean_ctor_set(x_16, 1, x_42);
lean_ctor_set(x_16, 0, x_41);
lean_ctor_set(x_26, 0, x_16);
@ -1775,9 +1775,9 @@ x_47 = lean_unsigned_to_nat(1u);
x_48 = lean_nat_sub(x_44, x_47);
lean_dec(x_44);
x_49 = lean_nat_add(x_48, x_47);
x_50 = l_Fin_ofNat(x_48, x_19);
lean_dec(x_19);
lean_dec(x_48);
x_50 = lean_nat_mod(x_19, x_49);
lean_dec(x_19);
lean_ctor_set(x_16, 1, x_50);
lean_ctor_set(x_16, 0, x_49);
x_51 = lean_alloc_ctor(1, 1, 0);
@ -1821,9 +1821,9 @@ x_58 = lean_unsigned_to_nat(1u);
x_59 = lean_nat_sub(x_54, x_58);
lean_dec(x_54);
x_60 = lean_nat_add(x_59, x_58);
x_61 = l_Fin_ofNat(x_59, x_19);
lean_dec(x_19);
lean_dec(x_59);
x_61 = lean_nat_mod(x_19, x_60);
lean_dec(x_19);
lean_ctor_set(x_16, 1, x_61);
lean_ctor_set(x_16, 0, x_60);
if (lean_is_scalar(x_55)) {
@ -1992,9 +1992,9 @@ x_92 = lean_unsigned_to_nat(1u);
x_93 = lean_nat_sub(x_88, x_92);
lean_dec(x_88);
x_94 = lean_nat_add(x_93, x_92);
x_95 = l_Fin_ofNat(x_93, x_74);
lean_dec(x_74);
lean_dec(x_93);
x_95 = lean_nat_mod(x_74, x_94);
lean_dec(x_74);
x_96 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_96, 0, x_94);
lean_ctor_set(x_96, 1, x_95);

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

File diff suppressed because it is too large Load diff

10209
stage0/stdlib/Lean/Meta/SynthInstance.c generated
View file

File diff suppressed because it is too large Load diff

3990
stage0/stdlib/Lean/Meta/Tactic/Backtrack.c generated
View file

File diff suppressed because it is too large Load diff

10028
stage0/stdlib/Lean/Meta/Tactic/FunInd.c generated
View file

File diff suppressed because it is too large Load diff

118
stage0/stdlib/Lean/Meta/Tactic/Grind/Preprocessor.c generated
View file

@ -36,7 +36,7 @@ lean_object* lean_mk_array(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Meta_Grind_Preprocessor_introNext___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_Preprocessor_instInhabitedState___closed__7;
static lean_object* l_Lean_Meta_Grind_Preprocessor_PreM_run___rarg___closed__9;
static lean_object* l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__5;
static uint32_t l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__5;
lean_object* l_Lean_MVarId_getTag(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Preprocessor_applyCases_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__2;
@ -51,6 +51,7 @@ lean_object* l_Lean_Meta_getSimpCongrTheorems___rarg(lean_object*, lean_object*)
static lean_object* l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__7;
LEAN_EXPORT lean_object* l_ReaderT_bind___at_Lean_Meta_Grind_Preprocessor_introNext___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Preprocessor_simp___boxed(lean_object*);
static lean_object* l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__13;
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Preprocessor_introNext___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_Preprocessor_PreM_run___rarg___closed__4;
lean_object* l_Lean_Name_mkStr3(lean_object*, lean_object*, lean_object*);
@ -60,6 +61,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Preprocessor_introNext(lean_object*,
lean_object* lean_st_ref_take(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Preprocessor_simp___rarg___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_Meta_Grind_Preprocessor_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint64_t lean_uint64_of_nat(lean_object*);
lean_object* l_Lean_Meta_Simp_SimprocExtension_getSimprocs(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Preprocessor_introNext___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MVarId_getType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -82,7 +84,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Preprocessor_pushResult___boxed(lean_
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_num___override(lean_object*, lean_object*);
lean_object* l_Lean_Meta_Grind_isGrindCasesTarget(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__3;
static uint64_t l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__3;
lean_object* l_ShareCommon_mkStateImpl(lean_object*);
lean_object* l_Lean_FVarId_getType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Meta_Grind_Preprocessor_introNext___spec__4___rarg(lean_object*, lean_object*);
@ -97,6 +99,7 @@ LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Meta_Grind_Preprocessor_intr
lean_object* l_Lean_LocalContext_mkLocalDecl(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, uint8_t);
extern lean_object* l_Lean_Meta_Grind_grindNormSimprocExt;
LEAN_EXPORT lean_object* l_List_mapTR_loop___at_Lean_Meta_Grind_Preprocessor_applyCases_x3f___spec__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__14;
static lean_object* l_Lean_Meta_Grind_main___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Preprocessor_simp(lean_object*);
lean_object* l_Lean_Meta_SimpExtension_getTheorems(lean_object*, lean_object*, lean_object*, lean_object*);
@ -124,6 +127,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Preprocessor_applyInjection_x3f(lean_
static lean_object* l_Lean_Meta_Grind_Preprocessor_PreM_run___rarg___closed__7;
lean_object* l_Lean_MVarId_transformTarget(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn(lean_object*);
uint32_t lean_uint32_of_nat(lean_object*);
static lean_object* l_Lean_Meta_Grind_main___closed__5;
lean_object* l_Lean_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*);
lean_object* l_List_reverse___rarg(lean_object*);
@ -232,28 +236,46 @@ lean_ctor_set_uint8(x_5, 17, x_1);
return x_5;
}
}
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__3() {
static uint64_t _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__3() {
_start:
{
uint64_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = 0;
x_2 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__2;
x_3 = lean_alloc_ctor(0, 1, 8);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint64(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint64_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_uint64_of_nat(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__4() {
_start:
{
lean_object* x_1; uint64_t x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__2;
x_2 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__3;
x_3 = lean_alloc_ctor(0, 1, 8);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint64(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static uint32_t _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__5() {
_start:
{
lean_object* x_1; uint32_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_uint32_of_nat(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__5() {
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -263,29 +285,29 @@ x_3 = l_Nat_nextPowerOfTwo_go(x_1, x_2, lean_box(0));
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__6() {
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__5;
x_2 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__7;
x_3 = lean_mk_array(x_2, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__7() {
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(0u);
x_2 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__6;
x_2 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__8;
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_Meta_Grind_Preprocessor_instInhabitedContext___closed__8() {
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__10() {
_start:
{
lean_object* x_1;
@ -293,23 +315,23 @@ x_1 = l_Lean_PersistentHashMap_mkEmptyEntriesArray(lean_box(0), lean_box(0));
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__9() {
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__8;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__10;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__10() {
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__12() {
_start:
{
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = 1;
x_2 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__7;
x_3 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__9;
x_2 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__9;
x_3 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__11;
x_4 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
@ -317,38 +339,38 @@ lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
return x_4;
}
}
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__11() {
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__13() {
_start:
{
uint32_t 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; uint8_t x_8; lean_object* x_9;
x_1 = 0;
x_2 = lean_box(0);
x_3 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__1;
x_4 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__3;
x_5 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__4;
x_6 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__10;
lean_object* x_1; lean_object* x_2; lean_object* x_3; uint32_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__1;
x_3 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__4;
x_4 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__5;
x_5 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__6;
x_6 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__12;
x_7 = lean_unsigned_to_nat(0u);
x_8 = 0;
x_9 = lean_alloc_ctor(0, 7, 9);
lean_ctor_set(x_9, 0, x_3);
lean_ctor_set(x_9, 1, x_4);
lean_ctor_set(x_9, 2, x_4);
lean_ctor_set(x_9, 0, x_2);
lean_ctor_set(x_9, 1, x_3);
lean_ctor_set(x_9, 2, x_3);
lean_ctor_set(x_9, 3, x_5);
lean_ctor_set(x_9, 4, x_6);
lean_ctor_set(x_9, 5, x_2);
lean_ctor_set(x_9, 5, x_1);
lean_ctor_set(x_9, 6, x_7);
lean_ctor_set_uint32(x_9, sizeof(void*)*7, x_1);
lean_ctor_set_uint32(x_9, sizeof(void*)*7 + 4, x_1);
lean_ctor_set_uint32(x_9, sizeof(void*)*7, x_4);
lean_ctor_set_uint32(x_9, sizeof(void*)*7 + 4, x_4);
lean_ctor_set_uint8(x_9, sizeof(void*)*7 + 8, x_8);
return x_9;
}
}
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__12() {
static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__11;
x_2 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__4;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__13;
x_2 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__6;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -359,7 +381,7 @@ static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext()
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__12;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__14;
return x_1;
}
}
@ -367,7 +389,7 @@ static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedState___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__9;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__11;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -379,7 +401,7 @@ static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedState___cl
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__4;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__6;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -399,7 +421,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; size_t x_4; lean_object* x_5;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedState___closed__2;
x_2 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__4;
x_2 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__6;
x_3 = lean_unsigned_to_nat(0u);
x_4 = l_Lean_Meta_Grind_Preprocessor_instInhabitedState___closed__3;
x_5 = lean_alloc_ctor(0, 4, sizeof(size_t)*1);
@ -415,7 +437,7 @@ static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedState___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__9;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__11;
x_2 = l_Lean_Meta_Grind_Preprocessor_instInhabitedState___closed__4;
x_3 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_3, 0, x_1);
@ -547,7 +569,7 @@ static lean_object* _init_l_Lean_Meta_Grind_Preprocessor_PreM_run___rarg___close
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__9;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__11;
x_2 = l_Lean_Meta_Grind_Preprocessor_PreM_run___rarg___closed__6;
x_3 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_3, 0, x_1);
@ -4575,7 +4597,7 @@ static lean_object* _init_l_Lean_Meta_Grind_main___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__7;
x_1 = l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__9;
x_2 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_2, 0, x_1);
lean_ctor_set(x_2, 1, x_1);
@ -5071,11 +5093,9 @@ lean_mark_persistent(l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___close
l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__2 = _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__2();
lean_mark_persistent(l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__2);
l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__3 = _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__3();
lean_mark_persistent(l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__3);
l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__4 = _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__4();
lean_mark_persistent(l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__4);
l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__5 = _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__5();
lean_mark_persistent(l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__5);
l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__6 = _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__6();
lean_mark_persistent(l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__6);
l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__7 = _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__7();
@ -5090,6 +5110,10 @@ l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__11 = _init_l_Lean_
lean_mark_persistent(l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__11);
l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__12 = _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__12();
lean_mark_persistent(l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__12);
l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__13 = _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__13();
lean_mark_persistent(l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__13);
l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__14 = _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__14();
lean_mark_persistent(l_Lean_Meta_Grind_Preprocessor_instInhabitedContext___closed__14);
l_Lean_Meta_Grind_Preprocessor_instInhabitedContext = _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedContext();
lean_mark_persistent(l_Lean_Meta_Grind_Preprocessor_instInhabitedContext);
l_Lean_Meta_Grind_Preprocessor_instInhabitedState___closed__1 = _init_l_Lean_Meta_Grind_Preprocessor_instInhabitedState___closed__1();

2001
stage0/stdlib/Lean/Meta/Tactic/LibrarySearch.c generated
View file

File diff suppressed because it is too large Load diff

771
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/Meta/Tactic/Simp/Main.c generated
View file

@ -11927,7 +11927,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Simp_simpProj___lambda__1___closed__1;
x_2 = l_Lean_Meta_Simp_simpProj___lambda__1___closed__2;
x_3 = lean_unsigned_to_nat(1735u);
x_3 = lean_unsigned_to_nat(1739u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l_Lean_Meta_Simp_simpProj___lambda__1___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -13813,7 +13813,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Simp_simpProj___lambda__1___closed__1;
x_2 = l_Lean_Meta_Simp_simpArrow___lambda__1___closed__1;
x_3 = lean_unsigned_to_nat(1761u);
x_3 = lean_unsigned_to_nat(1765u);
x_4 = lean_unsigned_to_nat(24u);
x_5 = l_Lean_Meta_Simp_simpArrow___lambda__1___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

4170
stage0/stdlib/Lean/Meta/Tactic/Simp/Rewrite.c generated
View file

File diff suppressed because it is too large Load diff

2
stage0/stdlib/Lean/Meta/Tactic/Simp/SimpTheorems.c generated
View file

@ -14095,7 +14095,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_SimpTheorem_getValue___closed__1;
x_2 = l_Lean_Meta_SimpTheorem_getValue___closed__2;
x_3 = lean_unsigned_to_nat(1702u);
x_3 = lean_unsigned_to_nat(1706u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l_Lean_Meta_SimpTheorem_getValue___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

118
stage0/stdlib/Lean/Meta/Tactic/Simp/Types.c generated
View file

@ -71,6 +71,7 @@ static lean_object* l___private_Lean_Meta_Tactic_Simp_Types_0__Lean_Meta_Simp_up
LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_Meta_Simp_UsedSimps_toArray___spec__3(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_panic___at_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_getConfig___boxed(lean_object*);
static lean_object* l_Lean_Meta_Simp_instInhabitedContext___closed__13;
LEAN_EXPORT uint8_t l_Lean_PersistentHashMap_containsAux___at_Lean_Meta_Simp_UsedSimps_insert___spec__2(lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_removeUnnecessaryCasts_elimDummyEqRec(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_withDischarger___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -175,6 +176,7 @@ static lean_object* l_Lean_addTrace___at_Lean_Meta_Simp_congrArgs___spec__2___cl
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_Result_mkEqSymm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_Types_0__Lean_Meta_Simp_updateArith___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getFunInfo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint64_t lean_uint64_of_nat(lean_object*);
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_toArray___at_Lean_Meta_Simp_UsedSimps_toArray___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Meta_Simp_congrArgs___spec__3(lean_object*, 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_object*);
lean_object* lean_nat_div(lean_object*, lean_object*);
@ -241,6 +243,7 @@ lean_object* l_panic___at_Lean_Expr_appFn_x21___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_mkCongrSimp_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Simp_removeUnnecessaryCasts_isDummyEqRec___closed__2;
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_mkEqTransResultStep(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Simp_instInhabitedContext___closed__12;
static lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Meta_Simp_congrArgs___spec__3___closed__2;
static lean_object* l___private_Lean_Meta_Tactic_Simp_Types_0__Lean_Meta_Simp_updateArith___closed__1;
LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___spec__2___lambda__3___boxed(lean_object**);
@ -298,7 +301,7 @@ static lean_object* l_Lean_Meta_Simp_instInhabitedMethods___lambda__2___closed__
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_instInhabitedDiagnostics;
static lean_object* l_Lean_Meta_Simp_removeUnnecessaryCasts_isDummyEqRec___closed__5;
lean_object* l_Lean_Meta_mkCongr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Simp_instInhabitedContext___closed__5;
static uint32_t l_Lean_Meta_Simp_instInhabitedContext___closed__5;
LEAN_EXPORT lean_object* l_Lean_Meta_isMatcher___at_Lean_Meta_Simp_mkCongrSimp_x3f___spec__8___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_Meta_Simp_recordTriedSimpTheorem(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkImpCongr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -378,6 +381,7 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_Simp_mkCongrSimp_x3f___spec__7(lean_object*, size_t, size_t);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_mkCongrSimp_x3f___lambda__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_Expr_getAppFn(lean_object*);
uint32_t lean_uint32_of_nat(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_DStep_addExtraArgs___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_post(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_withFreshCache___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -470,7 +474,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Simp_UsedSimps_to
static lean_object* l_Lean_Meta_Simp_instInhabitedMethods___closed__4;
lean_object* l_ReaderT_instMonad___rarg(lean_object*);
size_t lean_usize_land(size_t, size_t);
static lean_object* l_Lean_Meta_Simp_instInhabitedContext___closed__3;
static uint64_t l_Lean_Meta_Simp_instInhabitedContext___closed__3;
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_Context_setConfig(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Simp_instInhabitedUsedSimps___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_removeUnnecessaryCasts___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1311,28 +1315,46 @@ lean_ctor_set_uint8(x_5, 17, x_1);
return x_5;
}
}
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__3() {
static uint64_t _init_l_Lean_Meta_Simp_instInhabitedContext___closed__3() {
_start:
{
uint64_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = 0;
x_2 = l_Lean_Meta_Simp_instInhabitedContext___closed__2;
x_3 = lean_alloc_ctor(0, 1, 8);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint64(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint64_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_uint64_of_nat(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__4() {
_start:
{
lean_object* x_1; uint64_t x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Simp_instInhabitedContext___closed__2;
x_2 = l_Lean_Meta_Simp_instInhabitedContext___closed__3;
x_3 = lean_alloc_ctor(0, 1, 8);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint64(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static uint32_t _init_l_Lean_Meta_Simp_instInhabitedContext___closed__5() {
_start:
{
lean_object* x_1; uint32_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_uint32_of_nat(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__5() {
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -1342,29 +1364,29 @@ x_3 = l_Nat_nextPowerOfTwo_go(x_1, x_2, lean_box(0));
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__6() {
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Simp_instInhabitedContext___closed__5;
x_2 = l_Lean_Meta_Simp_instInhabitedContext___closed__7;
x_3 = lean_mk_array(x_2, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__7() {
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(0u);
x_2 = l_Lean_Meta_Simp_instInhabitedContext___closed__6;
x_2 = l_Lean_Meta_Simp_instInhabitedContext___closed__8;
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_Meta_Simp_instInhabitedContext___closed__8() {
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__10() {
_start:
{
lean_object* x_1;
@ -1372,23 +1394,23 @@ x_1 = l_Lean_PersistentHashMap_mkEmptyEntriesArray(lean_box(0), lean_box(0));
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__9() {
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Simp_instInhabitedContext___closed__8;
x_1 = l_Lean_Meta_Simp_instInhabitedContext___closed__10;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__10() {
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__12() {
_start:
{
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = 1;
x_2 = l_Lean_Meta_Simp_instInhabitedContext___closed__7;
x_3 = l_Lean_Meta_Simp_instInhabitedContext___closed__9;
x_2 = l_Lean_Meta_Simp_instInhabitedContext___closed__9;
x_3 = l_Lean_Meta_Simp_instInhabitedContext___closed__11;
x_4 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
@ -1396,28 +1418,28 @@ lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
return x_4;
}
}
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__11() {
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__13() {
_start:
{
uint32_t 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; uint8_t x_8; lean_object* x_9;
x_1 = 0;
x_2 = lean_box(0);
x_3 = l_Lean_Meta_Simp_instInhabitedContext___closed__1;
x_4 = l_Lean_Meta_Simp_instInhabitedContext___closed__3;
x_5 = l_Lean_Meta_Simp_instInhabitedContext___closed__4;
x_6 = l_Lean_Meta_Simp_instInhabitedContext___closed__10;
lean_object* x_1; lean_object* x_2; lean_object* x_3; uint32_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Simp_instInhabitedContext___closed__1;
x_3 = l_Lean_Meta_Simp_instInhabitedContext___closed__4;
x_4 = l_Lean_Meta_Simp_instInhabitedContext___closed__5;
x_5 = l_Lean_Meta_Simp_instInhabitedContext___closed__6;
x_6 = l_Lean_Meta_Simp_instInhabitedContext___closed__12;
x_7 = lean_unsigned_to_nat(0u);
x_8 = 0;
x_9 = lean_alloc_ctor(0, 7, 9);
lean_ctor_set(x_9, 0, x_3);
lean_ctor_set(x_9, 1, x_4);
lean_ctor_set(x_9, 2, x_4);
lean_ctor_set(x_9, 0, x_2);
lean_ctor_set(x_9, 1, x_3);
lean_ctor_set(x_9, 2, x_3);
lean_ctor_set(x_9, 3, x_5);
lean_ctor_set(x_9, 4, x_6);
lean_ctor_set(x_9, 5, x_2);
lean_ctor_set(x_9, 5, x_1);
lean_ctor_set(x_9, 6, x_7);
lean_ctor_set_uint32(x_9, sizeof(void*)*7, x_1);
lean_ctor_set_uint32(x_9, sizeof(void*)*7 + 4, x_1);
lean_ctor_set_uint32(x_9, sizeof(void*)*7, x_4);
lean_ctor_set_uint32(x_9, sizeof(void*)*7 + 4, x_4);
lean_ctor_set_uint8(x_9, sizeof(void*)*7 + 8, x_8);
return x_9;
}
@ -1426,7 +1448,7 @@ static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_Simp_instInhabitedContext___closed__11;
x_1 = l_Lean_Meta_Simp_instInhabitedContext___closed__13;
return x_1;
}
}
@ -2555,7 +2577,7 @@ static lean_object* _init_l_Lean_Meta_Simp_instInhabitedUsedSimps___closed__1()
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Simp_instInhabitedContext___closed__9;
x_1 = l_Lean_Meta_Simp_instInhabitedContext___closed__11;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -3888,7 +3910,7 @@ static lean_object* _init_l_Lean_Meta_Simp_instInhabitedDiagnostics___closed__1(
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Simp_instInhabitedContext___closed__4;
x_1 = l_Lean_Meta_Simp_instInhabitedContext___closed__6;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -3908,7 +3930,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; size_t x_4; lean_object* x_5;
x_1 = l_Lean_Meta_Simp_instInhabitedDiagnostics___closed__1;
x_2 = l_Lean_Meta_Simp_instInhabitedContext___closed__4;
x_2 = l_Lean_Meta_Simp_instInhabitedContext___closed__6;
x_3 = lean_unsigned_to_nat(0u);
x_4 = l_Lean_Meta_Simp_instInhabitedDiagnostics___closed__2;
x_5 = lean_alloc_ctor(0, 4, sizeof(size_t)*1);
@ -3924,7 +3946,7 @@ static lean_object* _init_l_Lean_Meta_Simp_instInhabitedDiagnostics___closed__4(
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Simp_instInhabitedContext___closed__9;
x_1 = l_Lean_Meta_Simp_instInhabitedContext___closed__11;
x_2 = l_Lean_Meta_Simp_instInhabitedDiagnostics___closed__3;
x_3 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_3, 0, x_1);
@ -5643,7 +5665,7 @@ _start:
lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = 0;
x_3 = l_Lean_Meta_Simp_instInhabitedContext___closed__4;
x_3 = l_Lean_Meta_Simp_instInhabitedContext___closed__6;
x_4 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
@ -5663,7 +5685,7 @@ static lean_object* _init_l_Lean_Meta_Simp_instInhabitedSimprocs___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Simp_instInhabitedContext___closed__9;
x_1 = l_Lean_Meta_Simp_instInhabitedContext___closed__11;
x_2 = l_Lean_PersistentHashMap_empty___at_Lean_KeyedDeclsAttribute_instInhabitedExtensionState___spec__1;
x_3 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_3, 0, x_1);
@ -6759,8 +6781,8 @@ _start:
{
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = 1;
x_2 = l_Lean_Meta_Simp_instInhabitedContext___closed__7;
x_3 = l_Lean_Meta_Simp_instInhabitedContext___closed__9;
x_2 = l_Lean_Meta_Simp_instInhabitedContext___closed__9;
x_3 = l_Lean_Meta_Simp_instInhabitedContext___closed__11;
x_4 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
@ -10749,7 +10771,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Simp_mkImpCongr___closed__1;
x_2 = l_Lean_Meta_Simp_mkImpCongr___closed__2;
x_3 = lean_unsigned_to_nat(1761u);
x_3 = lean_unsigned_to_nat(1765u);
x_4 = lean_unsigned_to_nat(24u);
x_5 = l_Lean_Meta_Simp_mkImpCongr___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -29013,11 +29035,9 @@ lean_mark_persistent(l_Lean_Meta_Simp_instInhabitedContext___closed__1);
l_Lean_Meta_Simp_instInhabitedContext___closed__2 = _init_l_Lean_Meta_Simp_instInhabitedContext___closed__2();
lean_mark_persistent(l_Lean_Meta_Simp_instInhabitedContext___closed__2);
l_Lean_Meta_Simp_instInhabitedContext___closed__3 = _init_l_Lean_Meta_Simp_instInhabitedContext___closed__3();
lean_mark_persistent(l_Lean_Meta_Simp_instInhabitedContext___closed__3);
l_Lean_Meta_Simp_instInhabitedContext___closed__4 = _init_l_Lean_Meta_Simp_instInhabitedContext___closed__4();
lean_mark_persistent(l_Lean_Meta_Simp_instInhabitedContext___closed__4);
l_Lean_Meta_Simp_instInhabitedContext___closed__5 = _init_l_Lean_Meta_Simp_instInhabitedContext___closed__5();
lean_mark_persistent(l_Lean_Meta_Simp_instInhabitedContext___closed__5);
l_Lean_Meta_Simp_instInhabitedContext___closed__6 = _init_l_Lean_Meta_Simp_instInhabitedContext___closed__6();
lean_mark_persistent(l_Lean_Meta_Simp_instInhabitedContext___closed__6);
l_Lean_Meta_Simp_instInhabitedContext___closed__7 = _init_l_Lean_Meta_Simp_instInhabitedContext___closed__7();
@ -29030,6 +29050,10 @@ l_Lean_Meta_Simp_instInhabitedContext___closed__10 = _init_l_Lean_Meta_Simp_inst
lean_mark_persistent(l_Lean_Meta_Simp_instInhabitedContext___closed__10);
l_Lean_Meta_Simp_instInhabitedContext___closed__11 = _init_l_Lean_Meta_Simp_instInhabitedContext___closed__11();
lean_mark_persistent(l_Lean_Meta_Simp_instInhabitedContext___closed__11);
l_Lean_Meta_Simp_instInhabitedContext___closed__12 = _init_l_Lean_Meta_Simp_instInhabitedContext___closed__12();
lean_mark_persistent(l_Lean_Meta_Simp_instInhabitedContext___closed__12);
l_Lean_Meta_Simp_instInhabitedContext___closed__13 = _init_l_Lean_Meta_Simp_instInhabitedContext___closed__13();
lean_mark_persistent(l_Lean_Meta_Simp_instInhabitedContext___closed__13);
l_Lean_Meta_Simp_instInhabitedContext = _init_l_Lean_Meta_Simp_instInhabitedContext();
lean_mark_persistent(l_Lean_Meta_Simp_instInhabitedContext);
l___private_Lean_Meta_Tactic_Simp_Types_0__Lean_Meta_Simp_updateArith___closed__1 = _init_l___private_Lean_Meta_Tactic_Simp_Types_0__Lean_Meta_Simp_updateArith___closed__1();

10
stage0/stdlib/Lean/Meta/Transform.c generated
View file

@ -1286,7 +1286,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__2;
x_3 = lean_unsigned_to_nat(1781u);
x_3 = lean_unsigned_to_nat(1785u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -1424,7 +1424,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__4___closed__1;
x_3 = lean_unsigned_to_nat(1761u);
x_3 = lean_unsigned_to_nat(1765u);
x_4 = lean_unsigned_to_nat(24u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__4___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -1562,7 +1562,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__6___closed__1;
x_3 = lean_unsigned_to_nat(1790u);
x_3 = lean_unsigned_to_nat(1794u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__6___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -1734,7 +1734,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__9___closed__1;
x_3 = lean_unsigned_to_nat(1724u);
x_3 = lean_unsigned_to_nat(1728u);
x_4 = lean_unsigned_to_nat(17u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__9___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -1806,7 +1806,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__10___closed__1;
x_3 = lean_unsigned_to_nat(1735u);
x_3 = lean_unsigned_to_nat(1739u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__10___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

File diff suppressed because it is too large Load diff

2001
stage0/stdlib/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.c generated
View file

File diff suppressed because it is too large Load diff

1963
stage0/stdlib/Lean/Server/Watchdog.c generated
View file

File diff suppressed because it is too large Load diff

2126
stage0/stdlib/Lean/Util/Trace.c generated
View file

File diff suppressed because it is too large Load diff

6
stage0/stdlib/Std/Time/DateTime/PlainDateTime.c generated
View file

@ -87,7 +87,6 @@ static lean_object* l_Std_Time_PlainDateTime_instHAddOffset__1___closed__1;
static lean_object* l_Std_Time_instInhabitedPlainDateTime___closed__17;
static lean_object* l_Std_Time_PlainDateTime_ofTimestampAssumingUTC___lambda__2___closed__9;
LEAN_EXPORT lean_object* l_Std_Time_PlainDateTime_addDays___boxed(lean_object*, lean_object*);
lean_object* l_Fin_ofNat(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_x27_loop___at_Std_Time_PlainDateTime_ofTimestampAssumingUTC___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_PlainDateTime_instHAddOffset__5;
static lean_object* l_Std_Time_PlainDateTime_ofTimestampAssumingUTC___lambda__2___closed__3;
@ -204,6 +203,7 @@ LEAN_EXPORT lean_object* l_Std_Time_PlainDateTime_addHours(lean_object*, lean_ob
static lean_object* l_Std_Time_PlainDateTime_ofTimestampAssumingUTC___lambda__2___closed__14;
static lean_object* l_Std_Time_instInhabitedPlainDateTime___closed__35;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* lean_nat_mod(lean_object*, lean_object*);
static lean_object* l_Std_Time_instInhabitedPlainDateTime___closed__39;
LEAN_EXPORT lean_object* l_Std_Time_PlainDateTime_instHAddOffset__6;
LEAN_EXPORT lean_object* l_Std_Time_PlainDateTime_subYearsClip___boxed(lean_object*, lean_object*);
@ -1654,8 +1654,8 @@ lean_inc(x_31);
lean_dec(x_29);
x_32 = l_Int_toNat(x_31);
lean_dec(x_31);
x_33 = lean_unsigned_to_nat(30u);
x_34 = l_Fin_ofNat(x_33, x_32);
x_33 = lean_unsigned_to_nat(31u);
x_34 = lean_nat_mod(x_32, x_33);
lean_dec(x_32);
x_35 = lean_unsigned_to_nat(10u);
x_36 = lean_nat_dec_lt(x_35, x_30);

34
stage0/stdlib/Std/Time/Format.c generated
View file

@ -114,7 +114,6 @@ static lean_object* l_Std_Time_Formats_rfc822___closed__15;
static lean_object* l_Std_Time_Formats_ascTime___closed__16;
LEAN_EXPORT lean_object* l_Std_Time_PlainTime_fromTime24Hour(lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_ZonedDateTime_toRFC822String(lean_object*);
lean_object* l_Fin_ofNat(lean_object*, lean_object*);
static lean_object* l_Std_Time_Formats_rfc850___closed__6;
LEAN_EXPORT lean_object* l_Std_Time_DateTime_fromLongDateFormatString(lean_object*);
static lean_object* l_Std_Time_Formats_leanDateTimeWithIdentifier___closed__10;
@ -183,7 +182,6 @@ static lean_object* l_Std_Time_Formats_dateTime24Hour___closed__13;
LEAN_EXPORT lean_object* l_Std_Time_Formats_time12Hour;
LEAN_EXPORT lean_object* l_Std_Time_PlainTime_fromLeanTime24Hour(lean_object*);
static lean_object* l_Std_Time_Formats_leanDateTimeWithIdentifier___closed__5;
static lean_object* l_Std_Time_PlainTime_fromTime24Hour___lambda__1___closed__1;
static lean_object* l_Std_Time_Formats_iso8601___closed__13;
static lean_object* l_Std_Time_Formats_longDateFormat___closed__7;
static lean_object* l_Std_Time_Formats_longDateFormat___closed__2;
@ -349,7 +347,6 @@ static lean_object* l_Std_Time_Formats_time12Hour___closed__6;
static lean_object* l_Std_Time_Formats_time12Hour___closed__2;
static lean_object* l_Std_Time_Formats_europeanDate___closed__2;
static lean_object* l_Std_Time_Formats_leanDateTimeWithZone___closed__7;
static lean_object* l_Std_Time_PlainTime_fromTime24Hour___lambda__1___closed__2;
static lean_object* l_Std_Time_Formats_leanDateTimeWithIdentifierAndNanos___closed__5;
static lean_object* l_Std_Time_TimeZone_fromTimeZone___closed__3;
static lean_object* l_Std_Time_Formats_ascTime___closed__6;
@ -4550,25 +4547,6 @@ lean_dec(x_1);
return x_3;
}
}
static lean_object* _init_l_Std_Time_PlainTime_fromTime24Hour___lambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(999999999u);
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Fin_ofNat(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Std_Time_PlainTime_fromTime24Hour___lambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Time_PlainTime_fromTime24Hour___lambda__1___closed__1;
x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Std_Time_PlainTime_fromTime24Hour___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -4577,7 +4555,7 @@ x_4 = !lean_is_exclusive(x_3);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = l_Std_Time_PlainTime_fromTime24Hour___lambda__1___closed__2;
x_5 = l_Std_Time_PlainDate_format___lambda__1___closed__2;
x_6 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_2);
@ -4598,7 +4576,7 @@ lean_dec(x_3);
x_10 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_10, 0, x_8);
lean_ctor_set(x_10, 1, x_9);
x_11 = l_Std_Time_PlainTime_fromTime24Hour___lambda__1___closed__2;
x_11 = l_Std_Time_PlainDate_format___lambda__1___closed__2;
x_12 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_12, 0, x_1);
lean_ctor_set(x_12, 1, x_2);
@ -4796,7 +4774,7 @@ if (x_11 == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_12 = l_Std_Time_HourMarker_toAbsolute(x_4, x_1);
x_13 = l_Std_Time_PlainTime_fromTime24Hour___lambda__1___closed__2;
x_13 = l_Std_Time_PlainDate_format___lambda__1___closed__2;
x_14 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_14, 0, x_12);
lean_ctor_set(x_14, 1, x_2);
@ -4818,7 +4796,7 @@ x_18 = l_Std_Time_HourMarker_toAbsolute(x_4, x_1);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_16);
lean_ctor_set(x_19, 1, x_17);
x_20 = l_Std_Time_PlainTime_fromTime24Hour___lambda__1___closed__2;
x_20 = l_Std_Time_PlainDate_format___lambda__1___closed__2;
x_21 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_21, 0, x_18);
lean_ctor_set(x_21, 1, x_2);
@ -7905,10 +7883,6 @@ l_Std_Time_PlainDate_instRepr___closed__4 = _init_l_Std_Time_PlainDate_instRepr_
lean_mark_persistent(l_Std_Time_PlainDate_instRepr___closed__4);
l_Std_Time_PlainTime_format___lambda__1___closed__1 = _init_l_Std_Time_PlainTime_format___lambda__1___closed__1();
lean_mark_persistent(l_Std_Time_PlainTime_format___lambda__1___closed__1);
l_Std_Time_PlainTime_fromTime24Hour___lambda__1___closed__1 = _init_l_Std_Time_PlainTime_fromTime24Hour___lambda__1___closed__1();
lean_mark_persistent(l_Std_Time_PlainTime_fromTime24Hour___lambda__1___closed__1);
l_Std_Time_PlainTime_fromTime24Hour___lambda__1___closed__2 = _init_l_Std_Time_PlainTime_fromTime24Hour___lambda__1___closed__2();
lean_mark_persistent(l_Std_Time_PlainTime_fromTime24Hour___lambda__1___closed__2);
l_Std_Time_PlainTime_fromTime24Hour___closed__1 = _init_l_Std_Time_PlainTime_fromTime24Hour___closed__1();
lean_mark_persistent(l_Std_Time_PlainTime_fromTime24Hour___closed__1);
l_Std_Time_PlainTime_fromLeanTime24Hour___closed__1 = _init_l_Std_Time_PlainTime_fromLeanTime24Hour___closed__1();

613
stage0/stdlib/Std/Time/Format/Basic.c generated
View file

@ -181,7 +181,6 @@ static lean_object* l_Std_Time_Awareness_instInhabitedType___lambda__2___closed_
static lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_formatMonthLong___closed__8;
static lean_object* l_Std_Time_OffsetZ_classify___closed__2;
LEAN_EXPORT lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_reprOffsetO____x40_Std_Time_Format_Basic___hyg_1279____boxed(lean_object*, lean_object*);
static lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__20;
static lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_reprModifier____x40_Std_Time_Format_Basic___hyg_1845____closed__29;
LEAN_EXPORT lean_object* l_Std_Internal_Parsec_manyCharsCore___at___private_Std_Time_Format_Basic_0__Std_Time_parseFormatPart___spec__4(uint32_t, lean_object*, lean_object*);
static lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_reprModifier____x40_Std_Time_Format_Basic___hyg_1845____closed__2;
@ -327,7 +326,6 @@ static lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_parseModifier_
static lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_parseModifier___closed__29;
LEAN_EXPORT lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_formatQuarterLong___boxed(lean_object*);
LEAN_EXPORT lean_object* l_panic___at_Std_Time_GenericFormat_spec_x21___spec__1___rarg(lean_object*);
lean_object* l_Fin_ofNat(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_instInhabitedModifier;
LEAN_EXPORT lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_Awareness_getD___boxed(lean_object*, lean_object*);
static lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_formatMarkerLong___closed__2;
@ -595,7 +593,6 @@ static lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_formatMarkerSh
static lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_reprOffsetO____x40_Std_Time_Format_Basic___hyg_1279____closed__1;
static lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_reprText____x40_Std_Time_Format_Basic___hyg_15____closed__13;
lean_object* lean_int_div(lean_object*, lean_object*);
static lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__19;
static lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_formatWith___closed__5;
static lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_parseFormatPart___closed__4;
LEAN_EXPORT lean_object* l___private_Std_Time_Format_Basic_0__Std_Time_reprOffsetX____x40_Std_Time_Format_Basic___hyg_1001____boxed(lean_object*, lean_object*);
@ -85783,27 +85780,28 @@ static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericF
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(999999999u);
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Fin_ofNat(x_1, x_2);
x_1 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__27;
x_2 = l___private_Std_Time_Format_Basic_0__Std_Time_reprText____x40_Std_Time_Format_Basic___hyg_15____closed__6;
x_3 = lean_int_add(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__4;
x_2 = lean_nat_to_int(x_1);
return x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__21;
x_2 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__4;
x_3 = lean_int_emod(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__27;
x_2 = l___private_Std_Time_Format_Basic_0__Std_Time_reprText____x40_Std_Time_Format_Basic___hyg_15____closed__6;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__5;
x_2 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__4;
x_3 = lean_int_add(x_1, x_2);
return x_3;
}
@ -85812,8 +85810,8 @@ static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericF
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__21;
x_2 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__6;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__6;
x_2 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__4;
x_3 = lean_int_emod(x_1, x_2);
return x_3;
}
@ -85823,7 +85821,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__7;
x_2 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__6;
x_2 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__1;
x_3 = lean_int_add(x_1, x_2);
return x_3;
}
@ -85831,29 +85829,9 @@ return x_3;
static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__8;
x_2 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__6;
x_3 = lean_int_emod(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__9;
x_2 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__1;
x_3 = lean_int_add(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__11() {
_start:
{
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = 0;
x_2 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__10;
x_2 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__8;
x_3 = lean_box(x_1);
x_4 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_4, 0, x_3);
@ -85861,7 +85839,7 @@ lean_ctor_set(x_4, 1, x_2);
return x_4;
}
}
static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__12() {
static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -85871,6 +85849,26 @@ x_3 = lean_int_sub(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__10;
x_2 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__12;
x_3 = lean_int_emod(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__11;
x_2 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__12;
x_3 = lean_int_add(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__13() {
_start:
{
@ -85886,7 +85884,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__13;
x_2 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__12;
x_2 = l___private_Std_Time_Format_Basic_0__Std_Time_reprText____x40_Std_Time_Format_Basic___hyg_15____closed__6;
x_3 = lean_int_add(x_1, x_2);
return x_3;
}
@ -85895,8 +85893,8 @@ static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericF
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__14;
x_2 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__12;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__10;
x_2 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__4;
x_3 = lean_int_emod(x_1, x_2);
return x_3;
}
@ -85906,7 +85904,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__15;
x_2 = l___private_Std_Time_Format_Basic_0__Std_Time_reprText____x40_Std_Time_Format_Basic___hyg_15____closed__6;
x_2 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__4;
x_3 = lean_int_add(x_1, x_2);
return x_3;
}
@ -85915,7 +85913,7 @@ static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericF
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__12;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__16;
x_2 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__4;
x_3 = lean_int_emod(x_1, x_2);
return x_3;
@ -85926,26 +85924,6 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__17;
x_2 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__4;
x_3 = lean_int_add(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__19() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__18;
x_2 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__4;
x_3 = lean_int_emod(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__20() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__19;
x_2 = l___private_Std_Time_Format_Basic_0__Std_Time_reprText____x40_Std_Time_Format_Basic___hyg_15____closed__6;
x_3 = lean_int_add(x_1, x_2);
return x_3;
@ -85981,64 +85959,64 @@ x_64 = lean_ctor_get(x_1, 22);
lean_inc(x_64);
if (lean_obj_tag(x_53) == 0)
{
lean_object* x_234;
x_234 = lean_ctor_get(x_1, 27);
lean_inc(x_234);
if (lean_obj_tag(x_234) == 0)
{
lean_object* x_235;
x_235 = lean_ctor_get(x_1, 27);
x_235 = lean_ctor_get(x_1, 28);
lean_inc(x_235);
if (lean_obj_tag(x_235) == 0)
{
lean_object* x_236;
x_236 = lean_ctor_get(x_1, 28);
x_236 = lean_ctor_get(x_1, 29);
lean_inc(x_236);
if (lean_obj_tag(x_236) == 0)
{
lean_object* x_237;
x_237 = lean_ctor_get(x_1, 29);
lean_inc(x_237);
if (lean_obj_tag(x_237) == 0)
x_237 = l_Std_Time_TimeZone_Offset_zero;
x_65 = x_237;
goto block_233;
}
else
{
lean_object* x_238;
x_238 = l_Std_Time_TimeZone_Offset_zero;
x_238 = lean_ctor_get(x_236, 0);
lean_inc(x_238);
lean_dec(x_236);
x_65 = x_238;
goto block_234;
goto block_233;
}
}
else
{
lean_object* x_239;
x_239 = lean_ctor_get(x_237, 0);
x_239 = lean_ctor_get(x_235, 0);
lean_inc(x_239);
lean_dec(x_237);
lean_dec(x_235);
x_65 = x_239;
goto block_234;
goto block_233;
}
}
else
{
lean_object* x_240;
x_240 = lean_ctor_get(x_236, 0);
x_240 = lean_ctor_get(x_234, 0);
lean_inc(x_240);
lean_dec(x_236);
lean_dec(x_234);
x_65 = x_240;
goto block_234;
goto block_233;
}
}
else
{
lean_object* x_241;
x_241 = lean_ctor_get(x_235, 0);
x_241 = lean_ctor_get(x_53, 0);
lean_inc(x_241);
lean_dec(x_235);
x_65 = x_241;
goto block_234;
}
}
else
{
lean_object* x_242;
x_242 = lean_ctor_get(x_53, 0);
lean_inc(x_242);
lean_dec(x_53);
x_65 = x_242;
goto block_234;
x_65 = x_241;
goto block_233;
}
block_52:
{
@ -86147,81 +86125,81 @@ return x_51;
}
}
}
block_234:
block_233:
{
lean_object* x_66;
if (lean_obj_tag(x_54) == 0)
{
lean_object* x_229;
x_229 = lean_ctor_get(x_1, 24);
lean_inc(x_229);
if (lean_obj_tag(x_229) == 0)
lean_object* x_228;
x_228 = lean_ctor_get(x_1, 24);
lean_inc(x_228);
if (lean_obj_tag(x_228) == 0)
{
uint8_t x_230; lean_object* x_231;
x_230 = 1;
uint8_t x_229; lean_object* x_230;
x_229 = 1;
lean_inc(x_65);
x_231 = l_Std_Time_TimeZone_Offset_toIsoString(x_65, x_230);
x_230 = l_Std_Time_TimeZone_Offset_toIsoString(x_65, x_229);
x_66 = x_230;
goto block_227;
}
else
{
lean_object* x_231;
x_231 = lean_ctor_get(x_228, 0);
lean_inc(x_231);
lean_dec(x_228);
x_66 = x_231;
goto block_228;
goto block_227;
}
}
else
{
lean_object* x_232;
x_232 = lean_ctor_get(x_229, 0);
x_232 = lean_ctor_get(x_54, 0);
lean_inc(x_232);
lean_dec(x_229);
x_66 = x_232;
goto block_228;
}
}
else
{
lean_object* x_233;
x_233 = lean_ctor_get(x_54, 0);
lean_inc(x_233);
lean_dec(x_54);
x_66 = x_233;
goto block_228;
x_66 = x_232;
goto block_227;
}
block_228:
block_227:
{
lean_object* x_67;
if (lean_obj_tag(x_55) == 0)
{
uint8_t x_225; lean_object* x_226;
x_225 = 1;
uint8_t x_224; lean_object* x_225;
x_224 = 1;
lean_inc(x_65);
x_226 = l_Std_Time_TimeZone_Offset_toIsoString(x_65, x_225);
x_67 = x_226;
goto block_224;
x_225 = l_Std_Time_TimeZone_Offset_toIsoString(x_65, x_224);
x_67 = x_225;
goto block_223;
}
else
{
lean_object* x_227;
x_227 = lean_ctor_get(x_55, 0);
lean_inc(x_227);
lean_object* x_226;
x_226 = lean_ctor_get(x_55, 0);
lean_inc(x_226);
lean_dec(x_55);
x_67 = x_227;
goto block_224;
x_67 = x_226;
goto block_223;
}
block_224:
block_223:
{
lean_object* x_68; lean_object* x_118;
if (lean_obj_tag(x_56) == 0)
{
lean_object* x_222;
x_222 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__20;
x_118 = x_222;
goto block_221;
lean_object* x_221;
x_221 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__18;
x_118 = x_221;
goto block_220;
}
else
{
lean_object* x_223;
x_223 = lean_ctor_get(x_56, 0);
lean_inc(x_223);
lean_object* x_222;
x_222 = lean_ctor_get(x_56, 0);
lean_inc(x_222);
lean_dec(x_56);
x_118 = x_223;
goto block_221;
x_118 = x_222;
goto block_220;
}
block_117:
{
@ -86385,111 +86363,111 @@ return x_99;
}
}
}
block_221:
block_220:
{
lean_object* x_119;
if (lean_obj_tag(x_57) == 0)
{
lean_object* x_219;
x_219 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__16;
x_119 = x_219;
goto block_218;
lean_object* x_218;
x_218 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__14;
x_119 = x_218;
goto block_217;
}
else
{
lean_object* x_220;
x_220 = lean_ctor_get(x_57, 0);
lean_inc(x_220);
lean_object* x_219;
x_219 = lean_ctor_get(x_57, 0);
lean_inc(x_219);
lean_dec(x_57);
x_119 = x_220;
goto block_218;
x_119 = x_219;
goto block_217;
}
block_218:
block_217:
{
lean_object* x_120;
if (lean_obj_tag(x_58) == 0)
{
if (lean_obj_tag(x_59) == 0)
{
lean_object* x_204;
x_204 = lean_ctor_get(x_1, 1);
lean_inc(x_204);
if (lean_obj_tag(x_204) == 0)
{
lean_object* x_205;
x_205 = lean_ctor_get(x_1, 1);
lean_inc(x_205);
if (lean_obj_tag(x_205) == 0)
{
lean_object* x_206;
x_206 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__1;
x_120 = x_206;
goto block_204;
x_205 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__1;
x_120 = x_205;
goto block_203;
}
else
{
lean_object* x_207; uint8_t x_208; lean_object* x_209;
x_207 = lean_ctor_get(x_205, 0);
lean_inc(x_207);
lean_dec(x_205);
x_208 = 1;
x_209 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_convertYearAndEra(x_207, x_208);
lean_dec(x_207);
x_120 = x_209;
goto block_204;
lean_object* x_206; uint8_t x_207; lean_object* x_208;
x_206 = lean_ctor_get(x_204, 0);
lean_inc(x_206);
lean_dec(x_204);
x_207 = 1;
x_208 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_convertYearAndEra(x_206, x_207);
lean_dec(x_206);
x_120 = x_208;
goto block_203;
}
}
else
{
lean_object* x_210;
x_210 = lean_ctor_get(x_59, 0);
lean_inc(x_210);
lean_object* x_209;
x_209 = lean_ctor_get(x_59, 0);
lean_inc(x_209);
lean_dec(x_59);
x_120 = x_210;
goto block_204;
x_120 = x_209;
goto block_203;
}
}
else
{
if (lean_obj_tag(x_59) == 0)
{
lean_object* x_210;
x_210 = lean_ctor_get(x_1, 1);
lean_inc(x_210);
if (lean_obj_tag(x_210) == 0)
{
lean_object* x_211;
x_211 = lean_ctor_get(x_1, 1);
lean_inc(x_211);
if (lean_obj_tag(x_211) == 0)
{
lean_object* x_212;
lean_dec(x_58);
x_212 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__1;
x_120 = x_212;
goto block_204;
x_211 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__1;
x_120 = x_211;
goto block_203;
}
else
{
lean_object* x_213; lean_object* x_214; uint8_t x_215; lean_object* x_216;
x_213 = lean_ctor_get(x_58, 0);
lean_object* x_212; lean_object* x_213; uint8_t x_214; lean_object* x_215;
x_212 = lean_ctor_get(x_58, 0);
lean_inc(x_212);
lean_dec(x_58);
x_213 = lean_ctor_get(x_210, 0);
lean_inc(x_213);
lean_dec(x_58);
x_214 = lean_ctor_get(x_211, 0);
lean_inc(x_214);
lean_dec(x_211);
x_215 = lean_unbox(x_213);
lean_dec(x_210);
x_214 = lean_unbox(x_212);
lean_dec(x_212);
x_215 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_convertYearAndEra(x_213, x_214);
lean_dec(x_213);
x_216 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_convertYearAndEra(x_214, x_215);
lean_dec(x_214);
x_120 = x_216;
goto block_204;
x_120 = x_215;
goto block_203;
}
}
else
{
lean_object* x_217;
lean_object* x_216;
lean_dec(x_58);
x_217 = lean_ctor_get(x_59, 0);
lean_inc(x_217);
x_216 = lean_ctor_get(x_59, 0);
lean_inc(x_216);
lean_dec(x_59);
x_120 = x_217;
goto block_204;
x_120 = x_216;
goto block_203;
}
}
block_204:
block_203:
{
lean_object* x_121; lean_object* x_122; lean_object* x_123; uint8_t x_124; lean_object* x_125; lean_object* x_148; lean_object* x_180;
lean_object* x_121; lean_object* x_122; lean_object* x_123; uint8_t x_124; lean_object* x_125; lean_object* x_148; lean_object* x_179;
x_121 = l___private_Std_Time_Format_Basic_0__Std_Time_dateFromModifier___closed__1;
x_122 = lean_int_mod(x_120, x_121);
x_123 = l_Std_Time_Awareness_instInhabitedType___lambda__2___closed__1;
@ -86497,64 +86475,64 @@ x_124 = lean_int_dec_eq(x_122, x_123);
lean_dec(x_122);
if (lean_obj_tag(x_60) == 0)
{
lean_object* x_190;
x_190 = lean_box(0);
x_180 = x_190;
goto block_189;
lean_object* x_189;
x_189 = lean_box(0);
x_179 = x_189;
goto block_188;
}
else
{
lean_object* x_190;
x_190 = lean_ctor_get(x_1, 13);
lean_inc(x_190);
if (lean_obj_tag(x_190) == 0)
{
lean_object* x_191;
x_191 = lean_ctor_get(x_1, 13);
x_191 = lean_ctor_get(x_1, 14);
lean_inc(x_191);
if (lean_obj_tag(x_191) == 0)
{
lean_object* x_192;
x_192 = lean_ctor_get(x_1, 14);
lean_inc(x_192);
if (lean_obj_tag(x_192) == 0)
{
lean_object* x_193;
lean_dec(x_60);
x_193 = lean_box(0);
x_180 = x_193;
goto block_189;
x_192 = lean_box(0);
x_179 = x_192;
goto block_188;
}
else
{
lean_object* x_194; lean_object* x_195; lean_object* x_196; lean_object* x_197; uint8_t x_198; lean_object* x_199;
x_194 = lean_ctor_get(x_60, 0);
lean_object* x_193; lean_object* x_194; lean_object* x_195; lean_object* x_196; uint8_t x_197; lean_object* x_198;
x_193 = lean_ctor_get(x_60, 0);
lean_inc(x_193);
lean_dec(x_60);
x_194 = lean_ctor_get(x_191, 0);
lean_inc(x_194);
lean_dec(x_60);
x_195 = lean_ctor_get(x_192, 0);
lean_inc(x_195);
lean_dec(x_192);
x_196 = l___private_Std_Time_Format_Basic_0__Std_Time_reprText____x40_Std_Time_Format_Basic___hyg_15____closed__6;
x_197 = lean_int_add(x_195, x_196);
lean_dec(x_195);
x_198 = lean_unbox(x_194);
lean_dec(x_191);
x_195 = l___private_Std_Time_Format_Basic_0__Std_Time_reprText____x40_Std_Time_Format_Basic___hyg_15____closed__6;
x_196 = lean_int_add(x_194, x_195);
lean_dec(x_194);
x_199 = l_Std_Time_HourMarker_toAbsolute(x_198, x_197);
lean_dec(x_197);
x_148 = x_199;
goto block_179;
x_197 = lean_unbox(x_193);
lean_dec(x_193);
x_198 = l_Std_Time_HourMarker_toAbsolute(x_197, x_196);
lean_dec(x_196);
x_148 = x_198;
goto block_178;
}
}
else
{
lean_object* x_200; lean_object* x_201; uint8_t x_202; lean_object* x_203;
x_200 = lean_ctor_get(x_60, 0);
lean_inc(x_200);
lean_object* x_199; lean_object* x_200; uint8_t x_201; lean_object* x_202;
x_199 = lean_ctor_get(x_60, 0);
lean_inc(x_199);
lean_dec(x_60);
x_201 = lean_ctor_get(x_191, 0);
lean_inc(x_201);
lean_dec(x_191);
x_202 = lean_unbox(x_200);
x_200 = lean_ctor_get(x_190, 0);
lean_inc(x_200);
lean_dec(x_190);
x_201 = lean_unbox(x_199);
lean_dec(x_199);
x_202 = l_Std_Time_HourMarker_toAbsolute(x_201, x_200);
lean_dec(x_200);
x_203 = l_Std_Time_HourMarker_toAbsolute(x_202, x_201);
lean_dec(x_201);
x_148 = x_203;
goto block_179;
x_148 = x_202;
goto block_178;
}
}
block_147:
@ -86667,45 +86645,45 @@ goto block_117;
}
}
}
block_179:
block_178:
{
lean_object* x_149;
if (lean_obj_tag(x_61) == 0)
{
lean_object* x_177;
x_177 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__10;
x_149 = x_177;
goto block_176;
lean_object* x_176;
x_176 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__8;
x_149 = x_176;
goto block_175;
}
else
{
lean_object* x_178;
x_178 = lean_ctor_get(x_61, 0);
lean_inc(x_178);
lean_object* x_177;
x_177 = lean_ctor_get(x_61, 0);
lean_inc(x_177);
lean_dec(x_61);
x_149 = x_178;
goto block_176;
x_149 = x_177;
goto block_175;
}
block_176:
block_175:
{
lean_object* x_150;
if (lean_obj_tag(x_62) == 0)
{
lean_object* x_174;
x_174 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__11;
x_150 = x_174;
goto block_173;
lean_object* x_173;
x_173 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__9;
x_150 = x_173;
goto block_172;
}
else
{
lean_object* x_175;
x_175 = lean_ctor_get(x_62, 0);
lean_inc(x_175);
lean_object* x_174;
x_174 = lean_ctor_get(x_62, 0);
lean_inc(x_174);
lean_dec(x_62);
x_150 = x_175;
goto block_173;
x_150 = x_174;
goto block_172;
}
block_173:
block_172:
{
lean_object* x_151;
if (lean_obj_tag(x_63) == 0)
@ -86723,67 +86701,66 @@ lean_inc(x_162);
lean_dec(x_1);
if (lean_obj_tag(x_162) == 0)
{
lean_object* x_163; lean_object* x_164;
x_163 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__5;
x_164 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_164, 0, x_148);
lean_ctor_set(x_164, 1, x_149);
lean_ctor_set(x_164, 2, x_150);
lean_ctor_set(x_164, 3, x_163);
x_125 = x_164;
lean_object* x_163;
x_163 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_163, 0, x_148);
lean_ctor_set(x_163, 1, x_149);
lean_ctor_set(x_163, 2, x_150);
lean_ctor_set(x_163, 3, x_123);
x_125 = x_163;
goto block_147;
}
else
{
lean_object* x_165; lean_object* x_166; lean_object* x_167; lean_object* x_168;
lean_object* x_164; lean_object* x_165; lean_object* x_166; lean_object* x_167;
lean_dec(x_150);
lean_dec(x_149);
lean_dec(x_148);
x_165 = lean_ctor_get(x_162, 0);
lean_inc(x_165);
x_164 = lean_ctor_get(x_162, 0);
lean_inc(x_164);
lean_dec(x_162);
x_166 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__3;
x_167 = lean_int_mul(x_165, x_166);
lean_dec(x_165);
x_168 = l_Std_Time_PlainTime_ofNanoseconds(x_167);
lean_dec(x_167);
x_125 = x_168;
x_165 = l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__3;
x_166 = lean_int_mul(x_164, x_165);
lean_dec(x_164);
x_167 = l_Std_Time_PlainTime_ofNanoseconds(x_166);
lean_dec(x_166);
x_125 = x_167;
goto block_147;
}
}
else
{
lean_object* x_169; lean_object* x_170;
lean_object* x_168; lean_object* x_169;
lean_dec(x_150);
lean_dec(x_149);
lean_dec(x_148);
lean_dec(x_1);
x_169 = lean_ctor_get(x_64, 0);
lean_inc(x_169);
x_168 = lean_ctor_get(x_64, 0);
lean_inc(x_168);
lean_dec(x_64);
x_170 = l_Std_Time_PlainTime_ofNanoseconds(x_169);
lean_dec(x_169);
x_125 = x_170;
x_169 = l_Std_Time_PlainTime_ofNanoseconds(x_168);
lean_dec(x_168);
x_125 = x_169;
goto block_147;
}
}
else
{
lean_object* x_171;
x_171 = lean_ctor_get(x_161, 0);
lean_inc(x_171);
lean_object* x_170;
x_170 = lean_ctor_get(x_161, 0);
lean_inc(x_170);
lean_dec(x_161);
x_151 = x_171;
x_151 = x_170;
goto block_160;
}
}
else
{
lean_object* x_172;
x_172 = lean_ctor_get(x_63, 0);
lean_inc(x_172);
lean_object* x_171;
x_171 = lean_ctor_get(x_63, 0);
lean_inc(x_171);
lean_dec(x_63);
x_151 = x_172;
x_151 = x_171;
goto block_160;
}
block_160:
@ -86844,58 +86821,58 @@ goto block_147;
}
}
}
block_189:
block_188:
{
lean_object* x_180;
lean_dec(x_179);
x_180 = lean_ctor_get(x_1, 15);
lean_inc(x_180);
if (lean_obj_tag(x_180) == 0)
{
lean_object* x_181;
lean_dec(x_180);
x_181 = lean_ctor_get(x_1, 15);
x_181 = lean_ctor_get(x_1, 16);
lean_inc(x_181);
if (lean_obj_tag(x_181) == 0)
{
lean_object* x_182;
x_182 = lean_ctor_get(x_1, 16);
lean_inc(x_182);
if (lean_obj_tag(x_182) == 0)
{
x_148 = x_123;
goto block_179;
goto block_178;
}
else
{
lean_object* x_182;
x_182 = lean_ctor_get(x_181, 0);
lean_inc(x_182);
lean_dec(x_181);
x_148 = x_182;
goto block_178;
}
}
else
{
lean_object* x_183;
x_183 = lean_ctor_get(x_182, 0);
x_183 = lean_ctor_get(x_1, 16);
lean_inc(x_183);
lean_dec(x_182);
x_148 = x_183;
goto block_179;
}
}
else
if (lean_obj_tag(x_183) == 0)
{
lean_object* x_184;
x_184 = lean_ctor_get(x_1, 16);
lean_object* x_184; lean_object* x_185; lean_object* x_186;
x_184 = lean_ctor_get(x_180, 0);
lean_inc(x_184);
if (lean_obj_tag(x_184) == 0)
{
lean_object* x_185; lean_object* x_186; lean_object* x_187;
x_185 = lean_ctor_get(x_181, 0);
lean_inc(x_185);
lean_dec(x_181);
x_186 = l___private_Std_Time_Format_Basic_0__Std_Time_parseOffset___closed__8;
x_187 = lean_int_add(x_185, x_186);
lean_dec(x_185);
x_148 = x_187;
goto block_179;
lean_dec(x_180);
x_185 = l___private_Std_Time_Format_Basic_0__Std_Time_parseOffset___closed__8;
x_186 = lean_int_add(x_184, x_185);
lean_dec(x_184);
x_148 = x_186;
goto block_178;
}
else
{
lean_object* x_188;
lean_dec(x_181);
x_188 = lean_ctor_get(x_184, 0);
lean_inc(x_188);
lean_dec(x_184);
x_148 = x_188;
goto block_179;
lean_object* x_187;
lean_dec(x_180);
x_187 = lean_ctor_get(x_183, 0);
lean_inc(x_187);
lean_dec(x_183);
x_148 = x_187;
goto block_178;
}
}
}
@ -89490,10 +89467,6 @@ l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___
lean_mark_persistent(l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__17);
l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__18 = _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__18();
lean_mark_persistent(l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__18);
l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__19 = _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__19();
lean_mark_persistent(l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__19);
l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__20 = _init_l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__20();
lean_mark_persistent(l___private_Std_Time_Format_Basic_0__Std_Time_GenericFormat_DateBuilder_build___closed__20);
l_Std_Time_GenericFormat_spec_x21___closed__1 = _init_l_Std_Time_GenericFormat_spec_x21___closed__1();
lean_mark_persistent(l_Std_Time_GenericFormat_spec_x21___closed__1);
l_Std_Time_GenericFormat_spec_x21___closed__2 = _init_l_Std_Time_GenericFormat_spec_x21___closed__2();

32
stage0/stdlib/Std/Time/Time/PlainTime.c generated
View file

@ -50,16 +50,13 @@ LEAN_EXPORT lean_object* l_Std_Time_PlainTime_addHours___boxed(lean_object*, lea
static lean_object* l_Std_Time_instReprPlainTime___closed__1;
lean_object* lean_int_emod(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_PlainTime_instHAddOffset__1;
static lean_object* l_Std_Time_PlainTime_midnight___closed__4;
static lean_object* l_Std_Time_PlainTime_instHAddOffset__1___closed__1;
static lean_object* l_Std_Time_instInhabitedPlainTime___closed__3;
static lean_object* l_Std_Time_PlainTime_midnight___closed__3;
LEAN_EXPORT lean_object* l_Std_Time_PlainTime_subMilliseconds(lean_object*, lean_object*);
static lean_object* l___private_Std_Time_Time_PlainTime_0__Std_Time_reprPlainTime____x40_Std_Time_Time_PlainTime___hyg_43____closed__3;
LEAN_EXPORT lean_object* l_Std_Time_PlainTime_addSeconds___boxed(lean_object*, lean_object*);
static lean_object* l___private_Std_Time_Time_PlainTime_0__Std_Time_reprPlainTime____x40_Std_Time_Time_PlainTime___hyg_43____closed__33;
static lean_object* l___private_Std_Time_Time_PlainTime_0__Std_Time_reprPlainTime____x40_Std_Time_Time_PlainTime___hyg_43____closed__8;
lean_object* l_Fin_ofNat(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_instBEqPlainTime___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_PlainTime_instHSubOffset__1;
static lean_object* l___private_Std_Time_Time_PlainTime_0__Std_Time_reprPlainTime____x40_Std_Time_Time_PlainTime___hyg_43____closed__27;
@ -1341,30 +1338,11 @@ return x_4;
static lean_object* _init_l_Std_Time_PlainTime_midnight___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(999999999u);
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Fin_ofNat(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Std_Time_PlainTime_midnight___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Time_PlainTime_midnight___closed__2;
x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
static lean_object* _init_l_Std_Time_PlainTime_midnight___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Std_Time_instInhabitedPlainTime___closed__10;
x_2 = l_Std_Time_instInhabitedPlainTime___closed__18;
x_3 = l_Std_Time_PlainTime_midnight___closed__1;
x_4 = l_Std_Time_PlainTime_midnight___closed__3;
x_4 = l___private_Std_Time_Time_PlainTime_0__Std_Time_reprPlainTime____x40_Std_Time_Time_PlainTime___hyg_43____closed__8;
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -1377,7 +1355,7 @@ static lean_object* _init_l_Std_Time_PlainTime_midnight() {
_start:
{
lean_object* x_1;
x_1 = l_Std_Time_PlainTime_midnight___closed__4;
x_1 = l_Std_Time_PlainTime_midnight___closed__2;
return x_1;
}
}
@ -1415,7 +1393,7 @@ x_5 = lean_box(x_1);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_5);
lean_ctor_set(x_6, 1, x_4);
x_7 = l_Std_Time_PlainTime_midnight___closed__3;
x_7 = l___private_Std_Time_Time_PlainTime_0__Std_Time_reprPlainTime____x40_Std_Time_Time_PlainTime___hyg_43____closed__8;
x_8 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_8, 0, x_2);
lean_ctor_set(x_8, 1, x_3);
@ -2535,10 +2513,6 @@ l_Std_Time_PlainTime_midnight___closed__1 = _init_l_Std_Time_PlainTime_midnight_
lean_mark_persistent(l_Std_Time_PlainTime_midnight___closed__1);
l_Std_Time_PlainTime_midnight___closed__2 = _init_l_Std_Time_PlainTime_midnight___closed__2();
lean_mark_persistent(l_Std_Time_PlainTime_midnight___closed__2);
l_Std_Time_PlainTime_midnight___closed__3 = _init_l_Std_Time_PlainTime_midnight___closed__3();
lean_mark_persistent(l_Std_Time_PlainTime_midnight___closed__3);
l_Std_Time_PlainTime_midnight___closed__4 = _init_l_Std_Time_PlainTime_midnight___closed__4();
lean_mark_persistent(l_Std_Time_PlainTime_midnight___closed__4);
l_Std_Time_PlainTime_midnight = _init_l_Std_Time_PlainTime_midnight();
lean_mark_persistent(l_Std_Time_PlainTime_midnight);
l_Std_Time_PlainTime_toMilliseconds___closed__1 = _init_l_Std_Time_PlainTime_toMilliseconds___closed__1();

39
stage0/stdlib/Std/Time/Time/Unit/Nanosecond.c generated
View file

@ -34,7 +34,6 @@ LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_instOffsetLE;
uint8_t lean_int_dec_le(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_instOffsetNeg;
LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_Span_toOffset(lean_object*);
lean_object* l_Fin_ofNat(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_Ordinal_ofInt(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_Offset_ofNat(lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_instSpanLE;
@ -47,7 +46,6 @@ LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_instDecidableLtOrdinal___boxed(le
LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_Ordinal_toOffset(lean_object*);
static lean_object* l_Std_Time_Nanosecond_instInhabitedOrdinal___closed__1;
static lean_object* l_Std_Time_Nanosecond_instOrdinalRepr___closed__1;
static lean_object* l_Std_Time_Nanosecond_instOffsetInhabited___closed__1;
LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_instOrdinalLT;
lean_object* l_Std_Time_Internal_UnitVal_add___rarg___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_instOfNatOrdinal(lean_object*);
@ -64,6 +62,7 @@ LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_Ordinal_instOfDayLT;
LEAN_EXPORT uint8_t l_Std_Time_Nanosecond_instDecidableLtOrdinal(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_instSpanBEq;
LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_instSpanLT;
lean_object* lean_nat_mod(lean_object*, lean_object*);
lean_object* l_Std_Time_Internal_UnitVal_instRepr___rarg___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_Ordinal_instOfDayLE;
uint8_t lean_int_dec_lt(lean_object*, lean_object*);
@ -76,7 +75,6 @@ LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_instInhabitedOrdinal;
LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_instOffsetSub;
static lean_object* l_Std_Time_Nanosecond_instOffsetRepr___closed__1;
lean_object* l_Std_Time_Internal_Bounded_instBEq___rarg___boxed(lean_object*, lean_object*);
static lean_object* l_Std_Time_Nanosecond_instInhabitedOrdinal___closed__2;
LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_instOffsetBEq;
static lean_object* l_Std_Time_Nanosecond_instOffsetNeg___closed__1;
static lean_object* _init_l_Std_Time_Nanosecond_instOrdinalRepr___closed__1() {
@ -131,8 +129,8 @@ LEAN_EXPORT lean_object* l_Std_Time_Nanosecond_instOfNatOrdinal(lean_object* x_1
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = lean_unsigned_to_nat(999999999u);
x_3 = l_Fin_ofNat(x_2, x_1);
x_2 = lean_unsigned_to_nat(1000000000u);
x_3 = lean_nat_mod(x_1, x_2);
x_4 = lean_nat_to_int(x_3);
return x_4;
}
@ -149,18 +147,8 @@ return x_2;
static lean_object* _init_l_Std_Time_Nanosecond_instInhabitedOrdinal___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(999999999u);
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Fin_ofNat(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Std_Time_Nanosecond_instInhabitedOrdinal___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Time_Nanosecond_instInhabitedOrdinal___closed__1;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_nat_to_int(x_1);
return x_2;
}
@ -169,7 +157,7 @@ static lean_object* _init_l_Std_Time_Nanosecond_instInhabitedOrdinal() {
_start:
{
lean_object* x_1;
x_1 = l_Std_Time_Nanosecond_instInhabitedOrdinal___closed__2;
x_1 = l_Std_Time_Nanosecond_instInhabitedOrdinal___closed__1;
return x_1;
}
}
@ -243,20 +231,11 @@ x_1 = l_Std_Time_Nanosecond_instOffsetBEq___closed__1;
return x_1;
}
}
static lean_object* _init_l_Std_Time_Nanosecond_instOffsetInhabited___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
static lean_object* _init_l_Std_Time_Nanosecond_instOffsetInhabited() {
_start:
{
lean_object* x_1;
x_1 = l_Std_Time_Nanosecond_instOffsetInhabited___closed__1;
x_1 = l_Std_Time_Nanosecond_instInhabitedOrdinal___closed__1;
return x_1;
}
}
@ -427,7 +406,7 @@ static lean_object* _init_l_Std_Time_Nanosecond_instInhabitedSpan() {
_start:
{
lean_object* x_1;
x_1 = l_Std_Time_Nanosecond_instOffsetInhabited___closed__1;
x_1 = l_Std_Time_Nanosecond_instInhabitedOrdinal___closed__1;
return x_1;
}
}
@ -554,8 +533,6 @@ l_Std_Time_Nanosecond_instOrdinalLT = _init_l_Std_Time_Nanosecond_instOrdinalLT(
lean_mark_persistent(l_Std_Time_Nanosecond_instOrdinalLT);
l_Std_Time_Nanosecond_instInhabitedOrdinal___closed__1 = _init_l_Std_Time_Nanosecond_instInhabitedOrdinal___closed__1();
lean_mark_persistent(l_Std_Time_Nanosecond_instInhabitedOrdinal___closed__1);
l_Std_Time_Nanosecond_instInhabitedOrdinal___closed__2 = _init_l_Std_Time_Nanosecond_instInhabitedOrdinal___closed__2();
lean_mark_persistent(l_Std_Time_Nanosecond_instInhabitedOrdinal___closed__2);
l_Std_Time_Nanosecond_instInhabitedOrdinal = _init_l_Std_Time_Nanosecond_instInhabitedOrdinal();
lean_mark_persistent(l_Std_Time_Nanosecond_instInhabitedOrdinal);
l_Std_Time_Nanosecond_instOffsetRepr___closed__1 = _init_l_Std_Time_Nanosecond_instOffsetRepr___closed__1();
@ -566,8 +543,6 @@ l_Std_Time_Nanosecond_instOffsetBEq___closed__1 = _init_l_Std_Time_Nanosecond_in
lean_mark_persistent(l_Std_Time_Nanosecond_instOffsetBEq___closed__1);
l_Std_Time_Nanosecond_instOffsetBEq = _init_l_Std_Time_Nanosecond_instOffsetBEq();
lean_mark_persistent(l_Std_Time_Nanosecond_instOffsetBEq);
l_Std_Time_Nanosecond_instOffsetInhabited___closed__1 = _init_l_Std_Time_Nanosecond_instOffsetInhabited___closed__1();
lean_mark_persistent(l_Std_Time_Nanosecond_instOffsetInhabited___closed__1);
l_Std_Time_Nanosecond_instOffsetInhabited = _init_l_Std_Time_Nanosecond_instOffsetInhabited();
lean_mark_persistent(l_Std_Time_Nanosecond_instOffsetInhabited);
l_Std_Time_Nanosecond_instOffsetAdd___closed__1 = _init_l_Std_Time_Nanosecond_instOffsetAdd___closed__1();

579
stage0/stdlib/Std/Time/Zoned/Database.c generated
View file

@ -13,29 +13,467 @@
#ifdef __cplusplus
extern "C" {
#endif
LEAN_EXPORT lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__9;
static uint64_t l_Std_Time_Database_defaultGetLocalZoneRules___closed__2;
lean_object* lean_io_getenv(lean_object*, lean_object*);
lean_object* l_Std_Time_Database_TZdb_localRules(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_Database_defaultGetLocalZoneRules(lean_object*);
static uint64_t l_Std_Time_Database_defaultGetLocalZoneRules___closed__3;
static lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__5;
lean_object* l_System_FilePath_pathExists(lean_object*, lean_object*);
static lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__8;
LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Std_Time_Database_defaultGetZoneRules___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint64_t lean_int64_neg(uint64_t);
static lean_object* l_Std_Time_Database_defaultGetLocalZoneRules___closed__4;
static lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__7;
LEAN_EXPORT lean_object* l_Std_Time_Database_defaultGetLocalZoneRules___closed__4___boxed__const__1;
static size_t l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__11;
static lean_object* l_Std_Time_Database_defaultGetZoneRules___closed__1;
static lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__10;
static lean_object* l_Std_Time_Database_defaultGetLocalZoneRules___closed__5;
static lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__3;
lean_object* l_Std_Time_Database_Windows_getLocalTimeZoneIdentifierAt___boxed(lean_object*, lean_object*);
static lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__6;
uint64_t lean_int64_of_nat(lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__1___closed__1;
lean_object* l_Bind_bindLeft___at_Std_Time_Database_WindowsDb_inst___spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Std_Time_Database_defaultGetZoneRules___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*);
lean_object* lean_array_mk(lean_object*);
lean_object* l_Std_Time_Database_Windows_getZoneRules___boxed(lean_object*, lean_object*);
size_t lean_usize_add(size_t, size_t);
lean_object* lean_array_uget(lean_object*, size_t);
size_t lean_array_size(lean_object*);
lean_object* l_Std_Time_Database_TZdb_readRulesFromDisk(lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__4;
static lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__2;
lean_object* lean_string_append(lean_object*, lean_object*);
uint8_t lean_usize_dec_lt(size_t, size_t);
static lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__1;
LEAN_EXPORT lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__2(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_Database_defaultGetZoneRules(lean_object*, lean_object*);
extern uint8_t l_System_Platform_isWindows;
static lean_object* l_Std_Time_Database_defaultGetLocalZoneRules___closed__1;
lean_object* l_Std_Time_Database_Windows_getZoneRules(lean_object*, lean_object*);
static lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__1___closed__2;
LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Std_Time_Database_defaultGetZoneRules___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, size_t x_6, size_t x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
uint8_t x_10;
x_10 = lean_usize_dec_lt(x_7, x_6);
if (x_10 == 0)
{
lean_object* x_11;
lean_dec(x_4);
lean_dec(x_1);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_8);
lean_ctor_set(x_11, 1, x_9);
return x_11;
}
else
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; uint8_t x_15;
lean_dec(x_8);
x_12 = lean_array_uget(x_5, x_7);
x_13 = l_System_FilePath_pathExists(x_12, x_9);
x_14 = lean_ctor_get(x_13, 0);
lean_inc(x_14);
x_15 = lean_unbox(x_14);
lean_dec(x_14);
if (x_15 == 0)
{
lean_object* x_16; size_t x_17; size_t x_18;
lean_dec(x_12);
x_16 = lean_ctor_get(x_13, 1);
lean_inc(x_16);
lean_dec(x_13);
x_17 = 1;
x_18 = lean_usize_add(x_7, x_17);
lean_inc(x_4);
{
size_t _tmp_6 = x_18;
lean_object* _tmp_7 = x_4;
lean_object* _tmp_8 = x_16;
x_7 = _tmp_6;
x_8 = _tmp_7;
x_9 = _tmp_8;
}
goto _start;
}
else
{
uint8_t x_20;
lean_dec(x_4);
x_20 = !lean_is_exclusive(x_13);
if (x_20 == 0)
{
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_13, 1);
x_22 = lean_ctor_get(x_13, 0);
lean_dec(x_22);
x_23 = l_Std_Time_Database_TZdb_readRulesFromDisk(x_12, x_1, x_21);
if (lean_obj_tag(x_23) == 0)
{
uint8_t x_24;
x_24 = !lean_is_exclusive(x_23);
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_25 = lean_ctor_get(x_23, 0);
x_26 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_26, 0, x_25);
x_27 = lean_box(0);
lean_ctor_set(x_13, 1, x_27);
lean_ctor_set(x_13, 0, x_26);
lean_ctor_set(x_23, 0, x_13);
return x_23;
}
else
{
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_28 = lean_ctor_get(x_23, 0);
x_29 = lean_ctor_get(x_23, 1);
lean_inc(x_29);
lean_inc(x_28);
lean_dec(x_23);
x_30 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_30, 0, x_28);
x_31 = lean_box(0);
lean_ctor_set(x_13, 1, x_31);
lean_ctor_set(x_13, 0, x_30);
x_32 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_32, 0, x_13);
lean_ctor_set(x_32, 1, x_29);
return x_32;
}
}
else
{
uint8_t x_33;
lean_free_object(x_13);
x_33 = !lean_is_exclusive(x_23);
if (x_33 == 0)
{
return x_23;
}
else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36;
x_34 = lean_ctor_get(x_23, 0);
x_35 = lean_ctor_get(x_23, 1);
lean_inc(x_35);
lean_inc(x_34);
lean_dec(x_23);
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_34);
lean_ctor_set(x_36, 1, x_35);
return x_36;
}
}
}
else
{
lean_object* x_37; lean_object* x_38;
x_37 = lean_ctor_get(x_13, 1);
lean_inc(x_37);
lean_dec(x_13);
x_38 = l_Std_Time_Database_TZdb_readRulesFromDisk(x_12, x_1, x_37);
if (lean_obj_tag(x_38) == 0)
{
lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45;
x_39 = lean_ctor_get(x_38, 0);
lean_inc(x_39);
x_40 = lean_ctor_get(x_38, 1);
lean_inc(x_40);
if (lean_is_exclusive(x_38)) {
lean_ctor_release(x_38, 0);
lean_ctor_release(x_38, 1);
x_41 = x_38;
} else {
lean_dec_ref(x_38);
x_41 = lean_box(0);
}
x_42 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_42, 0, x_39);
x_43 = lean_box(0);
x_44 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_44, 0, x_42);
lean_ctor_set(x_44, 1, x_43);
if (lean_is_scalar(x_41)) {
x_45 = lean_alloc_ctor(0, 2, 0);
} else {
x_45 = x_41;
}
lean_ctor_set(x_45, 0, x_44);
lean_ctor_set(x_45, 1, x_40);
return x_45;
}
else
{
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49;
x_46 = lean_ctor_get(x_38, 0);
lean_inc(x_46);
x_47 = lean_ctor_get(x_38, 1);
lean_inc(x_47);
if (lean_is_exclusive(x_38)) {
lean_ctor_release(x_38, 0);
lean_ctor_release(x_38, 1);
x_48 = x_38;
} else {
lean_dec_ref(x_38);
x_48 = lean_box(0);
}
if (lean_is_scalar(x_48)) {
x_49 = lean_alloc_ctor(1, 2, 0);
} else {
x_49 = x_48;
}
lean_ctor_set(x_49, 0, x_46);
lean_ctor_set(x_49, 1, x_47);
return x_49;
}
}
}
}
}
}
static lean_object* _init_l_Std_Time_Database_defaultGetZoneRules___lambda__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("cannot find ", 12, 12);
return x_1;
}
}
static lean_object* _init_l_Std_Time_Database_defaultGetZoneRules___lambda__1___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked(" in the local timezone database", 31, 31);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_4 = l_Std_Time_Database_defaultGetZoneRules___lambda__1___closed__1;
x_5 = lean_string_append(x_4, x_1);
x_6 = l_Std_Time_Database_defaultGetZoneRules___lambda__1___closed__2;
x_7 = lean_string_append(x_5, x_6);
x_8 = lean_alloc_ctor(18, 1, 0);
lean_ctor_set(x_8, 0, x_7);
x_9 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_9, 0, x_8);
lean_ctor_set(x_9, 1, x_3);
return x_9;
}
}
static lean_object* _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("/usr/share/lib/zoneinfo", 23, 23);
return x_1;
}
}
static lean_object* _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__1;
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_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("/etc/zoneinfo", 13, 13);
return x_1;
}
}
static lean_object* _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__3;
x_2 = l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__2;
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_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("/share/zoneinfo", 15, 15);
return x_1;
}
}
static lean_object* _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__5;
x_2 = l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__4;
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_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("/usr/share/zoneinfo", 19, 19);
return x_1;
}
}
static lean_object* _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__7;
x_2 = l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__6;
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_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__8;
x_2 = lean_array_mk(x_1);
return x_2;
}
}
static lean_object* _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = lean_box(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;
}
}
static size_t _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__11() {
_start:
{
lean_object* x_1; size_t x_2;
x_1 = l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__9;
x_2 = lean_array_size(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; size_t x_6; lean_object* x_7; size_t x_8; lean_object* x_9;
x_4 = l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__9;
x_5 = lean_box(0);
x_6 = 0;
x_7 = l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__10;
x_8 = l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__11;
lean_inc(x_1);
x_9 = l_Array_forIn_x27Unsafe_loop___at_Std_Time_Database_defaultGetZoneRules___spec__1(x_1, x_4, x_5, x_7, x_4, x_8, x_6, x_7, x_3);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11;
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
lean_dec(x_10);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = lean_ctor_get(x_9, 1);
lean_inc(x_12);
lean_dec(x_9);
x_13 = lean_box(0);
x_14 = l_Std_Time_Database_defaultGetZoneRules___lambda__1(x_1, x_13, x_12);
lean_dec(x_1);
return x_14;
}
else
{
uint8_t x_15;
lean_dec(x_1);
x_15 = !lean_is_exclusive(x_9);
if (x_15 == 0)
{
lean_object* x_16; lean_object* x_17;
x_16 = lean_ctor_get(x_9, 0);
lean_dec(x_16);
x_17 = lean_ctor_get(x_11, 0);
lean_inc(x_17);
lean_dec(x_11);
lean_ctor_set(x_9, 0, x_17);
return x_9;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_18 = lean_ctor_get(x_9, 1);
lean_inc(x_18);
lean_dec(x_9);
x_19 = lean_ctor_get(x_11, 0);
lean_inc(x_19);
lean_dec(x_11);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_18);
return x_20;
}
}
}
else
{
uint8_t x_21;
lean_dec(x_1);
x_21 = !lean_is_exclusive(x_9);
if (x_21 == 0)
{
return x_9;
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_22 = lean_ctor_get(x_9, 0);
x_23 = lean_ctor_get(x_9, 1);
lean_inc(x_23);
lean_inc(x_22);
lean_dec(x_9);
x_24 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_24, 0, x_22);
lean_ctor_set(x_24, 1, x_23);
return x_24;
}
}
}
}
static lean_object* _init_l_Std_Time_Database_defaultGetZoneRules___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("/usr/share/zoneinfo/", 20, 20);
x_1 = lean_mk_string_unchecked("TZDIR", 5, 5);
return x_1;
}
}
@ -46,18 +484,118 @@ uint8_t x_3;
x_3 = l_System_Platform_isWindows;
if (x_3 == 0)
{
lean_object* x_4; lean_object* x_5;
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = l_Std_Time_Database_defaultGetZoneRules___closed__1;
x_5 = l_Std_Time_Database_TZdb_readRulesFromDisk(x_4, x_1, x_2);
return x_5;
x_5 = lean_io_getenv(x_4, x_2);
x_6 = lean_ctor_get(x_5, 0);
lean_inc(x_6);
if (lean_obj_tag(x_6) == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_5, 1);
lean_inc(x_7);
lean_dec(x_5);
x_8 = lean_box(0);
x_9 = l_Std_Time_Database_defaultGetZoneRules___lambda__2(x_1, x_8, x_7);
return x_9;
}
else
{
lean_object* x_6;
x_6 = l_Std_Time_Database_Windows_getZoneRules(x_1, x_2);
lean_dec(x_1);
return x_6;
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = lean_ctor_get(x_5, 1);
lean_inc(x_10);
lean_dec(x_5);
x_11 = lean_ctor_get(x_6, 0);
lean_inc(x_11);
lean_dec(x_6);
x_12 = l_Std_Time_Database_TZdb_readRulesFromDisk(x_11, x_1, x_10);
if (lean_obj_tag(x_12) == 0)
{
uint8_t x_13;
x_13 = !lean_is_exclusive(x_12);
if (x_13 == 0)
{
return x_12;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_14 = lean_ctor_get(x_12, 0);
x_15 = lean_ctor_get(x_12, 1);
lean_inc(x_15);
lean_inc(x_14);
lean_dec(x_12);
x_16 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_16, 0, x_14);
lean_ctor_set(x_16, 1, x_15);
return x_16;
}
}
else
{
uint8_t x_17;
x_17 = !lean_is_exclusive(x_12);
if (x_17 == 0)
{
return x_12;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_18 = lean_ctor_get(x_12, 0);
x_19 = lean_ctor_get(x_12, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_12);
x_20 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_20, 0, x_18);
lean_ctor_set(x_20, 1, x_19);
return x_20;
}
}
}
}
else
{
lean_object* x_21;
x_21 = l_Std_Time_Database_Windows_getZoneRules(x_1, x_2);
lean_dec(x_1);
return x_21;
}
}
}
LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Std_Time_Database_defaultGetZoneRules___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
size_t x_10; size_t x_11; lean_object* x_12;
x_10 = lean_unbox_usize(x_6);
lean_dec(x_6);
x_11 = lean_unbox_usize(x_7);
lean_dec(x_7);
x_12 = l_Array_forIn_x27Unsafe_loop___at_Std_Time_Database_defaultGetZoneRules___spec__1(x_1, x_2, x_3, x_4, x_5, x_10, x_11, x_8, x_9);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
return x_12;
}
}
LEAN_EXPORT lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Std_Time_Database_defaultGetZoneRules___lambda__1(x_1, x_2, x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Std_Time_Database_defaultGetZoneRules___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Std_Time_Database_defaultGetZoneRules___lambda__2(x_1, x_2, x_3);
lean_dec(x_2);
return x_4;
}
}
static lean_object* _init_l_Std_Time_Database_defaultGetLocalZoneRules___closed__1() {
@ -160,6 +698,31 @@ lean_dec_ref(res);
res = initialize_Init_System_Platform(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Std_Time_Database_defaultGetZoneRules___lambda__1___closed__1 = _init_l_Std_Time_Database_defaultGetZoneRules___lambda__1___closed__1();
lean_mark_persistent(l_Std_Time_Database_defaultGetZoneRules___lambda__1___closed__1);
l_Std_Time_Database_defaultGetZoneRules___lambda__1___closed__2 = _init_l_Std_Time_Database_defaultGetZoneRules___lambda__1___closed__2();
lean_mark_persistent(l_Std_Time_Database_defaultGetZoneRules___lambda__1___closed__2);
l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__1 = _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__1();
lean_mark_persistent(l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__1);
l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__2 = _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__2();
lean_mark_persistent(l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__2);
l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__3 = _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__3();
lean_mark_persistent(l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__3);
l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__4 = _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__4();
lean_mark_persistent(l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__4);
l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__5 = _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__5();
lean_mark_persistent(l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__5);
l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__6 = _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__6();
lean_mark_persistent(l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__6);
l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__7 = _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__7();
lean_mark_persistent(l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__7);
l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__8 = _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__8();
lean_mark_persistent(l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__8);
l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__9 = _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__9();
lean_mark_persistent(l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__9);
l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__10 = _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__10();
lean_mark_persistent(l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__10);
l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__11 = _init_l_Std_Time_Database_defaultGetZoneRules___lambda__2___closed__11();
l_Std_Time_Database_defaultGetZoneRules___closed__1 = _init_l_Std_Time_Database_defaultGetZoneRules___closed__1();
lean_mark_persistent(l_Std_Time_Database_defaultGetZoneRules___closed__1);
l_Std_Time_Database_defaultGetLocalZoneRules___closed__1 = _init_l_Std_Time_Database_defaultGetLocalZoneRules___closed__1();

4
stage0/stdlib/Std/Time/Zoned/Database/Basic.c generated
View file

@ -37,6 +37,7 @@ LEAN_EXPORT uint8_t l_Std_Time_TimeZone_convertWall(uint8_t);
LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop___at_Std_Time_TimeZone_convertTZifV1___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_TimeZone_convertTransition(lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_x27_loop___at_Std_Time_TimeZone_convertTZifV1___spec__1___closed__1;
extern uint8_t l_instInhabitedUInt8;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_x27_loop___at_Std_Time_TimeZone_convertTZifV1___spec__2___closed__1;
@ -50,7 +51,6 @@ LEAN_EXPORT lean_object* l_Std_Time_TimeZone_convertWall___boxed(lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_TimeZone_convertLocalTimeType___boxed(lean_object*, lean_object*, lean_object*);
extern uint8_t l_UInt8_instInhabited;
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Data_Repr_0__Nat_reprFast(lean_object*);
@ -546,7 +546,7 @@ x_4 = lean_ctor_get(x_3, 1);
x_5 = l_Int_instInhabited;
x_6 = lean_array_get(x_5, x_4, x_2);
x_7 = lean_ctor_get(x_3, 2);
x_8 = l_UInt8_instInhabited;
x_8 = l_instInhabitedUInt8;
x_9 = lean_box(x_8);
x_10 = lean_array_get(x_9, x_7, x_2);
x_11 = lean_unbox(x_10);

895
stage0/stdlib/Std/Time/Zoned/Database/TZdb.c generated
View file

File diff suppressed because it is too large Load diff

62
stage0/stdlib/Std/Time/Zoned/Database/TzIf.c generated
View file

@ -22,6 +22,7 @@ static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZon
LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_parseFooter___spec__3(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*);
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_parseLocalTimeTypes___closed__1;
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprTZifV1____x40_Std_Time_Zoned_Database_TzIf___hyg_532____closed__15;
uint8_t lean_uint8_of_nat(lean_object*);
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprLocalTimeType____x40_Std_Time_Zoned_Database_TzIf___hyg_278____closed__14;
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprHeader____x40_Std_Time_Zoned_Database_TzIf___hyg_76____closed__17;
LEAN_EXPORT lean_object* l_Std_Time_TimeZone_TZif_instInhabitedLeapSecond;
@ -85,6 +86,7 @@ LEAN_EXPORT lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_Ti
LEAN_EXPORT lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_pu64(lean_object*);
LEAN_EXPORT lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_parseTransitionTimes___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_toInt32(lean_object*);
extern uint32_t l_instInhabitedUInt32;
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_toInt64___closed__2;
LEAN_EXPORT lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprTZifV2____x40_Std_Time_Zoned_Database_TzIf___hyg_748____boxed(lean_object*, lean_object*);
lean_object* lean_string_push(lean_object*, uint32_t);
@ -113,7 +115,7 @@ LEAN_EXPORT lean_object* l_repr___at___private_Std_Time_Zoned_Database_TzIf_0__S
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprLocalTimeType____x40_Std_Time_Zoned_Database_TzIf___hyg_278____closed__6;
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_parseTZifV2___closed__1;
LEAN_EXPORT lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_parseFooter(lean_object*);
static lean_object* l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__1;
static uint8_t l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__1;
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprTZif____x40_Std_Time_Zoned_Database_TzIf___hyg_838____closed__7;
static lean_object* l_Std_Time_TimeZone_TZif_instReprTZifV1___closed__1;
LEAN_EXPORT lean_object* l_panic___at___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_toUInt32___spec__1___boxed__const__1;
@ -182,6 +184,7 @@ static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZon
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprLocalTimeType____x40_Std_Time_Zoned_Database_TzIf___hyg_278____closed__7;
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprHeader____x40_Std_Time_Zoned_Database_TzIf___hyg_76____closed__16;
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprLocalTimeType____x40_Std_Time_Zoned_Database_TzIf___hyg_278____closed__1;
static uint32_t l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__2;
LEAN_EXPORT lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_toInt64(lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_TimeZone_TZif_instInhabitedHeader;
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_parseHeader___closed__2;
@ -191,6 +194,8 @@ LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop___at___private_Std_Time_Zone
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprLocalTimeType____x40_Std_Time_Zoned_Database_TzIf___hyg_278____closed__13;
LEAN_EXPORT lean_object* l_repr___at___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprTZifV1____x40_Std_Time_Zoned_Database_TzIf___hyg_532____spec__4(lean_object*);
LEAN_EXPORT lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_pu32(lean_object*);
static lean_object* l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__3;
extern uint8_t l_instInhabitedUInt8;
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_toInt64___closed__1;
LEAN_EXPORT lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprTZifV2____x40_Std_Time_Zoned_Database_TzIf___hyg_748_(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Time_TimeZone_TZif_instReprHeader;
@ -229,6 +234,7 @@ LEAN_EXPORT lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_Ti
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprHeader____x40_Std_Time_Zoned_Database_TzIf___hyg_76____closed__6;
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprHeader____x40_Std_Time_Zoned_Database_TzIf___hyg_76____closed__24;
static lean_object* l_Std_Time_TimeZone_TZif_instReprLocalTimeType___closed__1;
uint32_t lean_uint32_of_nat(lean_object*);
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprLocalTimeType____x40_Std_Time_Zoned_Database_TzIf___hyg_278____closed__11;
LEAN_EXPORT lean_object* l_repr___at___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprTZifV1____x40_Std_Time_Zoned_Database_TzIf___hyg_532____spec__3(lean_object*);
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprTZif____x40_Std_Time_Zoned_Database_TzIf___hyg_838____closed__6;
@ -243,7 +249,6 @@ static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZon
lean_object* lean_array_mk(lean_object*);
LEAN_EXPORT lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_parseIndicators___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Format_joinSep___at___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprTZifV1____x40_Std_Time_Zoned_Database_TzIf___hyg_532____spec__14(lean_object*, lean_object*);
extern uint32_t l_UInt32_instInhabited;
uint8_t lean_byte_array_get(lean_object*, lean_object*);
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprTZifV1____x40_Std_Time_Zoned_Database_TzIf___hyg_532____closed__11;
lean_object* lean_uint8_to_nat(uint8_t);
@ -276,7 +281,6 @@ static lean_object* l_Std_Time_TimeZone_TZif_instInhabitedLeapSecond___closed__1
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprTZifV1____x40_Std_Time_Zoned_Database_TzIf___hyg_532____closed__22;
LEAN_EXPORT lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_pu8(lean_object*);
uint8_t lean_usize_dec_lt(size_t, size_t);
extern uint8_t l_UInt8_instInhabited;
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_toUInt32___closed__1;
lean_object* lean_nat_add(lean_object*, lean_object*);
static lean_object* l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprLocalTimeType____x40_Std_Time_Zoned_Database_TzIf___hyg_278____closed__12;
@ -788,12 +792,30 @@ x_1 = l_Std_Time_TimeZone_TZif_instReprHeader___closed__1;
return x_1;
}
}
static lean_object* _init_l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__1() {
static uint8_t _init_l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__1() {
_start:
{
lean_object* x_1; uint8_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_uint8_of_nat(x_1);
return x_2;
}
}
static uint32_t _init_l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__2() {
_start:
{
lean_object* x_1; uint32_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_uint32_of_nat(x_1);
return x_2;
}
}
static lean_object* _init_l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__3() {
_start:
{
uint8_t x_1; uint32_t x_2; lean_object* x_3;
x_1 = 0;
x_2 = 0;
x_1 = l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__1;
x_2 = l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__2;
x_3 = lean_alloc_ctor(0, 0, 25);
lean_ctor_set_uint8(x_3, 24, x_1);
lean_ctor_set_uint32(x_3, 0, x_2);
@ -809,7 +831,7 @@ static lean_object* _init_l_Std_Time_TimeZone_TZif_instInhabitedHeader() {
_start:
{
lean_object* x_1;
x_1 = l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__1;
x_1 = l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__3;
return x_1;
}
}
@ -1194,14 +1216,14 @@ return x_1;
static lean_object* _init_l_Std_Time_TimeZone_TZif_instInhabitedLocalTimeType___closed__1() {
_start:
{
uint8_t x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = 0;
x_2 = l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprLocalTimeType____x40_Std_Time_Zoned_Database_TzIf___hyg_278____closed__6;
x_3 = 0;
lean_object* x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
x_1 = l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprLocalTimeType____x40_Std_Time_Zoned_Database_TzIf___hyg_278____closed__6;
x_2 = 0;
x_3 = l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__1;
x_4 = lean_alloc_ctor(0, 1, 2);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*1, x_3);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 1, x_1);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, sizeof(void*)*1, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 1, x_3);
return x_4;
}
}
@ -2929,7 +2951,7 @@ static lean_object* _init_l_Std_Time_TimeZone_TZif_instInhabitedTZifV1___closed_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__1;
x_1 = l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__3;
x_2 = l_Std_Time_TimeZone_TZif_instInhabitedTZifV1___closed__1;
x_3 = lean_alloc_ctor(0, 8, 0);
lean_ctor_set(x_3, 0, x_1);
@ -3437,7 +3459,7 @@ static lean_object* _init_l_panic___at___private_Std_Time_Zoned_Database_TzIf_0_
_start:
{
uint32_t x_1; lean_object* x_2;
x_1 = l_UInt32_instInhabited;
x_1 = l_instInhabitedUInt32;
x_2 = lean_box_uint32(x_1);
return x_2;
}
@ -4988,7 +5010,7 @@ if (x_17 == 0)
lean_object* x_18; lean_object* x_19; uint8_t x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; uint8_t x_24; uint8_t x_25;
x_18 = lean_ctor_get(x_9, 0);
x_19 = lean_ctor_get(x_9, 1);
x_20 = l_UInt8_instInhabited;
x_20 = l_instInhabitedUInt8;
x_21 = lean_box(x_20);
x_22 = lean_array_get(x_21, x_1, x_7);
x_23 = lean_unbox(x_22);
@ -5031,7 +5053,7 @@ x_34 = lean_ctor_get(x_9, 1);
lean_inc(x_34);
lean_inc(x_33);
lean_dec(x_9);
x_35 = l_UInt8_instInhabited;
x_35 = l_instInhabitedUInt8;
x_36 = lean_box(x_35);
x_37 = lean_array_get(x_36, x_1, x_7);
x_38 = lean_unbox(x_37);
@ -6733,7 +6755,9 @@ lean_mark_persistent(l_Std_Time_TimeZone_TZif_instReprHeader___closed__1);
l_Std_Time_TimeZone_TZif_instReprHeader = _init_l_Std_Time_TimeZone_TZif_instReprHeader();
lean_mark_persistent(l_Std_Time_TimeZone_TZif_instReprHeader);
l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__1 = _init_l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__1();
lean_mark_persistent(l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__1);
l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__2 = _init_l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__2();
l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__3 = _init_l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__3();
lean_mark_persistent(l_Std_Time_TimeZone_TZif_instInhabitedHeader___closed__3);
l_Std_Time_TimeZone_TZif_instInhabitedHeader = _init_l_Std_Time_TimeZone_TZif_instInhabitedHeader();
lean_mark_persistent(l_Std_Time_TimeZone_TZif_instInhabitedHeader);
l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprLocalTimeType____x40_Std_Time_Zoned_Database_TzIf___hyg_278____closed__1 = _init_l___private_Std_Time_Zoned_Database_TzIf_0__Std_Time_TimeZone_TZif_reprLocalTimeType____x40_Std_Time_Zoned_Database_TzIf___hyg_278____closed__1();