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:
Kim Morrison 2025-10-25 19:01:48 +11:00 • committed by Kim Morrison
parent 9166c71e08
commit a9d6bc60d0
2 changed files with 5752 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
stage0/stdlib/Lean/PremiseSelection.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.PremiseSelection
// Imports: import Lean.PremiseSelection.Basic import Lean.PremiseSelection.MePo
// Imports: import Lean.PremiseSelection.Basic import Lean.PremiseSelection.SymbolFrequency import Lean.PremiseSelection.MePo
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -14,6 +14,7 @@
extern "C" {
#endif
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);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_PremiseSelection(uint8_t builtin) {
@ -23,6 +24,9 @@ _G_initialized = true;
res = initialize_Lean_PremiseSelection_Basic(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_PremiseSelection_SymbolFrequency(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_PremiseSelection_MePo(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

5747
stage0/stdlib/Lean/PremiseSelection/SymbolFrequency.c generated Normal file
View file

File diff suppressed because it is too large Load diff