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-18 13:31:05 -08:00
parent b09fb4348d
commit cba3dabcec
60 changed files with 110 additions and 133 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/parser.cpp
View file

@ -1527,8 +1527,7 @@ struct to_pattern_fn {
buffer<expr> args;
get_app_args(e, args);
args[0] = fix_quoted_name(args[0]);
// return mk_app(mk_constant(get_lean_name_str_name()), args);
return mk_app(mk_constant(name{"Lean", "Name", "mkString"}), args);
return mk_app(mk_constant(get_lean_name_str_name()), args);
}
expr fix_quoted_names(expr const & e) {

2
stage0/library/Init/Lean/AuxRecursor.c generated
View file

@ -33,9 +33,9 @@ lean_object* l_Lean_noConfusionExt___elambda__4___boxed(lean_object*);
lean_object* l_Lean_noConfusionExt___elambda__4___rarg(lean_object*);
lean_object* l_Lean_noConfusionExt___elambda__2(lean_object*);
lean_object* l_Lean_auxRecExt___elambda__1(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_auxRecExt___elambda__3(lean_object*, lean_object*);
lean_object* l_Lean_auxRecExt___elambda__2(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_noConfusionExt___elambda__1(lean_object*);
lean_object* l_Lean_mkAuxRecursorExtension___closed__1;
lean_object* l_Lean_mkAuxRecursorExtension(lean_object*);

2
stage0/library/Init/Lean/Class.c generated
View file

@ -132,6 +132,7 @@ lean_object* l_Lean_hasOutParams___boxed(lean_object*, lean_object*);
lean_object* l_Lean_SMap_contains___at_Lean_isClass___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_SMap_empty___at_Lean_ClassState_Inhabited___spec__1___closed__1;
size_t lean_name_hash_usize(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_ClassState_addEntry___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_Lean_ClassState_switch(lean_object*);
@ -163,7 +164,6 @@ extern lean_object* l_Char_HasRepr___closed__1;
uint8_t l_Lean_SMap_contains___at_Lean_isInstance___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_addClass___closed__3;
lean_object* l_Lean_classExtension___elambda__3___boxed(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_mkClassExtension___closed__1;
lean_object* lean_nat_add(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;

2
stage0/library/Init/Lean/Compiler/ClosedTermCache.c generated
View file

@ -68,6 +68,7 @@ lean_object* l_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_objec
lean_object* l_Array_iterateMAux___main___at_Lean_mkClosedTermCacheExtension___spec__16(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyRangeMAux___main___at_Lean_mkClosedTermCacheExtension___spec__21___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkClosedTermCacheExtension___closed__5;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_insert___at_Lean_mkClosedTermCacheExtension___spec__2(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
uint8_t lean_expr_eqv(lean_object*, lean_object*);
@ -82,7 +83,6 @@ lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkClosedTermCacheExtens
lean_object* l_Lean_SMap_empty___at_Lean_mkClosedTermCacheExtension___spec__12___closed__2;
lean_object* l_HashMapImp_moveEntries___main___at_Lean_mkClosedTermCacheExtension___spec__9(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkClosedTermCacheExtension___closed__4;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_mkClosedTermCacheExtension___spec__15___boxed(lean_object*, lean_object*);
lean_object* l_AssocList_find___main___at_Lean_getClosedTermName___spec__6___boxed(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);

2
stage0/library/Init/Lean/Compiler/ConstFolding.c generated
View file

@ -126,6 +126,7 @@ lean_object* l_Lean_Compiler_foldUIntDiv___lambda__1(lean_object*, uint8_t, lean
lean_object* l_Lean_Compiler_natFoldFns___closed__7;
lean_object* l_Lean_Compiler_foldBinOp___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_foldr___main___at_Lean_Compiler_isOfNat___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_foldNatDecEq___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_natFoldFns___closed__3;
lean_object* l_Lean_Compiler_numScalarTypes___closed__8;
@ -174,7 +175,6 @@ uint8_t l_List_foldr___main___at_Lean_Compiler_isOfNat___spec__1(lean_object*, u
lean_object* l_Lean_Compiler_mkUInt32Lit(lean_object*);
lean_object* l_Lean_Compiler_foldNatDecLe(uint8_t, lean_object*, lean_object*);
lean_object* l_List_append___rarg(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_foldNatPow(uint8_t);
lean_object* l_Lean_Compiler_boolFoldFns___closed__5;
lean_object* l_Lean_Compiler_natFoldFns___closed__10;

2
stage0/library/Init/Lean/Compiler/ExportAttr.c generated
View file

@ -50,6 +50,7 @@ extern lean_object* l_Lean_AttributeImpl_inhabited___closed__4;
lean_object* l_Lean_registerTagAttribute___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_String_anyAux___main___at___private_Init_Lean_Compiler_ExportAttr_1__isValidCppId___spec__2(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkExportAttr___closed__1;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___lambda__1___boxed(lean_object*);
@ -62,7 +63,6 @@ uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___lambda__1(lean_object*);
extern lean_object* l_Lean_ParametricAttribute_Inhabited___closed__1;
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkExportAttr___spec__7(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;
lean_object* l_Lean_PersistentEnvExtension_getModuleEntries___rarg(lean_object*, lean_object*, lean_object*);

2
stage0/library/Init/Lean/Compiler/ExternAttr.c generated
View file

@ -72,6 +72,7 @@ extern lean_object* l_Lean_AttributeImpl_inhabited___closed__4;
lean_object* l_Lean_registerTagAttribute___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_String_Iterator_next(lean_object*);
lean_object* l_RBNode_find___main___at_Lean_getExternAttrData___spec__2(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
lean_object* l_Lean_ExternEntry_backend___boxed(lean_object*);
@ -97,7 +98,6 @@ extern lean_object* l_Lean_ParametricAttribute_Inhabited___closed__1;
lean_object* l_Lean_expandExternPatternAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Environment_isProjectionFn(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Compiler_ExternAttr_3__parseOptNum___main(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Compiler_ExternAttr_1__syntaxToExternEntries___main___closed__2;
lean_object* l___private_Init_Lean_Compiler_ExternAttr_2__syntaxToExternAttrData___closed__5;
lean_object* lean_nat_add(lean_object*, lean_object*);

2
stage0/library/Init/Lean/Compiler/IR/Basic.c generated
View file

@ -101,6 +101,7 @@ lean_object* l_Lean_IR_Decl_isExtern___boxed(lean_object*);
lean_object* l_Lean_IR_Arg_alphaEqv___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_RBNode_ins___main___at_Lean_IR_LocalContext_addLocal___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_LocalContext_addJP(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at_Lean_IR_mmodifyJPs___spec__1___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_AltCore_body(lean_object*);
lean_object* l_Lean_IR_AltCore_mmodifyBody___rarg(lean_object*, lean_object*, lean_object*);
@ -132,7 +133,6 @@ lean_object* l_Lean_IR_LocalContext_eraseJoinPointDecl(lean_object*, lean_object
lean_object* l_Lean_IR_Decl_name___boxed(lean_object*);
lean_object* l_Lean_IR_mkIf___closed__7;
lean_object* l_Lean_IR_LitVal_beq___boxed(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_IR_mkIf___closed__2;
lean_object* l_RBNode_appendTrees___main___rarg(lean_object*, lean_object*);
lean_object* lean_ir_mk_ret(lean_object*);

2
stage0/library/Init/Lean/Compiler/IR/Boxing.c generated
View file

@ -58,6 +58,7 @@ lean_object* l_Lean_IR_ExplicitBoxing_castArgsIfNeededAux___at_Lean_IR_ExplicitB
lean_object* l_Lean_IR_ExplicitBoxing_unboxResultIfNeeded___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_findEnvDecl_x27(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_LocalContext_addJP(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Nat_foldMAux___main___at_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_Monad___rarg(lean_object*);
lean_object* l_Lean_IR_reshape(lean_object*, lean_object*);
@ -78,7 +79,6 @@ lean_object* l_Lean_IR_ExplicitBoxing_castResultIfNeeded(lean_object*, lean_obje
lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
uint8_t l_Lean_IR_ExplicitBoxing_eqvTypes(lean_object*, lean_object*);
lean_object* l_Lean_IR_ExplicitBoxing_getVarType(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_IR_ExplicitBoxing_mkCast___closed__1;
lean_object* l_Lean_IR_ExplicitBoxing_mkBoxedVersionAux(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);

2
stage0/library/Init/Lean/Compiler/IR/CompilerM.c generated
View file

@ -93,6 +93,7 @@ lean_object* l_Lean_IR_mkDeclMapExtension(lean_object*);
lean_object* l_Lean_IR_tracePrefixOptionName;
lean_object* l_PersistentHashMap_find___at_Lean_IR_findEnvDecl___spec__2(lean_object*, lean_object*);
size_t lean_name_hash_usize(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
uint8_t l_PersistentHashMap_contains___at_Lean_IR_containsDecl___spec__3(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_IR_LogEntry_fmt___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
@ -121,7 +122,6 @@ lean_object* l_Lean_IR_mkDeclMapExtension___lambda__2(lean_object*);
lean_object* l_Lean_IR_declMapExt;
lean_object* l_Array_iterateMAux___main___at_Lean_IR_mkDeclMapExtension___spec__9(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_IR_mkDeclMapExtension___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_IR_declMapExt___elambda__2(lean_object*);
lean_object* l_Lean_IR_LogEntry_Lean_HasFormat;
lean_object* l_Lean_IR_findDecl___boxed(lean_object*, lean_object*, lean_object*);

2
stage0/library/Init/Lean/Compiler/IR/Default.c generated
View file

@ -48,6 +48,7 @@ lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___closed__2
extern lean_object* l_Lean_IR_tracePrefixOptionName;
lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___closed__28;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Compiler_IR_Default_1__compileAux___spec__5(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___closed__4;
@ -56,7 +57,6 @@ uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_IR_inferBorrow(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_Decl_elimDead(lean_object*);
extern lean_object* l_Lean_IR_declMapExt;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Array_forMAux___main___at_Lean_IR_addBoxedVersionAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___closed__19;

2
stage0/library/Init/Lean/Compiler/IR/ElimDeadBranches.c generated
View file

@ -121,6 +121,7 @@ uint8_t l_List_foldr___main___at_Lean_IR_UnreachableBranches_Value_beq___main___
uint8_t l_Lean_IR_UnreachableBranches_containsCtor___main(lean_object*, lean_object*);
lean_object* l_Lean_IR_UnreachableBranches_elimDead___boxed(lean_object*, lean_object*);
size_t lean_name_hash_usize(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_AssocList_contains___main___at_Lean_IR_UnreachableBranches_mkFunctionSummariesExtension___spec__7___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_Lean_IR_UnreachableBranches_updateVarAssignment___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -157,7 +158,6 @@ lean_object* l_AssocList_replace___main___at_Lean_IR_UnreachableBranches_mkFunct
lean_object* l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__1;
lean_object* l_PersistentArray_modify___at_Lean_IR_UnreachableBranches_updateCurrFnSummary___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_getPrefix(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_mkHashMap___at_Lean_IR_UnreachableBranches_mkFunctionSummariesExtension___spec__13(lean_object*);
lean_object* l_AssocList_find___main___at_Lean_IR_UnreachableBranches_findVarValue___spec__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_IR_UnreachableBranches_functionSummariesExt___closed__4;

2
stage0/library/Init/Lean/Compiler/IR/EmitC.c generated
View file

@ -217,6 +217,7 @@ lean_object* l_Lean_IR_mkVarJPMaps(lean_object*);
lean_object* l_Lean_IR_EmitC_emitNumLit___closed__1;
lean_object* l_Lean_IR_EmitC_toStringArgs___boxed(lean_object*);
lean_object* l_Lean_IR_EmitC_emitInitFn(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Nat_forMAux___main___at_Lean_IR_EmitC_emitTailCall___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_AltCore_body(lean_object*);
lean_object* l_Lean_IR_EmitC_emitMainFn(lean_object*, lean_object*);
@ -284,7 +285,6 @@ lean_object* l_Lean_IR_EmitC_emitArg(lean_object*, lean_object*, lean_object*);
lean_object* l_List_foldl___main___at_Lean_IR_EmitC_emitFnDecls___spec__1___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_IR_declMapExt;
lean_object* l_Lean_IR_EmitC_emitCtorScalarSize___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitMainFn___closed__29;
lean_object* l_Lean_IR_EmitC_emitMainFn___closed__39;
extern lean_object* l_Char_quoteCore___closed__5;

2
stage0/library/Init/Lean/Compiler/IR/UnboxResult.c generated
View file

@ -23,8 +23,8 @@ lean_object* l_Lean_IR_UnboxResult_mkUnboxAttr___lambda__1___closed__5;
lean_object* l_Lean_IR_UnboxResult_mkUnboxAttr___lambda__1___closed__7;
lean_object* l_Lean_IR_UnboxResult_mkUnboxAttr___lambda__1___closed__6;
lean_object* l_Lean_registerTagAttribute(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_UnboxResult_mkUnboxAttr(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_IR_UnboxResult_mkUnboxAttr(lean_object*);
lean_object* l_Lean_IR_UnboxResult_mkUnboxAttr___closed__2;
lean_object* l_Lean_IR_UnboxResult_mkUnboxAttr___lambda__1___closed__4;
uint8_t l_Lean_TagAttribute_hasTag(lean_object*, lean_object*, lean_object*);

2
stage0/library/Init/Lean/Compiler/ImplementedByAttr.c generated
View file

@ -45,6 +45,7 @@ lean_object* l_Lean_registerTagAttribute___lambda__5___boxed(lean_object*, lean_
lean_object* l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1___lambda__1___boxed(lean_object*);
lean_object* l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1___lambda__1(lean_object*);
lean_object* l_Lean_Compiler_mkImplementedByAttr___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
uint8_t lean_expr_eqv(lean_object*, lean_object*);
lean_object* l_Array_binSearchAux___main___at_Lean_Compiler_getImplementedBy___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
@ -58,7 +59,6 @@ uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_mkImplementedByAttr___lambda__1___closed__1;
extern lean_object* l_Char_HasRepr___closed__1;
extern lean_object* l_Lean_ParametricAttribute_Inhabited___closed__1;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_mkImplementedByAttr___closed__3;
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_mkImplementedByAttr___lambda__2(lean_object*, lean_object*, lean_object*);

2
stage0/library/Init/Lean/Compiler/InitAttr.c generated
View file

@ -58,6 +58,7 @@ lean_object* l_Lean_initAttr;
lean_object* l_RBNode_fold___main___at_Lean_mkInitAttr___spec__2(lean_object*, lean_object*);
uint8_t l_Lean_hasInitAttr(lean_object*, lean_object*);
lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_mkInitAttr___spec__5(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
uint8_t lean_expr_eqv(lean_object*, lean_object*);
lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
@ -69,7 +70,6 @@ extern lean_object* l_Lean_registerParametricAttribute___rarg___closed__2;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
extern lean_object* l_Char_HasRepr___closed__1;
extern lean_object* l_Lean_ParametricAttribute_Inhabited___closed__1;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_mkInitAttr___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;

2
stage0/library/Init/Lean/Compiler/InlineAttrs.c generated
View file

@ -63,6 +63,7 @@ lean_object* l_Lean_Compiler_mkInlineAttrs___lambda__1(lean_object*, lean_object
lean_object* l_Lean_Compiler_mkInlineAttrs___closed__17;
lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_Compiler_mkInlineAttrs___spec__4___closed__1;
lean_object* l_List_forM___main___at_Lean_registerEnumAttributes___spec__11(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Environment_getModuleIdxFor(lean_object*, lean_object*);
@ -83,7 +84,6 @@ lean_object* l_Lean_Compiler_mkInlineAttrs___closed__2;
lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_getPrefix(lean_object*);
lean_object* l_Lean_Compiler_mkInlineAttrs(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_mkInlineAttrs___closed__4;
lean_object* lean_nat_add(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;

2
stage0/library/Init/Lean/Compiler/NeverExtractAttr.c generated
View file

@ -17,9 +17,9 @@ lean_object* l_Lean_neverExtractAttr;
extern lean_object* l_Lean_TagAttribute_Inhabited___closed__3;
lean_object* l_Lean_hasNeverExtractAttribute___boxed(lean_object*, lean_object*);
lean_object* l_Lean_registerTagAttribute(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_mkNeverExtractAttr___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Name_getPrefix(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_mkNeverExtractAttr___closed__2;
lean_object* l___private_Init_Lean_Compiler_NeverExtractAttr_1__hasNeverExtractAttributeAux___boxed(lean_object*, lean_object*);
uint8_t l_Lean_TagAttribute_hasTag(lean_object*, lean_object*, lean_object*);

2
stage0/library/Init/Lean/Compiler/Specialize.c generated
View file

@ -110,6 +110,7 @@ lean_object* l_List_forM___main___at_Lean_registerEnumAttributes___spec__11(lean
lean_object* l_Lean_Compiler_specExtension;
lean_object* l_Lean_Compiler_specExtension___closed__1;
size_t lean_name_hash_usize(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_SMap_insert___at_Lean_Compiler_SpecState_addEntry___spec__12(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_Array_iterateMAux___main___at_Lean_Compiler_mkSpecExtension___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
@ -142,7 +143,6 @@ lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Compiler_mkSpecExtension___spec__7___closed__2;
lean_object* l_Lean_SMap_insert___at_Lean_Compiler_SpecState_addEntry___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_Compiler_mkSpecializeAttrs___spec__5(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_registerSimplePersistentEnvExtension___at_Lean_Compiler_mkSpecExtension___spec__4(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;

2
stage0/library/Init/Lean/Compiler/Util.c generated
View file

@ -32,12 +32,12 @@ lean_object* l_Lean_Compiler_mkLcProof(lean_object*);
lean_object* l_Lean_Compiler_objectType___closed__3;
lean_object* l_Nat_repr(lean_object*);
lean_object* l_Lean_Compiler_neutralExpr___closed__1;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_objectType;
lean_object* l_Lean_Compiler_neutralExpr___closed__3;
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_atMostOnce___closed__1;
lean_object* l_Lean_Compiler_objectType___closed__2;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_atMostOnce_visit___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_atMostOnce___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_objectType___closed__1;

2
stage0/library/Init/Lean/Elaborator/Alias.c generated
View file

@ -73,6 +73,7 @@ lean_object* l_Lean_aliasExtension___elambda__4___boxed(lean_object*);
lean_object* l_Lean_aliasExtension___closed__6;
lean_object* l_Lean_addAlias(lean_object*, lean_object*, lean_object*);
size_t lean_name_hash_usize(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_findAux___main___at_Lean_addAliasEntry___spec__3(lean_object*, size_t, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_Array_iterateMAux___main___at_Lean_mkAliasExtension___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -88,7 +89,6 @@ lean_object* l_HashMapImp_find___at_Lean_addAliasEntry___spec__5(lean_object*, l
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_SMap_find___at_Lean_addAliasEntry___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_aliasExtension___closed__1;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_HashMapImp_moveEntries___main___at_Lean_addAliasEntry___spec__15(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;

4
stage0/library/Init/Lean/Elaborator/Basic.c generated
View file

@ -27,6 +27,7 @@ lean_object* l_Lean_Elab_withInPattern___rarg(lean_object*, lean_object*, lean_o
lean_object* l_Lean_Elab_toBaseDir(lean_object*, lean_object*);
extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__4;
lean_object* l_Lean_attrParamSyntaxToIdentifier(lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_AssocList_replace___main___at_Lean_addBuiltinTermElab___spec__16(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Name_beq___main(lean_object*, lean_object*);
lean_object* l_Lean_ElabScope_Inhabited;
@ -201,6 +202,7 @@ extern lean_object* l_Lean_NameGenerator_Inhabited___closed__3;
lean_object* l_Lean_Elab_getNamespace(lean_object*);
lean_object* l_Lean_Elab_logErrorAt___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_name_hash_usize(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkLocalDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_Lean_Elab_modifyScope___at_Lean_Elab_mkAnonymousInstName___spec__1___rarg(lean_object*);
@ -248,7 +250,6 @@ lean_object* l_System_FilePath_dirName(lean_object*);
lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
lean_object* l_Lean_SMap_empty___at_Lean_mkBuiltinCommandElabTable___spec__1;
lean_object* l_Lean_Elab_getUniverses___rarg(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Elab_resolveNamespaceUsingScopes___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkMessage(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_nameToExprAux___main(lean_object*);
@ -341,7 +342,6 @@ lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkTermElabAttribute___s
size_t lean_usize_modn(size_t, lean_object*);
lean_object* l_Lean_ParametricAttribute_setParam___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerBuiltinTermElabAttr___lambda__1___closed__3;
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_Lean_ConstantInfo_type(lean_object*);
lean_object* lean_environment_find(lean_object*, lean_object*);
lean_object* l_Lean_Elab_getElabContext(lean_object*, lean_object*);

2
stage0/library/Init/Lean/Elaborator/Command.c generated
View file

@ -118,6 +118,7 @@ lean_object* l_Lean_Elab_elabOpenRenaming(lean_object*, lean_object*, lean_objec
extern lean_object* l_Lean_Parser_Command_mixfix___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__2;
lean_object* l_Lean_addAlias(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Command_universes___elambda__1___closed__2;
lean_object* l_Lean_Elab_elabVariable___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_elabOpen___closed__1;
@ -141,7 +142,6 @@ lean_object* l_Lean_Elab_elabExport(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Command_resolve__name___elambda__1___rarg___closed__2;
extern lean_object* l_Lean_Parser_Command_notation___elambda__1___closed__2;
lean_object* l_Lean_Elab_getUniverses___rarg(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
extern lean_object* l_String_Iterator_HasRepr___closed__2;
extern lean_object* l_Lean_Parser_Command_open___elambda__1___closed__2;

2
stage0/library/Init/Lean/Elaborator/ElabStrategyAttrs.c generated
View file

@ -59,6 +59,7 @@ lean_object* l_Lean_registerTagAttribute___lambda__5___boxed(lean_object*, lean_
extern lean_object* l_Lean_EnumAttributes_Inhabited___closed__1;
lean_object* l_Lean_mkElaboratorStrategyAttrs___closed__15;
lean_object* l_List_forM___main___at_Lean_registerEnumAttributes___spec__11(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_mkElaboratorStrategyAttrs___spec__4___closed__1;
@ -71,7 +72,6 @@ lean_object* l_Lean_mkElaboratorStrategyAttrs___closed__17;
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkElaboratorStrategyAttrs___spec__7(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_mkElaboratorStrategyAttrs___lambda__1___closed__1;
lean_object* l_Lean_mkElaboratorStrategyAttrs(lean_object*);
lean_object* l_List_map___main___at_Lean_mkElaboratorStrategyAttrs___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*);

2
stage0/library/Init/Lean/Elaborator/PreTerm.c generated
View file

@ -124,6 +124,7 @@ lean_object* l_Lean_registerBuiltinPreTermElabAttr(lean_object*);
lean_object* l_Lean_Elab_convertSort(lean_object*, lean_object*);
lean_object* l_Lean_mkAsPattern(lean_object*, lean_object*);
size_t lean_name_hash_usize(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Elab_toPreTerm___closed__1;
lean_object* l___private_Init_Lean_Elaborator_PreTerm_1__setPos___closed__3;
lean_object* l_Lean_Elab_localContext___rarg(lean_object*);
@ -157,7 +158,6 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_convertType___closed__4;
lean_object* l_Lean_Syntax_getId___rarg(lean_object*);
lean_object* l_Lean_mkFVar(lean_object*);
lean_object* l_Lean_Elab_getUniverses___rarg(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elaborator_PreTerm_5__processBinders(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerBuiltinPreTermElabAttr___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_convertProp(lean_object*);

2
stage0/library/Init/Lean/Elaborator/Term.c generated
View file

@ -42,6 +42,7 @@ lean_object* l_Lean_Elab_mkExplicitBinder___rarg___closed__3;
lean_object* l_Lean_Elab_elabListLit___closed__4;
lean_object* l___regBuiltinTermElab_Lean_Elab_elabListLit(lean_object*);
size_t lean_name_hash_usize(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_elabTermAux___main___closed__1;
lean_object* l___regBuiltinTermElab_Lean_Elab_elabArrow___closed__1;
@ -58,7 +59,6 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_elabArrow(lean_object*);
lean_object* l_AssocList_find___main___at_Lean_Elab_elabTermAux___main___spec__6___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_elabListLit___closed__3;
lean_object* l_Array_umapMAux___main___at_Lean_Elab_elabTermAux___main___spec__7(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Elab_elabListLit___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_nullKind;

2
stage0/library/Init/Lean/Environment.c generated
View file

@ -195,6 +195,7 @@ lean_object* l_Lean_CPPExtensionState_inhabited;
lean_object* l_Lean_Environment_displayStats___closed__1;
lean_object* l_Lean_Environment_displayStats___closed__2;
size_t lean_name_hash_usize(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_readModuleData___boxed(lean_object*, lean_object*);
lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_PersistentHashMap_foldlM___at_Lean_mkModuleData___spec__2___boxed(lean_object*, lean_object*);
@ -250,7 +251,6 @@ lean_object* l_Lean_Environment_Inhabited___closed__3;
lean_object* l_Lean_SimplePersistentEnvExtension_getEntries(lean_object*, lean_object*);
lean_object* l_Lean_SimplePersistentEnvExtension_getState___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_namespacesExt___closed__4;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Environment_3__getTrustLevel___boxed(lean_object*);
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_regModListExtension___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg(lean_object*, lean_object*, lean_object*);

2
stage0/library/Init/Lean/EqnCompiler/MatchPattern.c generated
View file

@ -21,9 +21,9 @@ lean_object* l_Lean_EqnCompiler_mkMatchPatternAttr(lean_object*);
lean_object* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___closed__1;
lean_object* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_registerTagAttribute(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_EqnCompiler_hasMatchPatternAttribute___boxed(lean_object*, lean_object*);
lean_object* l_Lean_EqnCompiler_mkMatchPatternAttr___closed__4;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
uint8_t l_Lean_TagAttribute_hasTag(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_EqnCompiler_mkMatchPatternAttr___closed__1;
lean_object* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1(lean_object*, lean_object*);

2
stage0/library/Init/Lean/Expr.c generated
View file

@ -189,6 +189,7 @@ uint8_t l_Lean_BinderInfo_isAuxDecl(uint8_t);
lean_object* l___private_Init_Lean_Expr_6__mkAppRevRangeAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isMData___boxed(lean_object*);
size_t lean_name_hash_usize(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateForall_x21___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_Hashable___closed__1;
uint8_t lean_expr_eqv(lean_object*, lean_object*);
@ -245,7 +246,6 @@ lean_object* l_Lean_Literal_inhabited___closed__1;
lean_object* l_Lean_mkDecIsFalse(lean_object*, lean_object*);
lean_object* l_Lean_mkFVar(lean_object*);
lean_object* l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__2;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_ExprStructEq_beq___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Expr_8__etaExpandedBody___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_HasRepr;

2
stage0/library/Init/Lean/Format.c generated
View file

@ -86,6 +86,7 @@ lean_object* l_Lean_Format_getUnicode___closed__1;
lean_object* l_Lean_Format_joinArraySep(lean_object*);
lean_object* l_Lean_toStringToFormat___rarg___closed__1;
lean_object* l_Lean_fmt___at_Lean_arrayHasFormat___spec__1___rarg(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_uint64HasFormat(uint64_t);
lean_object* l_Lean_toStringToFormat___rarg___lambda__1(lean_object*);
lean_object* l_Lean_Format_repr___main___closed__17;
@ -115,7 +116,6 @@ lean_object* l_Lean_arrayHasFormat___rarg(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Format_joinArraySep___spec__1(lean_object*);
lean_object* l_Lean_formatEntry(lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Format_joinArraySep___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_natHasFormat(lean_object*);
lean_object* l_Lean_Format_repr___main___closed__19;
lean_object* l_Int_repr(lean_object*);

2
stage0/library/Init/Lean/Meta/Basic.c generated
View file

@ -25,6 +25,7 @@ lean_object* l_Lean_Meta_mkFreshLevelMVarId___boxed(lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getEnv___boxed(lean_object*);
lean_object* l_Lean_Meta_usingAtLeastTransparency___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___main___at_Lean_Meta_forallTelescope___spec__1(lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_resettingTypeClassCache___rarg(lean_object*, lean_object*, lean_object*);
@ -158,7 +159,6 @@ lean_object* l_Lean_Meta_throwBug(lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_8__forallTelescopeReducingAux(lean_object*);
lean_object* l_Lean_Meta_usingTransparency___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkForall(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_Lean_Meta_getExprMVarAssignment___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_environment_find(lean_object*, lean_object*);
size_t lean_usize_mix_hash(size_t, size_t);

2
stage0/library/Init/Lean/Meta/Default.c generated
View file

@ -112,6 +112,7 @@ lean_object* l_Nat_foldMAux___main___at_Lean_Meta_getFunInfo___spec__2___boxed(l
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_getFunInfo___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_reduceRec___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___main___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__37(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Meta_isClassExpensive___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__34(lean_object*, lean_object*, lean_object*);
uint8_t lean_expr_eqv(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_WHNF_9__deltaBetaDefinition___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__23(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -140,7 +141,6 @@ lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_isProp___sp
lean_object* l_Lean_mkFVar(lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___main___at_Lean_Meta_isProp___spec__9(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_reduceRec___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Meta_getConstAux(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* lean_instantiate_value_lparams(lean_object*, lean_object*);
uint8_t l_Lean_LocalDecl_binderInfo(lean_object*);

4
stage0/library/Init/Lean/Meta/ExprDefEq.c generated
View file

@ -19,6 +19,7 @@ lean_object* l_Array_anyRangeMAux___main___at_Lean_Meta_CheckAssignment_checkFVa
lean_object* l___private_Init_Lean_Meta_ExprDefEq_8__checkAssignmentFailure___closed__12;
uint8_t l_Lean_Expr_hasFVar(lean_object*);
lean_object* l___private_Init_Lean_Meta_ExprDefEq_4__isDefEqArgs___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
uint8_t l_Lean_Name_beq___main(lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_checkMVar(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_ExprDefEq_14__processAssignmentAux___main___closed__4;
@ -87,6 +88,7 @@ lean_object* l_Lean_Meta_isDefEqBindingDomain(lean_object*, lean_object*, lean_o
lean_object* l___private_Init_Lean_Meta_ExprDefEq_3__isDefEqArgsAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_AssocList_find___main___at_Lean_Meta_CheckAssignment_findCached___spec__2(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_ExprDefEq_8__checkAssignmentFailure___closed__6;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
uint8_t lean_expr_eqv(lean_object*, lean_object*);
uint8_t l_Array_anyRangeMAux___main___at_Lean_Meta_checkAssignment___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkLambda(lean_object*, lean_object*, lean_object*, lean_object*);
@ -114,7 +116,6 @@ lean_object* l_Lean_mkFVar(lean_object*);
lean_object* l___private_Init_Lean_Meta_ExprDefEq_8__checkAssignmentFailure___closed__21;
lean_object* l_Lean_Meta_CheckAssignment_getMCtx___boxed(lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_check___main(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_ExprDefEq_3__isDefEqArgsAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isEtaUnassignedMVar___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
@ -169,7 +170,6 @@ lean_object* l___private_Init_Lean_Expr_3__getAppArgsAux___main(lean_object*, le
lean_object* l___private_Init_Lean_Meta_ExprDefEq_2__isDefEqArgsFirstPass___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_usize_modn(size_t, lean_object*);
lean_object* l_Lean_LocalDecl_value_x3f(lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_13__restore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_checkFVar(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_ExprDefEq_5__isDefEqBindingAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

2
stage0/library/Init/Lean/Meta/LevelDefEq.c generated
View file

@ -45,6 +45,7 @@ lean_object* l___private_Init_Lean_Meta_LevelDefEq_7__isLevelDefEqAux___boxed(le
lean_object* l___private_Init_Lean_Meta_LevelDefEq_7__isLevelDefEqAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_repr(lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_6__getLevelConstraintKind___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_12__processPostponed___closed__2;
extern lean_object* l_PersistentArray_empty___closed__3;
lean_object* l___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep(lean_object*, lean_object*);
@ -60,7 +61,6 @@ uint8_t l_Lean_Level_isSucc(lean_object*);
lean_object* l_Lean_Level_dec___main(lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_7__isLevelDefEqAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentArray_foldlM___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_4__solveSelfMax___rarg(lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Lean_Meta_LevelDefEq_1__strictOccursMaxAux(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);

2
stage0/library/Init/Lean/MetavarContext.c generated
View file

@ -34,6 +34,7 @@ lean_object* l___private_Init_Lean_MetavarContext_5__instantiateDelayedAux___mai
lean_object* l___private_Init_Lean_MetavarContext_10__dep___main___at___private_Init_Lean_MetavarContext_13__collectDeps___spec__27___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MetavarContext_MkBinding_Exception_hasToString___closed__1;
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_MetavarContext_13__collectDeps___spec__46(lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
uint8_t l_Lean_Name_beq___main(lean_object*, lean_object*);
lean_object* l_Nat_foldRevMAux___main___at_Lean_MetavarContext_mkBinding___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentHashMap_findAux___main___at_Lean_MetavarContext_getLevelAssignment___spec__2(lean_object*, size_t, lean_object*);
@ -360,7 +361,6 @@ size_t lean_usize_modn(size_t, lean_object*);
lean_object* l_Lean_MetavarContext_Inhabited;
lean_object* l_Lean_MetavarContext_mkBinding(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentArray_foldlMAux___main___at___private_Init_Lean_MetavarContext_13__collectDeps___spec__42(lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_PersistentArray_foldlFromM___at___private_Init_Lean_MetavarContext_13__collectDeps___spec__40(lean_object*);
lean_object* l_Array_umapMAux___main___at_Lean_MetavarContext_MkBinding_Exception_toString___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_MetavarContext_13__collectDeps___spec__45___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

4
stage0/library/Init/Lean/Modifiers.c generated
View file

@ -15,6 +15,7 @@ extern "C" {
#endif
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_namespacesExt___closed__1;
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
uint8_t l_Lean_Name_beq___main(lean_object*, lean_object*);
lean_object* lean_environment_main_module(lean_object*);
extern lean_object* l_Array_empty___closed__1;
@ -40,13 +41,13 @@ lean_object* lean_io_initializing(lean_object*);
lean_object* l_Lean_protectedExt___elambda__1(lean_object*);
lean_object* l_Lean_mkPrivateExtension___closed__1;
lean_object* l_Lean_protectedExt___closed__3;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_protectedExt___closed__5;
lean_object* l_Lean_mkProtectedExtension___closed__1;
lean_object* l_Lean_protectedExt___closed__2;
lean_object* l_Lean_privateExt___closed__1;
lean_object* l___private_Init_Lean_Modifiers_2__privatePrefixAux(lean_object*);
uint8_t l_Lean_isPrivateName___main(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_protectedExt;
lean_object* l_Lean_privateHeader;
lean_object* lean_nat_add(lean_object*, lean_object*);
@ -60,7 +61,6 @@ lean_object* l_Lean_protectedExt___elambda__3(lean_object*, lean_object*);
lean_object* lean_mk_private_name(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*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
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*);

49
stage0/library/Init/Lean/Name.c generated
View file

@ -13,6 +13,7 @@
#ifdef __cplusplus
extern "C" {
#endif
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
uint8_t l_Lean_Name_beq___main(lean_object*, lean_object*);
lean_object* l_Lean_Name_HasToString;
lean_object* l_Lean_Name_toStringWithSep___main___closed__1;
@ -24,7 +25,6 @@ lean_object* l_RBNode_find___main___at_Lean_NameMap_find___spec__1(lean_object*)
lean_object* l_Lean_Name_quickLtAux___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Name_Hashable;
lean_object* l_Lean_stringToName;
lean_object* l_Lean_Name_mkNumeral___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Name_isPrefixOf___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Name_hasLtQuick;
lean_object* l_Lean_Name_replacePrefix___boxed(lean_object*, lean_object*, lean_object*);
@ -41,10 +41,8 @@ lean_object* l_Lean_Inhabited;
uint8_t l_Lean_Name_isPrefixOf(lean_object*, lean_object*);
lean_object* l_Lean_Name_quickLt___boxed(lean_object*, lean_object*);
uint8_t l_Lean_Name_isAtomic(lean_object*);
lean_object* l_Lean_mkSimpleName(lean_object*);
lean_object* l_Lean_Name_getNumParts___boxed(lean_object*);
lean_object* l_Lean_NameMap_find___rarg(lean_object*, lean_object*);
lean_object* l_Lean_mkStrName(lean_object*, lean_object*);
uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*);
lean_object* l_Nat_repr(lean_object*);
lean_object* l_Lean_mkNameStr(lean_object*, lean_object*);
@ -52,6 +50,7 @@ lean_object* l_Lean_Name_append(lean_object*, lean_object*);
lean_object* l_RBNode_insert___at_Lean_NameSet_insert___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkNameNum(lean_object*, lean_object*);
size_t lean_name_hash_usize(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Name_HasAppend___closed__1;
lean_object* l_Lean_Name_DecidableRel___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Name_append___main___boxed(lean_object*, lean_object*);
@ -68,7 +67,7 @@ lean_object* l_Lean_NameSet_contains___boxed(lean_object*, lean_object*);
lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_getPrefix(lean_object*);
lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Name_mkString(lean_object*, lean_object*);
lean_object* l_Lean_mkNameSet;
lean_object* lean_nat_add(lean_object*, lean_object*);
uint8_t l_Lean_NameMap_contains___rarg(lean_object*, lean_object*);
@ -103,8 +102,8 @@ lean_object* l_RBNode_find___main___at_Lean_NameMap_find___spec__1___rarg(lean_o
uint8_t l_Lean_Name_lt(lean_object*, lean_object*);
lean_object* l_Lean_Name_isAtomic___boxed(lean_object*);
uint8_t l_Lean_Name_quickLt(lean_object*, lean_object*);
lean_object* l_Lean_Name_num___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Name_appendAfter(lean_object*, lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_RBNode_ins___main___at_Lean_NameMap_insert___spec__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_String_toName(lean_object*);
lean_object* l_Lean_Name_beq___main___boxed(lean_object*, lean_object*);
@ -123,10 +122,10 @@ lean_object* l_Lean_Name_replacePrefix(lean_object*, lean_object*, lean_object*)
lean_object* l_String_splitOn(lean_object*, lean_object*);
uint8_t l_Lean_Name_isPrefixOf___main(lean_object*, lean_object*);
lean_object* l_List_foldl___main___at_String_toName___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkNameSimple(lean_object*);
lean_object* l_Lean_Name_lt___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Name_replacePrefix___main___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_HasAppend;
lean_object* l_Lean_Name_mkString___boxed(lean_object*, lean_object*);
lean_object* l_Lean_NameSet_insert(lean_object*, lean_object*);
lean_object* l_RBNode_find___main___at_Lean_NameMap_contains___spec__1___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Name_quickLtAux___main___boxed(lean_object*, lean_object*);
@ -135,7 +134,6 @@ lean_object* l_Lean_NameMap_contains___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1(lean_object*);
lean_object* l_Lean_Name_toStringWithSep___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkNumName(lean_object*, lean_object*);
lean_object* l_Lean_Name_HasToString___closed__1;
uint8_t l_Lean_Name_isInternal(lean_object*);
lean_object* l_Lean_Name_toString(lean_object*);
@ -143,7 +141,8 @@ lean_object* l_RBNode_ins___main___at_Lean_NameSet_insert___spec__2(lean_object*
lean_object* l_RBNode_ins___main___at_Lean_NameMap_insert___spec__3___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_NameSet_HasEmptyc;
lean_object* l_Lean_NameMap_find___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Name_mkString___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_Name_str___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Name_str___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
@ -151,7 +150,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Name_mkNumeral___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_Name_num___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
@ -159,6 +158,14 @@ x_3 = lean_name_mk_numeral(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Name_mkString(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Inhabited() {
_start:
{
@ -167,7 +174,7 @@ x_1 = lean_box(0);
return x_1;
}
}
lean_object* l_Lean_mkStrName(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_mkNameStr(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
@ -175,7 +182,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_mkNumName(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_mkNameNum(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
@ -183,7 +190,7 @@ x_3 = lean_name_mk_numeral(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_mkSimpleName(lean_object* x_1) {
lean_object* l_Lean_mkNameSimple(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -196,7 +203,7 @@ lean_object* _init_l_Lean_stringToName___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_mkSimpleName), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_mkNameSimple), 1, 0);
return x_1;
}
}
@ -9039,22 +9046,6 @@ x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_Lean_mkNameStr(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_mkNameNum(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_name_mk_numeral(x_1, x_2);
return x_3;
}
}
lean_object* l_List_foldl___main___at_String_toName___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{

4
stage0/library/Init/Lean/NameGenerator.c generated
View file

@ -13,15 +13,15 @@
#ifdef __cplusplus
extern "C" {
#endif
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_Lean_NameGenerator_mkChild(lean_object*);
lean_object* l_Lean_NameGenerator_Inhabited___closed__1;
lean_object* l_Lean_NameGenerator_next(lean_object*);
lean_object* l_Lean_NameGenerator_Inhabited___closed__3;
lean_object* l_Lean_NameGenerator_Inhabited___closed__2;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_NameGenerator_Inhabited___closed__2;
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_NameGenerator_curr(lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_Lean_NameGenerator_Inhabited;
lean_object* _init_l_Lean_NameGenerator_Inhabited___closed__1() {
_start:

2
stage0/library/Init/Lean/Options.c generated
View file

@ -30,13 +30,13 @@ extern lean_object* l_Bool_HasRepr___closed__2;
lean_object* l_Lean_setOptionFromString___closed__1;
lean_object* l_RBNode_find___main___at_Lean_getOptionDecl___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_KVMap_setInt(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Options_1__initOptionDeclsRef(lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_KVMap_setName(lean_object*, lean_object*, lean_object*);
lean_object* l_RBNode_find___main___at_Lean_getOptionDecl___spec__1___boxed(lean_object*, lean_object*);
extern lean_object* l_Char_HasRepr___closed__1;
lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_registerOption(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_NameMap_contains___rarg(lean_object*, lean_object*);
lean_object* l_Lean_setOptionFromString___closed__4;

2
stage0/library/Init/Lean/Parser/Command.c generated
View file

@ -481,6 +481,7 @@ lean_object* l_Lean_Parser_Command_protected___closed__3;
lean_object* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__6;
lean_object* l_Lean_Parser_Command_partial___closed__4;
lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_mixfixKind___elambda__1___boxed(lean_object*);
lean_object* l_Lean_Parser_Command_attribute___closed__3;
lean_object* l_Lean_Parser_Command_partial___closed__1;
@ -640,7 +641,6 @@ lean_object* l_Lean_Parser_Command_quotedSymbolPrec___closed__6;
lean_object* l_Lean_Parser_Command_symbol___closed__4;
lean_object* l_Lean_Parser_Command_private___elambda__1(lean_object*);
lean_object* l_Lean_Parser_Command_init__quot___elambda__1___rarg(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_example___closed__5;
lean_object* l_Lean_Parser_Command_quotedSymbolPrec___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_inferMod___closed__1;

2
stage0/library/Init/Lean/Parser/Level.c generated
View file

@ -72,6 +72,7 @@ lean_object* l_Lean_Parser_Level_paren___elambda__1(lean_object*);
lean_object* l_Lean_Parser_Level_paren___elambda__1___rarg___closed__8;
lean_object* l_Lean_Parser_Level_paren___elambda__1___rarg___closed__11;
lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_max___closed__4;
lean_object* l_Lean_Parser_Level_paren___elambda__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_max___closed__1;
@ -94,7 +95,6 @@ extern lean_object* l_Char_HasRepr___closed__1;
lean_object* l_Lean_Parser_levelParserAttribute;
lean_object* l_Lean_Parser_mkLevelParserAttribute___closed__2;
lean_object* l_Lean_Parser_Level_paren___closed__7;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__2;
lean_object* l_Lean_Parser_Level_num___elambda__1(lean_object*);
lean_object* l_Lean_Parser_regBuiltinLevelParserAttr___closed__4;

2
stage0/library/Init/Lean/Parser/Module.c generated
View file

@ -65,6 +65,7 @@ lean_object* l_Lean_Parser_Module_header___closed__2;
lean_object* l___private_Init_Lean_Parser_Module_3__consumeInput(lean_object*, lean_object*);
lean_object* l_Lean_Parser_testModuleParser___closed__1;
lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Module_header___closed__1;
lean_object* l_Lean_Parser_Module_import___closed__3;
lean_object* l_Lean_Parser_Module_header___elambda__1___closed__1;
@ -84,7 +85,6 @@ extern lean_object* l_Char_HasRepr___closed__1;
lean_object* l_Lean_Parser_Module_import___elambda__1___closed__4;
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Module_importPath___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Module_import;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Parser_testModuleParser___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Module_importPath___closed__4;
lean_object* l_Lean_Parser_Module_importPath___closed__3;

2
stage0/library/Init/Lean/Parser/Parser.c generated
View file

@ -343,6 +343,7 @@ uint8_t l_HashMapImp_contains___at_Lean_Parser_isValidSyntaxNodeKind___spec__1(l
lean_object* l_Lean_Parser_trailingNode(lean_object*, lean_object*);
lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
size_t lean_name_hash_usize(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_Lean_Parser_ParserState_next___boxed(lean_object*, lean_object*, lean_object*);
@ -437,7 +438,6 @@ lean_object* l_Lean_Parser_whitespace___boxed(lean_object*, lean_object*);
lean_object* l_List_append___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_fieldIdxFn___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_declareBuiltinParser___closed__2;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
uint8_t l___private_Init_Lean_Parser_Parser_4__isToken(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_decimalNumberFn___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_nameToExprAux___main(lean_object*);

2
stage0/library/Init/Lean/Parser/Term.c generated
View file

@ -681,6 +681,7 @@ lean_object* l_Lean_Parser_Term_nomatch___elambda__1___rarg___closed__1;
lean_object* l___regBuiltinParser_Lean_Parser_Term_seqRight(lean_object*);
lean_object* l_Lean_Parser_Term_sub___elambda__1___closed__3;
lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_listLit___closed__7;
lean_object* l_Lean_Parser_Term_doLet___closed__4;
lean_object* l___regBuiltinParser_Lean_Parser_Term_suffices(lean_object*);
@ -858,7 +859,6 @@ lean_object* l_Lean_Parser_Term_bracketedDoSeq___closed__3;
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letEqns___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Term_sorry(lean_object*);
lean_object* l_Lean_Parser_Term_if___elambda__1___rarg___closed__4;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_explicit___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_uminus___closed__1;
lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__15;

2
stage0/library/Init/Lean/Parser/Transform.c generated
View file

@ -21,13 +21,13 @@ lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_declareLeadingBuiltinParser___closed__1;
lean_object* l_Lean_Syntax_removeParen___closed__1;
lean_object* l_Lean_Syntax_getTailInfo___main___rarg(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNone___rarg(lean_object*);
lean_object* l_Lean_Syntax_getArg___rarg(lean_object*, lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
extern lean_object* l_Option_HasRepr___rarg___closed__3;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_SourceInfo_truncateTrailing(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_manyToSepBy___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);

2
stage0/library/Init/Lean/Path.c generated
View file

@ -52,6 +52,7 @@ lean_object* lean_io_getenv(lean_object*, lean_object*);
extern lean_object* l_List_repr___rarg___closed__2;
lean_object* l_Lean_getSearchPathFromEnv___closed__2;
lean_object* l_Lean_findFile(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* lean_io_file_exists(lean_object*, lean_object*);
lean_object* l_Lean_realPathNormalized(lean_object*, lean_object*);
lean_object* l_Lean_modNameToFileName___boxed(lean_object*);
@ -70,7 +71,6 @@ lean_object* l_List_reprAux___main___at_Lean_findAtSearchPath___spec__3___boxed(
lean_object* l_System_FilePath_dirName(lean_object*);
lean_object* l_Lean_getBuiltinSearchPath___closed__1;
lean_object* l_List_append___rarg(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_List_foldl___main___at_Lean_moduleNameOfFileName___spec__1(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_findLeanFile___closed__2;

2
stage0/library/Init/Lean/ProjFns.c generated
View file

@ -46,6 +46,7 @@ lean_object* lean_io_initializing(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_projectionFnInfoExt___elambda__4(lean_object*);
lean_object* lean_name_mk_string(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*);
@ -61,7 +62,6 @@ lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_obje
uint8_t l_Lean_Environment_isProjectionFn(lean_object*, lean_object*);
uint8_t l_Array_anyRangeMAux___main___at_Lean_mkProjectionFnInfoExtension___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_mkProjectionFnInfoExtension___spec__2___closed__1;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_projectionFnInfoExt___closed__1;
lean_object* lean_nat_add(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;

2
stage0/library/Init/Lean/ReducibilityAttrs.c generated
View file

@ -59,6 +59,7 @@ extern lean_object* l_Lean_EnumAttributes_Inhabited___closed__1;
lean_object* l_Lean_mkReducibilityAttrs___closed__8;
lean_object* l_Lean_mkReducibilityAttrs___lambda__1(lean_object*, lean_object*, uint8_t);
lean_object* l_List_forM___main___at_Lean_registerEnumAttributes___spec__11(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
lean_object* l_Lean_mkReducibilityAttrs___closed__3;
@ -71,7 +72,6 @@ lean_object* l_Lean_mkReducibilityAttrs___closed__11;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_mkReducibilityAttrs___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_RBNode_fold___main___at_Lean_mkReducibilityAttrs___spec__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_registerEnumAttributes___at_Lean_mkReducibilityAttrs___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);

2
stage0/library/Init/Lean/Scopes.c generated
View file

@ -55,6 +55,7 @@ lean_object* l_Lean_Environment_inSection___boxed(lean_object*);
lean_object* l_RBNode_insert___at_Lean_NameSet_insert___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_regScopeManagerExtension___lambda__2___boxed(lean_object*);
lean_object* l_Lean_regScopeManagerExtension(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Environment_getNamespaceSet(lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_regScopeManagerExtension___spec__1___boxed(lean_object*, lean_object*);
@ -63,7 +64,6 @@ lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_regScopeManagerExtension___spec__5(lean_object*, lean_object*);
lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;
uint8_t lean_is_namespace(lean_object*, lean_object*);

2
stage0/library/Init/Lean/Syntax.c generated
View file

@ -120,6 +120,7 @@ lean_object* l_Lean_Syntax_getIdAt(lean_object*);
lean_object* l_Lean_mkAtomFrom___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mreplace___main___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_updateTrailing___rarg(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mreplace___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkStxNumLit(lean_object*, lean_object*);
lean_object* l_Lean_numLitKind___closed__2;
@ -170,7 +171,6 @@ lean_object* l_Lean_unreachIsNodeAtom(lean_object*, lean_object*, lean_object*,
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_findMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1(lean_object*);
lean_object* l___private_Init_Lean_Syntax_5__decodeBinLitAux___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mrewriteBottomUp___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind(lean_object*);
lean_object* l___private_Init_Lean_Syntax_5__decodeBinLitAux___main___boxed(lean_object*, lean_object*, lean_object*);

45
stage0/library/Init/Lean/ToExpr.c generated
View file

@ -18,14 +18,13 @@ lean_object* l_Lean_mkStrLit(lean_object*);
lean_object* l_Lean_nameToExprAux___main___closed__3;
lean_object* l_Lean_nameToExprAux___main___closed__1;
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_nameToExprAux___main___closed__7;
lean_object* l_Lean_nameToExprAux___main___closed__8;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_nameToExprAux___main(lean_object*);
extern lean_object* l_liftRefl___closed__1;
lean_object* l_Lean_nameToExprAux___main___closed__6;
lean_object* l_Lean_nameToExprAux(lean_object*);
lean_object* l_Lean_nameToExprAux___main___closed__9;
lean_object* l_Lean_mkNatLit(lean_object*);
lean_object* l_Lean_mkCAppB(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_strToExpr___closed__1;
@ -114,45 +113,35 @@ return x_3;
lean_object* _init_l_Lean_nameToExprAux___main___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_nameToExprAux___main___closed__4;
x_2 = l_Lean_nameToExprAux___main___closed__2;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
lean_object* x_1;
x_1 = lean_mk_string("mkNameStr");
return x_1;
}
}
lean_object* _init_l_Lean_nameToExprAux___main___closed__6() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("mkString");
return x_1;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_nameToExprAux___main___closed__4;
x_2 = l_Lean_nameToExprAux___main___closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_nameToExprAux___main___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_nameToExprAux___main___closed__5;
x_2 = l_Lean_nameToExprAux___main___closed__6;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
lean_object* x_1;
x_1 = lean_mk_string("mkNameNum");
return x_1;
}
}
lean_object* _init_l_Lean_nameToExprAux___main___closed__8() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("mkNumeral");
return x_1;
}
}
lean_object* _init_l_Lean_nameToExprAux___main___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_nameToExprAux___main___closed__5;
x_2 = l_Lean_nameToExprAux___main___closed__8;
x_1 = l_Lean_nameToExprAux___main___closed__4;
x_2 = l_Lean_nameToExprAux___main___closed__7;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -184,7 +173,7 @@ lean_inc(x_11);
lean_dec(x_1);
x_12 = l_Lean_nameToExprAux___main(x_10);
x_13 = l_Lean_mkStrLit(x_11);
x_14 = l_Lean_nameToExprAux___main___closed__7;
x_14 = l_Lean_nameToExprAux___main___closed__6;
x_15 = l_Lean_mkCAppB(x_14, x_12, x_13);
return x_15;
}
@ -198,7 +187,7 @@ lean_inc(x_17);
lean_dec(x_1);
x_18 = l_Lean_nameToExprAux___main(x_16);
x_19 = l_Lean_mkNatLit(x_17);
x_20 = l_Lean_nameToExprAux___main___closed__9;
x_20 = l_Lean_nameToExprAux___main___closed__8;
x_21 = l_Lean_mkCAppB(x_20, x_18, x_19);
return x_21;
}
@ -264,8 +253,6 @@ l_Lean_nameToExprAux___main___closed__7 = _init_l_Lean_nameToExprAux___main___cl
lean_mark_persistent(l_Lean_nameToExprAux___main___closed__7);
l_Lean_nameToExprAux___main___closed__8 = _init_l_Lean_nameToExprAux___main___closed__8();
lean_mark_persistent(l_Lean_nameToExprAux___main___closed__8);
l_Lean_nameToExprAux___main___closed__9 = _init_l_Lean_nameToExprAux___main___closed__9();
lean_mark_persistent(l_Lean_nameToExprAux___main___closed__9);
l_Lean_nameToExpr___closed__1 = _init_l_Lean_nameToExpr___closed__1();
lean_mark_persistent(l_Lean_nameToExpr___closed__1);
l_Lean_nameToExpr = _init_l_Lean_nameToExpr();

2
stage0/library/Init/Lean/Trace.c generated
View file

@ -48,6 +48,7 @@ lean_object* l___private_Init_Lean_Trace_5__checkTraceOption___rarg___lambda__1_
lean_object* l_Lean_MonadTracerAdapter_traceCtx___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TraceState_HasToString;
lean_object* l_Lean_SimpleMonadTracerAdapter_getTraces___rarg(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_SimpleMonadTracerAdapter_isTracingEnabledFor___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_monadTracerAdapter___rarg(lean_object*, lean_object*);
lean_object* l_Lean_SimpleMonadTracerAdapter_getTraces(lean_object*);
@ -63,7 +64,6 @@ uint8_t l___private_Init_Lean_Trace_4__checkTraceOptionAux(lean_object*, lean_ob
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Trace_5__checkTraceOption___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SimpleMonadTracerAdapter_enableTracing___rarg___boxed(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_MonadTracerAdapter_trace___boxed(lean_object*);
lean_object* l_Lean_SimpleMonadTracerAdapter_modifyTraces___rarg(lean_object*, lean_object*);

4
stage0/library/Init/Lean/TypeClass/Context.c generated
View file

@ -20,6 +20,7 @@ uint8_t l_Lean_TypeClass_Context_eHasETmpMVar(lean_object*);
lean_object* l_Lean_Expr_bindingBody_x21(lean_object*);
lean_object* l_Lean_TypeClass_Context_internalize___lambda__2(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eHasTmpMVar___closed__1;
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
uint8_t l_Lean_Name_beq___main(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_internalize___closed__4;
lean_object* l_Lean_TypeClass_Context_eMetaNormalizeCore___rarg(lean_object*, lean_object*, lean_object*);
@ -104,6 +105,7 @@ uint8_t l_Lean_TypeClass_Context_eFind___main(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eIsMeta___boxed(lean_object*);
lean_object* l_Lean_TypeClass_Context__u03b1Norm___lambda__2(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_uIsMeta___boxed(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
uint8_t lean_expr_eqv(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_uInstantiate___main___boxed(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eUnify___main___closed__4;
@ -129,7 +131,6 @@ lean_object* lean_expr_update_const(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eInstantiate(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eMetaIdx___boxed(lean_object*);
lean_object* l_Lean_TypeClass_Context_eAssignIdx___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
uint8_t l_List_foldr___main___at_Lean_TypeClass_Context_eHasTmpMVar___spec__1(uint8_t, lean_object*);
extern lean_object* l___private_Init_Lean_MetavarContext_5__instantiateDelayedAux___main___closed__1;
lean_object* l_PersistentArray_getAux___main___at_Lean_TypeClass_Context_eInferIdx___spec__2___boxed(lean_object*, lean_object*, lean_object*);
@ -168,7 +169,6 @@ lean_object* l_Lean_TypeClass_Context_uAssignIdx(lean_object*, lean_object*, lea
lean_object* l_Lean_TypeClass_Context_slowWhnfApp___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_RBNode_insert___at_Lean_TypeClass_Context__u03b1Norm___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentArray_getAux___main___at_Lean_TypeClass_Context_eLookupIdx___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_uInstantiate___main(lean_object*, lean_object*);
uint8_t l_Lean_TypeClass_Context_uOccursIn(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eInfer___closed__2;

4
stage0/library/Init/Lean/TypeClass/Synth.c generated
View file

@ -15,6 +15,7 @@ extern "C" {
#endif
lean_object* l_PersistentHashMap_insertAux___main___at_Lean_TypeClass_newSubgoal___spec__3(lean_object*, size_t, size_t, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_introduceLocals(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
size_t l_USize_mul(size_t, size_t);
lean_object* l_Lean_TypeClass_synth___closed__2;
extern lean_object* l_Array_empty___closed__1;
@ -85,6 +86,7 @@ lean_object* l_PersistentHashMap_insertAux___main___at_Lean_TypeClass_newSubgoal
lean_object* l_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Node_Inhabited___closed__1;
extern lean_object* l_Lean_TypeClass_Context_Inhabited;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_constNameToTypedExpr(lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_TypeClass_newAnswer___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_expr_eqv(lean_object*, lean_object*);
@ -110,7 +112,6 @@ uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_mkFVar(lean_object*);
lean_object* l_Lean_TypeClass_collectEReplacements(lean_object*);
lean_object* l_List_append___rarg(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_collectEReplacements___main___closed__2;
lean_object* l_Lean_TypeClass_ConsumerNode_Inhabited___closed__1;
lean_object* lean_nat_add(lean_object*, lean_object*);
@ -152,7 +153,6 @@ lean_object* lean_array_pop(lean_object*);
lean_object* lean_instantiate_type_lparams(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_newSubgoal___closed__3;
lean_object* l_Lean_TypeClass_preprocessForOutParams(lean_object*, lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* lean_environment_find(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_collectEReplacements___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_is_class(lean_object*, lean_object*);

2
stage0/library/Init/Lean/WHNF.c generated
View file

@ -89,6 +89,7 @@ lean_object* l_Lean_whnfCore___boxed(lean_object*);
lean_object* l___private_Init_Lean_WHNF_3__toCtorIfLit___closed__1;
lean_object* l_Lean_mkSmartUnfoldingNameFor(lean_object*);
lean_object* l_Lean_reduceQuotRec___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
uint8_t lean_expr_eqv(lean_object*, lean_object*);
lean_object* l_Lean_whnfCore___main___rarg___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_ConstantInfo_hasValue(lean_object*);
@ -107,7 +108,6 @@ lean_object* l_Lean_reduceRec___rarg___lambda__3(lean_object*, lean_object*, lea
lean_object* l___private_Init_Lean_WHNF_3__toCtorIfLit___boxed(lean_object*);
lean_object* l_Lean_whnfMain___boxed(lean_object*);
lean_object* l___private_Init_Lean_WHNF_3__toCtorIfLit___closed__4;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_unfoldDefinitionAux___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
lean_object* lean_instantiate_value_lparams(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);

2
stage0/src/frontends/lean/parser.cpp generated
View file

@ -1527,7 +1527,7 @@ struct to_pattern_fn {
buffer<expr> args;
get_app_args(e, args);
args[0] = fix_quoted_name(args[0]);
return mk_app(mk_constant(get_lean_name_mk_string_name()), args);
return mk_app(mk_constant(get_lean_name_str_name()), args);
}
expr fix_quoted_names(expr const & e) {

16
stage0/src/library/constants.cpp generated
View file

@ -116,8 +116,8 @@ name const * g_monad = nullptr;
name const * g_monad_fail = nullptr;
name const * g_lean_name = nullptr;
name const * g_lean_name_anonymous = nullptr;
name const * g_lean_name_mk_numeral = nullptr;
name const * g_lean_name_mk_string = nullptr;
name const * g_lean_name_num = nullptr;
name const * g_lean_name_str = nullptr;
name const * g_lean_mk_name_num = nullptr;
name const * g_lean_mk_name_str = nullptr;
name const * g_lean_parser_leading_node = nullptr;
@ -305,8 +305,8 @@ void initialize_constants() {
g_monad_fail = new name{"MonadFail"};
g_lean_name = new name{"Lean", "Name"};
g_lean_name_anonymous = new name{"Lean", "Name", "anonymous"};
g_lean_name_mk_numeral = new name{"Lean", "Name", "mkNumeral"};
g_lean_name_mk_string = new name{"Lean", "Name", "mkString"};
g_lean_name_num = new name{"Lean", "Name", "num"};
g_lean_name_str = new name{"Lean", "Name", "str"};
g_lean_mk_name_num = new name{"Lean", "mkNameNum"};
g_lean_mk_name_str = new name{"Lean", "mkNameStr"};
g_lean_parser_leading_node = new name{"Lean", "Parser", "leadingNode"};
@ -495,8 +495,8 @@ void finalize_constants() {
delete g_monad_fail;
delete g_lean_name;
delete g_lean_name_anonymous;
delete g_lean_name_mk_numeral;
delete g_lean_name_mk_string;
delete g_lean_name_num;
delete g_lean_name_str;
delete g_lean_mk_name_num;
delete g_lean_mk_name_str;
delete g_lean_parser_leading_node;
@ -684,8 +684,8 @@ name const & get_monad_name() { return *g_monad; }
name const & get_monad_fail_name() { return *g_monad_fail; }
name const & get_lean_name_name() { return *g_lean_name; }
name const & get_lean_name_anonymous_name() { return *g_lean_name_anonymous; }
name const & get_lean_name_mk_numeral_name() { return *g_lean_name_mk_numeral; }
name const & get_lean_name_mk_string_name() { return *g_lean_name_mk_string; }
name const & get_lean_name_num_name() { return *g_lean_name_num; }
name const & get_lean_name_str_name() { return *g_lean_name_str; }
name const & get_lean_mk_name_num_name() { return *g_lean_mk_name_num; }
name const & get_lean_mk_name_str_name() { return *g_lean_mk_name_str; }
name const & get_lean_parser_leading_node_name() { return *g_lean_parser_leading_node; }

4
stage0/src/library/constants.h generated
View file

@ -118,8 +118,8 @@ name const & get_monad_name();
name const & get_monad_fail_name();
name const & get_lean_name_name();
name const & get_lean_name_anonymous_name();
name const & get_lean_name_mk_numeral_name();
name const & get_lean_name_mk_string_name();
name const & get_lean_name_num_name();
name const & get_lean_name_str_name();
name const & get_lean_mk_name_num_name();
name const & get_lean_mk_name_str_name();
name const & get_lean_parser_leading_node_name();

4
stage0/src/library/constants.txt generated
View file

@ -111,8 +111,8 @@ Monad
MonadFail
Lean.Name
Lean.Name.anonymous
Lean.Name.mkNumeral
Lean.Name.mkString
Lean.Name.num
Lean.Name.str
Lean.mkNameNum
Lean.mkNameStr
Lean.Parser.leadingNode

4
stage0/src/library/util.cpp generated
View file

@ -1009,12 +1009,12 @@ optional<name> is_unsafe_rec_name(name const & n) {
optional<name> name_lit_to_name(expr const & name_lit) {
if (is_constant(name_lit, get_lean_name_anonymous_name()))
return optional<name>(name());
if (is_app_of(name_lit, get_lean_name_mk_string_name(), 2)) {
if (is_app_of(name_lit, get_lean_name_str_name(), 2)) {
if (auto p = name_lit_to_name(app_arg(app_fn(name_lit))))
if (auto str = to_string(app_arg(name_lit)))
return optional<name>(name(*p, str->c_str()));
}
if (is_app_of(name_lit, get_lean_name_mk_numeral_name(), 2)) {
if (is_app_of(name_lit, get_lean_name_num_name(), 2)) {
if (auto p = name_lit_to_name(app_arg(app_fn(name_lit))))
if (auto n = to_num(app_arg(name_lit)))
return optional<name>(name(*p, n->get_unsigned_int()));