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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2024-05-18 20:49:44 -07:00 • committed by Leonardo de Moura
parent 47c8e340d6
commit 239ade80dc
4 changed files with 761 additions and 19580 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

File diff suppressed because it is too large Load diff

18035
stage0/stdlib/Lean/Elab/Calc.c generated
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

199
stage0/stdlib/Lean/Elab/Tactic/Calc.c generated
View file

@ -25,18 +25,14 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalc___closed__3;
extern lean_object* l_Lean_Elab_Tactic_tacticElabAttribute;
lean_object* l_Lean_MVarId_assign___at_Lean_Elab_Tactic_closeMainGoal___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCalc___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__5;
lean_object* l_Lean_Elab_Tactic_getMainGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addBuiltinDeclarationRanges(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange(lean_object*);
lean_object* l_Lean_Elab_Tactic_getMainTag(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_stringToMessageData(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__7;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalc_declRange___closed__1;
lean_object* l_Lean_Elab_Tactic_runTermElab___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabCalcSteps(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_evalCalc_throwFailed___closed__5;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalc_declRange___closed__3;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCalc___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_evalCalc___lambda__2___closed__4;
@ -49,20 +45,14 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalc___closed__7;
static lean_object* l_Lean_Elab_Tactic_evalCalc___lambda__2___closed__2;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCalc___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_Elab_Tactic_evalCalc_throwFailed___closed__4;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCalcOld(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__3;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__1;
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalc_declRange___closed__2;
lean_object* l_Lean_Elab_Term_getCalcRelation_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalc___closed__8;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalc_docString(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalc___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalc_declRange___closed__7;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCalcOld___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCalc___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkCalcTrans(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Term_synthesizeInstMVarCore___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -72,16 +62,13 @@ lean_object* l_Lean_Name_mkStr2(lean_object*, lean_object*);
lean_object* l_Lean_indentExpr(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalc_declRange___closed__5;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalc_declRange___closed__4;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__6;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalc_docString___closed__1;
lean_object* l_Lean_Elab_Tactic_withCollectingNewGoalsFrom(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_evalCalc_throwFailed___closed__2;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCalc(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCalc_throwFailed___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalcOld(lean_object*);
lean_object* l_Lean_Name_mkStr4(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalc___closed__9;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__4;
lean_object* l_Lean_Meta_mkFreshExprSyntheticOpaqueMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalc___closed__6;
@ -92,7 +79,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCalc___lambda__1(lean_object*, l
lean_object* l_Lean_Elab_Tactic_replaceMainGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalc___closed__2;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCalc_throwFailed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__3;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCalc___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* _init_l_Lean_Elab_Tactic_evalCalc_throwFailed___closed__1() {
_start:
@ -1140,165 +1126,6 @@ x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCalcOld(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11;
x_11 = l_Lean_Elab_Tactic_evalCalc(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_11;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCalcOld___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, lean_object* x_10) {
_start:
{
lean_object* x_11;
x_11 = l_Lean_Elab_Tactic_evalCalcOld(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_1);
return x_11;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("evalCalcOld", 11);
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___regBuiltin_Lean_Elab_Tactic_evalCalc___closed__1;
x_2 = l___regBuiltin_Lean_Elab_Tactic_evalCalc___closed__4;
x_3 = l___regBuiltin_Lean_Elab_Tactic_evalCalc___closed__5;
x_4 = l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__1;
x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
return x_5;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalCalcOld___boxed), 10, 0);
return x_1;
}
}
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalcOld(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Lean_Elab_Tactic_evalCalc___closed__8;
x_3 = l___regBuiltin_Lean_Elab_Tactic_evalCalc___closed__3;
x_4 = l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__2;
x_5 = l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__3;
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(38u);
x_2 = lean_unsigned_to_nat(0u);
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___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(38u);
x_2 = lean_unsigned_to_nat(36u);
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___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__1;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__2;
x_4 = lean_unsigned_to_nat(36u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
lean_ctor_set(x_5, 2, x_3);
lean_ctor_set(x_5, 3, x_4);
return x_5;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(38u);
x_2 = lean_unsigned_to_nat(4u);
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___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(38u);
x_2 = lean_unsigned_to_nat(15u);
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___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__4;
x_2 = lean_unsigned_to_nat(4u);
x_3 = l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__5;
x_4 = lean_unsigned_to_nat(15u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
lean_ctor_set(x_5, 2, x_3);
lean_ctor_set(x_5, 3, x_4);
return x_5;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__3;
x_2 = l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___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);
return x_3;
}
}
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__2;
x_3 = l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__7;
x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1);
return x_4;
}
}
lean_object* initialize_Lean_Elab_Calc(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Elab_Tactic_ElabTerm(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
@ -1377,32 +1204,6 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalCalc_declRange___closed
if (builtin) {res = l___regBuiltin_Lean_Elab_Tactic_evalCalc_declRange(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
}l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__1);
l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__2);
l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__3 = _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalCalcOld___closed__3);
if (builtin) {res = l___regBuiltin_Lean_Elab_Tactic_evalCalcOld(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
}l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__1);
l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__2);
l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__3 = _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__3);
l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__4 = _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__4();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__4);
l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__5 = _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__5();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__5);
l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__6 = _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__6();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__6);
l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__7 = _init_l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__7();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange___closed__7);
if (builtin) {res = l___regBuiltin_Lean_Elab_Tactic_evalCalcOld_declRange(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
}return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus