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:
Scott Morrison 2024-02-15 13:41:45 +11:00 • committed by Scott Morrison
parent 98085661c7
commit 144c1bbbaf
32 changed files with 31114 additions and 7268 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

72
stage0/src/library/compiler/llvm.cpp generated
View file

@ -18,6 +18,7 @@ Lean's IR.
#include "runtime/string_ref.h"
#ifdef LEAN_LLVM
#include "llvm-c/Analysis.h"
#include "llvm-c/BitReader.h"
#include "llvm-c/BitWriter.h"
#include "llvm-c/Core.h"
@ -1424,3 +1425,74 @@ extern "C" LEAN_EXPORT lean_object *llvm_is_declaration(size_t ctx, size_t globa
return lean_io_result_mk_ok(lean_box(is_bool));
#endif // LEAN_LLVM
}
extern "C" LEAN_EXPORT lean_object *lean_llvm_verify_module(size_t ctx, size_t mod,
lean_object * /* w */) {
#ifndef LEAN_LLVM
lean_always_assert(
false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
"the LLVM backend function."));
#else
char* msg = NULL;
LLVMBool broken = LLVMVerifyModule(lean_to_Module(mod), LLVMReturnStatusAction, &msg);
if (broken) {
return lean_io_result_mk_ok(lean::mk_option_some(lean_mk_string(msg)));
} else {
return lean_io_result_mk_ok(lean::mk_option_none());
}
#endif // LEAN_LLVM
}
extern "C" LEAN_EXPORT lean_object *lean_llvm_count_basic_blocks(size_t ctx, size_t fn_val,
lean_object * /* w */) {
#ifndef LEAN_LLVM
lean_always_assert(
false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
"the LLVM backend function."));
#else
LLVMValueRef fn_ref = lean_to_Value(fn_val);
return lean_io_result_mk_ok(lean_box_uint64((uint64_t)LLVMCountBasicBlocks(fn_ref)));
#endif // LEAN_LLVM
}
extern "C" LEAN_EXPORT lean_object *lean_llvm_get_entry_basic_block(size_t ctx, size_t fn_val,
lean_object * /* w */) {
#ifndef LEAN_LLVM
lean_always_assert(
false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
"the LLVM backend function."));
#else
LLVMValueRef fn_ref = lean_to_Value(fn_val);
LLVMBasicBlockRef bb_ref = LLVMGetEntryBasicBlock(fn_ref);
return lean_io_result_mk_ok(lean_box_usize(BasicBlock_to_lean(bb_ref)));
#endif // LEAN_LLVM
}
extern "C" LEAN_EXPORT lean_object *lean_llvm_get_first_instruction(size_t ctx, size_t bb,
lean_object * /* w */) {
#ifndef LEAN_LLVM
lean_always_assert(
false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
"the LLVM backend function."));
#else
LLVMBasicBlockRef bb_ref = lean_to_BasicBlock(bb);
LLVMValueRef instr_ref = LLVMGetFirstInstruction(bb_ref);
if (instr_ref == NULL) {
return lean_io_result_mk_ok(lean::mk_option_none());
} else {
return lean_io_result_mk_ok(lean::mk_option_some(lean_box_usize(Value_to_lean(instr_ref))));
}
#endif // LEAN_LLVM
}
extern "C" LEAN_EXPORT lean_object *lean_llvm_position_builder_before(
size_t ctx, size_t builder, size_t instr, lean_object * /* w */) {
#ifndef LEAN_LLVM
lean_always_assert(
false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
"the LLVM backend function."));
#else
LLVMPositionBuilderBefore(lean_to_Builder(builder), lean_to_Value(instr));
return lean_io_result_mk_ok(lean_box(0));
#endif // LEAN_LLVM
}

10
stage0/stdlib/Init.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init
// Imports: Init.Prelude Init.Notation Init.Tactics Init.TacticsExtra Init.RCases Init.Core Init.Control Init.Data.Basic Init.WF Init.WFTactics Init.Data Init.System Init.Util Init.Dynamic Init.ShareCommon Init.MetaTypes Init.Meta Init.NotationExtra Init.SimpLemmas Init.Hints Init.Conv Init.Guard Init.Simproc Init.SizeOfLemmas Init.BinderPredicates
// Imports: Init.Prelude Init.Notation Init.Tactics Init.TacticsExtra Init.ByCases Init.RCases Init.Core Init.Control Init.Data.Basic Init.WF Init.WFTactics Init.Data Init.System Init.Util Init.Dynamic Init.ShareCommon Init.MetaTypes Init.Meta Init.NotationExtra Init.SimpLemmas Init.PropLemmas Init.Hints Init.Conv Init.Guard Init.Simproc Init.SizeOfLemmas Init.BinderPredicates
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -17,6 +17,7 @@ lean_object* initialize_Init_Prelude(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Notation(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Tactics(uint8_t builtin, lean_object*);
lean_object* initialize_Init_TacticsExtra(uint8_t builtin, lean_object*);
lean_object* initialize_Init_ByCases(uint8_t builtin, lean_object*);
lean_object* initialize_Init_RCases(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Core(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Control(uint8_t builtin, lean_object*);
@ -32,6 +33,7 @@ lean_object* initialize_Init_MetaTypes(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Meta(uint8_t builtin, lean_object*);
lean_object* initialize_Init_NotationExtra(uint8_t builtin, lean_object*);
lean_object* initialize_Init_SimpLemmas(uint8_t builtin, lean_object*);
lean_object* initialize_Init_PropLemmas(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Hints(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Conv(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Guard(uint8_t builtin, lean_object*);
@ -55,6 +57,9 @@ lean_dec_ref(res);
res = initialize_Init_TacticsExtra(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_ByCases(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_RCases(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
@ -100,6 +105,9 @@ lean_dec_ref(res);
res = initialize_Init_SimpLemmas(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_PropLemmas(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Hints(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

975
stage0/stdlib/Init/BinderPredicates.c generated
View file

File diff suppressed because it is too large Load diff

1158
stage0/stdlib/Init/ByCases.c generated Normal file
View file

File diff suppressed because it is too large Load diff

1139
stage0/stdlib/Init/Classical.c generated
View file

File diff suppressed because it is too large Load diff

174
stage0/stdlib/Init/Core.c generated
View file

@ -31,8 +31,10 @@ LEAN_EXPORT lean_object* l_Quotient_lift___rarg(lean_object*, lean_object*, lean
static lean_object* l___aux__Init__Core______macroRules__term___u2295____1___closed__7;
LEAN_EXPORT lean_object* l_bne(lean_object*);
static lean_object* l___aux__Init__Core______macroRules__term___x3c_x2d_x3e____1___closed__13;
LEAN_EXPORT lean_object* l_And_elim___rarg(lean_object*, lean_object*);
static lean_object* l___aux__Init__Core______macroRules__term___x21_x3d____1___closed__7;
LEAN_EXPORT lean_object* l_Thunk_map___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instDecidableEqEmpty___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instInhabitedProd(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Quotient_rec___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___aux__Init__Core______unexpand__PSum__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -56,6 +58,7 @@ LEAN_EXPORT lean_object* l_iteInduction(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instDecidableEqSum___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_reduceBool(uint8_t);
LEAN_EXPORT lean_object* l_instDecidableEqProd(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Empty_elim(lean_object*, uint8_t);
LEAN_EXPORT lean_object* l_Quotient_rec(lean_object*, lean_object*, lean_object*);
static lean_object* l_term_u2205___closed__4;
LEAN_EXPORT lean_object* l___aux__Init__Core______unexpand__Iff__2___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -116,6 +119,7 @@ LEAN_EXPORT lean_object* l_Quot_liftOn(lean_object*, lean_object*, lean_object*)
LEAN_EXPORT lean_object* l_Quotient_recOnSubsingleton(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___aux__Init__Core______unexpand__EmptyCollection__emptyCollection__1___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_bne___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instDecidableEqEmpty(uint8_t, uint8_t);
lean_object* l_Lean_Syntax_getNumArgs(lean_object*);
LEAN_EXPORT lean_object* l_instInhabitedPUnit;
static lean_object* l_term___u2194_____closed__4;
@ -156,11 +160,14 @@ static lean_object* l___aux__Init__Core______macroRules__Lean__Parser__Tactic__t
LEAN_EXPORT lean_object* l_Squash_mk___rarg(lean_object*);
static lean_object* l_term___x21_x3d_____closed__6;
LEAN_EXPORT lean_object* l_Quotient_rec___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_PEmpty_elim___rarg___boxed(lean_object*);
LEAN_EXPORT lean_object* l_instDecidableDitePropNot___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instDecidableEqPEmpty(uint8_t, uint8_t);
uint8_t lean_strict_or(uint8_t, uint8_t);
static lean_object* l_term___u2260_____closed__1;
LEAN_EXPORT lean_object* l_instInhabitedForInStep__1(lean_object*);
static lean_object* l_term___u2260_____closed__6;
LEAN_EXPORT lean_object* l_And_elim(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_flip___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Eq_mpr___rarg(lean_object*);
LEAN_EXPORT lean_object* l___aux__Init__Core______macroRules__term___u2248____1(lean_object*, lean_object*, lean_object*);
@ -169,6 +176,7 @@ LEAN_EXPORT lean_object* l_Task_bind___boxed(lean_object*, lean_object*, lean_ob
static lean_object* l___aux__Init__Core______macroRules__term___u2295_x27____1___closed__1;
static lean_object* l___aux__Init__Core______macroRules__term___u2248____1___closed__1;
LEAN_EXPORT lean_object* l_strictOr___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_PEmpty_elim(lean_object*);
LEAN_EXPORT lean_object* l_Eq_ndrecOn___rarg___boxed(lean_object*);
LEAN_EXPORT lean_object* l___aux__Init__Core______unexpand__PSum__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Core______macroRules__term___x21_x3d____1___closed__1;
@ -235,12 +243,14 @@ LEAN_EXPORT lean_object* l_Thunk_bind(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Quotient_recOn___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instInhabitedForInStep(lean_object*);
LEAN_EXPORT lean_object* l_Quotient_mk_x27(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Not_elim(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_thunk(lean_object*);
LEAN_EXPORT lean_object* l_term___u2295_x27__;
lean_object* lean_thunk_pure(lean_object*);
static lean_object* l___aux__Init__Core______macroRules__term___x3c_x2d_x3e____1___closed__6;
static lean_object* l___aux__Init__Core______macroRules__term___x3c_x2d_x3e____1___closed__7;
LEAN_EXPORT lean_object* l_instBEqProd(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instInhabitedPSum__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Thunk_map___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_toBoolUsing___rarg___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Quotient_lift_u2082___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -283,6 +293,7 @@ LEAN_EXPORT lean_object* l_term___u2295__;
static lean_object* l_term___x3c_x2d_x3e_____closed__10;
LEAN_EXPORT lean_object* l_instDecidableDitePropNot___rarg(uint8_t, lean_object*, lean_object*);
static lean_object* l_term___x3c_x2d_x3e_____closed__4;
LEAN_EXPORT lean_object* l_instInhabitedPSum___rarg(lean_object*);
static lean_object* l___aux__Init__Core______unexpand__Iff__1___closed__3;
LEAN_EXPORT lean_object* l_Task_Priority_dedicated;
LEAN_EXPORT lean_object* l_Quotient_mk_x27___rarg(lean_object*);
@ -291,7 +302,9 @@ LEAN_EXPORT lean_object* l___aux__Init__Core______unexpand__bne__1(lean_object*,
static lean_object* l_term___u2248_____closed__2;
LEAN_EXPORT lean_object* l_instInhabitedMProd(lean_object*, lean_object*);
lean_object* l_Lean_Name_mkStr2(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_PEmpty_elim___rarg(uint8_t);
LEAN_EXPORT uint8_t l_instDecidableForAll___rarg(uint8_t, uint8_t);
LEAN_EXPORT lean_object* l_Iff_elim(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Decidable_byCases(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_reduceNat___boxed(lean_object*);
LEAN_EXPORT lean_object* l_instInhabitedMProd___rarg(lean_object*, lean_object*);
@ -310,6 +323,7 @@ static lean_object* l_term___u2260_____closed__3;
LEAN_EXPORT lean_object* l_instDecidableIff___rarg___boxed(lean_object*, lean_object*);
lean_object* lean_task_map(lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* lean_nat_sub(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instTransPropIff;
LEAN_EXPORT lean_object* l_Quotient_lift(lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Core______macroRules__term___u2295____1___closed__5;
static lean_object* l___aux__Init__Core______macroRules__term___x21_x3d____1___closed__4;
@ -326,6 +340,7 @@ static lean_object* l_term_x7b_x7d___closed__6;
LEAN_EXPORT lean_object* l_Thunk_mk___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Quotient_mk___boxed(lean_object*, lean_object*);
static lean_object* l_term___u2295_____closed__7;
LEAN_EXPORT lean_object* l_instInhabitedPSum__1___rarg(lean_object*);
LEAN_EXPORT lean_object* l_noConfusionEnum___rarg___lambda__1(lean_object*);
static lean_object* l___aux__Init__Core______macroRules__term___x3c_x2d_x3e____1___closed__2;
static lean_object* l_term___x3c_x2d_x3e_____closed__6;
@ -341,6 +356,7 @@ static lean_object* l_term___u2248_____closed__6;
LEAN_EXPORT lean_object* l_Eq_ndrecOn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___aux__Init__Core______unexpand__Iff__1___lambda__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___aux__Init__Core______unexpand__Iff__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Empty_elim___boxed(lean_object*, lean_object*);
static lean_object* l_term_x7b_x7d___closed__8;
LEAN_EXPORT uint8_t l_instDecidableEqPUnit(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Squash_lift___rarg(lean_object*, lean_object*);
@ -374,6 +390,8 @@ LEAN_EXPORT lean_object* l_instDecidableEqPUnit___boxed(lean_object*, lean_objec
static lean_object* l_term___x21_x3d_____closed__3;
LEAN_EXPORT lean_object* l_Quotient_liftOn_u2082(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Iff_elim___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instDecidableEqPEmpty___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___aux__Init__Core______unexpand__bne__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___aux__Init__Core______macroRules__term___x3c_x2d_x3e____1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Quotient_liftOn___rarg(lean_object*, lean_object*, lean_object*);
@ -384,6 +402,7 @@ static lean_object* l_term___u2295_____closed__1;
LEAN_EXPORT lean_object* l_Lean_reduceBool___boxed(lean_object*);
static lean_object* l_term___u2194_____closed__1;
LEAN_EXPORT lean_object* l_Thunk_get___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instInhabitedPSum(lean_object*, lean_object*);
static lean_object* l___aux__Init__Core______macroRules__term___u2295_x27____1___closed__4;
LEAN_EXPORT lean_object* l_Quot_hrecOn(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___aux__Init__Core______unexpand__HasEquiv__Equiv__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -441,6 +460,82 @@ x_4 = lean_alloc_closure((void*)(l_flip___rarg), 3, 0);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Empty_elim(lean_object* x_1, uint8_t x_2) {
_start:
{
lean_internal_panic_unreachable();
}
}
LEAN_EXPORT lean_object* l_Empty_elim___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_unbox(x_2);
lean_dec(x_2);
x_4 = l_Empty_elim(x_1, x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_instDecidableEqEmpty(uint8_t x_1, uint8_t x_2) {
_start:
{
lean_internal_panic_unreachable();
}
}
LEAN_EXPORT lean_object* l_instDecidableEqEmpty___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = lean_unbox(x_2);
lean_dec(x_2);
x_5 = l_instDecidableEqEmpty(x_3, x_4);
return x_5;
}
}
LEAN_EXPORT lean_object* l_PEmpty_elim___rarg(uint8_t x_1) {
_start:
{
lean_internal_panic_unreachable();
}
}
LEAN_EXPORT lean_object* l_PEmpty_elim(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_PEmpty_elim___rarg___boxed), 1, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_PEmpty_elim___rarg___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_PEmpty_elim___rarg(x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_instDecidableEqPEmpty(uint8_t x_1, uint8_t x_2) {
_start:
{
lean_internal_panic_unreachable();
}
}
LEAN_EXPORT lean_object* l_instDecidableEqPEmpty___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = lean_unbox(x_2);
lean_dec(x_2);
x_5 = l_instDecidableEqPEmpty(x_3, x_4);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Thunk_mk___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -2172,6 +2267,40 @@ lean_dec(x_1);
return x_8;
}
}
LEAN_EXPORT lean_object* l_instInhabitedPSum___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_instInhabitedPSum(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_instInhabitedPSum___rarg), 1, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_instInhabitedPSum__1___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_instInhabitedPSum__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_instInhabitedPSum__1___rarg), 1, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_instInhabitedForInStep___rarg(lean_object* x_1) {
_start:
{
@ -4150,6 +4279,12 @@ return x_22;
}
}
}
static lean_object* _init_l_instTransPropIff() {
_start:
{
return lean_box(0);
}
}
LEAN_EXPORT uint8_t l_toBoolUsing___rarg(uint8_t x_1) {
_start:
{
@ -5033,6 +5168,44 @@ x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Not_elim(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_internal_panic_unreachable();
}
}
LEAN_EXPORT lean_object* l_And_elim___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_apply_2(x_1, lean_box(0), lean_box(0));
return x_3;
}
}
LEAN_EXPORT lean_object* l_And_elim(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_And_elim___rarg), 2, 0);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Iff_elim___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_apply_2(x_1, lean_box(0), lean_box(0));
return x_3;
}
}
LEAN_EXPORT lean_object* l_Iff_elim(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Iff_elim___rarg), 2, 0);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Quot_liftOn___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -5824,6 +5997,7 @@ l___aux__Init__Core______macroRules__Lean__Parser__Tactic__tacticRfl__1___closed
lean_mark_persistent(l___aux__Init__Core______macroRules__Lean__Parser__Tactic__tacticRfl__1___closed__10);
l___aux__Init__Core______macroRules__Lean__Parser__Tactic__tacticRfl__1___closed__11 = _init_l___aux__Init__Core______macroRules__Lean__Parser__Tactic__tacticRfl__1___closed__11();
lean_mark_persistent(l___aux__Init__Core______macroRules__Lean__Parser__Tactic__tacticRfl__1___closed__11);
l_instTransPropIff = _init_l_instTransPropIff();
l_instDecidableTrue = _init_l_instDecidableTrue();
l_instDecidableFalse = _init_l_instDecidableFalse();
l_noConfusionEnum___rarg___closed__1 = _init_l_noConfusionEnum___rarg___closed__1();

6
stage0/stdlib/Init/Data/Array/DecidableEq.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data.Array.DecidableEq
// Imports: Init.Data.Array.Basic Init.Classical
// Imports: Init.Data.Array.Basic Init.ByCases
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -135,7 +135,7 @@ return x_5;
}
}
lean_object* initialize_Init_Data_Array_Basic(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Classical(uint8_t builtin, lean_object*);
lean_object* initialize_Init_ByCases(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data_Array_DecidableEq(uint8_t builtin, lean_object* w) {
lean_object * res;
@ -144,7 +144,7 @@ _G_initialized = true;
res = initialize_Init_Data_Array_Basic(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Classical(builtin, lean_io_mk_world());
res = initialize_Init_ByCases(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));

232
stage0/stdlib/Init/Data/List/Basic.c generated
View file

@ -83,11 +83,13 @@ lean_object* l_Lean_Syntax_node5(lean_object*, lean_object*, lean_object*, lean_
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
lean_object* l_List_get___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_bind(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_mapTR_loop___at_List_zipWithAll___spec__1___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_term_x5b___x5d___closed__13;
LEAN_EXPORT lean_object* l_List_find_x3f(lean_object*);
LEAN_EXPORT lean_object* l_List_reverseAux(lean_object*);
LEAN_EXPORT uint8_t l_List_any___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_and___boxed(lean_object*);
LEAN_EXPORT lean_object* l_List_zipWithAll___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_eraseIdx___rarg___boxed(lean_object*, lean_object*);
static lean_object* l_Lean___aux__Init__Data__List__Basic______macroRules__term_x5b___x5d__1_expandListLit___closed__9;
LEAN_EXPORT lean_object* l_List_eraseIdx___rarg(lean_object*, lean_object*);
@ -132,10 +134,12 @@ static lean_object* l_Lean___aux__Init__Data__List__Basic______macroRules__term_
LEAN_EXPORT lean_object* l___private_Init_Data_List_Basic_0__List_lengthTRAux_match__1_splitter(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_filter___rarg(lean_object*, lean_object*);
lean_object* l_Lean_SourceInfo_fromRef(lean_object*, uint8_t);
LEAN_EXPORT lean_object* l_List_zipWithAll(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_findSome_x3f___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_zip(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_dropLast(lean_object*);
LEAN_EXPORT lean_object* l_List_replicate___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_mapTR_loop___at_List_zipWithAll___spec__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_term_x25_x5b___x7c___x5d___closed__6;
static lean_object* l_term_x5b___x5d___closed__7;
LEAN_EXPORT lean_object* l_List_span___rarg(lean_object*, lean_object*);
@ -245,6 +249,7 @@ static lean_object* l_Lean___aux__Init__Data__List__Basic______macroRules__term_
LEAN_EXPORT lean_object* l_List_any(lean_object*);
lean_object* l_id___rarg___boxed(lean_object*);
lean_object* l_Lean_Name_mkStr2(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_mapTR_loop___at_List_zipWithAll___spec__2___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_List_instAppendList___closed__1;
LEAN_EXPORT lean_object* l_List_eraseReps___rarg(lean_object*, lean_object*);
static lean_object* l_term_x5b___x5d___closed__21;
@ -284,6 +289,7 @@ LEAN_EXPORT lean_object* l_List_maximum_x3f(lean_object*);
LEAN_EXPORT lean_object* l_List_isPrefixOf_x3f(lean_object*);
LEAN_EXPORT lean_object* l_List_or___boxed(lean_object*);
LEAN_EXPORT lean_object* l_List_foldr(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_mapTR_loop___at_List_zipWithAll___spec__2(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_appendTR(lean_object*);
LEAN_EXPORT lean_object* l_List_takeWhile(lean_object*);
LEAN_EXPORT lean_object* l_List_take(lean_object*);
@ -4001,6 +4007,232 @@ lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_List_mapTR_loop___at_List_zipWithAll___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_4;
lean_dec(x_1);
x_4 = l_List_reverse___rarg(x_3);
return x_4;
}
else
{
uint8_t x_5;
x_5 = !lean_is_exclusive(x_2);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_6 = lean_ctor_get(x_2, 0);
x_7 = lean_ctor_get(x_2, 1);
x_8 = lean_box(0);
x_9 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_9, 0, x_6);
lean_inc(x_1);
x_10 = lean_apply_2(x_1, x_8, x_9);
lean_ctor_set(x_2, 1, x_3);
lean_ctor_set(x_2, 0, x_10);
{
lean_object* _tmp_1 = x_7;
lean_object* _tmp_2 = x_2;
x_2 = _tmp_1;
x_3 = _tmp_2;
}
goto _start;
}
else
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_12 = lean_ctor_get(x_2, 0);
x_13 = lean_ctor_get(x_2, 1);
lean_inc(x_13);
lean_inc(x_12);
lean_dec(x_2);
x_14 = lean_box(0);
x_15 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_15, 0, x_12);
lean_inc(x_1);
x_16 = lean_apply_2(x_1, x_14, x_15);
x_17 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_3);
x_2 = x_13;
x_3 = x_17;
goto _start;
}
}
}
}
LEAN_EXPORT lean_object* l_List_mapTR_loop___at_List_zipWithAll___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_List_mapTR_loop___at_List_zipWithAll___spec__1___rarg), 3, 0);
return x_4;
}
}
LEAN_EXPORT lean_object* l_List_mapTR_loop___at_List_zipWithAll___spec__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_4;
lean_dec(x_1);
x_4 = l_List_reverse___rarg(x_3);
return x_4;
}
else
{
uint8_t x_5;
x_5 = !lean_is_exclusive(x_2);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_6 = lean_ctor_get(x_2, 0);
x_7 = lean_ctor_get(x_2, 1);
x_8 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_8, 0, x_6);
x_9 = lean_box(0);
lean_inc(x_1);
x_10 = lean_apply_2(x_1, x_8, x_9);
lean_ctor_set(x_2, 1, x_3);
lean_ctor_set(x_2, 0, x_10);
{
lean_object* _tmp_1 = x_7;
lean_object* _tmp_2 = x_2;
x_2 = _tmp_1;
x_3 = _tmp_2;
}
goto _start;
}
else
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_12 = lean_ctor_get(x_2, 0);
x_13 = lean_ctor_get(x_2, 1);
lean_inc(x_13);
lean_inc(x_12);
lean_dec(x_2);
x_14 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_14, 0, x_12);
x_15 = lean_box(0);
lean_inc(x_1);
x_16 = lean_apply_2(x_1, x_14, x_15);
x_17 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_3);
x_2 = x_13;
x_3 = x_17;
goto _start;
}
}
}
}
LEAN_EXPORT lean_object* l_List_mapTR_loop___at_List_zipWithAll___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_List_mapTR_loop___at_List_zipWithAll___spec__2___rarg), 3, 0);
return x_4;
}
}
LEAN_EXPORT lean_object* l_List_zipWithAll___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_box(0);
x_5 = l_List_mapTR_loop___at_List_zipWithAll___spec__1___rarg(x_1, x_3, x_4);
return x_5;
}
else
{
if (lean_obj_tag(x_3) == 0)
{
uint8_t x_6;
x_6 = !lean_is_exclusive(x_2);
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8;
x_7 = lean_box(0);
x_8 = l_List_mapTR_loop___at_List_zipWithAll___spec__2___rarg(x_1, x_2, x_7);
return x_8;
}
else
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_9 = lean_ctor_get(x_2, 0);
x_10 = lean_ctor_get(x_2, 1);
lean_inc(x_10);
lean_inc(x_9);
lean_dec(x_2);
x_11 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_11, 0, x_9);
lean_ctor_set(x_11, 1, x_10);
x_12 = lean_box(0);
x_13 = l_List_mapTR_loop___at_List_zipWithAll___spec__2___rarg(x_1, x_11, x_12);
return x_13;
}
}
else
{
lean_object* x_14; lean_object* x_15; uint8_t x_16;
x_14 = lean_ctor_get(x_2, 0);
lean_inc(x_14);
x_15 = lean_ctor_get(x_2, 1);
lean_inc(x_15);
lean_dec(x_2);
x_16 = !lean_is_exclusive(x_3);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_17 = lean_ctor_get(x_3, 0);
x_18 = lean_ctor_get(x_3, 1);
x_19 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_19, 0, x_14);
x_20 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_20, 0, x_17);
lean_inc(x_1);
x_21 = lean_apply_2(x_1, x_19, x_20);
x_22 = l_List_zipWithAll___rarg(x_1, x_15, x_18);
lean_ctor_set(x_3, 1, x_22);
lean_ctor_set(x_3, 0, x_21);
return x_3;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_23 = lean_ctor_get(x_3, 0);
x_24 = lean_ctor_get(x_3, 1);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_3);
x_25 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_25, 0, x_14);
x_26 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_26, 0, x_23);
lean_inc(x_1);
x_27 = lean_apply_2(x_1, x_25, x_26);
x_28 = l_List_zipWithAll___rarg(x_1, x_15, x_24);
x_29 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
return x_29;
}
}
}
}
}
LEAN_EXPORT lean_object* l_List_zipWithAll(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_List_zipWithAll___rarg), 3, 0);
return x_4;
}
}
LEAN_EXPORT lean_object* l_List_unzip___rarg(lean_object* x_1) {
_start:
{

10
stage0/stdlib/Init/Data/Nat.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data.Nat
// Imports: Init.Data.Nat.Basic Init.Data.Nat.Div Init.Data.Nat.Gcd Init.Data.Nat.Bitwise Init.Data.Nat.Control Init.Data.Nat.Log2 Init.Data.Nat.Power2 Init.Data.Nat.Linear Init.Data.Nat.SOM
// Imports: Init.Data.Nat.Basic Init.Data.Nat.Div Init.Data.Nat.Dvd Init.Data.Nat.Gcd Init.Data.Nat.MinMax Init.Data.Nat.Bitwise Init.Data.Nat.Control Init.Data.Nat.Log2 Init.Data.Nat.Power2 Init.Data.Nat.Linear Init.Data.Nat.SOM
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -15,7 +15,9 @@ extern "C" {
#endif
lean_object* initialize_Init_Data_Nat_Basic(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Nat_Div(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Nat_Dvd(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Nat_Gcd(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Nat_MinMax(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Nat_Bitwise(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Nat_Control(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Nat_Log2(uint8_t builtin, lean_object*);
@ -33,9 +35,15 @@ lean_dec_ref(res);
res = initialize_Init_Data_Nat_Div(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Nat_Dvd(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Nat_Gcd(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Nat_MinMax(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Nat_Bitwise(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

66
stage0/stdlib/Init/Data/Nat/Dvd.c generated Normal file
View file

@ -0,0 +1,66 @@
// Lean compiler output
// Module: Init.Data.Nat.Dvd
// Imports: Init.Data.Nat.Div
#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_EXPORT lean_object* l_Nat_decidable__dvd___boxed(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Nat_decidable__dvd(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Nat_instDvdNat;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* lean_nat_mod(lean_object*, lean_object*);
static lean_object* _init_l_Nat_instDvdNat() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
LEAN_EXPORT uint8_t l_Nat_decidable__dvd(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_3 = lean_nat_mod(x_2, x_1);
x_4 = lean_unsigned_to_nat(0u);
x_5 = lean_nat_dec_eq(x_3, x_4);
lean_dec(x_3);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Nat_decidable__dvd___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Nat_decidable__dvd(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* initialize_Init_Data_Nat_Div(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data_Nat_Dvd(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_Data_Nat_Div(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Nat_instDvdNat = _init_l_Nat_instDvdNat();
lean_mark_persistent(l_Nat_instDvdNat);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

6
stage0/stdlib/Init/Data/Nat/Gcd.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data.Nat.Gcd
// Imports: Init.Data.Nat.Div
// Imports: Init.Data.Nat.Dvd
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -25,13 +25,13 @@ lean_dec(x_1);
return x_3;
}
}
lean_object* initialize_Init_Data_Nat_Div(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Nat_Dvd(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data_Nat_Gcd(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_Data_Nat_Div(builtin, lean_io_mk_world());
res = initialize_Init_Data_Nat_Dvd(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));

10
stage0/stdlib/Init/Data/Nat/Linear.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data.Nat.Linear
// Imports: Init.Coe Init.Classical Init.SimpLemmas Init.Data.Nat.Basic Init.Data.List.Basic Init.Data.Prod
// Imports: Init.Coe Init.ByCases Init.Data.Nat.Basic Init.Data.List.Basic Init.Data.Prod
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -4016,8 +4016,7 @@ return x_4;
}
}
lean_object* initialize_Init_Coe(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Classical(uint8_t builtin, lean_object*);
lean_object* initialize_Init_SimpLemmas(uint8_t builtin, lean_object*);
lean_object* initialize_Init_ByCases(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Nat_Basic(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_List_Basic(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Prod(uint8_t builtin, lean_object*);
@ -4029,10 +4028,7 @@ _G_initialized = true;
res = initialize_Init_Coe(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Classical(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_SimpLemmas(builtin, lean_io_mk_world());
res = initialize_Init_ByCases(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Nat_Basic(builtin, lean_io_mk_world());

29
stage0/stdlib/Init/Data/Nat/MinMax.c generated Normal file
View file

@ -0,0 +1,29 @@
// Lean compiler output
// Module: Init.Data.Nat.MinMax
// Imports: Init.ByCases
#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_ByCases(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data_Nat_MinMax(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_ByCases(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

409
stage0/stdlib/Init/Notation.c generated
View file

@ -20,6 +20,7 @@ static lean_object* l___aux__Init__Notation______macroRules__termWithout__expect
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x2f____1(lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Notation______macroRules__term___x5c_x2f____1___closed__7;
static lean_object* l_termDepIfThenElse___closed__6;
LEAN_EXPORT lean_object* l_Lean_runMeta;
static lean_object* l_precArg___closed__5;
static lean_object* l___aux__Init__Notation______macroRules__termWithout__expected__type____1___closed__9;
static lean_object* l_boolIfThenElse___closed__9;
@ -99,6 +100,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x3e_x3e____1
static lean_object* l_Lean_binderIdent___closed__4;
static lean_object* l_term___x24_______closed__1;
static lean_object* l_termIfThenElse___closed__4;
static lean_object* l_Lean_runMeta___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term_x7b___x3a___x2f_x2f___x7d__1___closed__7;
static lean_object* l___aux__Init__Notation______macroRules__term___x3d_x3d____1___closed__6;
static lean_object* l_term_x7e_x7e_x7e_____closed__7;
@ -114,6 +116,7 @@ static lean_object* l_term___x3c_x3d_____closed__4;
LEAN_EXPORT lean_object* l_Lean_Parser_Category_command;
static lean_object* l_term___x26_x26_x26_____closed__2;
static lean_object* l_termDepIfThenElse___closed__21;
static lean_object* l_Lean_runCmd___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__termDepIfThenElse__1___closed__4;
LEAN_EXPORT lean_object* l_term___x26_x26__;
static lean_object* l_termIfLet___closed__17;
@ -148,6 +151,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x3d____2
static lean_object* l_term___x3e_____closed__5;
static lean_object* l___aux__Init__Notation______macroRules__term_x2d____1___closed__7;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__or__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_runCmd___closed__5;
static lean_object* l_term___x3c_x24_x3e_____closed__5;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x3d____2___closed__2;
static lean_object* l___aux__Init__Notation______macroRules__term___u2218____1___closed__4;
@ -169,6 +173,7 @@ lean_object* lean_array_push(lean_object*, lean_object*);
static lean_object* l_term___x5e_x5e_x5e_____closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___x3d_x3d____1___closed__2;
static lean_object* l_Lean_rawStx_quot___closed__9;
static lean_object* l_Lean_byElab___closed__2;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term_x21____1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_Category_rawStx;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___u2264____2(lean_object*, lean_object*, lean_object*);
@ -247,6 +252,7 @@ static lean_object* l_termDepIfThenElse___closed__11;
static lean_object* l_stx___x2c_x2a_x2c_x3f___closed__4;
static lean_object* l_term___x3d_____closed__2;
static lean_object* l___aux__Init__Notation______macroRules__boolIfThenElse__1___closed__7;
static lean_object* l_Lean_runMeta___closed__6;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__Neg__neg__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Syntax_addPrec___closed__3;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__HDiv__hDiv__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -271,6 +277,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a_x3e_
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__HDiv__hDiv__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_term___x5e_x5e_x5e_____closed__6;
static lean_object* l___aux__Init__Notation______macroRules__term___x3e____1___closed__6;
static lean_object* l_Lean_byElab___closed__7;
static lean_object* l_term___x2f_x5c_____closed__4;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__HShiftRight__hShiftRight__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_precLead___closed__3;
@ -316,6 +323,7 @@ static lean_object* l_term___x3c_x2a_x3e_____closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___x2a_x3e____1___closed__1;
static lean_object* l___aux__Init__Notation______macroRules__term___x2a_x3e____1___closed__5;
static lean_object* l_term___x5e_x5e_x5e_____closed__2;
static lean_object* l_Lean_runMeta___closed__1;
LEAN_EXPORT lean_object* l_Lean_Parser_Category_term;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__stx___x2c_x2b__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_term___x3c_x2a_____closed__4;
@ -355,12 +363,14 @@ static lean_object* l_term___u2208_____closed__3;
static lean_object* l___aux__Init__Notation______macroRules__termWithout__expected__type____1___closed__2;
static lean_object* l_term___x7c_x7c_____closed__2;
static lean_object* l_Lean_withAnnotateTerm___closed__1;
static lean_object* l_Lean_runCmd___closed__2;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c____1___closed__1;
static lean_object* l_precMax___closed__2;
static lean_object* l_Lean_Attr_coe___closed__4;
static lean_object* l_Lean_deprecated___closed__1;
static lean_object* l_term___u2223_____closed__3;
static lean_object* l_term_x7b___x3a___x2f_x2f___x7d___closed__18;
static lean_object* l_Lean_runElab___closed__1;
static lean_object* l_termIfLet___closed__9;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x25____1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x2b_x2b____1(lean_object*, lean_object*, lean_object*);
@ -394,6 +404,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a_x3e_
static lean_object* l___aux__Init__Notation______macroRules__term___x5e____2___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term_x2d____1___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__termIfLet__1___closed__9;
static lean_object* l_Lean_byElab___closed__5;
static lean_object* l_term___x3c_x3c_x3c_____closed__1;
static lean_object* l_termDepIfThenElse___closed__18;
static lean_object* l_termMax__prec___closed__1;
@ -443,6 +454,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Category_stx;
static lean_object* l___aux__Init__Notation______macroRules__boolIfThenElse__1___closed__1;
static lean_object* l_term___x5e_____closed__7;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x3c_x3d____1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_runCmd___closed__4;
static lean_object* l_prec_x28___x29___closed__8;
static lean_object* l___aux__Init__Notation______macroRules__term___xd7____1___closed__7;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a_x3e____1___closed__15;
@ -504,6 +516,7 @@ static lean_object* l_Lean_Parser_Syntax_subPrio___closed__1;
LEAN_EXPORT lean_object* l_Lean_instCoeSyntaxTSyntaxConsSyntaxNodeKindMkStr1Nil(lean_object*);
static lean_object* l_term___x7c_x7c_____closed__4;
static lean_object* l_termIfLet___closed__7;
static lean_object* l_Lean_byElab___closed__9;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x26_x26____1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Syntax_subPrec___closed__1;
static lean_object* l_term___x3d_x3d_____closed__3;
@ -514,6 +527,7 @@ LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__Prod__1(lean_obj
static lean_object* l_termIfThenElse___closed__9;
static lean_object* l___aux__Init__Notation______macroRules__term___x3e_x3d____1___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term_x2d____2___closed__1;
static lean_object* l_Lean_runElab___closed__2;
static lean_object* l___aux__Init__Notation______macroRules__termIfLet__1___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term___x26_x26____1___closed__7;
static lean_object* l_term_x7e_x7e_x7e_____closed__3;
@ -675,6 +689,7 @@ static lean_object* l_termDepIfThenElse___closed__9;
static lean_object* l_term_x2d_____closed__4;
LEAN_EXPORT lean_object* l_Lean_Parser_Category_attr;
static lean_object* l___aux__Init__Notation______macroRules__term___x3e_x3d____1___closed__5;
static lean_object* l_Lean_runElab___closed__6;
static lean_object* l___aux__Init__Notation______macroRules__term___xd7____1___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___x3e____1___closed__5;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__HAdd__hAdd__1(lean_object*, lean_object*, lean_object*);
@ -687,6 +702,7 @@ static lean_object* l_Lean_Parser_Syntax_addPrec___closed__7;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x3c_x3c____1___closed__3;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__HAppend__hAppend__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Notation______macroRules__prioMid__1___closed__1;
static lean_object* l_Lean_byElab___closed__3;
static lean_object* l_term___xd7_____closed__1;
static lean_object* l_term___x3a_x3a_____closed__5;
static lean_object* l___aux__Init__Notation______macroRules__term___x2b_x2b____1___closed__2;
@ -772,6 +788,7 @@ static lean_object* l___aux__Init__Notation______macroRules__boolIfThenElse__1__
static lean_object* l_term___x2b_x2b_____closed__3;
static lean_object* l_prioDefault___closed__5;
static lean_object* l_term_x7b___x3a___x2f_x2f___x7d___closed__11;
LEAN_EXPORT lean_object* l_Lean_runCmd;
static lean_object* l___aux__Init__Notation______macroRules__stx___x2b__1___closed__1;
static lean_object* l_Lean_rawStx_quot___closed__8;
static lean_object* l___aux__Init__Notation______macroRules__term___u2218____1___closed__6;
@ -859,6 +876,7 @@ static lean_object* l_term___x5c_x2f_____closed__3;
static lean_object* l_term___x3d_x3d_____closed__5;
static lean_object* l_termIfThenElse___closed__1;
static lean_object* l___aux__Init__Notation______macroRules__term_x7b___x3a___x2f_x2f___x7d__1___closed__4;
static lean_object* l_Lean_byElab___closed__8;
static lean_object* l_precMax___closed__5;
LEAN_EXPORT lean_object* l_boolIfThenElse;
static lean_object* l_term___u2218_____closed__1;
@ -872,7 +890,9 @@ lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Notation______macroRules__term___x3e_x3e_x3d____1___closed__4;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__SeqRight__seqRight__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_node4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_runElab;
LEAN_EXPORT lean_object* l_Lean_Parser_Syntax_addPrio;
static lean_object* l_Lean_byElab___closed__1;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x5c_x2f____1(lean_object*, lean_object*, lean_object*);
static lean_object* l_term___x26_x26_____closed__1;
static lean_object* l_Lean_Parser_Tactic_caseArg___closed__1;
@ -999,6 +1019,7 @@ static lean_object* l___aux__Init__Notation______macroRules__termIfThenElse__1__
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__LE__le__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_term___x5e_____closed__3;
static lean_object* l_stx___x2a___closed__5;
static lean_object* l_Lean_runElab___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a____1___closed__7;
static lean_object* l_termDepIfThenElse___closed__5;
LEAN_EXPORT lean_object* l_termMax__prec;
@ -1018,6 +1039,7 @@ static lean_object* l_Lean_Parser_Syntax_subPrec___closed__2;
static lean_object* l___aux__Init__Notation______macroRules__term___x2b____1___closed__5;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__HXor__hXor__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_stx___x3f___closed__2;
static lean_object* l_Lean_runMeta___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c____1___closed__5;
static lean_object* l_Lean_Attr_coe___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term___x2f_x5c____1___closed__5;
@ -1084,6 +1106,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___xd7____1___c
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__Functor__map__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_termIfThenElse;
static lean_object* l___aux__Init__Notation______macroRules__term___x7c_x7c____1___closed__3;
static lean_object* l_Lean_byElab___closed__6;
static lean_object* l_term___x3e_x3e_x3e_____closed__1;
static lean_object* l_term___x5e_x5e_x5e_____closed__1;
static lean_object* l_stx___x2a___closed__4;
@ -1091,6 +1114,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x2f____1___c
static lean_object* l_term___u2227_____closed__4;
static lean_object* l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__3;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__and__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_byElab___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term_x7e_x7e_x7e____1___closed__2;
LEAN_EXPORT lean_object* l_term___x2a__;
static lean_object* l_Lean_Parser_Tactic_caseArg___closed__5;
@ -1210,6 +1234,7 @@ static lean_object* l_term___x2b_x2b_____closed__2;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c____1___closed__7;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a_x3e____1___closed__10;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__LE__le__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_runMeta___closed__5;
static lean_object* l_term___x26_x26_____closed__6;
static lean_object* l_term___x3d_x3d_____closed__6;
static lean_object* l___aux__Init__Notation______macroRules__term___u2218____1___closed__7;
@ -1225,6 +1250,7 @@ LEAN_EXPORT lean_object* l_term___u2227__;
static lean_object* l_term_x7e_x7e_x7e_____closed__4;
static lean_object* l_term___x3a_x3a_____closed__4;
static lean_object* l_prec_x28___x29___closed__7;
static lean_object* l_Lean_runElab___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term_x7e_x7e_x7e____1___closed__3;
static lean_object* l_term___x3e_____closed__2;
static lean_object* l___aux__Init__Notation______macroRules__term___u2218____1___closed__12;
@ -1266,6 +1292,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x5e____2___c
static lean_object* l___aux__Init__Notation______macroRules__term___x5e____1___closed__2;
static lean_object* l_termDepIfThenElse___closed__7;
static lean_object* l_Lean_deprecated___closed__5;
static lean_object* l_Lean_runCmd___closed__1;
static lean_object* l_termWithout__expected__type_____closed__1;
static lean_object* l_term_x7b___x3a___x2f_x2f___x7d___closed__1;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
@ -1291,6 +1318,7 @@ static lean_object* l_prio_x28___x29___closed__1;
static lean_object* l___aux__Init__Notation______macroRules__term___x26_x26____1___closed__3;
LEAN_EXPORT lean_object* l_term_xac__;
static lean_object* l___aux__Init__Notation______macroRules__term___xd7____1___closed__5;
static lean_object* l_Lean_runMeta___closed__2;
static lean_object* l___aux__Init__Notation______macroRules__term___x3a_x3a____1___closed__1;
static lean_object* l___aux__Init__Notation______macroRules__term___x2a____1___closed__5;
LEAN_EXPORT lean_object* l_Lean_instCoeOutTSyntaxSyntax___rarg___boxed(lean_object*);
@ -1304,14 +1332,17 @@ static lean_object* l_termWithout__expected__type_____closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___x25____1___closed__7;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__Function__comp__1___lambda__1(lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Notation______macroRules__term_xac____1___closed__1;
static lean_object* l_Lean_runCmd___closed__6;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__List__cons__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Notation______macroRules__term___x3e_x3d____1___closed__6;
static lean_object* l_term___x2b_x2b_____closed__4;
LEAN_EXPORT lean_object* l_Lean_byElab;
static lean_object* l_stx___x2b___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a____1___closed__3;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__SeqRight__seqRight__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_withAnnotateTerm___closed__3;
static lean_object* l_term___x24_______closed__4;
static lean_object* l_Lean_runElab___closed__5;
static lean_object* l___aux__Init__Notation______macroRules__term_x7e_x7e_x7e____1___closed__7;
static lean_object* l_Lean_Parser_Syntax_subPrio___closed__2;
LEAN_EXPORT lean_object* l_stx___x2c_x2a;
@ -25976,6 +26007,106 @@ return x_35;
}
}
}
static lean_object* _init_l_Lean_byElab___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("byElab", 6);
return x_1;
}
}
static lean_object* _init_l_Lean_byElab___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__1;
x_2 = l_Lean_byElab___closed__1;
x_3 = l_Lean_Name_mkStr2(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_byElab___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("by_elab ", 8);
return x_1;
}
}
static lean_object* _init_l_Lean_byElab___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_byElab___closed__3;
x_2 = lean_alloc_ctor(5, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_byElab___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("doSeq", 5);
return x_1;
}
}
static lean_object* _init_l_Lean_byElab___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_byElab___closed__5;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_byElab___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_byElab___closed__6;
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_byElab___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__7;
x_2 = l_Lean_byElab___closed__4;
x_3 = l_Lean_byElab___closed__7;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_byElab___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_byElab___closed__2;
x_2 = lean_unsigned_to_nat(1022u);
x_3 = l_Lean_byElab___closed__8;
x_4 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_byElab() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_byElab___closed__9;
return x_1;
}
}
static lean_object* _init_l_Lean_rawStx_quot___closed__1() {
_start:
{
@ -26467,6 +26598,222 @@ x_1 = l_Lean_includeStr___closed__6;
return x_1;
}
}
static lean_object* _init_l_Lean_runCmd___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("runCmd", 6);
return x_1;
}
}
static lean_object* _init_l_Lean_runCmd___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__1;
x_2 = l_Lean_runCmd___closed__1;
x_3 = l_Lean_Name_mkStr2(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_runCmd___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("run_cmd ", 8);
return x_1;
}
}
static lean_object* _init_l_Lean_runCmd___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_runCmd___closed__3;
x_2 = lean_alloc_ctor(5, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_runCmd___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__7;
x_2 = l_Lean_runCmd___closed__4;
x_3 = l_Lean_byElab___closed__7;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_runCmd___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_runCmd___closed__2;
x_2 = lean_unsigned_to_nat(1022u);
x_3 = l_Lean_runCmd___closed__5;
x_4 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_runCmd() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_runCmd___closed__6;
return x_1;
}
}
static lean_object* _init_l_Lean_runElab___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("runElab", 7);
return x_1;
}
}
static lean_object* _init_l_Lean_runElab___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__1;
x_2 = l_Lean_runElab___closed__1;
x_3 = l_Lean_Name_mkStr2(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_runElab___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("run_elab ", 9);
return x_1;
}
}
static lean_object* _init_l_Lean_runElab___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_runElab___closed__3;
x_2 = lean_alloc_ctor(5, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_runElab___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__7;
x_2 = l_Lean_runElab___closed__4;
x_3 = l_Lean_byElab___closed__7;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_runElab___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_runElab___closed__2;
x_2 = lean_unsigned_to_nat(1022u);
x_3 = l_Lean_runElab___closed__5;
x_4 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_runElab() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_runElab___closed__6;
return x_1;
}
}
static lean_object* _init_l_Lean_runMeta___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("runMeta", 7);
return x_1;
}
}
static lean_object* _init_l_Lean_runMeta___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__1;
x_2 = l_Lean_runMeta___closed__1;
x_3 = l_Lean_Name_mkStr2(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_runMeta___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("run_meta ", 9);
return x_1;
}
}
static lean_object* _init_l_Lean_runMeta___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_runMeta___closed__3;
x_2 = lean_alloc_ctor(5, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_runMeta___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__7;
x_2 = l_Lean_runMeta___closed__4;
x_3 = l_Lean_byElab___closed__7;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_runMeta___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_runMeta___closed__2;
x_2 = lean_unsigned_to_nat(1022u);
x_3 = l_Lean_runMeta___closed__5;
x_4 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_runMeta() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_runMeta___closed__6;
return x_1;
}
}
lean_object* initialize_Init_Prelude(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Coe(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
@ -28650,6 +28997,26 @@ l___aux__Init__Notation______macroRules__termWithout__expected__type____1___clos
lean_mark_persistent(l___aux__Init__Notation______macroRules__termWithout__expected__type____1___closed__8);
l___aux__Init__Notation______macroRules__termWithout__expected__type____1___closed__9 = _init_l___aux__Init__Notation______macroRules__termWithout__expected__type____1___closed__9();
lean_mark_persistent(l___aux__Init__Notation______macroRules__termWithout__expected__type____1___closed__9);
l_Lean_byElab___closed__1 = _init_l_Lean_byElab___closed__1();
lean_mark_persistent(l_Lean_byElab___closed__1);
l_Lean_byElab___closed__2 = _init_l_Lean_byElab___closed__2();
lean_mark_persistent(l_Lean_byElab___closed__2);
l_Lean_byElab___closed__3 = _init_l_Lean_byElab___closed__3();
lean_mark_persistent(l_Lean_byElab___closed__3);
l_Lean_byElab___closed__4 = _init_l_Lean_byElab___closed__4();
lean_mark_persistent(l_Lean_byElab___closed__4);
l_Lean_byElab___closed__5 = _init_l_Lean_byElab___closed__5();
lean_mark_persistent(l_Lean_byElab___closed__5);
l_Lean_byElab___closed__6 = _init_l_Lean_byElab___closed__6();
lean_mark_persistent(l_Lean_byElab___closed__6);
l_Lean_byElab___closed__7 = _init_l_Lean_byElab___closed__7();
lean_mark_persistent(l_Lean_byElab___closed__7);
l_Lean_byElab___closed__8 = _init_l_Lean_byElab___closed__8();
lean_mark_persistent(l_Lean_byElab___closed__8);
l_Lean_byElab___closed__9 = _init_l_Lean_byElab___closed__9();
lean_mark_persistent(l_Lean_byElab___closed__9);
l_Lean_byElab = _init_l_Lean_byElab();
lean_mark_persistent(l_Lean_byElab);
l_Lean_rawStx_quot___closed__1 = _init_l_Lean_rawStx_quot___closed__1();
lean_mark_persistent(l_Lean_rawStx_quot___closed__1);
l_Lean_rawStx_quot___closed__2 = _init_l_Lean_rawStx_quot___closed__2();
@ -28738,6 +29105,48 @@ l_Lean_includeStr___closed__6 = _init_l_Lean_includeStr___closed__6();
lean_mark_persistent(l_Lean_includeStr___closed__6);
l_Lean_includeStr = _init_l_Lean_includeStr();
lean_mark_persistent(l_Lean_includeStr);
l_Lean_runCmd___closed__1 = _init_l_Lean_runCmd___closed__1();
lean_mark_persistent(l_Lean_runCmd___closed__1);
l_Lean_runCmd___closed__2 = _init_l_Lean_runCmd___closed__2();
lean_mark_persistent(l_Lean_runCmd___closed__2);
l_Lean_runCmd___closed__3 = _init_l_Lean_runCmd___closed__3();
lean_mark_persistent(l_Lean_runCmd___closed__3);
l_Lean_runCmd___closed__4 = _init_l_Lean_runCmd___closed__4();
lean_mark_persistent(l_Lean_runCmd___closed__4);
l_Lean_runCmd___closed__5 = _init_l_Lean_runCmd___closed__5();
lean_mark_persistent(l_Lean_runCmd___closed__5);
l_Lean_runCmd___closed__6 = _init_l_Lean_runCmd___closed__6();
lean_mark_persistent(l_Lean_runCmd___closed__6);
l_Lean_runCmd = _init_l_Lean_runCmd();
lean_mark_persistent(l_Lean_runCmd);
l_Lean_runElab___closed__1 = _init_l_Lean_runElab___closed__1();
lean_mark_persistent(l_Lean_runElab___closed__1);
l_Lean_runElab___closed__2 = _init_l_Lean_runElab___closed__2();
lean_mark_persistent(l_Lean_runElab___closed__2);
l_Lean_runElab___closed__3 = _init_l_Lean_runElab___closed__3();
lean_mark_persistent(l_Lean_runElab___closed__3);
l_Lean_runElab___closed__4 = _init_l_Lean_runElab___closed__4();
lean_mark_persistent(l_Lean_runElab___closed__4);
l_Lean_runElab___closed__5 = _init_l_Lean_runElab___closed__5();
lean_mark_persistent(l_Lean_runElab___closed__5);
l_Lean_runElab___closed__6 = _init_l_Lean_runElab___closed__6();
lean_mark_persistent(l_Lean_runElab___closed__6);
l_Lean_runElab = _init_l_Lean_runElab();
lean_mark_persistent(l_Lean_runElab);
l_Lean_runMeta___closed__1 = _init_l_Lean_runMeta___closed__1();
lean_mark_persistent(l_Lean_runMeta___closed__1);
l_Lean_runMeta___closed__2 = _init_l_Lean_runMeta___closed__2();
lean_mark_persistent(l_Lean_runMeta___closed__2);
l_Lean_runMeta___closed__3 = _init_l_Lean_runMeta___closed__3();
lean_mark_persistent(l_Lean_runMeta___closed__3);
l_Lean_runMeta___closed__4 = _init_l_Lean_runMeta___closed__4();
lean_mark_persistent(l_Lean_runMeta___closed__4);
l_Lean_runMeta___closed__5 = _init_l_Lean_runMeta___closed__5();
lean_mark_persistent(l_Lean_runMeta___closed__5);
l_Lean_runMeta___closed__6 = _init_l_Lean_runMeta___closed__6();
lean_mark_persistent(l_Lean_runMeta___closed__6);
l_Lean_runMeta = _init_l_Lean_runMeta();
lean_mark_persistent(l_Lean_runMeta);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

295
stage0/stdlib/Init/PropLemmas.c generated Normal file
View file

@ -0,0 +1,295 @@
// Lean compiler output
// Module: Init.PropLemmas
// Imports: Init.Core Init.NotationExtra
#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_EXPORT lean_object* l_decidable__of__iff(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Or_by__cases_x27(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_exists__prop__decidable___rarg___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_forall__prop__decidable(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_exists__prop__decidable___rarg(uint8_t, lean_object*);
LEAN_EXPORT lean_object* l_forall__prop__decidable___rarg___boxed(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_decidable__of__bool___rarg(uint8_t, lean_object*);
LEAN_EXPORT lean_object* l_Or_by__cases(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_decidable__of__bool(lean_object*);
LEAN_EXPORT uint8_t l_decidable__of__iff_x27___rarg(uint8_t);
LEAN_EXPORT lean_object* l_decidable__of__bool___rarg___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_decidable__of__iff___rarg___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Or_by__cases___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_decidable__of__iff___rarg(uint8_t);
LEAN_EXPORT lean_object* l_decidable__of__iff_x27(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Decidable_predToBool___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Decidable_predToBool(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_decidable__of__iff_x27___rarg___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Or_by__cases___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_forall__prop__decidable___rarg(uint8_t, lean_object*);
LEAN_EXPORT lean_object* l_exists__prop__decidable(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Or_by__cases_x27___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Or_by__cases_x27___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Or_by__cases___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
if (x_1 == 0)
{
lean_object* x_6;
lean_dec(x_4);
x_6 = lean_apply_1(x_5, lean_box(0));
return x_6;
}
else
{
lean_object* x_7;
lean_dec(x_5);
x_7 = lean_apply_1(x_4, lean_box(0));
return x_7;
}
}
}
LEAN_EXPORT lean_object* l_Or_by__cases(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Or_by__cases___rarg___boxed), 5, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Or_by__cases___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
uint8_t x_6; lean_object* x_7;
x_6 = lean_unbox(x_1);
lean_dec(x_1);
x_7 = l_Or_by__cases___rarg(x_6, x_2, x_3, x_4, x_5);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Or_by__cases_x27___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
if (x_1 == 0)
{
lean_object* x_6;
lean_dec(x_5);
x_6 = lean_apply_1(x_4, lean_box(0));
return x_6;
}
else
{
lean_object* x_7;
lean_dec(x_4);
x_7 = lean_apply_1(x_5, lean_box(0));
return x_7;
}
}
}
LEAN_EXPORT lean_object* l_Or_by__cases_x27(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Or_by__cases_x27___rarg___boxed), 5, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Or_by__cases_x27___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
uint8_t x_6; lean_object* x_7;
x_6 = lean_unbox(x_1);
lean_dec(x_1);
x_7 = l_Or_by__cases_x27___rarg(x_6, x_2, x_3, x_4, x_5);
return x_7;
}
}
LEAN_EXPORT lean_object* l_exists__prop__decidable___rarg(uint8_t x_1, lean_object* x_2) {
_start:
{
if (x_1 == 0)
{
uint8_t x_3; lean_object* x_4;
lean_dec(x_2);
x_3 = 0;
x_4 = lean_box(x_3);
return x_4;
}
else
{
lean_object* x_5;
x_5 = lean_apply_1(x_2, lean_box(0));
return x_5;
}
}
}
LEAN_EXPORT lean_object* l_exists__prop__decidable(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_exists__prop__decidable___rarg___boxed), 2, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_exists__prop__decidable___rarg___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = l_exists__prop__decidable___rarg(x_3, x_2);
return x_4;
}
}
LEAN_EXPORT lean_object* l_forall__prop__decidable___rarg(uint8_t x_1, lean_object* x_2) {
_start:
{
if (x_1 == 0)
{
uint8_t x_3; lean_object* x_4;
lean_dec(x_2);
x_3 = 1;
x_4 = lean_box(x_3);
return x_4;
}
else
{
lean_object* x_5;
x_5 = lean_apply_1(x_2, lean_box(0));
return x_5;
}
}
}
LEAN_EXPORT lean_object* l_forall__prop__decidable(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_forall__prop__decidable___rarg___boxed), 2, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_forall__prop__decidable___rarg___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = l_forall__prop__decidable___rarg(x_3, x_2);
return x_4;
}
}
LEAN_EXPORT uint8_t l_decidable__of__iff___rarg(uint8_t x_1) {
_start:
{
return x_1;
}
}
LEAN_EXPORT lean_object* l_decidable__of__iff(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_decidable__of__iff___rarg___boxed), 1, 0);
return x_4;
}
}
LEAN_EXPORT lean_object* l_decidable__of__iff___rarg___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; uint8_t x_3; lean_object* x_4;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_decidable__of__iff___rarg(x_2);
x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT uint8_t l_decidable__of__iff_x27___rarg(uint8_t x_1) {
_start:
{
return x_1;
}
}
LEAN_EXPORT lean_object* l_decidable__of__iff_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_decidable__of__iff_x27___rarg___boxed), 1, 0);
return x_4;
}
}
LEAN_EXPORT lean_object* l_decidable__of__iff_x27___rarg___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; uint8_t x_3; lean_object* x_4;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_decidable__of__iff_x27___rarg(x_2);
x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Decidable_predToBool___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_apply_1(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Decidable_predToBool(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Decidable_predToBool___rarg), 2, 0);
return x_3;
}
}
LEAN_EXPORT uint8_t l_decidable__of__bool___rarg(uint8_t x_1, lean_object* x_2) {
_start:
{
return x_1;
}
}
LEAN_EXPORT lean_object* l_decidable__of__bool(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_decidable__of__bool___rarg___boxed), 2, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_decidable__of__bool___rarg___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = l_decidable__of__bool___rarg(x_3, x_2);
x_5 = lean_box(x_4);
return x_5;
}
}
lean_object* initialize_Init_Core(uint8_t builtin, lean_object*);
lean_object* initialize_Init_NotationExtra(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_PropLemmas(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_Core(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_NotationExtra(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

718
stage0/stdlib/Init/Tactics.c generated
View file

File diff suppressed because it is too large Load diff

614
stage0/stdlib/Init/TacticsExtra.c generated
View file

@ -16,7 +16,10 @@ extern "C" {
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__31;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__27;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__25;
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__4;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__30;
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__20;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1(lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__49;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__19;
@ -31,16 +34,20 @@ static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIf
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__40;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__18;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__35;
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__8;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacIfThenElse__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__13;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__41;
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacDepIfThenElse__1___closed__1;
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__3;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__51;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__16;
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacIfThenElse__1___lambda__1___closed__2;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__56;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__11;
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__9;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__3;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__55;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__42;
@ -48,16 +55,23 @@ size_t lean_usize_of_nat(lean_object*);
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacIfThenElse__1___lambda__1___closed__3;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__26;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__22;
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__1;
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacDepIfThenElse__1___lambda__1___closed__3;
lean_object* l_Lean_SourceInfo_fromRef(lean_object*, uint8_t);
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__10;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__4;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__1;
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__12;
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacIfThenElse__1___lambda__1___closed__1;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___spec__1(size_t, size_t, lean_object*);
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__6;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacIfThenElse__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__15;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__12;
lean_object* l_Lean_Syntax_node3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacDepIfThenElse__1___lambda__1___closed__1;
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__5;
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__4;
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__21;
lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
@ -67,19 +81,27 @@ static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIf
LEAN_EXPORT lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__15;
uint8_t l_Lean_Syntax_matchesNull(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticIterate________;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__36;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__9;
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__16;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__52;
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__22;
lean_object* l_Array_append___rarg(lean_object*, lean_object*);
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__45;
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__21;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__32;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__54;
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__2;
lean_object* l_Lean_Syntax_node4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacDepIfThenElse__1___lambda__1___closed__4;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacDepIfThenElse__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacDepIfThenElse__1___lambda__1___closed__5;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__24;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Name_mkStr2(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__1;
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacDepIfThenElse__1___closed__2;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__10;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__8;
@ -87,22 +109,30 @@ lean_object* l_Lean_Syntax_node1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkSepArray(lean_object*, lean_object*);
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__23;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__5;
lean_object* lean_nat_sub(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacDepIfThenElse__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__19;
size_t lean_usize_add(size_t, size_t);
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__28;
lean_object* l_Lean_Syntax_node8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_uget(lean_object*, size_t);
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__18;
lean_object* l_Lean_Name_mkStr4(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__48;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__17;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___spec__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__14;
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__17;
lean_object* lean_array_get_size(lean_object*);
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__5;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__13;
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacIfThenElse__1___closed__2;
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__11;
uint8_t lean_usize_dec_lt(size_t, size_t);
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__37;
lean_object* l_Array_mkArray2___rarg(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__14;
static lean_object* l_Lean_Parser_Tactic_tacticIterate___________closed__7;
lean_object* lean_nat_add(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacDepIfThenElse__1___lambda__1___closed__2;
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__53;
@ -111,8 +141,13 @@ static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIf
lean_object* l_String_toSubstring_x27(lean_object*);
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__38;
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__2;
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacIfThenElse__1___closed__1;
lean_object* l_Nat_repr(lean_object*);
lean_object* l_Lean_Syntax_toNat(lean_object*);
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__34;
static lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__3;
lean_object* l_Lean_Syntax_mkNumLit(lean_object*, lean_object*);
static lean_object* l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__29;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___spec__1(size_t x_1, size_t x_2, lean_object* x_3) {
_start:
@ -2390,6 +2425,529 @@ return x_29;
}
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("tacticIterate____", 17);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________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___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__1;
x_2 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__2;
x_3 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__12;
x_4 = l_Lean_Parser_Tactic_tacticIterate___________closed__1;
x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("andthen", 7);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Tactic_tacticIterate___________closed__3;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("iterate", 7);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__6() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_tacticIterate___________closed__5;
x_2 = 0;
x_3 = lean_alloc_ctor(6, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("optional", 8);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Tactic_tacticIterate___________closed__7;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__9() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("ppSpace", 7);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Tactic_tacticIterate___________closed__9;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_tacticIterate___________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_Parser_Tactic_tacticIterate___________closed__12() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("num", 3);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__13() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Tactic_tacticIterate___________closed__12;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_tacticIterate___________closed__13;
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_Parser_Tactic_tacticIterate___________closed__15() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_tacticIterate___________closed__4;
x_2 = l_Lean_Parser_Tactic_tacticIterate___________closed__11;
x_3 = l_Lean_Parser_Tactic_tacticIterate___________closed__14;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_tacticIterate___________closed__8;
x_2 = l_Lean_Parser_Tactic_tacticIterate___________closed__15;
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_Lean_Parser_Tactic_tacticIterate___________closed__17() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_tacticIterate___________closed__4;
x_2 = l_Lean_Parser_Tactic_tacticIterate___________closed__6;
x_3 = l_Lean_Parser_Tactic_tacticIterate___________closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_tacticIterate___________closed__4;
x_2 = l_Lean_Parser_Tactic_tacticIterate___________closed__17;
x_3 = l_Lean_Parser_Tactic_tacticIterate___________closed__11;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__19() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__23;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__20() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_tacticIterate___________closed__19;
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_Parser_Tactic_tacticIterate___________closed__21() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_tacticIterate___________closed__4;
x_2 = l_Lean_Parser_Tactic_tacticIterate___________closed__18;
x_3 = l_Lean_Parser_Tactic_tacticIterate___________closed__20;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate___________closed__22() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_tacticIterate___________closed__2;
x_2 = lean_unsigned_to_nat(1022u);
x_3 = l_Lean_Parser_Tactic_tacticIterate___________closed__21;
x_4 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticIterate________() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_tacticIterate___________closed__22;
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("seq1", 4);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___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___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__1;
x_2 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__2;
x_3 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__12;
x_4 = l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__1;
x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("tacticTry_", 10);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___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___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__1;
x_2 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__2;
x_3 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__12;
x_4 = l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__3;
x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("try", 3);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = l_Lean_Parser_Tactic_tacticIterate___________closed__2;
lean_inc(x_1);
x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7;
lean_dec(x_2);
lean_dec(x_1);
x_6 = lean_box(1);
x_7 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_3);
return x_7;
}
else
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_8 = lean_unsigned_to_nat(1u);
x_9 = l_Lean_Syntax_getArg(x_1, x_8);
x_10 = lean_unsigned_to_nat(0u);
lean_inc(x_9);
x_11 = l_Lean_Syntax_matchesNull(x_9, x_10);
if (x_11 == 0)
{
uint8_t x_12;
lean_inc(x_9);
x_12 = l_Lean_Syntax_matchesNull(x_9, x_8);
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14;
lean_dec(x_9);
lean_dec(x_2);
lean_dec(x_1);
x_13 = lean_box(1);
x_14 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_3);
return x_14;
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19;
x_15 = l_Lean_Syntax_getArg(x_9, x_10);
lean_dec(x_9);
x_16 = lean_unsigned_to_nat(2u);
x_17 = l_Lean_Syntax_getArg(x_1, x_16);
lean_dec(x_1);
x_18 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__24;
lean_inc(x_17);
x_19 = l_Lean_Syntax_isOfKind(x_17, x_18);
if (x_19 == 0)
{
lean_object* x_20; lean_object* x_21;
lean_dec(x_17);
lean_dec(x_15);
lean_dec(x_2);
x_20 = lean_box(1);
x_21 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_3);
return x_21;
}
else
{
lean_object* x_22; uint8_t x_23;
x_22 = l_Lean_Syntax_toNat(x_15);
lean_dec(x_15);
x_23 = lean_nat_dec_eq(x_22, x_10);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25; uint8_t x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; 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; lean_object* x_46; lean_object* x_47;
x_24 = lean_nat_sub(x_22, x_8);
lean_dec(x_22);
x_25 = lean_ctor_get(x_2, 5);
lean_inc(x_25);
lean_dec(x_2);
x_26 = 0;
x_27 = l_Lean_SourceInfo_fromRef(x_25, x_26);
x_28 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__35;
lean_inc(x_27);
x_29 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
x_30 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__51;
lean_inc(x_27);
x_31 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_31, 0, x_27);
lean_ctor_set(x_31, 1, x_30);
x_32 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__34;
lean_inc(x_17);
lean_inc(x_27);
x_33 = l_Lean_Syntax_node3(x_27, x_32, x_29, x_17, x_31);
x_34 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__49;
lean_inc(x_27);
x_35 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_35, 0, x_27);
lean_ctor_set(x_35, 1, x_34);
x_36 = l_Lean_Parser_Tactic_tacticIterate___________closed__5;
lean_inc(x_27);
x_37 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_37, 0, x_27);
lean_ctor_set(x_37, 1, x_36);
x_38 = l_Nat_repr(x_24);
x_39 = lean_box(2);
x_40 = l_Lean_Syntax_mkNumLit(x_38, x_39);
x_41 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__16;
lean_inc(x_27);
x_42 = l_Lean_Syntax_node1(x_27, x_41, x_40);
lean_inc(x_27);
x_43 = l_Lean_Syntax_node3(x_27, x_4, x_37, x_42, x_17);
lean_inc(x_27);
x_44 = l_Lean_Syntax_node3(x_27, x_41, x_33, x_35, x_43);
x_45 = l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__2;
x_46 = l_Lean_Syntax_node1(x_27, x_45, x_44);
x_47 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_47, 0, x_46);
lean_ctor_set(x_47, 1, x_3);
return x_47;
}
else
{
lean_object* x_48; uint8_t x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55;
lean_dec(x_22);
lean_dec(x_17);
x_48 = lean_ctor_get(x_2, 5);
lean_inc(x_48);
lean_dec(x_2);
x_49 = 0;
x_50 = l_Lean_SourceInfo_fromRef(x_48, x_49);
x_51 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__30;
lean_inc(x_50);
x_52 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_52, 0, x_50);
lean_ctor_set(x_52, 1, x_51);
x_53 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__31;
x_54 = l_Lean_Syntax_node1(x_50, x_53, x_52);
x_55 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_55, 0, x_54);
lean_ctor_set(x_55, 1, x_3);
return x_55;
}
}
}
}
else
{
lean_object* x_56; lean_object* x_57; lean_object* x_58; uint8_t x_59;
lean_dec(x_9);
x_56 = lean_unsigned_to_nat(2u);
x_57 = l_Lean_Syntax_getArg(x_1, x_56);
lean_dec(x_1);
x_58 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__24;
lean_inc(x_57);
x_59 = l_Lean_Syntax_isOfKind(x_57, x_58);
if (x_59 == 0)
{
lean_object* x_60; lean_object* x_61;
lean_dec(x_57);
lean_dec(x_2);
x_60 = lean_box(1);
x_61 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_61, 0, x_60);
lean_ctor_set(x_61, 1, x_3);
return x_61;
}
else
{
lean_object* x_62; uint8_t x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87;
x_62 = lean_ctor_get(x_2, 5);
lean_inc(x_62);
lean_dec(x_2);
x_63 = 0;
x_64 = l_Lean_SourceInfo_fromRef(x_62, x_63);
x_65 = l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__5;
lean_inc(x_64);
x_66 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_66, 0, x_64);
lean_ctor_set(x_66, 1, x_65);
x_67 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__35;
lean_inc(x_64);
x_68 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_68, 0, x_64);
lean_ctor_set(x_68, 1, x_67);
x_69 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__51;
lean_inc(x_64);
x_70 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_70, 0, x_64);
lean_ctor_set(x_70, 1, x_69);
x_71 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__34;
lean_inc(x_57);
lean_inc(x_64);
x_72 = l_Lean_Syntax_node3(x_64, x_71, x_68, x_57, x_70);
x_73 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__49;
lean_inc(x_64);
x_74 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_74, 0, x_64);
lean_ctor_set(x_74, 1, x_73);
x_75 = l_Lean_Parser_Tactic_tacticIterate___________closed__5;
lean_inc(x_64);
x_76 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_76, 0, x_64);
lean_ctor_set(x_76, 1, x_75);
x_77 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__16;
x_78 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__21;
lean_inc(x_64);
x_79 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_79, 0, x_64);
lean_ctor_set(x_79, 1, x_77);
lean_ctor_set(x_79, 2, x_78);
lean_inc(x_64);
x_80 = l_Lean_Syntax_node3(x_64, x_4, x_76, x_79, x_57);
lean_inc(x_64);
x_81 = l_Lean_Syntax_node3(x_64, x_77, x_72, x_74, x_80);
x_82 = l___private_Init_TacticsExtra_0__Lean_Parser_Tactic_expandIfThenElse___closed__26;
lean_inc(x_64);
x_83 = l_Lean_Syntax_node1(x_64, x_82, x_81);
lean_inc(x_64);
x_84 = l_Lean_Syntax_node1(x_64, x_58, x_83);
x_85 = l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__4;
x_86 = l_Lean_Syntax_node2(x_64, x_85, x_66, x_84);
x_87 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_87, 0, x_86);
lean_ctor_set(x_87, 1, x_3);
return x_87;
}
}
}
}
}
lean_object* initialize_Init_Tactics(uint8_t builtin, lean_object*);
lean_object* initialize_Init_NotationExtra(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
@ -2541,6 +3099,62 @@ l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Ta
lean_mark_persistent(l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacIfThenElse__1___closed__1);
l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacIfThenElse__1___closed__2 = _init_l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacIfThenElse__1___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacIfThenElse__1___closed__2);
l_Lean_Parser_Tactic_tacticIterate___________closed__1 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__1);
l_Lean_Parser_Tactic_tacticIterate___________closed__2 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__2);
l_Lean_Parser_Tactic_tacticIterate___________closed__3 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__3);
l_Lean_Parser_Tactic_tacticIterate___________closed__4 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__4();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__4);
l_Lean_Parser_Tactic_tacticIterate___________closed__5 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__5);
l_Lean_Parser_Tactic_tacticIterate___________closed__6 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__6();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__6);
l_Lean_Parser_Tactic_tacticIterate___________closed__7 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__7();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__7);
l_Lean_Parser_Tactic_tacticIterate___________closed__8 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__8();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__8);
l_Lean_Parser_Tactic_tacticIterate___________closed__9 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__9();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__9);
l_Lean_Parser_Tactic_tacticIterate___________closed__10 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__10();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__10);
l_Lean_Parser_Tactic_tacticIterate___________closed__11 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__11();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__11);
l_Lean_Parser_Tactic_tacticIterate___________closed__12 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__12();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__12);
l_Lean_Parser_Tactic_tacticIterate___________closed__13 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__13();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__13);
l_Lean_Parser_Tactic_tacticIterate___________closed__14 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__14();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__14);
l_Lean_Parser_Tactic_tacticIterate___________closed__15 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__15();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__15);
l_Lean_Parser_Tactic_tacticIterate___________closed__16 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__16();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__16);
l_Lean_Parser_Tactic_tacticIterate___________closed__17 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__17();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__17);
l_Lean_Parser_Tactic_tacticIterate___________closed__18 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__18();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__18);
l_Lean_Parser_Tactic_tacticIterate___________closed__19 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__19();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__19);
l_Lean_Parser_Tactic_tacticIterate___________closed__20 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__20();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__20);
l_Lean_Parser_Tactic_tacticIterate___________closed__21 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__21();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__21);
l_Lean_Parser_Tactic_tacticIterate___________closed__22 = _init_l_Lean_Parser_Tactic_tacticIterate___________closed__22();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate___________closed__22);
l_Lean_Parser_Tactic_tacticIterate________ = _init_l_Lean_Parser_Tactic_tacticIterate________();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticIterate________);
l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__1 = _init_l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__1);
l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__2 = _init_l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__2);
l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__3 = _init_l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__3);
l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__4 = _init_l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__4();
lean_mark_persistent(l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__4);
l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__5 = _init_l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic___aux__Init__TacticsExtra______macroRules__Lean__Parser__Tactic__tacticIterate__________1___closed__5);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

4828
stage0/stdlib/Lean/Compiler/IR/EmitLLVM.c generated
View file

File diff suppressed because it is too large Load diff

99
stage0/stdlib/Lean/Compiler/IR/LLVMBindings.c generated
View file

@ -37,6 +37,7 @@ LEAN_EXPORT lean_object* l_LLVM_setDLLStorageClass___boxed(lean_object*, lean_ob
LEAN_EXPORT lean_object* l_LLVM_moduleToString___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint64_t l_LLVM_Linkage_weakAny;
LEAN_EXPORT lean_object* l_LLVM_constInt32___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_llvm_position_builder_before(size_t, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_getNextFunction___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_addGlobal___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_llvm_print_module_to_string(size_t, size_t, lean_object*);
@ -80,12 +81,14 @@ LEAN_EXPORT lean_object* l_LLVM_addAttributeAtIndex___boxed(lean_object*, lean_o
LEAN_EXPORT lean_object* l_LLVM_functionType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_PassManagerBuilder_setOptLevel___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_llvm_const_array(size_t, size_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_getEntryBasicBlock___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_llvm_get_named_global(size_t, size_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_countParams___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_setTailCall___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_constInt_x27(size_t, uint64_t, uint64_t, uint8_t, lean_object*);
lean_object* lean_llvm_build_mul(size_t, size_t, size_t, size_t, lean_object*, lean_object*);
lean_object* lean_llvm_build_unreachable(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_verifyModule___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_i16Type___boxed(lean_object*, lean_object*);
LEAN_EXPORT uint64_t l_LLVM_Linkage_common;
LEAN_EXPORT lean_object* l_LLVM_PassManagerBuilder_populateModulePassManager___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -111,6 +114,7 @@ lean_object* lean_llvm_create_pass_manager(size_t, lean_object*);
lean_object* lean_llvm_parse_bitcode(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_getFirstFunction___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_clearInsertionPosition___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_llvm_get_first_instruction(size_t, size_t, lean_object*);
lean_object* lean_llvm_create_builder_in_context(size_t, lean_object*);
lean_object* lean_llvm_build_cond_br(size_t, size_t, size_t, size_t, size_t, lean_object*);
lean_object* lean_llvm_set_linkage(size_t, size_t, uint64_t, lean_object*);
@ -125,6 +129,7 @@ LEAN_EXPORT lean_object* l_LLVM_Value_isNull(size_t);
LEAN_EXPORT lean_object* l_LLVM_buildGEP2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_i32Type___boxed(lean_object*, lean_object*);
lean_object* lean_llvm_add_global(size_t, size_t, lean_object*, size_t, lean_object*);
lean_object* lean_llvm_verify_module(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_isDeclaration___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_getNextGlobal___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_llvm_build_gep2(size_t, size_t, size_t, size_t, lean_object*, lean_object*, lean_object*);
@ -148,11 +153,14 @@ LEAN_EXPORT lean_object* l_LLVM_arrayType___boxed(lean_object*, lean_object*, le
LEAN_EXPORT lean_object* l_LLVM_buildZext___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_setVisibility___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_i8PtrType(size_t, lean_object*);
lean_object* lean_llvm_get_entry_basic_block(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_getUndef___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_disposePassManager___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_llvm_create_memory_buffer_with_contents_of_file(size_t, lean_object*, lean_object*);
lean_object* lean_llvm_run_pass_manager(size_t, size_t, size_t, lean_object*);
lean_object* lean_llvm_float_type_in_context(size_t, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_constIntSizeT(size_t, uint64_t, uint8_t, lean_object*);
lean_object* lean_llvm_count_basic_blocks(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_createMemoryBufferWithContentsOfFile___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_llvm_set_initializer(size_t, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_buildBr___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -173,6 +181,7 @@ lean_object* lean_llvm_build_sub(size_t, size_t, size_t, size_t, lean_object*, l
lean_object* lean_llvm_get_named_function(size_t, size_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_setInitializer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint64_t l_LLVM_Linkage_dllExport;
LEAN_EXPORT lean_object* l_LLVM_countBasicBlocks___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint64_t l_LLVM_Linkage_external;
LEAN_EXPORT lean_object* l_LLVM_i32Type(size_t, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_constIntUnsigned(size_t, uint64_t, uint8_t, lean_object*);
@ -189,6 +198,8 @@ LEAN_EXPORT lean_object* l_LLVM_disposePassManagerBuilder___boxed(lean_object*,
LEAN_EXPORT uint64_t l_LLVM_Linkage_linkerPrivate;
LEAN_EXPORT lean_object* l_LLVM_constPointerNull___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_llvm_dispose_module(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_constIntSizeT___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_positionBuilderBefore___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_buildSub___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_getTargetFromTriple___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_getNamedFunction___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -237,6 +248,7 @@ lean_object* lean_llvm_link_modules(size_t, size_t, size_t, lean_object*);
lean_object* lean_llvm_set_visibility(size_t, size_t, uint64_t, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_constArray___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_constTrue(size_t, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_getFirstInstruction___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_LLVM_buildRet___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint64_t l_LLVM_DLLStorageClass_import;
LEAN_EXPORT lean_object* l_LLVM_i64Type___boxed(lean_object*, lean_object*);
@ -733,6 +745,56 @@ lean_dec(x_3);
return x_7;
}
}
LEAN_EXPORT lean_object* l_LLVM_countBasicBlocks___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
size_t x_4; size_t x_5; lean_object* x_6;
x_4 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = lean_llvm_count_basic_blocks(x_4, x_5, x_3);
return x_6;
}
}
LEAN_EXPORT lean_object* l_LLVM_getEntryBasicBlock___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
size_t x_4; size_t x_5; lean_object* x_6;
x_4 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = lean_llvm_get_entry_basic_block(x_4, x_5, x_3);
return x_6;
}
}
LEAN_EXPORT lean_object* l_LLVM_getFirstInstruction___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
size_t x_4; size_t x_5; lean_object* x_6;
x_4 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = lean_llvm_get_first_instruction(x_4, x_5, x_3);
return x_6;
}
}
LEAN_EXPORT lean_object* l_LLVM_positionBuilderBefore___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; size_t x_7; lean_object* x_8;
x_5 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_6 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_7 = lean_unbox_usize(x_3);
lean_dec(x_3);
x_8 = lean_llvm_position_builder_before(x_5, x_6, x_7, x_4);
return x_8;
}
}
LEAN_EXPORT lean_object* l_LLVM_positionBuilderAtEnd___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
@ -1399,6 +1461,18 @@ x_6 = lean_llvm_dispose_module(x_4, x_5, x_3);
return x_6;
}
}
LEAN_EXPORT lean_object* l_LLVM_verifyModule___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
size_t x_4; size_t x_5; lean_object* x_6;
x_4 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = lean_llvm_verify_module(x_4, x_5, x_3);
return x_6;
}
}
LEAN_EXPORT lean_object* l_LLVM_createStringAttribute___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -2075,7 +2149,7 @@ x_8 = l_LLVM_constInt64(x_5, x_6, x_7, x_4);
return x_8;
}
}
LEAN_EXPORT lean_object* l_LLVM_constIntUnsigned(size_t x_1, uint64_t x_2, uint8_t x_3, lean_object* x_4) {
LEAN_EXPORT lean_object* l_LLVM_constIntSizeT(size_t x_1, uint64_t x_2, uint8_t x_3, lean_object* x_4) {
_start:
{
uint64_t x_5; lean_object* x_6;
@ -2084,6 +2158,29 @@ x_6 = l_LLVM_constInt_x27(x_1, x_5, x_2, x_3, x_4);
return x_6;
}
}
LEAN_EXPORT lean_object* l_LLVM_constIntSizeT___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; uint64_t x_6; uint8_t x_7; lean_object* x_8;
x_5 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_6 = lean_unbox_uint64(x_2);
lean_dec(x_2);
x_7 = lean_unbox(x_3);
lean_dec(x_3);
x_8 = l_LLVM_constIntSizeT(x_5, x_6, x_7, x_4);
return x_8;
}
}
LEAN_EXPORT lean_object* l_LLVM_constIntUnsigned(size_t x_1, uint64_t x_2, uint8_t x_3, lean_object* x_4) {
_start:
{
uint64_t x_5; lean_object* x_6;
x_5 = 32;
x_6 = l_LLVM_constInt_x27(x_1, x_5, x_2, x_3, x_4);
return x_6;
}
}
LEAN_EXPORT lean_object* l_LLVM_constIntUnsigned___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{

6014
stage0/stdlib/Lean/Elab/BuiltinCommand.c generated
View file

File diff suppressed because it is too large Load diff

1960
stage0/stdlib/Lean/Elab/BuiltinNotation.c generated
View file

File diff suppressed because it is too large Load diff

851
stage0/stdlib/Lean/Elab/Eval.c generated
View file

@ -13,18 +13,446 @@
#ifdef __cplusplus
extern "C" {
#endif
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__2;
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__16;
lean_object* l_Lean_Elab_Term_logUnassignedUsingErrorInfos(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__5;
lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTermEnsuringType(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instBEqLocalInstance___boxed(lean_object*, lean_object*);
lean_object* l_Lean_instantiateMVars___at_Lean_Elab_Term_MVarErrorInfo_logError___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__12;
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__13;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_evalTerm___rarg___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_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__8;
extern lean_object* l_Lean_Expr_instBEqExpr;
lean_object* l_instBEqProd___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_instHashableArray___rarg___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__7;
lean_object* lean_st_ref_take(lean_object*, lean_object*);
lean_object* l_Lean_Meta_evalExpr___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__4;
LEAN_EXPORT lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_instHashableExpr;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_evalTerm___rarg___lambda__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instHashableLocalInstance___boxed(lean_object*);
lean_object* l_instHashableProd___rarg___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__3;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_evalTerm___rarg___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*);
lean_object* l_Lean_Elab_throwAbortTerm___at_Lean_Elab_Term_ensureType___spec__1___rarg(lean_object*);
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__18;
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__1;
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__15;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_evalTerm(lean_object*);
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__19;
lean_object* l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey___boxed(lean_object*);
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__14;
lean_object* l_Lean_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*);
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__11;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_evalTerm___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__9;
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__10;
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__6;
lean_object* l_Array_instBEqArray___rarg___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__17;
static lean_object* _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_PersistentHashMap_mkEmptyEntriesArray(lean_box(0), lean_box(0));
return x_1;
}
}
static lean_object* _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__1;
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_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__2;
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_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__3;
x_2 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_2, 0, x_1);
lean_ctor_set(x_2, 1, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__2;
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_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__6() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey___boxed), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__2;
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_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__8() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_instBEqLocalInstance___boxed), 2, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__8;
x_2 = lean_alloc_closure((void*)(l_Array_instBEqArray___rarg___boxed), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__9;
x_2 = l_Lean_Expr_instBEqExpr;
x_3 = lean_alloc_closure((void*)(l_instBEqProd___rarg), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__11() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_instHashableLocalInstance___boxed), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__11;
x_2 = lean_alloc_closure((void*)(l_instHashableArray___rarg___boxed), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__13() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__12;
x_2 = l_Lean_Expr_instHashableExpr;
x_3 = lean_alloc_closure((void*)(l_instHashableProd___rarg___boxed), 3, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__2;
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_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__15() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Expr_instBEqExpr;
x_2 = lean_alloc_closure((void*)(l_instBEqProd___rarg), 4, 2);
lean_closure_set(x_2, 0, x_1);
lean_closure_set(x_2, 1, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Expr_instHashableExpr;
x_2 = lean_alloc_closure((void*)(l_instHashableProd___rarg___boxed), 3, 2);
lean_closure_set(x_2, 0, x_1);
lean_closure_set(x_2, 1, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__17() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__2;
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_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__17;
x_2 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_2, 0, x_1);
lean_ctor_set(x_2, 1, x_1);
lean_ctor_set(x_2, 2, x_1);
lean_ctor_set(x_2, 3, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__19() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__5;
x_2 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__7;
x_3 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__14;
x_4 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__18;
x_5 = lean_alloc_ctor(0, 7, 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_1);
lean_ctor_set(x_5, 4, x_1);
lean_ctor_set(x_5, 5, x_4);
lean_ctor_set(x_5, 6, x_4);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1(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) {
_start:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12;
x_9 = lean_st_ref_take(x_7, x_8);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = !lean_is_exclusive(x_10);
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21;
x_13 = lean_ctor_get(x_10, 4);
lean_dec(x_13);
x_14 = lean_ctor_get(x_10, 0);
lean_dec(x_14);
x_15 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__4;
lean_ctor_set(x_10, 4, x_15);
lean_ctor_set(x_10, 0, x_1);
x_16 = lean_st_ref_set(x_7, x_10, x_11);
x_17 = lean_ctor_get(x_16, 1);
lean_inc(x_17);
lean_dec(x_16);
x_18 = lean_st_ref_take(x_5, x_17);
x_19 = lean_ctor_get(x_18, 0);
lean_inc(x_19);
x_20 = lean_ctor_get(x_18, 1);
lean_inc(x_20);
lean_dec(x_18);
x_21 = !lean_is_exclusive(x_19);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25;
x_22 = lean_ctor_get(x_19, 1);
lean_dec(x_22);
x_23 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__19;
lean_ctor_set(x_19, 1, x_23);
x_24 = lean_st_ref_set(x_5, x_19, x_20);
x_25 = !lean_is_exclusive(x_24);
if (x_25 == 0)
{
lean_object* x_26; lean_object* x_27;
x_26 = lean_ctor_get(x_24, 0);
lean_dec(x_26);
x_27 = lean_box(0);
lean_ctor_set(x_24, 0, x_27);
return x_24;
}
else
{
lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_28 = lean_ctor_get(x_24, 1);
lean_inc(x_28);
lean_dec(x_24);
x_29 = lean_box(0);
x_30 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_30, 0, x_29);
lean_ctor_set(x_30, 1, x_28);
return x_30;
}
}
else
{
lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40;
x_31 = lean_ctor_get(x_19, 0);
x_32 = lean_ctor_get(x_19, 2);
x_33 = lean_ctor_get(x_19, 3);
lean_inc(x_33);
lean_inc(x_32);
lean_inc(x_31);
lean_dec(x_19);
x_34 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__19;
x_35 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_35, 0, x_31);
lean_ctor_set(x_35, 1, x_34);
lean_ctor_set(x_35, 2, x_32);
lean_ctor_set(x_35, 3, x_33);
x_36 = lean_st_ref_set(x_5, x_35, x_20);
x_37 = lean_ctor_get(x_36, 1);
lean_inc(x_37);
if (lean_is_exclusive(x_36)) {
lean_ctor_release(x_36, 0);
lean_ctor_release(x_36, 1);
x_38 = x_36;
} else {
lean_dec_ref(x_36);
x_38 = lean_box(0);
}
x_39 = lean_box(0);
if (lean_is_scalar(x_38)) {
x_40 = lean_alloc_ctor(0, 2, 0);
} else {
x_40 = x_38;
}
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_37);
return x_40;
}
}
else
{
lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63;
x_41 = lean_ctor_get(x_10, 1);
x_42 = lean_ctor_get(x_10, 2);
x_43 = lean_ctor_get(x_10, 3);
x_44 = lean_ctor_get(x_10, 5);
x_45 = lean_ctor_get(x_10, 6);
lean_inc(x_45);
lean_inc(x_44);
lean_inc(x_43);
lean_inc(x_42);
lean_inc(x_41);
lean_dec(x_10);
x_46 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__4;
x_47 = lean_alloc_ctor(0, 7, 0);
lean_ctor_set(x_47, 0, x_1);
lean_ctor_set(x_47, 1, x_41);
lean_ctor_set(x_47, 2, x_42);
lean_ctor_set(x_47, 3, x_43);
lean_ctor_set(x_47, 4, x_46);
lean_ctor_set(x_47, 5, x_44);
lean_ctor_set(x_47, 6, x_45);
x_48 = lean_st_ref_set(x_7, x_47, x_11);
x_49 = lean_ctor_get(x_48, 1);
lean_inc(x_49);
lean_dec(x_48);
x_50 = lean_st_ref_take(x_5, x_49);
x_51 = lean_ctor_get(x_50, 0);
lean_inc(x_51);
x_52 = lean_ctor_get(x_50, 1);
lean_inc(x_52);
lean_dec(x_50);
x_53 = lean_ctor_get(x_51, 0);
lean_inc(x_53);
x_54 = lean_ctor_get(x_51, 2);
lean_inc(x_54);
x_55 = lean_ctor_get(x_51, 3);
lean_inc(x_55);
if (lean_is_exclusive(x_51)) {
lean_ctor_release(x_51, 0);
lean_ctor_release(x_51, 1);
lean_ctor_release(x_51, 2);
lean_ctor_release(x_51, 3);
x_56 = x_51;
} else {
lean_dec_ref(x_51);
x_56 = lean_box(0);
}
x_57 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__19;
if (lean_is_scalar(x_56)) {
x_58 = lean_alloc_ctor(0, 4, 0);
} else {
x_58 = x_56;
}
lean_ctor_set(x_58, 0, x_53);
lean_ctor_set(x_58, 1, x_57);
lean_ctor_set(x_58, 2, x_54);
lean_ctor_set(x_58, 3, x_55);
x_59 = lean_st_ref_set(x_5, x_58, x_52);
x_60 = lean_ctor_get(x_59, 1);
lean_inc(x_60);
if (lean_is_exclusive(x_59)) {
lean_ctor_release(x_59, 0);
lean_ctor_release(x_59, 1);
x_61 = x_59;
} else {
lean_dec_ref(x_59);
x_61 = lean_box(0);
}
x_62 = lean_box(0);
if (lean_is_scalar(x_61)) {
x_63 = lean_alloc_ctor(0, 2, 0);
} else {
x_63 = x_61;
}
lean_ctor_set(x_63, 0, x_62);
lean_ctor_set(x_63, 1, x_60);
return x_63;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_evalTerm___rarg___lambda__1(lean_object* x_1, lean_object* x_2, uint8_t 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, lean_object* x_11) {
_start:
{
@ -36,196 +464,237 @@ return x_12;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_evalTerm___rarg(lean_object* x_1, lean_object* x_2, uint8_t 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; lean_object* x_12; uint8_t x_13; lean_object* x_14;
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_25; lean_object* x_26; uint8_t x_33; lean_object* x_34;
lean_inc(x_1);
x_11 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_11, 0, x_1);
x_12 = lean_box(0);
x_13 = 1;
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
x_14 = l_Lean_Elab_Term_elabTermEnsuringType(x_2, x_11, x_13, x_13, x_12, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_15; lean_object* x_16; uint8_t x_17; lean_object* x_18;
x_15 = lean_ctor_get(x_14, 0);
x_13 = lean_st_ref_get(x_9, x_10);
x_14 = lean_ctor_get(x_13, 0);
lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 1);
lean_inc(x_15);
x_16 = lean_ctor_get(x_14, 1);
lean_dec(x_13);
x_16 = lean_ctor_get(x_14, 0);
lean_inc(x_16);
lean_dec(x_14);
x_17 = 0;
x_33 = 1;
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
x_18 = l_Lean_Elab_Term_synthesizeSyntheticMVars(x_17, x_17, x_4, x_5, x_6, x_7, x_8, x_9, x_16);
if (lean_obj_tag(x_18) == 0)
x_34 = l_Lean_Elab_Term_elabTermEnsuringType(x_2, x_11, x_33, x_33, x_12, x_4, x_5, x_6, x_7, x_8, x_9, x_15);
if (lean_obj_tag(x_34) == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_19 = lean_ctor_get(x_18, 1);
lean_inc(x_19);
lean_dec(x_18);
x_20 = l_Lean_instantiateMVars___at_Lean_Elab_Term_MVarErrorInfo_logError___spec__1(x_15, x_4, x_5, x_6, x_7, x_8, x_9, x_19);
x_21 = lean_ctor_get(x_20, 0);
lean_inc(x_21);
x_22 = lean_ctor_get(x_20, 1);
lean_inc(x_22);
lean_dec(x_20);
lean_inc(x_21);
x_23 = l_Lean_Meta_getMVars(x_21, x_6, x_7, x_8, x_9, x_22);
x_24 = lean_ctor_get(x_23, 0);
lean_inc(x_24);
x_25 = lean_ctor_get(x_23, 1);
lean_inc(x_25);
lean_dec(x_23);
lean_object* x_35; lean_object* x_36; uint8_t x_37; lean_object* x_38;
x_35 = lean_ctor_get(x_34, 0);
lean_inc(x_35);
x_36 = lean_ctor_get(x_34, 1);
lean_inc(x_36);
lean_dec(x_34);
x_37 = 0;
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
x_26 = l_Lean_Elab_Term_logUnassignedUsingErrorInfos(x_24, x_12, x_4, x_5, x_6, x_7, x_8, x_9, x_25);
lean_dec(x_24);
if (lean_obj_tag(x_26) == 0)
lean_inc(x_5);
lean_inc(x_4);
x_38 = l_Lean_Elab_Term_synthesizeSyntheticMVars(x_37, x_37, x_4, x_5, x_6, x_7, x_8, x_9, x_36);
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; lean_object* x_46;
x_39 = lean_ctor_get(x_38, 1);
lean_inc(x_39);
lean_dec(x_38);
x_40 = l_Lean_instantiateMVars___at_Lean_Elab_Term_MVarErrorInfo_logError___spec__1(x_35, x_4, x_5, x_6, x_7, x_8, x_9, x_39);
x_41 = lean_ctor_get(x_40, 0);
lean_inc(x_41);
x_42 = lean_ctor_get(x_40, 1);
lean_inc(x_42);
lean_dec(x_40);
lean_inc(x_41);
x_43 = l_Lean_Meta_getMVars(x_41, x_6, x_7, x_8, x_9, x_42);
x_44 = lean_ctor_get(x_43, 0);
lean_inc(x_44);
x_45 = lean_ctor_get(x_43, 1);
lean_inc(x_45);
lean_dec(x_43);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
x_46 = l_Lean_Elab_Term_logUnassignedUsingErrorInfos(x_44, x_12, x_4, x_5, x_6, x_7, x_8, x_9, x_45);
lean_dec(x_44);
if (lean_obj_tag(x_46) == 0)
{
lean_object* x_47; uint8_t x_48;
x_47 = lean_ctor_get(x_46, 0);
lean_inc(x_47);
x_48 = lean_unbox(x_47);
lean_dec(x_47);
if (x_48 == 0)
{
lean_object* x_49; lean_object* x_50;
x_49 = lean_ctor_get(x_46, 1);
lean_inc(x_49);
lean_dec(x_46);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
x_50 = l_Lean_Meta_evalExpr___rarg(x_1, x_41, x_3, x_6, x_7, x_8, x_9, x_49);
if (lean_obj_tag(x_50) == 0)
{
lean_object* x_51; lean_object* x_52;
x_51 = lean_ctor_get(x_50, 0);
lean_inc(x_51);
x_52 = lean_ctor_get(x_50, 1);
lean_inc(x_52);
lean_dec(x_50);
x_17 = x_51;
x_18 = x_52;
goto block_24;
}
else
{
lean_object* x_53; lean_object* x_54;
x_53 = lean_ctor_get(x_50, 0);
lean_inc(x_53);
x_54 = lean_ctor_get(x_50, 1);
lean_inc(x_54);
lean_dec(x_50);
x_25 = x_53;
x_26 = x_54;
goto block_32;
}
}
else
{
lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58;
lean_dec(x_41);
lean_dec(x_1);
x_55 = lean_ctor_get(x_46, 1);
lean_inc(x_55);
lean_dec(x_46);
x_56 = l_Lean_Elab_throwAbortTerm___at_Lean_Elab_Term_ensureType___spec__1___rarg(x_55);
x_57 = lean_ctor_get(x_56, 0);
lean_inc(x_57);
x_58 = lean_ctor_get(x_56, 1);
lean_inc(x_58);
lean_dec(x_56);
x_25 = x_57;
x_26 = x_58;
goto block_32;
}
}
else
{
lean_object* x_59; lean_object* x_60;
lean_dec(x_41);
lean_dec(x_1);
x_59 = lean_ctor_get(x_46, 0);
lean_inc(x_59);
x_60 = lean_ctor_get(x_46, 1);
lean_inc(x_60);
lean_dec(x_46);
x_25 = x_59;
x_26 = x_60;
goto block_32;
}
}
else
{
lean_object* x_61; lean_object* x_62;
lean_dec(x_35);
lean_dec(x_1);
x_61 = lean_ctor_get(x_38, 0);
lean_inc(x_61);
x_62 = lean_ctor_get(x_38, 1);
lean_inc(x_62);
lean_dec(x_38);
x_25 = x_61;
x_26 = x_62;
goto block_32;
}
}
else
{
lean_object* x_63; lean_object* x_64;
lean_dec(x_1);
x_63 = lean_ctor_get(x_34, 0);
lean_inc(x_63);
x_64 = lean_ctor_get(x_34, 1);
lean_inc(x_64);
lean_dec(x_34);
x_25 = x_63;
x_26 = x_64;
goto block_32;
}
block_24:
{
lean_object* x_19; uint8_t x_20;
x_19 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1(x_16, x_4, x_5, x_6, x_7, x_8, x_9, x_18);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
x_20 = !lean_is_exclusive(x_19);
if (x_20 == 0)
{
lean_object* x_21;
x_21 = lean_ctor_get(x_19, 0);
lean_dec(x_21);
lean_ctor_set(x_19, 0, x_17);
return x_19;
}
else
{
lean_object* x_22; lean_object* x_23;
x_22 = lean_ctor_get(x_19, 1);
lean_inc(x_22);
lean_dec(x_19);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_17);
lean_ctor_set(x_23, 1, x_22);
return x_23;
}
}
block_32:
{
lean_object* x_27; uint8_t x_28;
x_27 = lean_ctor_get(x_26, 0);
lean_inc(x_27);
x_28 = lean_unbox(x_27);
lean_dec(x_27);
x_27 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1(x_16, x_4, x_5, x_6, x_7, x_8, x_9, x_26);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
x_28 = !lean_is_exclusive(x_27);
if (x_28 == 0)
{
lean_object* x_29; lean_object* x_30;
x_29 = lean_ctor_get(x_26, 1);
lean_inc(x_29);
lean_dec(x_26);
x_30 = l_Lean_Meta_evalExpr___rarg(x_1, x_21, x_3, x_6, x_7, x_8, x_9, x_29);
return x_30;
lean_object* x_29;
x_29 = lean_ctor_get(x_27, 0);
lean_dec(x_29);
lean_ctor_set_tag(x_27, 1);
lean_ctor_set(x_27, 0, x_25);
return x_27;
}
else
{
lean_object* x_31; lean_object* x_32; uint8_t x_33;
lean_dec(x_21);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_1);
x_31 = lean_ctor_get(x_26, 1);
lean_inc(x_31);
lean_dec(x_26);
x_32 = l_Lean_Elab_throwAbortTerm___at_Lean_Elab_Term_ensureType___spec__1___rarg(x_31);
x_33 = !lean_is_exclusive(x_32);
if (x_33 == 0)
{
return x_32;
}
else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36;
x_34 = lean_ctor_get(x_32, 0);
x_35 = lean_ctor_get(x_32, 1);
lean_inc(x_35);
lean_inc(x_34);
lean_dec(x_32);
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
{
uint8_t x_37;
lean_dec(x_21);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_1);
x_37 = !lean_is_exclusive(x_26);
if (x_37 == 0)
{
return x_26;
}
else
{
lean_object* x_38; lean_object* x_39; lean_object* x_40;
x_38 = lean_ctor_get(x_26, 0);
x_39 = lean_ctor_get(x_26, 1);
lean_inc(x_39);
lean_inc(x_38);
lean_dec(x_26);
x_40 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_40, 0, x_38);
lean_ctor_set(x_40, 1, x_39);
return x_40;
}
}
}
else
{
uint8_t x_41;
lean_dec(x_15);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_1);
x_41 = !lean_is_exclusive(x_18);
if (x_41 == 0)
{
return x_18;
}
else
{
lean_object* x_42; lean_object* x_43; lean_object* x_44;
x_42 = lean_ctor_get(x_18, 0);
x_43 = lean_ctor_get(x_18, 1);
lean_inc(x_43);
lean_inc(x_42);
lean_dec(x_18);
x_44 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_44, 0, x_42);
lean_ctor_set(x_44, 1, x_43);
return x_44;
}
}
}
else
{
uint8_t x_45;
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_1);
x_45 = !lean_is_exclusive(x_14);
if (x_45 == 0)
{
return x_14;
}
else
{
lean_object* x_46; lean_object* x_47; lean_object* x_48;
x_46 = lean_ctor_get(x_14, 0);
x_47 = lean_ctor_get(x_14, 1);
lean_inc(x_47);
lean_inc(x_46);
lean_dec(x_14);
x_48 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_48, 0, x_46);
lean_ctor_set(x_48, 1, x_47);
return x_48;
lean_object* x_30; lean_object* x_31;
x_30 = lean_ctor_get(x_27, 1);
lean_inc(x_30);
lean_dec(x_27);
x_31 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_31, 0, x_25);
lean_ctor_set(x_31, 1, x_30);
return x_31;
}
}
}
@ -238,6 +707,20 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_evalTerm___rarg___boxed), 10,
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___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) {
_start:
{
lean_object* x_9;
x_9 = l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_evalTerm___rarg___lambda__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, lean_object* x_10, lean_object* x_11) {
_start:
{
@ -278,6 +761,44 @@ lean_dec_ref(res);
res = initialize_Lean_Elab_SyntheticMVars(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__1 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__1();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__1);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__2 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__2();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__2);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__3 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__3();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__3);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__4 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__4();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__4);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__5 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__5();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__5);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__6 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__6();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__6);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__7 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__7();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__7);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__8 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__8();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__8);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__9 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__9();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__9);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__10 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__10();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__10);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__11 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__11();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__11);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__12 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__12();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__12);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__13 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__13();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__13);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__14 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__14();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__14);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__15 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__15();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__15);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__16 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__16();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__16);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__17 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__17();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__17);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__18 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__18();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__18);
l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__19 = _init_l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__19();
lean_mark_persistent(l_Lean_setEnv___at_Lean_Elab_Term_evalTerm___spec__1___closed__19);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

10
stage0/stdlib/Lean/Elab/Tactic.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Elab.Tactic
// Imports: Init Lean.Elab.Term Lean.Elab.Tactic.Basic Lean.Elab.Tactic.ElabTerm Lean.Elab.Tactic.Induction Lean.Elab.Tactic.Generalize Lean.Elab.Tactic.Injection Lean.Elab.Tactic.Match Lean.Elab.Tactic.Rewrite Lean.Elab.Tactic.Location Lean.Elab.Tactic.Simp Lean.Elab.Tactic.Simproc Lean.Elab.Tactic.BuiltinTactic Lean.Elab.Tactic.Split Lean.Elab.Tactic.Conv Lean.Elab.Tactic.Delta Lean.Elab.Tactic.Meta Lean.Elab.Tactic.Unfold Lean.Elab.Tactic.Cache Lean.Elab.Tactic.Calc Lean.Elab.Tactic.Congr Lean.Elab.Tactic.Guard Lean.Elab.Tactic.RCases Lean.Elab.Tactic.Change
// Imports: Init Lean.Elab.Term Lean.Elab.Tactic.Basic Lean.Elab.Tactic.ElabTerm Lean.Elab.Tactic.Induction Lean.Elab.Tactic.Generalize Lean.Elab.Tactic.Injection Lean.Elab.Tactic.Match Lean.Elab.Tactic.Rewrite Lean.Elab.Tactic.Location Lean.Elab.Tactic.Simp Lean.Elab.Tactic.Simproc Lean.Elab.Tactic.BuiltinTactic Lean.Elab.Tactic.Split Lean.Elab.Tactic.Conv Lean.Elab.Tactic.Delta Lean.Elab.Tactic.Meta Lean.Elab.Tactic.Unfold Lean.Elab.Tactic.Cache Lean.Elab.Tactic.Calc Lean.Elab.Tactic.Congr Lean.Elab.Tactic.Guard Lean.Elab.Tactic.RCases Lean.Elab.Tactic.Repeat Lean.Elab.Tactic.Change Lean.Elab.Tactic.HaveI
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -36,7 +36,9 @@ lean_object* initialize_Lean_Elab_Tactic_Calc(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Elab_Tactic_Congr(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Elab_Tactic_Guard(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Elab_Tactic_RCases(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Elab_Tactic_Repeat(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Elab_Tactic_Change(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Elab_Tactic_HaveI(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Elab_Tactic(uint8_t builtin, lean_object* w) {
lean_object * res;
@ -111,9 +113,15 @@ lean_dec_ref(res);
res = initialize_Lean_Elab_Tactic_RCases(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_Tactic_Repeat(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_Tactic_Change(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_Tactic_HaveI(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

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

File diff suppressed because it is too large Load diff

33
stage0/stdlib/Lean/Elab/Tactic/HaveI.c generated Normal file
View file

@ -0,0 +1,33 @@
// Lean compiler output
// Module: Lean.Elab.Tactic.HaveI
// Imports: Init Lean.Elab.ElabRules
#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(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Elab_ElabRules(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Elab_Tactic_HaveI(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(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_ElabRules(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

2447
stage0/stdlib/Lean/Elab/Tactic/Repeat.c generated Normal file
View file

File diff suppressed because it is too large Load diff

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

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Meta.Tactic
// Imports: Init Lean.Meta.Tactic.Intro Lean.Meta.Tactic.Assumption Lean.Meta.Tactic.Contradiction Lean.Meta.Tactic.Apply Lean.Meta.Tactic.Revert Lean.Meta.Tactic.Clear Lean.Meta.Tactic.Assert Lean.Meta.Tactic.Rewrite Lean.Meta.Tactic.Generalize Lean.Meta.Tactic.Replace Lean.Meta.Tactic.Induction Lean.Meta.Tactic.Cases Lean.Meta.Tactic.ElimInfo Lean.Meta.Tactic.Delta Lean.Meta.Tactic.Constructor Lean.Meta.Tactic.Simp Lean.Meta.Tactic.AuxLemma Lean.Meta.Tactic.SplitIf Lean.Meta.Tactic.Split Lean.Meta.Tactic.Cleanup Lean.Meta.Tactic.Unfold Lean.Meta.Tactic.Rename Lean.Meta.Tactic.LinearArith Lean.Meta.Tactic.AC Lean.Meta.Tactic.Refl Lean.Meta.Tactic.Congr
// Imports: Init Lean.Meta.Tactic.Intro Lean.Meta.Tactic.Assumption Lean.Meta.Tactic.Contradiction Lean.Meta.Tactic.Apply Lean.Meta.Tactic.Revert Lean.Meta.Tactic.Clear Lean.Meta.Tactic.Assert Lean.Meta.Tactic.Rewrite Lean.Meta.Tactic.Generalize Lean.Meta.Tactic.Replace Lean.Meta.Tactic.Induction Lean.Meta.Tactic.Cases Lean.Meta.Tactic.ElimInfo Lean.Meta.Tactic.Delta Lean.Meta.Tactic.Constructor Lean.Meta.Tactic.Simp Lean.Meta.Tactic.AuxLemma Lean.Meta.Tactic.SplitIf Lean.Meta.Tactic.Split Lean.Meta.Tactic.TryThis Lean.Meta.Tactic.Cleanup Lean.Meta.Tactic.Unfold Lean.Meta.Tactic.Rename Lean.Meta.Tactic.LinearArith Lean.Meta.Tactic.AC Lean.Meta.Tactic.Refl Lean.Meta.Tactic.Congr Lean.Meta.Tactic.Repeat
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -33,6 +33,7 @@ lean_object* initialize_Lean_Meta_Tactic_Simp(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_AuxLemma(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_SplitIf(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Split(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_TryThis(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Cleanup(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Unfold(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Rename(uint8_t builtin, lean_object*);
@ -40,6 +41,7 @@ lean_object* initialize_Lean_Meta_Tactic_LinearArith(uint8_t builtin, lean_objec
lean_object* initialize_Lean_Meta_Tactic_AC(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Refl(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Congr(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Repeat(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Meta_Tactic(uint8_t builtin, lean_object* w) {
lean_object * res;
@ -105,6 +107,9 @@ lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_Split(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_TryThis(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_Cleanup(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
@ -126,6 +131,9 @@ lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_Congr(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_Repeat(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

751
stage0/stdlib/Lean/Meta/Tactic/Repeat.c generated Normal file
View file

@ -0,0 +1,751 @@
// Lean compiler output
// Module: Lean.Meta.Tactic.Repeat
// Imports: Init Lean.Meta.Basic
#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
static lean_object* l_Lean_Meta_repeat1_x27___rarg___lambda__1___closed__2;
LEAN_EXPORT lean_object* l_Lean_Meta_repeat1_x27___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
LEAN_EXPORT lean_object* l_Functor_mapRev___at_Lean_Meta_repeat_x27___spec__1(lean_object*);
lean_object* l_not___boxed(lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
uint8_t lean_usize_dec_eq(size_t, size_t);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core_go(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core_go___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, uint8_t);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core_go___rarg___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*, lean_object*);
lean_object* l_Lean_observing_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1(lean_object*);
lean_object* l_Lean_stringToMessageData(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core_go___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_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat1_x27___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27___rarg___lambda__1(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27(lean_object*, lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core_go___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_repeat1_x27___rarg___lambda__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core___rarg___lambda__1(lean_object*, uint8_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat1_x27(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Functor_mapRev___at_Lean_Meta_repeat_x27___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_foldl___at_Lean_Meta_repeat_x27Core_go___spec__1(lean_object*, lean_object*);
lean_object* lean_array_to_list(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___lambda__2(size_t, lean_object*, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27___rarg___lambda__1___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core_go___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_repeat_x27___rarg___closed__1;
lean_object* l_Lean_throwError___rarg(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_List_foldl___at_Array_appendList___spec__1___rarg(lean_object*, lean_object*);
size_t lean_usize_add(size_t, size_t);
lean_object* lean_array_uget(lean_object*, size_t);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core_go___rarg___lambda__2___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* l_Lean_MVarId_isAssigned___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_repeat_x27Core___rarg___closed__1;
LEAN_EXPORT lean_object* l_List_foldl___at_Lean_Meta_repeat_x27Core_go___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
return x_1;
}
else
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_2);
x_5 = l_List_foldl___at_Array_appendList___spec__1___rarg(x_1, x_3);
x_1 = x_5;
x_2 = x_4;
goto _start;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core_go___rarg___lambda__1(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, uint8_t x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) {
_start:
{
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14;
x_13 = lean_array_push(x_1, x_2);
x_14 = l_Lean_Meta_repeat_x27Core_go___rarg(x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_13);
return x_14;
}
else
{
lean_object* x_15; lean_object* x_16; uint8_t x_17; lean_object* x_18;
lean_dec(x_2);
x_15 = lean_ctor_get(x_12, 0);
lean_inc(x_15);
lean_dec(x_12);
x_16 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_16, 0, x_10);
lean_ctor_set(x_16, 1, x_11);
x_17 = 1;
x_18 = l_Lean_Meta_repeat_x27Core_go___rarg(x_3, x_4, x_5, x_6, x_7, x_8, x_17, x_15, x_16, x_1);
return x_18;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core_go___rarg___lambda__2(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, uint8_t x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, uint8_t x_13) {
_start:
{
if (x_13 == 0)
{
lean_object* x_14; uint8_t x_15;
x_14 = lean_unsigned_to_nat(0u);
x_15 = lean_nat_dec_eq(x_1, x_14);
if (x_15 == 0)
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_16 = lean_unsigned_to_nat(1u);
x_17 = lean_nat_sub(x_1, x_16);
lean_dec(x_1);
lean_inc(x_2);
lean_inc(x_3);
x_18 = lean_apply_1(x_2, x_3);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
x_19 = l_Lean_observing_x3f___rarg(x_4, x_5, x_6, x_18);
x_20 = lean_box(x_9);
x_21 = lean_alloc_closure((void*)(l_Lean_Meta_repeat_x27Core_go___rarg___lambda__1___boxed), 12, 11);
lean_closure_set(x_21, 0, x_7);
lean_closure_set(x_21, 1, x_3);
lean_closure_set(x_21, 2, x_4);
lean_closure_set(x_21, 3, x_6);
lean_closure_set(x_21, 4, x_5);
lean_closure_set(x_21, 5, x_8);
lean_closure_set(x_21, 6, x_2);
lean_closure_set(x_21, 7, x_17);
lean_closure_set(x_21, 8, x_20);
lean_closure_set(x_21, 9, x_10);
lean_closure_set(x_21, 10, x_11);
x_22 = lean_apply_4(x_12, lean_box(0), lean_box(0), x_19, x_21);
return x_22;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
lean_dec(x_12);
lean_dec(x_8);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_23 = lean_ctor_get(x_4, 0);
lean_inc(x_23);
lean_dec(x_4);
x_24 = lean_ctor_get(x_23, 1);
lean_inc(x_24);
lean_dec(x_23);
x_25 = lean_array_push(x_7, x_3);
x_26 = l_List_foldl___at_Array_appendList___spec__1___rarg(x_25, x_10);
x_27 = l_List_foldl___at_Lean_Meta_repeat_x27Core_go___spec__1(x_26, x_11);
x_28 = lean_box(x_9);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_27);
x_30 = lean_apply_2(x_24, lean_box(0), x_29);
return x_30;
}
}
else
{
lean_object* x_31;
lean_dec(x_12);
lean_dec(x_3);
x_31 = l_Lean_Meta_repeat_x27Core_go___rarg(x_4, x_6, x_5, x_8, x_2, x_1, x_9, x_10, x_11, x_7);
return x_31;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core_go___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, uint8_t x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
if (lean_obj_tag(x_8) == 0)
{
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_11 = lean_ctor_get(x_1, 0);
lean_inc(x_11);
lean_dec(x_1);
x_12 = lean_ctor_get(x_11, 1);
lean_inc(x_12);
lean_dec(x_11);
x_13 = lean_box(x_7);
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_10);
x_15 = lean_apply_2(x_12, lean_box(0), x_14);
return x_15;
}
else
{
lean_object* x_16; lean_object* x_17;
x_16 = lean_ctor_get(x_9, 0);
lean_inc(x_16);
x_17 = lean_ctor_get(x_9, 1);
lean_inc(x_17);
lean_dec(x_9);
x_8 = x_16;
x_9 = x_17;
goto _start;
}
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_19 = lean_ctor_get(x_8, 0);
lean_inc(x_19);
x_20 = lean_ctor_get(x_8, 1);
lean_inc(x_20);
lean_dec(x_8);
x_21 = lean_ctor_get(x_1, 1);
lean_inc(x_21);
lean_inc(x_19);
lean_inc(x_4);
lean_inc(x_1);
x_22 = l_Lean_MVarId_isAssigned___rarg(x_1, x_4, x_19);
x_23 = lean_box(x_7);
lean_inc(x_21);
x_24 = lean_alloc_closure((void*)(l_Lean_Meta_repeat_x27Core_go___rarg___lambda__2___boxed), 13, 12);
lean_closure_set(x_24, 0, x_6);
lean_closure_set(x_24, 1, x_5);
lean_closure_set(x_24, 2, x_19);
lean_closure_set(x_24, 3, x_1);
lean_closure_set(x_24, 4, x_3);
lean_closure_set(x_24, 5, x_2);
lean_closure_set(x_24, 6, x_10);
lean_closure_set(x_24, 7, x_4);
lean_closure_set(x_24, 8, x_23);
lean_closure_set(x_24, 9, x_20);
lean_closure_set(x_24, 10, x_9);
lean_closure_set(x_24, 11, x_21);
x_25 = lean_apply_4(x_21, lean_box(0), lean_box(0), x_22, x_24);
return x_25;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core_go(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Lean_Meta_repeat_x27Core_go___rarg___boxed), 10, 0);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core_go___rarg___lambda__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, lean_object* x_10, lean_object* x_11, lean_object* x_12) {
_start:
{
uint8_t x_13; lean_object* x_14;
x_13 = lean_unbox(x_9);
lean_dec(x_9);
x_14 = l_Lean_Meta_repeat_x27Core_go___rarg___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_13, x_10, x_11, x_12);
return x_14;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core_go___rarg___lambda__2___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, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
_start:
{
uint8_t x_14; uint8_t x_15; lean_object* x_16;
x_14 = lean_unbox(x_9);
lean_dec(x_9);
x_15 = lean_unbox(x_13);
lean_dec(x_13);
x_16 = l_Lean_Meta_repeat_x27Core_go___rarg___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_14, x_10, x_11, x_12, x_15);
return x_16;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core_go___rarg___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:
{
uint8_t x_11; lean_object* x_12;
x_11 = lean_unbox(x_7);
lean_dec(x_7);
x_12 = l_Lean_Meta_repeat_x27Core_go___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_11, x_8, x_9, x_10);
return x_12;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, uint8_t x_4) {
_start:
{
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6;
lean_dec(x_3);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_apply_2(x_5, lean_box(0), x_2);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_1, 1);
lean_inc(x_7);
lean_dec(x_1);
x_8 = lean_array_push(x_2, x_3);
x_9 = lean_apply_2(x_7, lean_box(0), x_8);
return x_9;
}
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___lambda__2(size_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, size_t x_6, lean_object* x_7) {
_start:
{
size_t x_8; size_t x_9; lean_object* x_10;
x_8 = 1;
x_9 = lean_usize_add(x_1, x_8);
x_10 = l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg(x_2, x_3, x_4, x_5, x_9, x_6, x_7);
return x_10;
}
}
static lean_object* _init_l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_not___boxed), 1, 0);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, size_t x_5, size_t x_6, lean_object* x_7) {
_start:
{
uint8_t x_8;
x_8 = lean_usize_dec_eq(x_5, x_6);
if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_9 = lean_ctor_get(x_1, 1);
lean_inc(x_9);
x_10 = lean_array_uget(x_4, x_5);
x_11 = lean_ctor_get(x_1, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
lean_dec(x_12);
lean_inc(x_10);
lean_inc(x_2);
lean_inc(x_1);
x_14 = l_Lean_MVarId_isAssigned___rarg(x_1, x_2, x_10);
x_15 = l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___closed__1;
x_16 = lean_apply_4(x_13, lean_box(0), lean_box(0), x_15, x_14);
x_17 = lean_alloc_closure((void*)(l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___lambda__1___boxed), 4, 3);
lean_closure_set(x_17, 0, x_11);
lean_closure_set(x_17, 1, x_7);
lean_closure_set(x_17, 2, x_10);
lean_inc(x_3);
x_18 = lean_apply_4(x_3, lean_box(0), lean_box(0), x_16, x_17);
x_19 = lean_box_usize(x_5);
x_20 = lean_box_usize(x_6);
x_21 = lean_alloc_closure((void*)(l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___lambda__2___boxed), 7, 6);
lean_closure_set(x_21, 0, x_19);
lean_closure_set(x_21, 1, x_1);
lean_closure_set(x_21, 2, x_2);
lean_closure_set(x_21, 3, x_3);
lean_closure_set(x_21, 4, x_4);
lean_closure_set(x_21, 5, x_20);
x_22 = lean_apply_4(x_9, lean_box(0), lean_box(0), x_18, x_21);
return x_22;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25;
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_23 = lean_ctor_get(x_1, 0);
lean_inc(x_23);
lean_dec(x_1);
x_24 = lean_ctor_get(x_23, 1);
lean_inc(x_24);
lean_dec(x_23);
x_25 = lean_apply_2(x_24, lean_box(0), x_7);
return x_25;
}
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___boxed), 7, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core___rarg___lambda__1(lean_object* x_1, uint8_t 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 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
lean_dec(x_4);
x_6 = lean_array_to_list(lean_box(0), x_3);
x_7 = lean_box(x_2);
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_6);
x_9 = lean_apply_2(x_5, lean_box(0), x_8);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11;
x_6 = lean_ctor_get(x_5, 0);
lean_inc(x_6);
x_7 = lean_ctor_get(x_5, 1);
lean_inc(x_7);
lean_dec(x_5);
x_8 = lean_array_get_size(x_7);
x_9 = lean_unsigned_to_nat(0u);
x_10 = lean_nat_dec_lt(x_9, x_8);
lean_inc(x_1);
x_11 = lean_alloc_closure((void*)(l_Lean_Meta_repeat_x27Core___rarg___lambda__1___boxed), 3, 2);
lean_closure_set(x_11, 0, x_1);
lean_closure_set(x_11, 1, x_6);
if (x_10 == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_4);
x_12 = lean_ctor_get(x_1, 0);
lean_inc(x_12);
lean_dec(x_1);
x_13 = lean_ctor_get(x_12, 1);
lean_inc(x_13);
lean_dec(x_12);
x_14 = lean_apply_2(x_13, lean_box(0), x_2);
x_15 = lean_apply_4(x_3, lean_box(0), lean_box(0), x_14, x_11);
return x_15;
}
else
{
uint8_t x_16;
x_16 = lean_nat_dec_le(x_8, x_8);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_4);
x_17 = lean_ctor_get(x_1, 0);
lean_inc(x_17);
lean_dec(x_1);
x_18 = lean_ctor_get(x_17, 1);
lean_inc(x_18);
lean_dec(x_17);
x_19 = lean_apply_2(x_18, lean_box(0), x_2);
x_20 = lean_apply_4(x_3, lean_box(0), lean_box(0), x_19, x_11);
return x_20;
}
else
{
size_t x_21; size_t x_22; lean_object* x_23; lean_object* x_24;
x_21 = 0;
x_22 = lean_usize_of_nat(x_8);
lean_dec(x_8);
lean_inc(x_3);
x_23 = l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg(x_1, x_4, x_3, x_7, x_21, x_22, x_2);
x_24 = lean_apply_4(x_3, lean_box(0), lean_box(0), x_23, x_11);
return x_24;
}
}
}
}
static lean_object* _init_l_Lean_Meta_repeat_x27Core___rarg___closed__1() {
_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;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core___rarg(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) {
_start:
{
lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_8 = lean_ctor_get(x_1, 1);
lean_inc(x_8);
x_9 = lean_box(0);
x_10 = 0;
x_11 = l_Lean_Meta_repeat_x27Core___rarg___closed__1;
lean_inc(x_4);
lean_inc(x_1);
x_12 = l_Lean_Meta_repeat_x27Core_go___rarg(x_1, x_2, x_3, x_4, x_5, x_7, x_10, x_6, x_9, x_11);
lean_inc(x_8);
x_13 = lean_alloc_closure((void*)(l_Lean_Meta_repeat_x27Core___rarg___lambda__2), 5, 4);
lean_closure_set(x_13, 0, x_1);
lean_closure_set(x_13, 1, x_11);
lean_closure_set(x_13, 2, x_8);
lean_closure_set(x_13, 3, x_4);
x_14 = lean_apply_4(x_8, lean_box(0), lean_box(0), x_12, x_13);
return x_14;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Lean_Meta_repeat_x27Core___rarg), 7, 0);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5; lean_object* x_6;
x_5 = lean_unbox(x_4);
lean_dec(x_4);
x_6 = l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___lambda__1(x_1, x_2, x_3, x_5);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___lambda__2___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) {
_start:
{
size_t x_8; size_t x_9; lean_object* x_10;
x_8 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_9 = lean_unbox_usize(x_6);
lean_dec(x_6);
x_10 = l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___lambda__2(x_8, x_2, x_3, x_4, x_5, x_9, x_7);
return x_10;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___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) {
_start:
{
size_t x_8; size_t x_9; lean_object* x_10;
x_8 = lean_unbox_usize(x_5);
lean_dec(x_5);
x_9 = lean_unbox_usize(x_6);
lean_dec(x_6);
x_10 = l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg(x_1, x_2, x_3, x_4, x_8, x_9, x_7);
return x_10;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27Core___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = lean_unbox(x_2);
lean_dec(x_2);
x_5 = l_Lean_Meta_repeat_x27Core___rarg___lambda__1(x_1, x_4, x_3);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Functor_mapRev___at_Lean_Meta_repeat_x27___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_6 = lean_ctor_get(x_1, 0);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_ctor_get(x_6, 0);
lean_inc(x_7);
lean_dec(x_6);
x_8 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
lean_dec(x_7);
x_9 = lean_apply_4(x_8, lean_box(0), lean_box(0), x_5, x_4);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Functor_mapRev___at_Lean_Meta_repeat_x27___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Functor_mapRev___at_Lean_Meta_repeat_x27___spec__1___rarg), 5, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27___rarg___lambda__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_repeat_x27___rarg___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Meta_repeat_x27___rarg___lambda__1___boxed), 1, 0);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27___rarg(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) {
_start:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10;
lean_inc(x_1);
x_8 = l_Lean_Meta_repeat_x27Core___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
x_9 = l_Lean_Meta_repeat_x27___rarg___closed__1;
x_10 = l_Functor_mapRev___at_Lean_Meta_repeat_x27___spec__1___rarg(x_1, lean_box(0), lean_box(0), x_8, x_9);
return x_10;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Lean_Meta_repeat_x27___rarg), 7, 0);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat_x27___rarg___lambda__1___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Meta_repeat_x27___rarg___lambda__1(x_1);
lean_dec(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_repeat1_x27___rarg___lambda__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("repeat1' made no progress", 25);
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_repeat1_x27___rarg___lambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_repeat1_x27___rarg___lambda__1___closed__1;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat1_x27___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_unbox(x_4);
lean_dec(x_4);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7;
lean_dec(x_3);
x_6 = l_Lean_Meta_repeat1_x27___rarg___lambda__1___closed__2;
x_7 = l_Lean_throwError___rarg(x_1, x_2, x_6);
return x_7;
}
else
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
lean_dec(x_2);
x_8 = lean_ctor_get(x_3, 1);
lean_inc(x_8);
lean_dec(x_3);
x_9 = lean_ctor_get(x_1, 0);
lean_inc(x_9);
lean_dec(x_1);
x_10 = lean_ctor_get(x_9, 1);
lean_inc(x_10);
lean_dec(x_9);
x_11 = lean_apply_2(x_10, lean_box(0), x_8);
return x_11;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat1_x27___rarg(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) {
_start:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_1, 1);
lean_inc(x_9);
lean_inc(x_1);
x_10 = l_Lean_Meta_repeat_x27Core___rarg(x_1, x_3, x_4, x_5, x_6, x_7, x_8);
x_11 = lean_alloc_closure((void*)(l_Lean_Meta_repeat1_x27___rarg___lambda__1), 3, 2);
lean_closure_set(x_11, 0, x_1);
lean_closure_set(x_11, 1, x_2);
x_12 = lean_apply_4(x_9, lean_box(0), lean_box(0), x_10, x_11);
return x_12;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_repeat1_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Lean_Meta_repeat1_x27___rarg), 8, 0);
return x_4;
}
}
lean_object* initialize_Init(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Basic(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Meta_Tactic_Repeat(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(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Meta_Basic(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___closed__1 = _init_l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___closed__1();
lean_mark_persistent(l_Array_foldlMUnsafe_fold___at_Lean_Meta_repeat_x27Core___spec__1___rarg___closed__1);
l_Lean_Meta_repeat_x27Core___rarg___closed__1 = _init_l_Lean_Meta_repeat_x27Core___rarg___closed__1();
lean_mark_persistent(l_Lean_Meta_repeat_x27Core___rarg___closed__1);
l_Lean_Meta_repeat_x27___rarg___closed__1 = _init_l_Lean_Meta_repeat_x27___rarg___closed__1();
lean_mark_persistent(l_Lean_Meta_repeat_x27___rarg___closed__1);
l_Lean_Meta_repeat1_x27___rarg___lambda__1___closed__1 = _init_l_Lean_Meta_repeat1_x27___rarg___lambda__1___closed__1();
lean_mark_persistent(l_Lean_Meta_repeat1_x27___rarg___lambda__1___closed__1);
l_Lean_Meta_repeat1_x27___rarg___lambda__1___closed__2 = _init_l_Lean_Meta_repeat1_x27___rarg___lambda__1___closed__2();
lean_mark_persistent(l_Lean_Meta_repeat1_x27___rarg___lambda__1___closed__2);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

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

@ -10079,7 +10079,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_Array_forInUnsafe_loop___at_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___spec__2___lambda__3___closed__1;
x_2 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___spec__2___lambda__3___closed__2;
x_3 = lean_unsigned_to_nat(410u);
x_3 = lean_unsigned_to_nat(414u);
x_4 = lean_unsigned_to_nat(11u);
x_5 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___spec__2___lambda__3___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -14204,7 +14204,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_Array_forInUnsafe_loop___at_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___spec__2___lambda__3___closed__1;
x_2 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___spec__2___lambda__3___closed__2;
x_3 = lean_unsigned_to_nat(469u);
x_3 = lean_unsigned_to_nat(473u);
x_4 = lean_unsigned_to_nat(11u);
x_5 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___spec__2___lambda__3___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -18938,7 +18938,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_Array_forInUnsafe_loop___at_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___spec__2___lambda__3___closed__1;
x_2 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___spec__2___lambda__3___closed__2;
x_3 = lean_unsigned_to_nat(470u);
x_3 = lean_unsigned_to_nat(474u);
x_4 = lean_unsigned_to_nat(61u);
x_5 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___spec__2___lambda__3___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

10272
stage0/stdlib/Lean/Meta/Tactic/TryThis.c generated Normal file
View file

File diff suppressed because it is too large Load diff

2036
stage0/stdlib/Lean/Parser/Term.c generated
View file

File diff suppressed because it is too large Load diff

1322
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c generated
View file

File diff suppressed because it is too large Load diff