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 2025-04-14 07:03:16 +00:00
parent de25524dd6
commit 689acab1d3
7 changed files with 1391 additions and 1113 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
stage0/stdlib/Init/Data/List/Perm.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data.List.Perm
// Imports: Init.Data.List.Pairwise Init.Data.List.Erase
// Imports: Init.Data.List.Pairwise Init.Data.List.Erase Init.Data.List.Find
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -348,6 +348,7 @@ return x_5;
}
lean_object* initialize_Init_Data_List_Pairwise(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_List_Erase(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_List_Find(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data_List_Perm(uint8_t builtin, lean_object* w) {
lean_object * res;
@ -359,6 +360,9 @@ lean_dec_ref(res);
res = initialize_Init_Data_List_Erase(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_List_Find(builtin, 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

6
stage0/stdlib/Init/Grind.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Grind
// Imports: Init.Grind.Norm Init.Grind.Tactics Init.Grind.Lemmas Init.Grind.Cases Init.Grind.Propagator Init.Grind.Util Init.Grind.Offset Init.Grind.PP Init.Grind.CommRing
// Imports: Init.Grind.Norm Init.Grind.Tactics Init.Grind.Lemmas Init.Grind.Cases Init.Grind.Propagator Init.Grind.Util Init.Grind.Offset Init.Grind.PP Init.Grind.CommRing Init.Grind.Ext
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -22,6 +22,7 @@ lean_object* initialize_Init_Grind_Util(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Grind_Offset(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Grind_PP(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Grind_CommRing(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Grind_Ext(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Grind(uint8_t builtin, lean_object* w) {
lean_object * res;
@ -54,6 +55,9 @@ lean_dec_ref(res);
res = initialize_Init_Grind_CommRing(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Grind_Ext(builtin, 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

33
stage0/stdlib/Init/Grind/Ext.c generated Normal file
View file

@ -0,0 +1,33 @@
// Lean compiler output
// Module: Init.Grind.Ext
// Imports: Init.Ext Init.Grind.Tactics
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* initialize_Init_Ext(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Grind_Tactics(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Grind_Ext(uint8_t builtin, lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init_Ext(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Grind_Tactics(builtin, 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
}
#endif

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

@ -14851,7 +14851,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_foldr___at_Substring_toName___spec__1___closed__1;
x_2 = l_List_foldr___at_Substring_toName___spec__1___closed__2;
x_3 = lean_unsigned_to_nat(1031u);
x_3 = lean_unsigned_to_nat(1039u);
x_4 = lean_unsigned_to_nat(10u);
x_5 = l_List_foldr___at_Substring_toName___spec__1___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

2
stage0/stdlib/Lean/Meta/Tactic/Grind/ExtAttr.c generated
View file

@ -190,7 +190,7 @@ static lean_object* _init_l_Lean_Meta_Grind_validateExtAttr___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("` is tagged with `[ext]`", 24, 24);
x_1 = lean_mk_string_unchecked("` is not tagged with `[ext]`", 28, 28);
return x_1;
}
}