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-16 12:24:19 -08:00
parent 92a89a07ff
commit 587e4f199b
8 changed files with 327 additions and 408 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

File diff suppressed because it is too large Load diff

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

@ -67,6 +67,7 @@ lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
lean_object* l_Lean_Meta_isClassExpensive___main___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__5(lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_5__getTraceState___boxed(lean_object*);
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
lean_object* l___private_Init_Lean_Meta_Basic_5__getTraceState___rarg(lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___main___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_dbgTrace___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -229,7 +230,6 @@ lean_object* l___private_Init_Lean_Meta_Basic_9__lambdaTelescopeAux(lean_object*
lean_object* l_Lean_MetavarContext_MkBinding_mkBinding___at_Lean_MetavarContext_mkBinding___spec__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_MetaM_inhabited___rarg(lean_object*);
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_CachedData_binderInfo(uint64_t);
uint8_t _init_l_Lean_Meta_TransparencyMode_Inhabited() {
_start:
{

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

@ -75,6 +75,7 @@ lean_object* l_Array_anyRangeMAux___main___at___private_Init_Lean_Meta_Default_3
uint8_t l___private_Init_Lean_WHNF_6__isIdRhsApp(lean_object*);
lean_object* l___private_Init_Lean_WHNF_4__getRecRuleFor(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_WHNF_9__deltaBetaDefinition___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__25(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
lean_object* l_Lean_Literal_type(lean_object*);
lean_object* l_Lean_reduceQuotRec___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
@ -267,7 +268,6 @@ lean_object* l_ReaderT_pure___at___private_Init_Lean_Meta_Default_3__auxFixpoint
lean_object* l___private_Init_Lean_Meta_Default_3__auxFixpoint___main___closed__1;
lean_object* l___private_Init_Lean_Meta_InferType_7__inferLambdaType___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__31(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_getFunInfo___spec__7(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_CachedData_binderInfo(uint64_t);
uint8_t l_Lean_Expr_isLambda(lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__50(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Lean_Meta_Default_1__exprToBool(lean_object* x_1) {

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

@ -60,6 +60,7 @@ lean_object* l_Lean_mkMVar(lean_object*);
lean_object* l___private_Init_Lean_Meta_ExprDefEq_15__processAssignment(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_contains___at_Lean_Meta_CheckAssignment_checkFVar___spec__1___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_ExprDefEq_8__checkAssignmentFailure___closed__5;
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
lean_object* l_Lean_Expr_getAppNumArgsAux___main(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_ExprDefEq_9__isDefEqFOApprox(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_ExprDefEq_2__isDefEqArgsFirstPass(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -233,7 +234,6 @@ lean_object* l___private_Init_Lean_Meta_LevelDefEq_12__processPostponed(uint8_t,
lean_object* l___private_Init_Lean_Meta_ExprDefEq_8__checkAssignmentFailure___closed__15;
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_update_let(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_CachedData_binderInfo(uint64_t);
uint8_t l_Lean_Expr_isLambda(lean_object*);
lean_object* _init_l___private_Init_Lean_Meta_ExprDefEq_1__isDefEqEta___closed__1() {
_start:

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

@ -59,6 +59,7 @@ lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
lean_object* l_Lean_Meta_isClassExpensive___at_Lean_Meta_inferTypeAux___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_hasLooseBVars(lean_object*);
lean_object* l_Nat_foldMAux___main___at_Lean_Meta_inferTypeAux___spec__33___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
lean_object* l_Lean_Literal_type(lean_object*);
lean_object* l_Lean_Meta_inferTypeAuxAux(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppNumArgsAux___main(lean_object*, lean_object*);
@ -193,7 +194,6 @@ lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_inferTypeAu
lean_object* l___private_Init_Lean_Meta_InferType_12__isAlwaysZero___main___boxed(lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_inferTypeAux___spec__10___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_InferType_6__inferForallType___at_Lean_Meta_inferTypeAux___spec__16(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_CachedData_binderInfo(uint64_t);
lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___main___at_Lean_Meta_inferTypeAux___spec__23(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_InferType_1__getForallResultType___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) {
_start:

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

@ -140,6 +140,7 @@ uint8_t l_Lean_LocalContext_contains(lean_object*, lean_object*);
lean_object* l_List_mapM___main___at_Lean_MetavarContext_InstantiateExprMVars_main___main___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_MetavarContext_isLevelAssignable___closed__1;
lean_object* l_Lean_mkMVar(lean_object*);
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
lean_object* l_Lean_MetavarContext_hasAssignedLevelMVar___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppNumArgsAux___main(lean_object*, lean_object*);
extern lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkBinding___spec__1___closed__1;
@ -501,7 +502,6 @@ lean_object* l_Lean_MetavarContext_MkBinding_mkBinding___at_Lean_MetavarContext_
lean_object* l_Array_iterateMAux___main___at_Lean_MetavarContext_addExprMVarDecl___spec__4(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentArray_foldlFromM___at___private_Init_Lean_MetavarContext_13__collectDeps___spec__40___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_update_let(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_CachedData_binderInfo(uint64_t);
uint8_t l_Lean_Expr_isLambda(lean_object*);
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l_PersistentHashMap_insertAux___main___at_Lean_MetavarContext_assignLevel___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*);

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

@ -66,6 +66,7 @@ lean_object* l_Lean_TypeClass_Context_eAssign___boxed(lean_object*, lean_object*
lean_object* l_Lean_TypeClass_Context_uNewMeta(lean_object*);
lean_object* l_Lean_TypeClass_Context_uUnify___main___closed__3;
lean_object* l_Lean_mkMVar(lean_object*);
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
lean_object* l_Lean_TypeClass_Context_eAssign(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context__u03b1Norm___closed__5;
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
@ -232,7 +233,6 @@ lean_object* l_Lean_TypeClass_Context__u03b1Norm___closed__2;
lean_object* l_Lean_TypeClass_Context_uAssign___closed__1;
lean_object* l_Lean_TypeClass_Context_uUnify___main___closed__5;
lean_object* l_Lean_TypeClass_Context__u03b1Norm___closed__6;
uint8_t l_Lean_Expr_CachedData_binderInfo(uint64_t);
lean_object* l_Lean_TypeClass_Context_uMetaNormalizeCore___rarg(lean_object*, lean_object*, lean_object*);
lean_object* _init_l_Lean_TypeClass_Context_Inhabited___closed__1() {
_start:

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

@ -59,6 +59,7 @@ lean_object* l_Lean_TypeClass_Context_uNewMeta(lean_object*);
lean_object* l_Stack_pop___at_Lean_TypeClass_consume___spec__3(lean_object*);
lean_object* l_Lean_TypeClass_TypedExpr_HasToString___boxed(lean_object*);
lean_object* l_Lean_TypeClass_TypedExpr_HasToString___closed__1;
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
extern lean_object* l_Lean_formatDataValue___closed__1;
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_TypedExpr_Inhabited;
@ -203,7 +204,6 @@ lean_object* l_Array_back___at_Lean_TypeClass_generate___spec__2___boxed(lean_ob
lean_object* l_Lean_TypeClass_synth___closed__3;
lean_object* l_Lean_TypeClass_constNameToTypedExpr___closed__2;
lean_object* l_Array_anyRangeMAux___main___at_Lean_TypeClass_newAnswer___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_CachedData_binderInfo(uint64_t);
uint8_t l_Lean_Expr_isLambda(lean_object*);
lean_object* _init_l_Lean_TypeClass_TypedExpr_HasToString___closed__1() {
_start: