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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-05 18:57:07 -08:00
parent e844a5be74
commit 94cddc299d
32 changed files with 15743 additions and 59782 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/stage0/CMakeLists.txt
View file

@ -1 +1 @@
add_library (stage0 OBJECT ./Init/Coe.c ./Init/Control/Alternative.c ./Init/Control/Applicative.c ./Init/Control/Conditional.c ./Init/Control/Default.c ./Init/Control/EState.c ./Init/Control/Except.c ./Init/Control/Functor.c ./Init/Control/Id.c ./Init/Control/Lift.c ./Init/Control/Monad.c ./Init/Control/MonadFail.c ./Init/Control/Option.c ./Init/Control/Reader.c ./Init/Control/State.c ./Init/Core.c ./Init/Data/Array/Basic.c ./Init/Data/Array/BinSearch.c ./Init/Data/Array/Default.c ./Init/Data/Array/QSort.c ./Init/Data/AssocList.c ./Init/Data/Basic.c ./Init/Data/BinomialHeap/Basic.c ./Init/Data/BinomialHeap/Default.c ./Init/Data/ByteArray/Basic.c ./Init/Data/ByteArray/Default.c ./Init/Data/Char/Basic.c ./Init/Data/Char/Default.c ./Init/Data/DList.c ./Init/Data/Default.c ./Init/Data/Fin/Basic.c ./Init/Data/Fin/Default.c ./Init/Data/HashMap/Basic.c ./Init/Data/HashMap/Default.c ./Init/Data/HashSet.c ./Init/Data/Hashable.c ./Init/Data/Int/Basic.c ./Init/Data/Int/Default.c ./Init/Data/List/Basic.c ./Init/Data/List/BasicAux.c ./Init/Data/List/Control.c ./Init/Data/List/Default.c ./Init/Data/List/Instances.c ./Init/Data/Nat/Basic.c ./Init/Data/Nat/Bitwise.c ./Init/Data/Nat/Control.c ./Init/Data/Nat/Default.c ./Init/Data/Nat/Div.c ./Init/Data/Option/Basic.c ./Init/Data/Option/BasicAux.c ./Init/Data/Option/Default.c ./Init/Data/Option/Instances.c ./Init/Data/PersistentArray/Basic.c ./Init/Data/PersistentArray/Default.c ./Init/Data/PersistentHashMap/Basic.c ./Init/Data/PersistentHashMap/Default.c ./Init/Data/PersistentHashSet.c ./Init/Data/Queue/Basic.c ./Init/Data/Queue/Default.c ./Init/Data/RBMap/Basic.c ./Init/Data/RBMap/BasicAux.c ./Init/Data/RBMap/Default.c ./Init/Data/RBTree/Basic.c ./Init/Data/RBTree/Default.c ./Init/Data/Random.c ./Init/Data/Repr.c ./Init/Data/Stack/Basic.c ./Init/Data/Stack/Default.c ./Init/Data/String/Basic.c ./Init/Data/String/Default.c ./Init/Data/ToString.c ./Init/Data/UInt.c ./Init/Default.c ./Init/Fix.c ./Init/Lean/AbstractMetavarContext.c ./Init/Lean/Attributes.c ./Init/Lean/AuxRecursor.c ./Init/Lean/Class.c ./Init/Lean/Compiler/ClosedTermCache.c ./Init/Lean/Compiler/ConstFolding.c ./Init/Lean/Compiler/Default.c ./Init/Lean/Compiler/ExportAttr.c ./Init/Lean/Compiler/ExternAttr.c ./Init/Lean/Compiler/IR/Basic.c ./Init/Lean/Compiler/IR/Borrow.c ./Init/Lean/Compiler/IR/Boxing.c ./Init/Lean/Compiler/IR/Checker.c ./Init/Lean/Compiler/IR/CompilerM.c ./Init/Lean/Compiler/IR/CtorLayout.c ./Init/Lean/Compiler/IR/Default.c ./Init/Lean/Compiler/IR/ElimDeadBranches.c ./Init/Lean/Compiler/IR/ElimDeadVars.c ./Init/Lean/Compiler/IR/EmitC.c ./Init/Lean/Compiler/IR/EmitUtil.c ./Init/Lean/Compiler/IR/ExpandResetReuse.c ./Init/Lean/Compiler/IR/Format.c ./Init/Lean/Compiler/IR/FreeVars.c ./Init/Lean/Compiler/IR/LiveVars.c ./Init/Lean/Compiler/IR/NormIds.c ./Init/Lean/Compiler/IR/PushProj.c ./Init/Lean/Compiler/IR/RC.c ./Init/Lean/Compiler/IR/ResetReuse.c ./Init/Lean/Compiler/IR/SimpCase.c ./Init/Lean/Compiler/IR/UnboxResult.c ./Init/Lean/Compiler/ImplementedByAttr.c ./Init/Lean/Compiler/InitAttr.c ./Init/Lean/Compiler/InlineAttrs.c ./Init/Lean/Compiler/NameMangling.c ./Init/Lean/Compiler/NeverExtractAttr.c ./Init/Lean/Compiler/Specialize.c ./Init/Lean/Compiler/Util.c ./Init/Lean/Declaration.c ./Init/Lean/Default.c ./Init/Lean/Elaborator/Alias.c ./Init/Lean/Elaborator/Basic.c ./Init/Lean/Elaborator/Command.c ./Init/Lean/Elaborator/Default.c ./Init/Lean/Elaborator/ElabStrategyAttrs.c ./Init/Lean/Elaborator/PreTerm.c ./Init/Lean/Elaborator/ResolveName.c ./Init/Lean/Elaborator/Term.c ./Init/Lean/Environment.c ./Init/Lean/EqnCompiler/Default.c ./Init/Lean/EqnCompiler/MatchPattern.c ./Init/Lean/Expr.c ./Init/Lean/Format.c ./Init/Lean/InductiveUtil.c ./Init/Lean/KVMap.c ./Init/Lean/LBool.c ./Init/Lean/Level.c ./Init/Lean/LocalContext.c ./Init/Lean/Message.c ./Init/Lean/MetavarContext.c ./Init/Lean/Modifiers.c ./Init/Lean/MonadCache.c ./Init/Lean/Name.c ./Init/Lean/NameGenerator.c ./Init/Lean/Options.c ./Init/Lean/Parser/Command.c ./Init/Lean/Parser/Default.c ./Init/Lean/Parser/Identifier.c ./Init/Lean/Parser/Level.c ./Init/Lean/Parser/Module.c ./Init/Lean/Parser/Parser.c ./Init/Lean/Parser/Term.c ./Init/Lean/Parser/Transform.c ./Init/Lean/Parser/Trie.c ./Init/Lean/Path.c ./Init/Lean/Position.c ./Init/Lean/ProjFns.c ./Init/Lean/QuotUtil.c ./Init/Lean/ReducibilityAttrs.c ./Init/Lean/Runtime.c ./Init/Lean/SMap.c ./Init/Lean/Scopes.c ./Init/Lean/Syntax.c ./Init/Lean/TmpMetavarContext.c ./Init/Lean/ToExpr.c ./Init/Lean/Trace.c ./Init/Lean/TypeClass/Basic.c ./Init/Lean/TypeClass/Context.c ./Init/Lean/TypeClass/Default.c ./Init/Lean/TypeClass/Synth.c ./Init/Lean/TypeUtil.c ./Init/Lean/Util.c ./Init/System/Default.c ./Init/System/FilePath.c ./Init/System/IO.c ./Init/System/Platform.c ./Init/Util.c ./Init/WF.c)
add_library (stage0 OBJECT ./Init/Coe.c ./Init/Control/Alternative.c ./Init/Control/Applicative.c ./Init/Control/Conditional.c ./Init/Control/Default.c ./Init/Control/EState.c ./Init/Control/Except.c ./Init/Control/Functor.c ./Init/Control/Id.c ./Init/Control/Lift.c ./Init/Control/Monad.c ./Init/Control/MonadFail.c ./Init/Control/Option.c ./Init/Control/Reader.c ./Init/Control/State.c ./Init/Core.c ./Init/Data/Array/Basic.c ./Init/Data/Array/BinSearch.c ./Init/Data/Array/Default.c ./Init/Data/Array/QSort.c ./Init/Data/AssocList.c ./Init/Data/Basic.c ./Init/Data/BinomialHeap/Basic.c ./Init/Data/BinomialHeap/Default.c ./Init/Data/ByteArray/Basic.c ./Init/Data/ByteArray/Default.c ./Init/Data/Char/Basic.c ./Init/Data/Char/Default.c ./Init/Data/DList.c ./Init/Data/Default.c ./Init/Data/Fin/Basic.c ./Init/Data/Fin/Default.c ./Init/Data/HashMap/Basic.c ./Init/Data/HashMap/Default.c ./Init/Data/HashSet.c ./Init/Data/Hashable.c ./Init/Data/Int/Basic.c ./Init/Data/Int/Default.c ./Init/Data/List/Basic.c ./Init/Data/List/BasicAux.c ./Init/Data/List/Control.c ./Init/Data/List/Default.c ./Init/Data/List/Instances.c ./Init/Data/Nat/Basic.c ./Init/Data/Nat/Bitwise.c ./Init/Data/Nat/Control.c ./Init/Data/Nat/Default.c ./Init/Data/Nat/Div.c ./Init/Data/Option/Basic.c ./Init/Data/Option/BasicAux.c ./Init/Data/Option/Default.c ./Init/Data/Option/Instances.c ./Init/Data/PersistentArray/Basic.c ./Init/Data/PersistentArray/Default.c ./Init/Data/PersistentHashMap/Basic.c ./Init/Data/PersistentHashMap/Default.c ./Init/Data/PersistentHashSet.c ./Init/Data/Queue/Basic.c ./Init/Data/Queue/Default.c ./Init/Data/RBMap/Basic.c ./Init/Data/RBMap/BasicAux.c ./Init/Data/RBMap/Default.c ./Init/Data/RBTree/Basic.c ./Init/Data/RBTree/Default.c ./Init/Data/Random.c ./Init/Data/Repr.c ./Init/Data/Stack/Basic.c ./Init/Data/Stack/Default.c ./Init/Data/String/Basic.c ./Init/Data/String/Default.c ./Init/Data/ToString.c ./Init/Data/UInt.c ./Init/Default.c ./Init/Fix.c ./Init/Lean/Attributes.c ./Init/Lean/AuxRecursor.c ./Init/Lean/Class.c ./Init/Lean/Compiler/ClosedTermCache.c ./Init/Lean/Compiler/ConstFolding.c ./Init/Lean/Compiler/Default.c ./Init/Lean/Compiler/ExportAttr.c ./Init/Lean/Compiler/ExternAttr.c ./Init/Lean/Compiler/IR/Basic.c ./Init/Lean/Compiler/IR/Borrow.c ./Init/Lean/Compiler/IR/Boxing.c ./Init/Lean/Compiler/IR/Checker.c ./Init/Lean/Compiler/IR/CompilerM.c ./Init/Lean/Compiler/IR/CtorLayout.c ./Init/Lean/Compiler/IR/Default.c ./Init/Lean/Compiler/IR/ElimDeadBranches.c ./Init/Lean/Compiler/IR/ElimDeadVars.c ./Init/Lean/Compiler/IR/EmitC.c ./Init/Lean/Compiler/IR/EmitUtil.c ./Init/Lean/Compiler/IR/ExpandResetReuse.c ./Init/Lean/Compiler/IR/Format.c ./Init/Lean/Compiler/IR/FreeVars.c ./Init/Lean/Compiler/IR/LiveVars.c ./Init/Lean/Compiler/IR/NormIds.c ./Init/Lean/Compiler/IR/PushProj.c ./Init/Lean/Compiler/IR/RC.c ./Init/Lean/Compiler/IR/ResetReuse.c ./Init/Lean/Compiler/IR/SimpCase.c ./Init/Lean/Compiler/IR/UnboxResult.c ./Init/Lean/Compiler/ImplementedByAttr.c ./Init/Lean/Compiler/InitAttr.c ./Init/Lean/Compiler/InlineAttrs.c ./Init/Lean/Compiler/NameMangling.c ./Init/Lean/Compiler/NeverExtractAttr.c ./Init/Lean/Compiler/Specialize.c ./Init/Lean/Compiler/Util.c ./Init/Lean/Declaration.c ./Init/Lean/Default.c ./Init/Lean/Elaborator/Alias.c ./Init/Lean/Elaborator/Basic.c ./Init/Lean/Elaborator/Command.c ./Init/Lean/Elaborator/Default.c ./Init/Lean/Elaborator/ElabStrategyAttrs.c ./Init/Lean/Elaborator/PreTerm.c ./Init/Lean/Elaborator/ResolveName.c ./Init/Lean/Elaborator/Term.c ./Init/Lean/Environment.c ./Init/Lean/EqnCompiler/Default.c ./Init/Lean/EqnCompiler/MatchPattern.c ./Init/Lean/Expr.c ./Init/Lean/Format.c ./Init/Lean/InductiveUtil.c ./Init/Lean/KVMap.c ./Init/Lean/LBool.c ./Init/Lean/Level.c ./Init/Lean/LocalContext.c ./Init/Lean/Message.c ./Init/Lean/MetavarContext.c ./Init/Lean/Modifiers.c ./Init/Lean/MonadCache.c ./Init/Lean/Name.c ./Init/Lean/NameGenerator.c ./Init/Lean/Options.c ./Init/Lean/Parser/Command.c ./Init/Lean/Parser/Default.c ./Init/Lean/Parser/Identifier.c ./Init/Lean/Parser/Level.c ./Init/Lean/Parser/Module.c ./Init/Lean/Parser/Parser.c ./Init/Lean/Parser/Term.c ./Init/Lean/Parser/Transform.c ./Init/Lean/Parser/Trie.c ./Init/Lean/Path.c ./Init/Lean/Position.c ./Init/Lean/ProjFns.c ./Init/Lean/QuotUtil.c ./Init/Lean/ReducibilityAttrs.c ./Init/Lean/Runtime.c ./Init/Lean/SMap.c ./Init/Lean/Scopes.c ./Init/Lean/Syntax.c ./Init/Lean/ToExpr.c ./Init/Lean/Trace.c ./Init/Lean/TypeClass/Basic.c ./Init/Lean/TypeClass/Context.c ./Init/Lean/TypeClass/Default.c ./Init/Lean/TypeClass/Synth.c ./Init/Lean/TypeUtil.c ./Init/Lean/Util.c ./Init/System/Default.c ./Init/System/FilePath.c ./Init/System/IO.c ./Init/System/Platform.c ./Init/Util.c ./Init/WF.c)

536
src/stage0/Init/Control/EState.c
View file

File diff suppressed because it is too large Load diff

27
src/stage0/Init/Core.c
View file

@ -154,7 +154,6 @@ lean_object* l_List_HasSizeof___rarg(lean_object*);
lean_object* l_ite_Decidable___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_decidableOfDecidableEq___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_beqOfEq___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_default___rarg(lean_object*);
lean_object* l_Thunk_mk___boxed(lean_object*, lean_object*);
lean_object* l_Subtype_HasSizeof___rarg(lean_object*, lean_object*);
lean_object* l_Bool_sizeof___boxed(lean_object*);
@ -237,7 +236,6 @@ lean_object* l_Task_pure___boxed(lean_object*, lean_object*);
lean_object* l_Function_const___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Subtype_HasSizeof(lean_object*);
lean_object* l_Sum_DecidableEq(lean_object*, lean_object*);
lean_object* l_default___rarg___boxed(lean_object*);
lean_object* l_dite___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Quot_recOnSubsingleton___rarg(lean_object*, lean_object*);
lean_object* l_dite_Decidable(lean_object*, lean_object*, lean_object*);
@ -293,7 +291,6 @@ lean_object* l_idRhs___rarg___boxed(lean_object*);
lean_object* l_Quotient_recOnSubsingleton_u2082___at_Quotient_DecidableEq___spec__1(lean_object*, lean_object*);
lean_object* l___private_Init_Core_20__funSetoid___boxed(lean_object*, lean_object*);
lean_object* l_Subtype_sizeof___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_default(lean_object*);
lean_object* l_Quotient_recOn___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Ne_Decidable___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_and___boxed(lean_object*, lean_object*);
@ -2624,30 +2621,6 @@ lean_dec(x_2);
return x_4;
}
}
lean_object* l_default___rarg(lean_object* x_1) {
_start:
{
lean_inc(x_1);
return x_1;
}
}
lean_object* l_default(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_default___rarg___boxed), 1, 0);
return x_2;
}
}
lean_object* l_default___rarg___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_default___rarg(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_arbitrary___rarg(lean_object* x_1) {
_start:
{

40293
src/stage0/Init/Lean/AbstractMetavarContext.c
View file

File diff suppressed because it is too large Load diff

14
src/stage0/Init/Lean/Attributes.c
View file

@ -205,7 +205,6 @@ lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_
lean_object* l_Array_anyMAux___main___at_Lean_registerTagAttribute___spec__3___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_RBNode_find___main___at_Lean_EnumAttributes_getValue___spec__1___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Array_qsortAux___main___at_Lean_registerParametricAttribute___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TagAttribute_Inhabited___closed__1;
lean_object* l_RBNode_fold___main___at_Lean_registerEnumAttributes___spec__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_registerTagAttribute___spec__4___closed__1;
@ -255,6 +254,7 @@ lean_object* l_Lean_AttributeImpl_inhabited___lambda__2(lean_object*, lean_objec
lean_object* l_Lean_registerTagAttribute___lambda__3___closed__3;
lean_object* l_Lean_AttributeImpl_inhabited___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_registerEnumAttributes___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_RBNode_find___main___at_Lean_EnumAttributes_getValue___spec__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_registerTagAttribute___lambda__3___boxed(lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
@ -2939,7 +2939,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_registerTagAttribute___spec__4(x_14, x_7);
@ -3148,7 +3148,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_registerTagAttribute___spec__4(x_67, x_60);
@ -4774,7 +4774,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_registerParametricAttribute___spec__9___rarg(x_14, x_7);
@ -4983,7 +4983,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_registerParametricAttribute___spec__9___rarg(x_67, x_60);
@ -6949,7 +6949,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_registerEnumAttributes___spec__9___rarg(x_14, x_7);
@ -7158,7 +7158,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_registerEnumAttributes___spec__9___rarg(x_67, x_60);

12
src/stage0/Init/Lean/Class.c
View file

@ -32,6 +32,7 @@ lean_object* l_AssocList_find___main___at_Lean_hasOutParams___spec__6(lean_objec
extern lean_object* l_Array_empty___closed__1;
lean_object* l_Lean_registerInstanceAttr___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_ConstantInfo_value_x3f(lean_object*);
extern lean_object* l_Lean_registerEnvExtensionUnsafe___rarg___closed__2;
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkClassExtension___spec__7___closed__2;
lean_object* l_Lean_isInstance___boxed(lean_object*, lean_object*);
@ -110,7 +111,6 @@ lean_object* l_Lean_SMap_empty___at_Lean_ClassState_Inhabited___spec__1___closed
lean_object* lean_io_initializing(lean_object*);
lean_object* l_Lean_SMap_switch___at_Lean_ClassState_switch___spec__2(lean_object*);
lean_object* l_AssocList_contains___main___at_Lean_ClassState_addEntry___spec__7___boxed(lean_object*, lean_object*);
lean_object* l_Lean_ConstantInfo_value(lean_object*);
lean_object* l_Lean_classExtension___closed__3;
lean_object* l_PersistentHashMap_insertAux___main___at_Lean_ClassState_addEntry___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkClassExtension___closed__5;
@ -194,7 +194,6 @@ lean_object* l_mkHashMap___at_Lean_ClassState_Inhabited___spec__2(lean_object*);
lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_mkClassExtension___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkClassExtension___lambda__1___boxed(lean_object*);
lean_object* l_Lean_SMap_find___at_Lean_ClassState_addEntry___spec__12(lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_AssocList_foldlM___main___at_Lean_ClassState_addEntry___spec__10(lean_object*, lean_object*);
lean_object* l_Lean_mkClassExtension___closed__4;
lean_object* l_Array_iterateMAux___main___at_Lean_ClassState_addEntry___spec__22___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -239,6 +238,7 @@ lean_object* l_Array_iterateMAux___main___at_Lean_mkClassExtension___spec__3(lea
lean_object* l_HashMapImp_insert___at_Lean_ClassState_addEntry___spec__6___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_AssocList_replace___main___at_Lean_ClassState_addEntry___spec__39(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerClassAttr___closed__1;
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_classExtension___elambda__4___rarg(lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
extern lean_object* l_Lean_Name_toString___closed__1;
@ -4132,7 +4132,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkClassExtension___spec__7(x_14, x_7);
@ -4341,7 +4341,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkClassExtension___spec__7(x_67, x_60);
@ -5854,7 +5854,7 @@ if (x_9 == 0)
{
lean_object* x_10; lean_object* x_11;
x_10 = lean_ctor_get(x_7, 0);
x_11 = l_Lean_ConstantInfo_value(x_10);
x_11 = l_Lean_ConstantInfo_value_x3f(x_10);
lean_dec(x_10);
if (lean_obj_tag(x_11) == 0)
{
@ -5911,7 +5911,7 @@ lean_object* x_21; lean_object* x_22;
x_21 = lean_ctor_get(x_7, 0);
lean_inc(x_21);
lean_dec(x_7);
x_22 = l_Lean_ConstantInfo_value(x_21);
x_22 = l_Lean_ConstantInfo_value_x3f(x_21);
lean_dec(x_21);
if (lean_obj_tag(x_22) == 0)
{

6
src/stage0/Init/Lean/Compiler/ClosedTermCache.c
View file

@ -102,7 +102,6 @@ lean_object* l_Lean_closedTermCacheExt___closed__3;
lean_object* l_Lean_SMap_insert___at_Lean_mkClosedTermCacheExtension___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_closedTermCacheExt___closed__1;
lean_object* l_AssocList_replace___main___at_Lean_mkClosedTermCacheExtension___spec__11(lean_object*, lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SMap_empty___at_Lean_mkClosedTermCacheExtension___spec__12___closed__1;
lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_io_ref_get(lean_object*, lean_object*);
@ -124,6 +123,7 @@ lean_object* l_Lean_closedTermCacheExt___closed__8;
lean_object* l_mkHashMapImp___rarg(lean_object*);
lean_object* lean_get_closed_term_name(lean_object*, lean_object*);
lean_object* l_Lean_closedTermCacheExt___elambda__3(lean_object*, lean_object*);
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
extern lean_object* l_Lean_Name_toString___closed__1;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
@ -1466,7 +1466,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkClosedTermCacheExtension___spec__21(x_14, x_7);
@ -1675,7 +1675,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkClosedTermCacheExtension___spec__21(x_67, x_60);

6
src/stage0/Init/Lean/Compiler/ExportAttr.c
View file

@ -78,7 +78,6 @@ lean_object* l_Lean_mkExportAttr___lambda__2___boxed(lean_object*, lean_object*,
lean_object* l_Lean_registerParametricAttribute___rarg___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Char_isDigit(uint32_t);
lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___closed__1;
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_registerTagAttribute___spec__4___closed__1;
lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkExportAttr___lambda__1___closed__1;
@ -93,6 +92,7 @@ extern lean_object* l_Substring_drop___closed__1;
lean_object* l_String_anyAux___main___at___private_Init_Lean_Compiler_ExportAttr_1__isValidCppId___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Lean_Compiler_ExportAttr_2__isValidCppName___main(lean_object*);
lean_object* lean_string_utf8_next(lean_object*, lean_object*);
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
extern lean_object* l_Lean_Name_toString___closed__1;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
@ -1024,7 +1024,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkExportAttr___spec__7(x_14, x_7);
@ -1233,7 +1233,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkExportAttr___spec__7(x_67, x_60);

6
src/stage0/Init/Lean/Compiler/ExternAttr.c
View file

@ -118,7 +118,6 @@ uint8_t l_UInt32_decEq(uint32_t, uint32_t);
lean_object* l___private_Init_Lean_Compiler_ExternAttr_1__syntaxToExternEntries___main___closed__6;
lean_object* l_Lean_registerParametricAttribute___rarg___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Compiler_ExternAttr_2__syntaxToExternAttrData___closed__7;
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Compiler_ExternAttr_2__syntaxToExternAttrData___closed__8;
lean_object* l___private_Init_Lean_Compiler_ExternAttr_2__syntaxToExternAttrData___closed__1;
extern lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_registerTagAttribute___spec__4___closed__1;
@ -141,6 +140,7 @@ lean_object* l_Lean_getExternEntryForAux(lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_getExternEntryForAux___main___boxed(lean_object*, lean_object*);
lean_object* l_Lean_ParametricAttribute_getParam___at_Lean_getExternAttrData___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_RBNode_find___main___at_Lean_getExternAttrData___spec__2___boxed(lean_object*, lean_object*);
@ -1314,7 +1314,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkExternAttr___spec__7(x_14, x_7);
@ -1523,7 +1523,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkExternAttr___spec__7(x_67, x_60);

6
src/stage0/Init/Lean/Compiler/IR/CompilerM.c
View file

@ -148,7 +148,6 @@ lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Compiler_IR_Com
lean_object* l_Array_iterateMAux___main___at_Lean_IR_mkDeclMapExtension___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_declMapExt___elambda__1(lean_object*);
lean_object* l_PersistentHashMap_insert___at_Lean_IR_mkDeclMapExtension___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_mkDeclMapExtension___closed__4;
lean_object* l_AssocList_replace___main___at___private_Init_Lean_Compiler_IR_CompilerM_4__mkEntryArray___spec__7(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_getDecl_x27(lean_object*, lean_object*, lean_object*, lean_object*);
@ -190,6 +189,7 @@ lean_object* l_Lean_IR_getEnv(lean_object*);
uint8_t l_HashMapImp_contains___at_Lean_IR_containsDecl___spec__2(lean_object*, lean_object*);
lean_object* l_Array_anyMAux___main___at_Lean_IR_mkDeclMapExtension___spec__13___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_IR_mkDeclMapExtension___spec__14___closed__2;
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
lean_object* l_Array_iterateMAux___main___at_Lean_IR_mkDeclMapExtension___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_Log_format___boxed(lean_object*);
@ -2234,7 +2234,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_IR_mkDeclMapExtension___spec__14(x_14, x_7);
@ -2443,7 +2443,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_IR_mkDeclMapExtension___spec__14(x_67, x_60);

6
src/stage0/Init/Lean/Compiler/IR/ElimDeadBranches.c
View file

@ -219,7 +219,6 @@ lean_object* l_Lean_IR_UnreachableBranches_functionSummariesExt___elambda__3(lea
extern lean_object* l_Array_HasRepr___rarg___closed__1;
lean_object* l_Lean_SMap_empty___at_Lean_IR_UnreachableBranches_mkFunctionSummariesExtension___spec__12___closed__2;
lean_object* l_Lean_IR_UnreachableBranches_projValue___boxed(lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_UnreachableBranches_functionSummariesExt___closed__2;
lean_object* l_panicWithPos___at_Lean_IR_UnreachableBranches_interpFnBody___main___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_UnreachableBranches_Value_format___main(lean_object*);
@ -271,6 +270,7 @@ lean_object* l_List_foldr___main___at_Lean_IR_UnreachableBranches_Value_beq___ma
lean_object* l_Lean_IR_UnreachableBranches_interpFnBody(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forMAux___main___at_Lean_IR_UnreachableBranches_interpFnBody___main___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_foldAux___main___at_Lean_IR_elimDeadBranches___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_UnreachableBranches_Value_merge(lean_object*, lean_object*);
lean_object* l_Lean_IR_UnreachableBranches_elimDeadAux___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
@ -3241,7 +3241,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_IR_UnreachableBranches_mkFunctionSummariesExtension___spec__21(x_14, x_7);
@ -3450,7 +3450,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_IR_UnreachableBranches_mkFunctionSummariesExtension___spec__21(x_67, x_60);

6
src/stage0/Init/Lean/Compiler/ImplementedByAttr.c
View file

@ -72,7 +72,6 @@ lean_object* l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplemented
lean_object* l_Lean_Compiler_implementedByAttr;
lean_object* l_Lean_Compiler_mkImplementedByAttr___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerParametricAttribute___rarg___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_registerTagAttribute___spec__4___closed__1;
lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_mkImplementedByAttr___closed__2;
@ -86,6 +85,7 @@ lean_object* l_Lean_ParametricAttribute_getParam___at_Lean_Compiler_getImplement
lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_Compiler_mkImplementedByAttr___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_mkImplementedByAttr___lambda__1___closed__2;
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
extern lean_object* l_Lean_Name_toString___closed__1;
@ -654,7 +654,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_Compiler_mkImplementedByAttr___spec__7(x_14, x_7);
@ -863,7 +863,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_Compiler_mkImplementedByAttr___spec__7(x_67, x_60);

6
src/stage0/Init/Lean/Compiler/InitAttr.c
View file

@ -89,7 +89,6 @@ lean_object* l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec
lean_object* l_Lean_mkInitAttr___closed__5;
lean_object* l_Lean_registerParametricAttribute___rarg___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerParametricAttribute___at_Lean_mkInitAttr___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Lean_Compiler_InitAttr_2__isUnitType(lean_object*);
extern lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_registerTagAttribute___spec__4___closed__1;
lean_object* l_Lean_mkInitAttr___lambda__1___closed__6;
@ -108,6 +107,7 @@ lean_object* l_Lean_setInitAttr(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Compiler_InitAttr_1__getIOTypeArg___closed__2;
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_mkInitAttr___spec__4___closed__1;
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
extern lean_object* l_Lean_Name_toString___closed__1;
lean_object* l___private_Init_Lean_Compiler_InitAttr_2__isUnitType___closed__1;
@ -836,7 +836,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkInitAttr___spec__7(x_14, x_7);
@ -1045,7 +1045,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkInitAttr___spec__7(x_67, x_60);

6
src/stage0/Init/Lean/Compiler/InlineAttrs.c
View file

@ -100,7 +100,6 @@ lean_object* l_Lean_Compiler_mkInlineAttrs___closed__21;
lean_object* l_Lean_Compiler_mkInlineAttrs___closed__22;
lean_object* l_Lean_registerEnumAttributes___at_Lean_Compiler_mkInlineAttrs___spec__1___closed__1;
lean_object* l_RBNode_find___main___at___private_Init_Lean_Compiler_InlineAttrs_1__hasInlineAttrAux___main___spec__2___boxed(lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_registerTagAttribute___spec__4___closed__1;
lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Compiler_InlineAttrs_1__hasInlineAttrAux___boxed(lean_object*, lean_object*, lean_object*);
@ -122,6 +121,7 @@ lean_object* l_RBNode_fold___main___at_Lean_Compiler_mkInlineAttrs___spec__2___b
lean_object* l_Lean_Compiler_mkInlineAttrs___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__5;
lean_object* l_Lean_Compiler_mkInlineAttrs___closed__26;
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
extern lean_object* l_Lean_Name_toString___closed__1;
lean_object* l_Array_qsortAux___main___at_Lean_Compiler_mkInlineAttrs___spec__3___boxed(lean_object*, lean_object*, lean_object*);
@ -809,7 +809,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_Compiler_mkInlineAttrs___spec__7(x_14, x_7);
@ -1018,7 +1018,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_Compiler_mkInlineAttrs___spec__7(x_67, x_60);

10
src/stage0/Init/Lean/Compiler/Specialize.c
View file

@ -174,7 +174,6 @@ lean_object* l_Lean_Compiler_mkSpecializeAttrs___closed__6;
lean_object* l_Lean_Compiler_mkSpecializeAttrs___closed__5;
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Compiler_getCachedSpecialization___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Array_anyMAux___main___at_Lean_Compiler_mkSpecializeAttrs___spec__6(lean_object*, lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_registerTagAttribute___spec__4___closed__1;
lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentHashMap_find___at_Lean_Compiler_getCachedSpecialization___spec__2___boxed(lean_object*, lean_object*);
@ -213,6 +212,7 @@ lean_object* l_List_map___main___at_Lean_Compiler_mkSpecializeAttrs___spec__8___
extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__5;
lean_object* l_List_map___main___at_Lean_Compiler_mkSpecializeAttrs___spec__8(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerEnumAttributes___at_Lean_Compiler_mkSpecializeAttrs___spec__1___lambda__2___boxed(lean_object*);
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
uint8_t l_Array_anyMAux___main___at_Lean_Compiler_mkSpecExtension___spec__6(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
extern lean_object* l_Lean_Name_toString___closed__1;
@ -885,7 +885,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_Compiler_mkSpecializeAttrs___spec__7(x_14, x_7);
@ -1094,7 +1094,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_Compiler_mkSpecializeAttrs___spec__7(x_67, x_60);
@ -4727,7 +4727,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_Compiler_mkSpecExtension___spec__7(x_14, x_7);
@ -4936,7 +4936,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_Compiler_mkSpecExtension___spec__7(x_67, x_60);

77
src/stage0/Init/Lean/Declaration.c
View file

@ -15,12 +15,13 @@ extern "C" {
#endif
lean_object* l_Lean_ConstantInfo_name(lean_object*);
lean_object* lean_task_get(lean_object*);
lean_object* l_Lean_ConstantInfo_value_x21___closed__2;
lean_object* l_Lean_ConstantInfo_value_x21___boxed(lean_object*);
lean_object* l_Lean_ConstantInfo_name___boxed(lean_object*);
lean_object* l_Lean_ConstantInfo_value_x3f(lean_object*);
lean_object* l_Lean_ConstantInfo_toConstantVal(lean_object*);
lean_object* l_Lean_ConstantInfo_value___boxed(lean_object*);
lean_object* l_Lean_ConstantInfo_instantiateValueLevelParams___boxed(lean_object*, lean_object*);
lean_object* l_Lean_RecursorVal_getInduct___boxed(lean_object*);
lean_object* l_Lean_ConstantInfo_value(lean_object*);
lean_object* l_Lean_ConstantInfo_lparams(lean_object*);
uint8_t l_Lean_ConstantInfo_hasValue(lean_object*);
lean_object* l_Lean_Name_getPrefix(lean_object*);
@ -31,13 +32,17 @@ lean_object* l_Lean_RecursorVal_getMajorIdx___boxed(lean_object*);
lean_object* l_Lean_RecursorVal_getInduct(lean_object*);
lean_object* l_Lean_ConstantInfo_instantiateTypeLevelParams___boxed(lean_object*, lean_object*);
lean_object* l_Lean_RecursorVal_getMajorIdx(lean_object*);
lean_object* l_Lean_ConstantInfo_value_x3f___boxed(lean_object*);
lean_object* l_Lean_ConstantInfo_hints(lean_object*);
lean_object* l_Lean_ConstantInfo_value_x21___closed__1;
lean_object* l_Lean_ConstantInfo_toConstantVal___boxed(lean_object*);
lean_object* lean_instantiate_type_lparams(lean_object*, lean_object*);
lean_object* l_Lean_ConstantInfo_type(lean_object*);
lean_object* l_Lean_ConstantInfo_type___boxed(lean_object*);
lean_object* l_Lean_ConstantInfo_lparams___boxed(lean_object*);
lean_object* l_Lean_ConstantInfo_value_x21(lean_object*);
lean_object* l_Lean_ConstantInfo_hasValue___boxed(lean_object*);
lean_object* l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_RecursorVal_getMajorIdx(lean_object* x_1) {
_start:
{
@ -161,7 +166,7 @@ lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_ConstantInfo_value(lean_object* x_1) {
lean_object* l_Lean_ConstantInfo_value_x3f(lean_object* x_1) {
_start:
{
switch (lean_obj_tag(x_1)) {
@ -194,11 +199,11 @@ return x_9;
}
}
}
lean_object* l_Lean_ConstantInfo_value___boxed(lean_object* x_1) {
lean_object* l_Lean_ConstantInfo_value_x3f___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_ConstantInfo_value(x_1);
x_2 = l_Lean_ConstantInfo_value_x3f(x_1);
lean_dec(x_1);
return x_2;
}
@ -238,6 +243,64 @@ x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* _init_l_Lean_ConstantInfo_value_x21___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Init.Lean.Declaration");
return x_1;
}
}
lean_object* _init_l_Lean_ConstantInfo_value_x21___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("declaration with value expected");
return x_1;
}
}
lean_object* l_Lean_ConstantInfo_value_x21(lean_object* x_1) {
_start:
{
switch (lean_obj_tag(x_1)) {
case 1:
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_2, 1);
lean_inc(x_3);
return x_3;
}
case 2:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_1, 0);
x_5 = lean_ctor_get(x_4, 1);
x_6 = lean_task_get(x_5);
return x_6;
}
default:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_7 = l_Lean_ConstantInfo_value_x21___closed__1;
x_8 = lean_unsigned_to_nat(177u);
x_9 = lean_unsigned_to_nat(31u);
x_10 = l_Lean_ConstantInfo_value_x21___closed__2;
x_11 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_7, x_8, x_9, x_10);
return x_11;
}
}
}
}
lean_object* l_Lean_ConstantInfo_value_x21___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_ConstantInfo_value_x21(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_ConstantInfo_hints(lean_object* x_1) {
_start:
{
@ -291,6 +354,10 @@ _G_initialized = true;
res = initialize_Init_Lean_Expr(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_ConstantInfo_value_x21___closed__1 = _init_l_Lean_ConstantInfo_value_x21___closed__1();
lean_mark_persistent(l_Lean_ConstantInfo_value_x21___closed__1);
l_Lean_ConstantInfo_value_x21___closed__2 = _init_l_Lean_ConstantInfo_value_x21___closed__2();
lean_mark_persistent(l_Lean_ConstantInfo_value_x21___closed__2);
return lean_mk_io_result(lean_box(0));
}
#ifdef __cplusplus

6
src/stage0/Init/Lean/Elaborator/Alias.c
View file

@ -106,7 +106,6 @@ lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkAliasExtension___spec
lean_object* l_Lean_aliasExtension___closed__8;
lean_object* l_List_elem___main___at_Lean_addAliasEntry___spec__18___boxed(lean_object*, lean_object*);
lean_object* l_Lean_getAliases___boxed(lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentHashMap_insert___at_Lean_addAliasEntry___spec__8(lean_object*, lean_object*, lean_object*);
lean_object* l_AssocList_find___main___at_Lean_addAliasEntry___spec__6___boxed(lean_object*, lean_object*);
lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
@ -122,6 +121,7 @@ lean_object* lean_array_get_size(lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_mkHashMapImp___rarg(lean_object*);
lean_object* l_Lean_aliasExtension___elambda__1___boxed(lean_object*);
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_aliasExtension___elambda__3___boxed(lean_object*, lean_object*);
lean_object* l_Lean_aliasExtension___elambda__4(lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
@ -1851,7 +1851,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkAliasExtension___spec__10(x_14, x_7);
@ -2060,7 +2060,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkAliasExtension___spec__10(x_67, x_60);

10
src/stage0/Init/Lean/Elaborator/Basic.c
View file

@ -316,7 +316,6 @@ lean_object* l_Lean_mkCommandElabAttribute(lean_object*);
lean_object* l_Lean_syntaxNodeKindOfAttrParam___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkTermElabAttribute___spec__4(lean_object*, lean_object*);
lean_object* l_Lean_Elab_getUniverses___boxed(lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_resolveNamespaceUsingOpenDecls(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_processCommandsAux___main___boxed(lean_object*);
uint8_t l_HashMapImp_contains___at_Lean_addBuiltinCommandElab___spec__2(lean_object*, lean_object*);
@ -385,6 +384,7 @@ lean_object* l_HashMapImp_moveEntries___main___at_Lean_addBuiltinCommandElab___s
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_processHeaderAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_mkTermElabAttribute___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_builtinCommandElabTable;
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkAnonymousInstName___boxed(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Path_1__pathSep___closed__1;
lean_object* l_Lean_Elab_getPosition(lean_object*, lean_object*, lean_object*);
@ -5059,7 +5059,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkTermElabAttribute___spec__4(x_14, x_7);
@ -5268,7 +5268,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkTermElabAttribute___spec__4(x_67, x_60);
@ -6002,7 +6002,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkCommandElabAttribute___spec__4(x_14, x_7);
@ -6211,7 +6211,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkCommandElabAttribute___spec__4(x_67, x_60);

6
src/stage0/Init/Lean/Elaborator/ElabStrategyAttrs.c
View file

@ -84,7 +84,6 @@ lean_object* l_RBNode_find___main___at_Lean_getElaboratorStrategy___spec__2(lean
lean_object* l_Lean_registerEnumAttributes___at_Lean_mkElaboratorStrategyAttrs___spec__1___closed__2;
lean_object* l_Lean_registerEnumAttributes___at_Lean_mkElaboratorStrategyAttrs___spec__1___lambda__2___boxed(lean_object*);
lean_object* l_Lean_registerEnumAttributes___at_Lean_mkElaboratorStrategyAttrs___spec__1___lambda__1(lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_registerTagAttribute___spec__4___closed__1;
lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkElaboratorStrategyAttrs___closed__5;
@ -102,6 +101,7 @@ lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_mkElaboratorStrategyAttrs___closed__18;
lean_object* l_Lean_mkElaboratorStrategyAttrs___closed__11;
extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__5;
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
extern lean_object* l_Lean_Name_toString___closed__1;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
@ -677,7 +677,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkElaboratorStrategyAttrs___spec__7(x_14, x_7);
@ -886,7 +886,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkElaboratorStrategyAttrs___spec__7(x_67, x_60);

20
src/stage0/Init/Lean/Environment.c
View file

@ -328,7 +328,6 @@ lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Environment_10_
lean_object* l_Lean_Environment_contains___boxed(lean_object*, lean_object*);
extern lean_object* l_Array_HasRepr___rarg___closed__1;
lean_object* lean_read_module_data(lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_IO_println___at_HasRepr_HasEval___spec__1(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_importModules___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__4___boxed(lean_object*);
@ -372,7 +371,6 @@ lean_object* lean_array_get_size(lean_object*);
lean_object* l___private_Init_Lean_Environment_11__finalizePersistentExtensions(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_importModules___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_EnvExtension_Inhabited(lean_object*);
lean_object* l_EState_pure___rarg(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Environment_10__setImportedEntries___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SimplePersistentEnvExtension_setState___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Environment_9__getEntriesFor___main(lean_object*, lean_object*, lean_object*);
@ -393,6 +391,7 @@ lean_object* l_Lean_SimplePersistentEnvExtension_Inhabited(lean_object*, lean_ob
uint32_t lean_environment_trust_level(lean_object*);
lean_object* l_Lean_modListExtension___closed__2;
lean_object* l_AssocList_find___main___at_Lean_Environment_find___spec__3___boxed(lean_object*, lean_object*);
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_get_extension(lean_object*, lean_object*);
lean_object* l_Lean_mkEmptyEnvironment___boxed(lean_object*, lean_object*);
lean_object* l_Lean_registerPersistentEnvExtension___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -414,6 +413,7 @@ uint8_t l_USize_decLe(size_t, size_t);
lean_object* lean_nat_div(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_insertAux___main___at_Lean_Environment_addAux___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkTagDeclarationExtension___closed__2;
lean_object* l_EStateM_pure___rarg(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Environment_displayStats___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PersistentEnvExtension_modifyState(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_mkModuleData___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
@ -4340,7 +4340,7 @@ x_12 = l_Array_empty___closed__1;
lean_inc(x_11);
x_13 = lean_apply_1(x_11, x_12);
x_14 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_15 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_15 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_15, 0, x_13);
lean_closure_set(x_15, 1, x_14);
x_16 = l_Lean_registerEnvExtensionUnsafe___at_Lean_registerPersistentEnvExtensionUnsafe___spec__2___rarg(x_1, x_15, x_8);
@ -4550,7 +4550,7 @@ x_65 = l_Array_empty___closed__1;
lean_inc(x_64);
x_66 = lean_apply_1(x_64, x_65);
x_67 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_68 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_68 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_68, 0, x_66);
lean_closure_set(x_68, 1, x_67);
x_69 = l_Lean_registerEnvExtensionUnsafe___at_Lean_registerPersistentEnvExtensionUnsafe___spec__2___rarg(x_1, x_68, x_61);
@ -5268,7 +5268,7 @@ x_12 = l_Array_empty___closed__1;
lean_inc(x_11);
x_13 = lean_apply_1(x_11, x_12);
x_14 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_15 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_15 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_15, 0, x_13);
lean_closure_set(x_15, 1, x_14);
x_16 = l_Lean_registerEnvExtensionUnsafe___at_Lean_registerSimplePersistentEnvExtension___spec__3___rarg(x_1, x_15, x_8);
@ -5478,7 +5478,7 @@ x_65 = l_Array_empty___closed__1;
lean_inc(x_64);
x_66 = lean_apply_1(x_64, x_65);
x_67 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_68 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_68 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_68, 0, x_66);
lean_closure_set(x_68, 1, x_67);
x_69 = l_Lean_registerEnvExtensionUnsafe___at_Lean_registerSimplePersistentEnvExtension___spec__3___rarg(x_1, x_68, x_61);
@ -6562,7 +6562,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkTagDeclarationExtension___spec__6(x_14, x_7);
@ -6771,7 +6771,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkTagDeclarationExtension___spec__6(x_67, x_60);
@ -7534,7 +7534,7 @@ lean_object* lean_register_extension(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = lean_alloc_closure((void*)(l_EState_pure___rarg), 2, 1);
x_2 = lean_alloc_closure((void*)(l_EStateM_pure___rarg), 2, 1);
lean_closure_set(x_2, 0, x_1);
x_3 = lean_box(0);
x_4 = l_Lean_registerEnvExtensionUnsafe___at_Lean_registerCPPExtension___spec__1(x_2, x_3);
@ -7897,7 +7897,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_box(0);
x_2 = lean_alloc_closure((void*)(l_EState_pure___rarg), 2, 1);
x_2 = lean_alloc_closure((void*)(l_EStateM_pure___rarg), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}

6
src/stage0/Init/Lean/Message.c
View file

@ -16,6 +16,7 @@ extern "C" {
lean_object* l_Lean_mkErrorStringWithPos(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MessageData_coeOfLevel(lean_object*);
lean_object* l_Lean_MessageLog_empty;
extern lean_object* l_EStateM_Result_toString___rarg___closed__2;
lean_object* l_Array_iterateMAux___main___at_Lean_MessageData_formatAux___main___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_MessageData_formatAux___main___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Message_toString___closed__2;
@ -26,7 +27,6 @@ lean_object* l_Lean_Message_Inhabited___closed__2;
lean_object* l_Lean_fmt___at_Lean_Message_toString___spec__1(lean_object*);
lean_object* l_Lean_Syntax_formatStx___main___rarg(lean_object*);
lean_object* l_Lean_MessageLog_append(lean_object*, lean_object*);
extern lean_object* l_EState_Result_toString___rarg___closed__2;
lean_object* l_List_reverse___rarg(lean_object*);
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
lean_object* l_Lean_MessageLog_toList(lean_object*);
@ -469,7 +469,7 @@ lean_object* _init_l_Lean_Message_toString___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_EState_Result_toString___rarg___closed__2;
x_1 = l_EStateM_Result_toString___rarg___closed__2;
x_2 = l_String_splitAux___main___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
@ -562,7 +562,7 @@ if (x_9 == 0)
lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
x_31 = l_Lean_Message_toString___closed__1;
x_32 = lean_string_append(x_7, x_31);
x_33 = l_EState_Result_toString___rarg___closed__2;
x_33 = l_EStateM_Result_toString___rarg___closed__2;
x_34 = lean_string_append(x_33, x_32);
lean_dec(x_32);
x_35 = lean_string_append(x_34, x_13);

21730
src/stage0/Init/Lean/MetavarContext.c
View file

File diff suppressed because it is too large Load diff

4
src/stage0/Init/Lean/Modifiers.c
View file

@ -65,11 +65,11 @@ lean_object* l_Lean_privateExt___elambda__1(lean_object*);
uint8_t lean_is_protected(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_isPrivateName___boxed(lean_object*);
lean_object* l_EState_pure___rarg(lean_object*, lean_object*);
lean_object* lean_mk_private_prefix(lean_object*);
lean_object* l_Lean_privateHeader___closed__2;
lean_object* l_Lean_mkPrivateExtension(lean_object*);
lean_object* l_Lean_mkTagDeclarationExtension(lean_object*, lean_object*);
lean_object* l_EStateM_pure___rarg(lean_object*, lean_object*);
lean_object* l_Lean_mkProtectedExtension(lean_object*);
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkPrivateExtension___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_protectedExt___elambda__4(lean_object*);
@ -508,7 +508,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(1u);
x_2 = lean_alloc_closure((void*)(l_EState_pure___rarg), 2, 1);
x_2 = lean_alloc_closure((void*)(l_EStateM_pure___rarg), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}

10
src/stage0/Init/Lean/Parser/Module.c
View file

@ -114,7 +114,6 @@ uint8_t l_Lean_Parser_isEOI(lean_object*);
lean_object* l_Lean_Parser_optionaInfo(lean_object*);
lean_object* l_Lean_Parser_testModuleParser___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Module_import___elambda__1___closed__2;
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Module_header___closed__3;
lean_object* l_Lean_Parser_Module_header___closed__5;
extern lean_object* l_Lean_Parser_Trie_HasEmptyc___closed__1;
@ -137,17 +136,18 @@ lean_object* l_Lean_Parser_nodeInfo(lean_object*, lean_object*);
lean_object* l_Lean_Message_toString(lean_object*);
lean_object* l_Lean_Parser_ModuleParserState_inhabited;
lean_object* lean_array_get_size(lean_object*);
lean_object* l_EState_pure___rarg(lean_object*, lean_object*);
lean_object* l_List_forM___main___at___private_Init_Lean_Parser_Module_4__testModuleParserAux___main___spec__5(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Module_import___elambda__1___closed__5;
lean_object* l_Lean_Parser_Module_prelude___elambda__1___rarg___closed__6;
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Module_header___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_parseCommand(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Module_import___closed__1;
lean_object* l_Lean_Parser_Module_prelude;
lean_object* l_Lean_Parser_Module_prelude___elambda__1___rarg___closed__1;
lean_object* l_Lean_Parser_Module_import___elambda__1___closed__1;
lean_object* l___private_Init_Lean_Parser_Module_2__mkEOI___closed__2;
lean_object* l_EStateM_pure___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Module_import___elambda__1___closed__7;
lean_object* l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(lean_object*);
lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
@ -2201,7 +2201,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_box(0);
x_2 = lean_alloc_closure((void*)(l_EState_pure___rarg), 2, 1);
x_2 = lean_alloc_closure((void*)(l_EStateM_pure___rarg), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
@ -2239,7 +2239,7 @@ if (x_4 == 0)
lean_object* x_16; lean_object* x_17; lean_object* x_18;
lean_dec(x_11);
x_16 = l_Lean_Parser_testModuleParser___closed__2;
x_17 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_17 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_17, 0, x_16);
lean_closure_set(x_17, 1, x_15);
x_18 = lean_io_timeit(x_7, x_17, x_5);
@ -2251,7 +2251,7 @@ else
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_alloc_closure((void*)(l_IO_println___at___private_Init_Lean_Parser_Module_4__testModuleParserAux___main___spec__1), 2, 1);
lean_closure_set(x_19, 0, x_11);
x_20 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_20 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_20, 0, x_19);
lean_closure_set(x_20, 1, x_15);
x_21 = lean_io_timeit(x_7, x_20, x_5);

10
src/stage0/Init/Lean/Parser/Parser.c
View file

@ -587,7 +587,6 @@ lean_object* l_Lean_Parser_ParserState_keepNewError(lean_object*, lean_object*);
lean_object* l_Lean_Parser_identFnAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_initCacheForInput___boxed(lean_object*);
lean_object* l_Lean_Parser_chFn___rarg(uint32_t, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_finishCommentBlock___main___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_takeWhileFn___at_Lean_Parser_octalNumberFn___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_Parser_FirstTokens_merge(lean_object*, lean_object*);
@ -737,6 +736,7 @@ lean_object* l_Lean_Parser_unicodeSymbolCheckPrecFnAux___boxed(lean_object*, lea
uint8_t l_Lean_Parser_ParserState_hasError(lean_object*);
lean_object* l_Lean_Parser_isValidSyntaxNodeKind___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_indexed(lean_object*);
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_registerBuiltinParserAttribute___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* l_Lean_Syntax_mfoldArgsAux___main___at_Lean_Syntax_foldArgs___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_chFn___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -24574,7 +24574,7 @@ lean_inc(x_11);
x_12 = lean_apply_1(x_10, x_11);
x_13 = lean_alloc_closure((void*)(l_Lean_registerPersistentEnvExtensionUnsafe___rarg___lambda__1), 3, 1);
lean_closure_set(x_13, 0, x_11);
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_Parser_mkTokenTableAttribute___spec__4(x_14, x_7);
@ -24788,7 +24788,7 @@ lean_inc(x_65);
x_66 = lean_apply_1(x_64, x_65);
x_67 = lean_alloc_closure((void*)(l_Lean_registerPersistentEnvExtensionUnsafe___rarg___lambda__1), 3, 1);
lean_closure_set(x_67, 0, x_65);
x_68 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_68 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_68, 0, x_66);
lean_closure_set(x_68, 1, x_67);
x_69 = l_Lean_registerEnvExtensionUnsafe___at_Lean_Parser_mkTokenTableAttribute___spec__4(x_68, x_61);
@ -27637,7 +27637,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_Parser_registerParserAttribute___spec__3(x_14, x_7);
@ -27846,7 +27846,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_Parser_registerParserAttribute___spec__3(x_67, x_60);

52
src/stage0/Init/Lean/ProjFns.c
View file

@ -27,12 +27,14 @@ extern lean_object* l_Lean_registerEnvExtensionUnsafe___rarg___closed__2;
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__2;
lean_object* lean_mk_array(lean_object*, lean_object*);
lean_object* l_Lean_reduceProjectionFnAux___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkProjectionFnInfoExtension___closed__4;
lean_object* l___private_Init_Lean_Expr_1__mkAppRangeAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyMAux___main___at_Lean_mkProjectionFnInfoExtension___spec__5___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Environment_5__envExtensionsRef;
lean_object* l_Lean_projectionFnInfoExt___elambda__1___boxed(lean_object*);
lean_object* l_Array_binSearchAux___main___at_Lean_Environment_getProjectionFnInfo___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_reduceProjectionFnAux___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_toArrayAux___main___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__4;
@ -42,21 +44,20 @@ lean_object* l_Lean_SimplePersistentEnvExtension_getState___rarg(lean_object*, l
extern lean_object* l_Lean_Inhabited;
lean_object* l_Lean_mkProjectionFnInfoExtension___closed__2;
lean_object* l_List_redLength___main___rarg(lean_object*);
lean_object* l_Lean_Environment_reduceProjectionFnAux___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_io_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_projectionFnInfoExt___closed__3;
lean_object* l_Lean_Environment_reduceProjectionFnAux___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getRevArg_x21___main(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppNumArgsAux___main(lean_object*, lean_object*);
lean_object* l_Lean_projectionFnInfoExt___closed__2;
lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__3(lean_object*, lean_object*);
lean_object* lean_io_initializing(lean_object*);
lean_object* l_Lean_reduceProjectionFnAux(lean_object*, lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l_Lean_projectionFnInfoExt___elambda__3___boxed(lean_object*, lean_object*);
lean_object* l_Lean_reduceProjectionFn___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_projectionFnInfoExt___elambda__4(lean_object*);
lean_object* l_Lean_Environment_reduceProjectionFn___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Environment_reduceProjectionFnAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_reduceProjectionFn___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_Lean_projectionFnInfoExt___elambda__4___rarg(lean_object*);
lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_mkProjectionFnInfoExtension___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -83,17 +84,13 @@ uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_projectionFnInfoExt___elambda__4___boxed(lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* l_Lean_mkProjectionFnInfoExtension___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Environment_reduceProjectionFn(lean_object*, lean_object*);
lean_object* l_Array_binSearchAux___main___at_Lean_Environment_getProjectionFnInfo___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___closed__1;
lean_object* l_Lean_addProjectionFnInfo___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_binSearchAux___main___at_Lean_Environment_isProjectionFn___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_projectionFnInfoExt___closed__5;
lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Environment_reduceProjectionFnAux(lean_object*, lean_object*);
lean_object* lean_add_projection_info(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_Environment_reduceProjectionFn___boxed(lean_object*, lean_object*);
lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_io_ref_get(lean_object*, lean_object*);
uint8_t l_Lean_Name_quickLt(lean_object*, lean_object*);
@ -101,10 +98,13 @@ lean_object* l_Lean_registerSimplePersistentEnvExtension___at_Lean_mkProjectionF
lean_object* lean_environment_find(lean_object*, lean_object*);
lean_object* lean_get_projection_info(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_reduceProjectionFnAux___boxed(lean_object*, lean_object*);
uint8_t l_Array_anyMAux___main___at_Lean_mkProjectionFnInfoExtension___spec__5(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_mkProjectionFnInfoExtension___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_reduceProjectionFnAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkProjectionFnInfoExtension(lean_object*);
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
extern lean_object* l_Lean_Name_toString___closed__1;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
@ -112,7 +112,6 @@ lean_object* lean_nat_div(lean_object*, lean_object*);
extern lean_object* l_Lean_mkTagDeclarationExtension___closed__2;
lean_object* l_Lean_projectionFnInfoExt;
lean_object* l_Lean_Environment_isProjectionFn___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Environment_reduceProjectionFnAux___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkProjectionFnInfoExtension___spec__6(lean_object*, lean_object*);
lean_object* l_Lean_projectionFnInfoExt___closed__4;
extern lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkTagDeclarationExtension___spec__6___closed__2;
@ -125,6 +124,7 @@ lean_object* lean_io_ref_reset(lean_object*, lean_object*);
extern lean_object* l_Lean_exprIsInhabited___closed__1;
lean_object* l_RBNode_find___main___at_Lean_Environment_getProjectionFnInfo___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_projectionFnInfoExt___elambda__1(lean_object*);
lean_object* l_Lean_reduceProjectionFn(lean_object*, lean_object*);
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* _init_l_Lean_ProjectionFunctionInfo_inhabited___closed__1() {
_start:
@ -672,7 +672,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkProjectionFnInfoExtension___spec__6(x_14, x_7);
@ -881,7 +881,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkProjectionFnInfoExtension___spec__6(x_67, x_60);
@ -1765,7 +1765,7 @@ x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_Lean_Environment_reduceProjectionFnAux___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) {
lean_object* l_Lean_reduceProjectionFnAux___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) {
_start:
{
lean_object* x_9;
@ -1834,7 +1834,7 @@ return x_29;
}
}
}
lean_object* l_Lean_Environment_reduceProjectionFnAux___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* l_Lean_reduceProjectionFnAux___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;
@ -1865,7 +1865,7 @@ x_14 = lean_ctor_get(x_1, 1);
lean_inc(x_14);
lean_dec(x_1);
x_15 = lean_apply_1(x_2, x_13);
x_16 = lean_alloc_closure((void*)(l_Lean_Environment_reduceProjectionFnAux___rarg___lambda__1___boxed), 8, 7);
x_16 = lean_alloc_closure((void*)(l_Lean_reduceProjectionFnAux___rarg___lambda__1___boxed), 8, 7);
lean_closure_set(x_16, 0, x_6);
lean_closure_set(x_16, 1, x_3);
lean_closure_set(x_16, 2, x_4);
@ -1878,19 +1878,19 @@ return x_17;
}
}
}
lean_object* l_Lean_Environment_reduceProjectionFnAux(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_reduceProjectionFnAux(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Lean_Environment_reduceProjectionFnAux___rarg), 7, 0);
x_3 = lean_alloc_closure((void*)(l_Lean_reduceProjectionFnAux___rarg), 7, 0);
return x_3;
}
}
lean_object* l_Lean_Environment_reduceProjectionFnAux___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* l_Lean_reduceProjectionFnAux___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) {
_start:
{
lean_object* x_9;
x_9 = l_Lean_Environment_reduceProjectionFnAux___rarg___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
x_9 = l_Lean_reduceProjectionFnAux___rarg___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_8);
lean_dec(x_6);
lean_dec(x_5);
@ -1899,16 +1899,16 @@ lean_dec(x_3);
return x_9;
}
}
lean_object* l_Lean_Environment_reduceProjectionFnAux___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_reduceProjectionFnAux___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Environment_reduceProjectionFnAux(x_1, x_2);
x_3 = l_Lean_reduceProjectionFnAux(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Lean_Environment_reduceProjectionFn___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* l_Lean_reduceProjectionFn___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) {
_start:
{
lean_object* x_7;
@ -1970,7 +1970,7 @@ x_22 = lean_unsigned_to_nat(1u);
x_23 = lean_nat_sub(x_19, x_22);
lean_dec(x_19);
x_24 = l___private_Init_Lean_Expr_2__getAppArgsAux___main(x_4, x_21, x_23);
x_25 = l_Lean_Environment_reduceProjectionFnAux___rarg(x_1, x_2, x_3, x_17, x_24, x_5, x_6);
x_25 = l_Lean_reduceProjectionFnAux___rarg(x_1, x_2, x_3, x_17, x_24, x_5, x_6);
return x_25;
}
}
@ -1990,19 +1990,19 @@ return x_27;
}
}
}
lean_object* l_Lean_Environment_reduceProjectionFn(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_reduceProjectionFn(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Lean_Environment_reduceProjectionFn___rarg), 6, 0);
x_3 = lean_alloc_closure((void*)(l_Lean_reduceProjectionFn___rarg), 6, 0);
return x_3;
}
}
lean_object* l_Lean_Environment_reduceProjectionFn___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_reduceProjectionFn___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Environment_reduceProjectionFn(x_1, x_2);
x_3 = l_Lean_reduceProjectionFn(x_1, x_2);
lean_dec(x_2);
return x_3;
}

6
src/stage0/Init/Lean/ReducibilityAttrs.c
View file

@ -86,7 +86,6 @@ lean_object* l_Lean_getReducibilityStatus___boxed(lean_object*, lean_object*);
lean_object* l_Lean_registerEnumAttributes___at_Lean_mkReducibilityAttrs___spec__1___closed__1;
uint8_t l_Lean_ReducibilityStatus_inhabited;
lean_object* l_Lean_registerEnumAttributes___at_Lean_mkReducibilityAttrs___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_registerTagAttribute___spec__4___closed__1;
lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkReducibilityAttrs___closed__18;
@ -99,6 +98,7 @@ lean_object* lean_array_get_size(lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_mkReducibilityAttrs___closed__9;
extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__5;
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
extern lean_object* l_Lean_Name_toString___closed__1;
lean_object* l_Lean_mkReducibilityAttrs___closed__5;
@ -678,7 +678,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkReducibilityAttrs___spec__7(x_14, x_7);
@ -887,7 +887,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_mkReducibilityAttrs___spec__7(x_67, x_60);

6
src/stage0/Init/Lean/Scopes.c
View file

@ -83,7 +83,6 @@ lean_object* l_Lean_regScopeManagerExtension___closed__3;
lean_object* l_Lean_scopeManagerExt___elambda__4___boxed(lean_object*);
lean_object* l_List_foldl___main___at_Lean_Environment_toValidNamespace___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ScopeManagerState_saveNamespace(lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_regScopeManagerExtension___closed__1;
lean_object* l_Lean_Environment_popScopeCore(lean_object*);
lean_object* l_Lean_Environment_getNamespaceSet___boxed(lean_object*);
@ -99,6 +98,7 @@ lean_object* l_Lean_Environment_registerNamespace___main(lean_object*, lean_obje
lean_object* l_Array_iterateMAux___main___at_Lean_regScopeManagerExtension___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_regScopeManagerExtension___closed__2;
lean_object* l_Array_iterateMAux___main___at_Lean_regScopeManagerExtension___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
extern lean_object* l_Lean_Name_toString___closed__1;
lean_object* l_Lean_Environment_pushScopeCore___boxed(lean_object*, lean_object*, lean_object*);
@ -579,7 +579,7 @@ x_11 = l_Array_empty___closed__1;
lean_inc(x_10);
x_12 = lean_apply_1(x_10, x_11);
x_13 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_14 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_14 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_registerEnvExtensionUnsafe___at_Lean_regScopeManagerExtension___spec__7(x_14, x_7);
@ -788,7 +788,7 @@ x_64 = l_Array_empty___closed__1;
lean_inc(x_63);
x_65 = lean_apply_1(x_63, x_64);
x_66 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
x_67 = lean_alloc_closure((void*)(l_EState_bind___rarg), 3, 2);
x_67 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_67, 0, x_65);
lean_closure_set(x_67, 1, x_66);
x_68 = l_Lean_registerEnvExtensionUnsafe___at_Lean_regScopeManagerExtension___spec__7(x_67, x_60);

886
src/stage0/Init/Lean/TmpMetavarContext.c
View file

@ -1,886 +0,0 @@
// Lean compiler output
// Module: Init.Lean.TmpMetavarContext
// Imports: Init.Lean.MetavarContext
#include "runtime/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* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__3(lean_object*, lean_object*);
uint8_t lean_name_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_TmpMetavarContext_Inhabited;
extern lean_object* l_Array_empty___closed__1;
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_array(lean_object*, lean_object*);
extern lean_object* l_Lean_exprIsInhabited;
lean_object* l_panicWithPos___at_Lean_TmpMetavarContext_isAbstractMetavarContext___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkTmpMetavarContext(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkTmpMVarId___closed__2;
extern lean_object* l_Lean_LocalContext_Inhabited___closed__1;
lean_object* l_Lean_TmpMetavarContext_Inhabited___closed__1;
lean_object* l_Lean_TmpMetavarContext_getDecl___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Name_getTmpMVarIdx___boxed(lean_object*);
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__8;
uint8_t l_Lean_Level_isTmpMVar(lean_object*);
lean_object* lean_metavar_ctx_get_expr_assignment(lean_object*, lean_object*);
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__3___boxed(lean_object*, lean_object*);
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__2___closed__1;
lean_object* l_Lean_TmpMetavarContext_getLevelAssignment(lean_object*, lean_object*);
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext;
lean_object* l_Nat_repr(lean_object*);
lean_object* l_Lean_TmpMetavarContext_assignLevel(lean_object*, lean_object*, lean_object*);
extern lean_object* l_panicWithPos___rarg___closed__3;
uint8_t l_Lean_Expr_isTmpMVar(lean_object*);
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__3;
lean_object* lean_string_append(lean_object*, lean_object*);
uint8_t l_Lean_Name_isTmpMVarId(lean_object*);
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__6;
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__2;
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__7;
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__4___boxed(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__5;
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_metavar_ctx_assign_expr(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__5___closed__1;
lean_object* l_Lean_TmpMetavarContext_getExprAssignment(lean_object*, lean_object*);
extern lean_object* l_panicWithPos___rarg___closed__1;
lean_object* l_panicWithPos___at_Lean_TmpMetavarContext_isAbstractMetavarContext___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TmpMetavarContext_getDecl(lean_object*, lean_object*);
lean_object* lean_array_set(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MetavarContext_getDecl(lean_object*, lean_object*);
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__4(lean_object*, lean_object*);
lean_object* lean_metavar_ctx_get_level_assignment(lean_object*, lean_object*);
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__1;
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Level_isTmpMVar___boxed(lean_object*);
lean_object* l_panic(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkTmpMVarId___closed__1;
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__10;
lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__4;
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__11;
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__9;
extern lean_object* l_Lean_MetavarContext_Inhabited___closed__1;
lean_object* l_Lean_Name_getTmpMVarIdx(lean_object*);
extern lean_object* l_panicWithPos___rarg___closed__2;
lean_object* l_Lean_mkTmpMVarId(lean_object*);
lean_object* l_Lean_Name_isTmpMVarId___boxed(lean_object*);
uint8_t l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Name_getTmpMVarIdx___closed__1;
lean_object* lean_metavar_ctx_assign_level(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TmpMetavarContext_assignExpr(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_getTmpMVarIdx___closed__2;
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isTmpMVar___boxed(lean_object*);
lean_object* l_panicWithPos___at_Array_findIdx_x21___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__1___boxed(lean_object*, lean_object*);
lean_object* _init_l_Lean_mkTmpMVarId___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("_tmp");
return x_1;
}
}
lean_object* _init_l_Lean_mkTmpMVarId___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_mkTmpMVarId___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_mkTmpMVarId(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_mkTmpMVarId___closed__2;
x_3 = lean_name_mk_numeral(x_2, x_1);
return x_3;
}
}
uint8_t l_Lean_Name_isTmpMVarId(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 2)
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = lean_ctor_get(x_1, 0);
x_3 = l_Lean_mkTmpMVarId___closed__2;
x_4 = lean_name_dec_eq(x_2, x_3);
if (x_4 == 0)
{
uint8_t x_5;
x_5 = 0;
return x_5;
}
else
{
uint8_t x_6;
x_6 = 1;
return x_6;
}
}
else
{
uint8_t x_7;
x_7 = 0;
return x_7;
}
}
}
lean_object* l_Lean_Name_isTmpMVarId___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Name_isTmpMVarId(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Name_getTmpMVarIdx___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Init.Lean.TmpMetavarContext");
return x_1;
}
}
lean_object* _init_l_Lean_Name_getTmpMVarIdx___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("expected a temporary metavariable name");
return x_1;
}
}
lean_object* l_Lean_Name_getTmpMVarIdx(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 2)
{
lean_object* x_2;
x_2 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
return x_2;
}
else
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = l_Lean_Name_getTmpMVarIdx___closed__1;
x_4 = lean_unsigned_to_nat(54u);
x_5 = lean_unsigned_to_nat(24u);
x_6 = l_Lean_Name_getTmpMVarIdx___closed__2;
x_7 = l_panicWithPos___at_Array_findIdx_x21___spec__1(x_3, x_4, x_5, x_6);
return x_7;
}
}
}
lean_object* l_Lean_Name_getTmpMVarIdx___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Name_getTmpMVarIdx(x_1);
lean_dec(x_1);
return x_2;
}
}
uint8_t l_Lean_Level_isTmpMVar(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 5)
{
lean_object* x_2; uint8_t x_3;
x_2 = lean_ctor_get(x_1, 0);
x_3 = l_Lean_Name_isTmpMVarId(x_2);
return x_3;
}
else
{
uint8_t x_4;
x_4 = 0;
return x_4;
}
}
}
lean_object* l_Lean_Level_isTmpMVar___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Level_isTmpMVar(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
uint8_t l_Lean_Expr_isTmpMVar(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 2)
{
lean_object* x_2; uint8_t x_3;
x_2 = lean_ctor_get(x_1, 0);
x_3 = l_Lean_Name_isTmpMVarId(x_2);
return x_3;
}
else
{
uint8_t x_4;
x_4 = 0;
return x_4;
}
}
}
lean_object* l_Lean_Expr_isTmpMVar___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Expr_isTmpMVar(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* l_Lean_mkTmpMetavarContext(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_5 = lean_box(0);
x_6 = lean_mk_array(x_4, x_5);
x_7 = lean_array_get_size(x_3);
x_8 = lean_mk_array(x_7, x_5);
x_9 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_9, 0, x_1);
lean_ctor_set(x_9, 1, x_2);
lean_ctor_set(x_9, 2, x_3);
lean_ctor_set(x_9, 3, x_6);
lean_ctor_set(x_9, 4, x_8);
return x_9;
}
}
lean_object* _init_l_Lean_TmpMetavarContext_Inhabited___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_MetavarContext_Inhabited___closed__1;
x_2 = l_Lean_LocalContext_Inhabited___closed__1;
x_3 = l_Array_empty___closed__1;
x_4 = lean_alloc_ctor(0, 5, 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);
lean_ctor_set(x_4, 3, x_3);
lean_ctor_set(x_4, 4, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_TmpMetavarContext_Inhabited() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_TmpMetavarContext_Inhabited___closed__1;
return x_1;
}
}
lean_object* l_Lean_TmpMetavarContext_getLevelAssignment(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = l_Lean_Name_isTmpMVarId(x_2);
if (x_3 == 0)
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_metavar_ctx_get_level_assignment(x_4, x_2);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_6 = lean_box(0);
x_7 = lean_ctor_get(x_1, 3);
lean_inc(x_7);
lean_dec(x_1);
x_8 = l_Lean_Name_getTmpMVarIdx(x_2);
lean_dec(x_2);
x_9 = lean_array_get(x_6, x_7, x_8);
lean_dec(x_8);
lean_dec(x_7);
return x_9;
}
}
}
lean_object* l_Lean_TmpMetavarContext_assignLevel(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
x_4 = l_Lean_Name_isTmpMVarId(x_2);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_5 = lean_ctor_get(x_1, 0);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_metavar_ctx_assign_level(x_5, x_2, x_3);
x_7 = l_Lean_LocalContext_Inhabited___closed__1;
x_8 = l_Array_empty___closed__1;
x_9 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_9, 0, x_6);
lean_ctor_set(x_9, 1, x_7);
lean_ctor_set(x_9, 2, x_8);
lean_ctor_set(x_9, 3, x_8);
lean_ctor_set(x_9, 4, x_8);
return x_9;
}
else
{
uint8_t x_10;
x_10 = !lean_is_exclusive(x_1);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_11 = lean_ctor_get(x_1, 3);
x_12 = l_Lean_Name_getTmpMVarIdx(x_2);
lean_dec(x_2);
x_13 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_13, 0, x_3);
x_14 = lean_array_set(x_11, x_12, x_13);
lean_dec(x_12);
lean_ctor_set(x_1, 3, x_14);
return x_1;
}
else
{
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; lean_object* x_23;
x_15 = lean_ctor_get(x_1, 0);
x_16 = lean_ctor_get(x_1, 1);
x_17 = lean_ctor_get(x_1, 2);
x_18 = lean_ctor_get(x_1, 3);
x_19 = lean_ctor_get(x_1, 4);
lean_inc(x_19);
lean_inc(x_18);
lean_inc(x_17);
lean_inc(x_16);
lean_inc(x_15);
lean_dec(x_1);
x_20 = l_Lean_Name_getTmpMVarIdx(x_2);
lean_dec(x_2);
x_21 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_21, 0, x_3);
x_22 = lean_array_set(x_18, x_20, x_21);
lean_dec(x_20);
x_23 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_23, 0, x_15);
lean_ctor_set(x_23, 1, x_16);
lean_ctor_set(x_23, 2, x_17);
lean_ctor_set(x_23, 3, x_22);
lean_ctor_set(x_23, 4, x_19);
return x_23;
}
}
}
}
lean_object* l_Lean_TmpMetavarContext_getExprAssignment(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = l_Lean_Name_isTmpMVarId(x_2);
if (x_3 == 0)
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_metavar_ctx_get_expr_assignment(x_4, x_2);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_6 = lean_box(0);
x_7 = lean_ctor_get(x_1, 4);
lean_inc(x_7);
lean_dec(x_1);
x_8 = l_Lean_Name_getTmpMVarIdx(x_2);
lean_dec(x_2);
x_9 = lean_array_get(x_6, x_7, x_8);
lean_dec(x_8);
lean_dec(x_7);
return x_9;
}
}
}
lean_object* l_Lean_TmpMetavarContext_assignExpr(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
x_4 = l_Lean_Name_isTmpMVarId(x_2);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_5 = lean_ctor_get(x_1, 0);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_metavar_ctx_assign_expr(x_5, x_2, x_3);
x_7 = l_Lean_LocalContext_Inhabited___closed__1;
x_8 = l_Array_empty___closed__1;
x_9 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_9, 0, x_6);
lean_ctor_set(x_9, 1, x_7);
lean_ctor_set(x_9, 2, x_8);
lean_ctor_set(x_9, 3, x_8);
lean_ctor_set(x_9, 4, x_8);
return x_9;
}
else
{
uint8_t x_10;
x_10 = !lean_is_exclusive(x_1);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_11 = lean_ctor_get(x_1, 4);
x_12 = l_Lean_Name_getTmpMVarIdx(x_2);
lean_dec(x_2);
x_13 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_13, 0, x_3);
x_14 = lean_array_set(x_11, x_12, x_13);
lean_dec(x_12);
lean_ctor_set(x_1, 4, x_14);
return x_1;
}
else
{
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; lean_object* x_23;
x_15 = lean_ctor_get(x_1, 0);
x_16 = lean_ctor_get(x_1, 1);
x_17 = lean_ctor_get(x_1, 2);
x_18 = lean_ctor_get(x_1, 3);
x_19 = lean_ctor_get(x_1, 4);
lean_inc(x_19);
lean_inc(x_18);
lean_inc(x_17);
lean_inc(x_16);
lean_inc(x_15);
lean_dec(x_1);
x_20 = l_Lean_Name_getTmpMVarIdx(x_2);
lean_dec(x_2);
x_21 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_21, 0, x_3);
x_22 = lean_array_set(x_19, x_20, x_21);
lean_dec(x_20);
x_23 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_23, 0, x_15);
lean_ctor_set(x_23, 1, x_16);
lean_ctor_set(x_23, 2, x_17);
lean_ctor_set(x_23, 3, x_18);
lean_ctor_set(x_23, 4, x_22);
return x_23;
}
}
}
}
lean_object* l_Lean_TmpMetavarContext_getDecl(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = l_Lean_Name_isTmpMVarId(x_2);
if (x_3 == 0)
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_ctor_get(x_1, 0);
x_5 = l_Lean_MetavarContext_getDecl(x_4, x_2);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12; lean_object* x_13;
x_6 = lean_ctor_get(x_1, 1);
x_7 = lean_ctor_get(x_1, 2);
x_8 = l_Lean_Name_getTmpMVarIdx(x_2);
x_9 = l_Lean_exprIsInhabited;
x_10 = lean_array_get(x_9, x_7, x_8);
lean_dec(x_8);
x_11 = lean_box(0);
x_12 = 0;
lean_inc(x_6);
x_13 = lean_alloc_ctor(0, 3, 1);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_6);
lean_ctor_set(x_13, 2, x_10);
lean_ctor_set_uint8(x_13, sizeof(void*)*3, x_12);
return x_13;
}
}
}
lean_object* l_Lean_TmpMetavarContext_getDecl___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_TmpMetavarContext_getDecl(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_panicWithPos___at_Lean_TmpMetavarContext_isAbstractMetavarContext___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
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; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_5 = l_panicWithPos___rarg___closed__1;
x_6 = lean_string_append(x_5, x_1);
x_7 = l_panicWithPos___rarg___closed__2;
x_8 = lean_string_append(x_6, x_7);
x_9 = l_Nat_repr(x_2);
x_10 = lean_string_append(x_8, x_9);
lean_dec(x_9);
x_11 = l_panicWithPos___rarg___closed__2;
x_12 = lean_string_append(x_10, x_11);
x_13 = l_Nat_repr(x_3);
x_14 = lean_string_append(x_12, x_13);
lean_dec(x_13);
x_15 = l_panicWithPos___rarg___closed__3;
x_16 = lean_string_append(x_14, x_15);
x_17 = lean_string_append(x_16, x_4);
x_18 = l_Lean_TmpMetavarContext_Inhabited;
x_19 = lean_panic_fn(x_17);
return x_19;
}
}
uint8_t l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = l_Lean_Name_isTmpMVarId(x_2);
if (x_3 == 0)
{
uint8_t x_4;
x_4 = 1;
return x_4;
}
else
{
uint8_t x_5;
x_5 = 0;
return x_5;
}
}
}
lean_object* _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__2___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("TmpMetavarContex does not support delayed assignments");
return x_1;
}
}
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___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; lean_object* x_10;
x_6 = l_Lean_Name_getTmpMVarIdx___closed__1;
x_7 = lean_unsigned_to_nat(126u);
x_8 = lean_unsigned_to_nat(43u);
x_9 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__2___closed__1;
x_10 = l_panicWithPos___at_Lean_TmpMetavarContext_isAbstractMetavarContext___spec__1(x_6, x_7, x_8, x_9);
return x_10;
}
}
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__3(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_box(0);
return x_3;
}
}
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__4(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = l_Lean_Name_getTmpMVarIdx___closed__1;
x_4 = lean_unsigned_to_nat(127u);
x_5 = lean_unsigned_to_nat(37u);
x_6 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__2___closed__1;
x_7 = l_panicWithPos___at_Lean_TmpMetavarContext_isAbstractMetavarContext___spec__1(x_3, x_4, x_5, x_6);
return x_7;
}
}
lean_object* _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__5___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("TmpMetavarContex does not support the creation of auxiliary metavariables");
return x_1;
}
}
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint8_t x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_6 = l_Lean_Name_getTmpMVarIdx___closed__1;
x_7 = lean_unsigned_to_nat(125u);
x_8 = lean_unsigned_to_nat(43u);
x_9 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__5___closed__1;
x_10 = l_panicWithPos___at_Lean_TmpMetavarContext_isAbstractMetavarContext___spec__1(x_6, x_7, x_8, x_9);
return x_10;
}
}
lean_object* _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__1___boxed), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_TmpMetavarContext_getLevelAssignment), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_TmpMetavarContext_assignLevel), 3, 0);
return x_1;
}
}
lean_object* _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_TmpMetavarContext_getExprAssignment), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_TmpMetavarContext_assignExpr), 3, 0);
return x_1;
}
}
lean_object* _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__6() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_TmpMetavarContext_getDecl___boxed), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__2___boxed), 5, 0);
return x_1;
}
}
lean_object* _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__8() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__3___boxed), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__9() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__4___boxed), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__10() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__5___boxed), 5, 0);
return x_1;
}
}
lean_object* _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__11() {
_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; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13;
x_1 = l_Lean_TmpMetavarContext_Inhabited___closed__1;
x_2 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__1;
x_3 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__2;
x_4 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__3;
x_5 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__4;
x_6 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__5;
x_7 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__6;
x_8 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__7;
x_9 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__8;
x_10 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__9;
x_11 = 0;
x_12 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__10;
x_13 = lean_alloc_ctor(0, 12, 1);
lean_ctor_set(x_13, 0, x_1);
lean_ctor_set(x_13, 1, x_2);
lean_ctor_set(x_13, 2, x_3);
lean_ctor_set(x_13, 3, x_4);
lean_ctor_set(x_13, 4, x_2);
lean_ctor_set(x_13, 5, x_5);
lean_ctor_set(x_13, 6, x_6);
lean_ctor_set(x_13, 7, x_7);
lean_ctor_set(x_13, 8, x_8);
lean_ctor_set(x_13, 9, x_9);
lean_ctor_set(x_13, 10, x_10);
lean_ctor_set(x_13, 11, x_12);
lean_ctor_set_uint8(x_13, sizeof(void*)*12, x_11);
return x_13;
}
}
lean_object* _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__11;
return x_1;
}
}
lean_object* l_panicWithPos___at_Lean_TmpMetavarContext_isAbstractMetavarContext___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_panicWithPos___at_Lean_TmpMetavarContext_isAbstractMetavarContext___spec__1(x_1, x_2, x_3, x_4);
lean_dec(x_4);
lean_dec(x_1);
return x_5;
}
}
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__1(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__2___boxed(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;
x_6 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__2(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_6;
}
}
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__3___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__3(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__4___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__4(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__5___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_5);
lean_dec(x_5);
x_7 = l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__5(x_1, x_2, x_3, x_4, x_6);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_7;
}
}
lean_object* initialize_Init_Lean_MetavarContext(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_TmpMetavarContext(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Lean_MetavarContext(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_mkTmpMVarId___closed__1 = _init_l_Lean_mkTmpMVarId___closed__1();
lean_mark_persistent(l_Lean_mkTmpMVarId___closed__1);
l_Lean_mkTmpMVarId___closed__2 = _init_l_Lean_mkTmpMVarId___closed__2();
lean_mark_persistent(l_Lean_mkTmpMVarId___closed__2);
l_Lean_Name_getTmpMVarIdx___closed__1 = _init_l_Lean_Name_getTmpMVarIdx___closed__1();
lean_mark_persistent(l_Lean_Name_getTmpMVarIdx___closed__1);
l_Lean_Name_getTmpMVarIdx___closed__2 = _init_l_Lean_Name_getTmpMVarIdx___closed__2();
lean_mark_persistent(l_Lean_Name_getTmpMVarIdx___closed__2);
l_Lean_TmpMetavarContext_Inhabited___closed__1 = _init_l_Lean_TmpMetavarContext_Inhabited___closed__1();
lean_mark_persistent(l_Lean_TmpMetavarContext_Inhabited___closed__1);
l_Lean_TmpMetavarContext_Inhabited = _init_l_Lean_TmpMetavarContext_Inhabited();
lean_mark_persistent(l_Lean_TmpMetavarContext_Inhabited);
l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__2___closed__1 = _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__2___closed__1();
lean_mark_persistent(l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__2___closed__1);
l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__5___closed__1 = _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__5___closed__1();
lean_mark_persistent(l_Lean_TmpMetavarContext_isAbstractMetavarContext___lambda__5___closed__1);
l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__1 = _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__1();
lean_mark_persistent(l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__1);
l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__2 = _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__2();
lean_mark_persistent(l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__2);
l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__3 = _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__3();
lean_mark_persistent(l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__3);
l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__4 = _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__4();
lean_mark_persistent(l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__4);
l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__5 = _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__5();
lean_mark_persistent(l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__5);
l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__6 = _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__6();
lean_mark_persistent(l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__6);
l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__7 = _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__7();
lean_mark_persistent(l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__7);
l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__8 = _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__8();
lean_mark_persistent(l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__8);
l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__9 = _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__9();
lean_mark_persistent(l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__9);
l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__10 = _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__10();
lean_mark_persistent(l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__10);
l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__11 = _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__11();
lean_mark_persistent(l_Lean_TmpMetavarContext_isAbstractMetavarContext___closed__11);
l_Lean_TmpMetavarContext_isAbstractMetavarContext = _init_l_Lean_TmpMetavarContext_isAbstractMetavarContext();
lean_mark_persistent(l_Lean_TmpMetavarContext_isAbstractMetavarContext);
return lean_mk_io_result(lean_box(0));
}
#ifdef __cplusplus
}
#endif

8
src/stage0/Init/Lean/TypeClass/Context.c
View file

@ -138,6 +138,7 @@ extern lean_object* l_PersistentArray_getAux___main___rarg___closed__1;
lean_object* l_Lean_TypeClass_Context_slowWhnfApp___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_uOccursIn___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
extern lean_object* l_panicWithPos___at___private_Init_Lean_MetavarContext_7__instantiateDelayedAux___main___spec__1___closed__1;
lean_object* lean_expr_mk_mvar(lean_object*);
lean_object* l_Lean_TypeClass_Context_eHasETmpMVar___boxed(lean_object*);
uint8_t l_Lean_Expr_isMVar(lean_object*);
@ -168,6 +169,7 @@ lean_object* l_PersistentArray_get_x21___at_Lean_TypeClass_Context_uLookupIdx___
lean_object* l_Lean_TypeClass_Context_eInfer___boxed(lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_metaPrefix;
lean_object* l_EStateM_Inhabited___rarg(lean_object*, lean_object*);
uint8_t l_Lean_TypeClass_Context_eIsMeta(lean_object*);
lean_object* l_RBNode_setBlack___rarg(lean_object*);
lean_object* l_List_foldr___main___at_Lean_TypeClass_Context_eHasTmpMVar___spec__1___boxed(lean_object*, lean_object*);
@ -186,7 +188,6 @@ lean_object* l_Lean_TypeClass_Context_eNewMeta(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_uHasTmpMVar___boxed(lean_object*);
lean_object* l_panicWithPos___at_Lean_TypeClass_Context_eUnify___main___spec__1___closed__1;
extern lean_object* l_panicWithPos___rarg___closed__2;
extern lean_object* l_panicWithPos___at_Lean_AbstractMetavarContext_InstantiateExprMVars_instantiateDelayedAux___main___spec__1___rarg___closed__1;
lean_object* l_PersistentArray_getAux___main___at_Lean_TypeClass_Context_uLookupIdx___spec__2(lean_object*, size_t, size_t);
lean_object* l_Lean_TypeClass_Context_uAssign(lean_object*, lean_object*, lean_object*);
size_t l_USize_shift__left(size_t, size_t);
@ -202,7 +203,6 @@ lean_object* l_Lean_TypeClass_Context_uOccursIn___boxed(lean_object*, lean_objec
lean_object* l_Lean_TypeClass_Context_uInstantiate(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_uUnify___main___closed__2;
uint8_t l_Lean_TypeClass_Context_eHasTmpMVar___lambda__1(lean_object*);
lean_object* l_EState_Inhabited___rarg(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eHasTmpMVar___lambda__1___boxed(lean_object*);
extern lean_object* l_Lean_exprIsInhabited___closed__1;
lean_object* lean_level_mk_max(lean_object*, lean_object*);
@ -822,7 +822,7 @@ lean_object* _init_l_panicWithPos___at_Lean_TypeClass_Context_eAssign___spec__1_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_panicWithPos___at_Lean_AbstractMetavarContext_InstantiateExprMVars_instantiateDelayedAux___main___spec__1___rarg___closed__1;
x_1 = l_panicWithPos___at___private_Init_Lean_MetavarContext_7__instantiateDelayedAux___main___spec__1___closed__1;
x_2 = l_PUnit_Inhabited;
x_3 = l_monadInhabited___rarg(x_1, x_2);
return x_3;
@ -2620,7 +2620,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_String_Inhabited;
x_2 = lean_alloc_closure((void*)(l_EState_Inhabited___rarg), 2, 1);
x_2 = lean_alloc_closure((void*)(l_EStateM_Inhabited___rarg), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}

11730
src/stage0/Init/Lean/TypeUtil.c
View file

File diff suppressed because it is too large Load diff

16
src/stage0/Init/System/IO.c
View file

@ -21,7 +21,6 @@ lean_object* l_IO_Ref_set___boxed(lean_object*, lean_object*);
lean_object* l_IO_Fs_handle_isEof___at_IO_Fs_handle_readToEnd___spec__1___boxed(lean_object*, lean_object*);
lean_object* lean_io_error_to_string(lean_object*);
lean_object* l_IO_Ref_get___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_EState_Monad(lean_object*, lean_object*);
lean_object* l_IO_Ref_swap___boxed(lean_object*, lean_object*);
lean_object* lean_io_realpath(lean_object*, lean_object*);
lean_object* l_IO_HasEval(lean_object*);
@ -120,7 +119,7 @@ lean_object* l_IO_Prim_handle_close___boxed(lean_object*, lean_object*);
lean_object* l_IO_Prim_handle_flush___boxed(lean_object*, lean_object*);
lean_object* l_IO_readTextFile(lean_object*, lean_object*);
lean_object* l_IO_println___boxed(lean_object*);
lean_object* l_EState_MonadExcept___rarg(lean_object*);
lean_object* l_EStateM_Monad(lean_object*, lean_object*);
lean_object* l_IO_Fs_handle_flush___boxed(lean_object*, lean_object*);
lean_object* l_IO_appPath___rarg___closed__1;
lean_object* lean_io_prim_handle_close(lean_object*, lean_object*);
@ -136,7 +135,6 @@ lean_object* l_IO_Fs_handle_mk___boxed(lean_object*, lean_object*);
lean_object* l_IO_mkRef___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_System_IO_1__putStr___boxed(lean_object*, lean_object*);
lean_object* l_IO_Fs_readFile___boxed(lean_object*);
lean_object* l_EState_nonBacktrackable(lean_object*);
lean_object* l_IO_Prim_fileExists___boxed(lean_object*, lean_object*);
lean_object* l_IO_Ref_get___boxed(lean_object*, lean_object*);
lean_object* l_IO_Fs_handle_getLine___at_IO_Fs_handle_readToEnd___spec__2(lean_object*, lean_object*);
@ -155,6 +153,7 @@ lean_object* l_IO_Fs_handle_getLine___rarg(lean_object*, lean_object*);
lean_object* l_IO_Prim_handle_getLine___boxed(lean_object*, lean_object*);
lean_object* l_IO_lazyPure(lean_object*);
lean_object* l_IO_Prim_Ref_set___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_EStateM_nonBacktrackable(lean_object*);
lean_object* l_IO_initializing___boxed(lean_object*);
lean_object* l_IO_appDir___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_IO_Fs_handle_close___boxed(lean_object*, lean_object*);
@ -163,6 +162,7 @@ lean_object* l_IOUnit_HasEval(lean_object*, lean_object*);
lean_object* l_EIO_Monad___closed__1;
lean_object* l_IO_Fs_handle_readToEnd___boxed(lean_object*, lean_object*);
lean_object* l_IO_Prim_Ref_reset___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_EStateM_Inhabited___rarg(lean_object*, lean_object*);
lean_object* l_IO_Fs_handle_isEof(lean_object*, lean_object*);
lean_object* l_IO_getEnv(lean_object*, lean_object*);
lean_object* l_IO_Prim_iterate___rarg(lean_object*, lean_object*, lean_object*);
@ -173,6 +173,7 @@ lean_object* l_IO_Fs_handle_readToEnd___rarg(lean_object*, lean_object*);
lean_object* l_HasRepr_HasEval(lean_object*);
lean_object* l_timeit___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_IO_isDir___rarg(lean_object*, lean_object*);
lean_object* l_EStateM_MonadExcept___rarg(lean_object*);
lean_object* l_IO_Fs_handle_isEof___boxed(lean_object*, lean_object*);
lean_object* l_IO_Prim_iterate___main(lean_object*, lean_object*);
lean_object* l_unsafeIO___rarg(lean_object*);
@ -192,14 +193,13 @@ lean_object* l_IO_println___rarg___closed__1;
lean_object* l_IO_Prim_mkRef___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_IO_lazyPure___rarg(lean_object*, lean_object*);
lean_object* l_IO_Fs_readFile(lean_object*);
lean_object* l_EState_Inhabited___rarg(lean_object*, lean_object*);
lean_object* lean_io_ref_reset(lean_object*, lean_object*);
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* _init_l_EIO_Monad___closed__1() {
_start:
{
lean_object* x_1;
x_1 = l_EState_Monad(lean_box(0), lean_box(0));
x_1 = l_EStateM_Monad(lean_box(0), lean_box(0));
return x_1;
}
}
@ -215,7 +215,7 @@ lean_object* _init_l_EIO_MonadExcept___closed__1() {
_start:
{
lean_object* x_1;
x_1 = l_EState_nonBacktrackable(lean_box(0));
x_1 = l_EStateM_nonBacktrackable(lean_box(0));
return x_1;
}
}
@ -224,7 +224,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_EIO_MonadExcept___closed__1;
x_2 = l_EState_MonadExcept___rarg(x_1);
x_2 = l_EStateM_MonadExcept___rarg(x_1);
return x_2;
}
}
@ -285,7 +285,7 @@ lean_object* l_EIO_Inhabited___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_EState_Inhabited___rarg), 2, 1);
x_2 = lean_alloc_closure((void*)(l_EStateM_Inhabited___rarg), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}