chore: update stage0
This commit is contained in:
parent
7a8c2daf96
commit
b2b385b456
7 changed files with 22420 additions and 6442 deletions
|
|
@ -49797,7 +49797,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_List_foldl___at___00List_foldl___at___00Lean_Compiler_LCNF_Simp_ConstantFold_initFn_00___x40_Lean_Compiler_LCNF_Simp_ConstantFold_4249470166____hygCtx___hyg_2__spec__2_spec__2___lam__0___closed__2;
|
||||
x_2 = lean_unsigned_to_nat(14u);
|
||||
x_3 = lean_unsigned_to_nat(65u);
|
||||
x_3 = lean_unsigned_to_nat(67u);
|
||||
x_4 = l_List_foldl___at___00List_foldl___at___00Lean_Compiler_LCNF_Simp_ConstantFold_initFn_00___x40_Lean_Compiler_LCNF_Simp_ConstantFold_4249470166____hygCtx___hyg_2__spec__2_spec__2___lam__0___closed__1;
|
||||
x_5 = l_List_foldl___at___00List_foldl___at___00Lean_Compiler_LCNF_Simp_ConstantFold_initFn_00___x40_Lean_Compiler_LCNF_Simp_ConstantFold_4249470166____hygCtx___hyg_2__spec__2_spec__2___lam__0___closed__0;
|
||||
x_6 = l_mkPanicMessageWithDecl(x_5, x_4, x_3, x_2, x_1);
|
||||
|
|
|
|||
2
stage0/stdlib/Lean/Data/SMap.c
generated
2
stage0/stdlib/Lean/Data/SMap.c
generated
|
|
@ -627,7 +627,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_SMap_find_x21___redArg___closed__2;
|
||||
x_2 = lean_unsigned_to_nat(14u);
|
||||
x_3 = lean_unsigned_to_nat(65u);
|
||||
x_3 = lean_unsigned_to_nat(67u);
|
||||
x_4 = l_Lean_SMap_find_x21___redArg___closed__1;
|
||||
x_5 = l_Lean_SMap_find_x21___redArg___closed__0;
|
||||
x_6 = l_mkPanicMessageWithDecl(x_5, x_4, x_3, x_2, x_1);
|
||||
|
|
|
|||
6
stage0/stdlib/Lean/PremiseSelection.c
generated
6
stage0/stdlib/Lean/PremiseSelection.c
generated
|
|
@ -1,6 +1,6 @@
|
|||
// Lean compiler output
|
||||
// Module: Lean.PremiseSelection
|
||||
// Imports: import Lean.PremiseSelection.Basic import Lean.PremiseSelection.SymbolFrequency import Lean.PremiseSelection.MePo
|
||||
// Imports: import Lean.PremiseSelection.Basic import Lean.PremiseSelection.SymbolFrequency import Lean.PremiseSelection.MePo import Lean.PremiseSelection.SineQuaNon
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
|
|
@ -16,6 +16,7 @@ extern "C" {
|
|||
lean_object* initialize_Lean_PremiseSelection_Basic(uint8_t builtin);
|
||||
lean_object* initialize_Lean_PremiseSelection_SymbolFrequency(uint8_t builtin);
|
||||
lean_object* initialize_Lean_PremiseSelection_MePo(uint8_t builtin);
|
||||
lean_object* initialize_Lean_PremiseSelection_SineQuaNon(uint8_t builtin);
|
||||
static bool _G_initialized = false;
|
||||
LEAN_EXPORT lean_object* initialize_Lean_PremiseSelection(uint8_t builtin) {
|
||||
lean_object * res;
|
||||
|
|
@ -30,6 +31,9 @@ lean_dec_ref(res);
|
|||
res = initialize_Lean_PremiseSelection_MePo(builtin);
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Lean_PremiseSelection_SineQuaNon(builtin);
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
return lean_io_result_mk_ok(lean_box(0));
|
||||
}
|
||||
#ifdef __cplusplus
|
||||
|
|
|
|||
5410
stage0/stdlib/Lean/PremiseSelection/Basic.c
generated
5410
stage0/stdlib/Lean/PremiseSelection/Basic.c
generated
File diff suppressed because it is too large
Load diff
2753
stage0/stdlib/Lean/PremiseSelection/MePo.c
generated
2753
stage0/stdlib/Lean/PremiseSelection/MePo.c
generated
File diff suppressed because it is too large
Load diff
15779
stage0/stdlib/Lean/PremiseSelection/SineQuaNon.c
generated
Normal file
15779
stage0/stdlib/Lean/PremiseSelection/SineQuaNon.c
generated
Normal file
File diff suppressed because it is too large
Load diff
4910
stage0/stdlib/Lean/PremiseSelection/SymbolFrequency.c
generated
4910
stage0/stdlib/Lean/PremiseSelection/SymbolFrequency.c
generated
File diff suppressed because it is too large
Load diff
Loading…
Add table
Reference in a new issue