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 2021-05-01 16:23:32 -07:00
parent 106952622a
commit e20a07bd6d
4 changed files with 56 additions and 55 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
stage0/src/kernel/inductive.cpp generated
View file

@ -593,7 +593,8 @@ public:
expr u_app = mk_app(u_i, xs);
C_app = mk_app(C_app, u_app);
expr v_i_ty = mk_pi(xs, C_app);
expr v_i = mk_local_decl(name("v").append_after(i), v_i_ty, binder_info());
local_decl u_i_decl = m_lctx.get_local_decl(fvar_name(u_i));
expr v_i = mk_local_decl(u_i_decl.get_user_name().append_after("_ih"), v_i_ty, binder_info());
v.push_back(v_i);
}
expr minor_ty = mk_pi(b_u, mk_pi(v, C_app));

98
stage0/stdlib/Lean/Elab/Match.c generated
View file

@ -154,6 +154,7 @@ lean_object* lean_environment_find(lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_15342____closed__8;
lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__3___lambda__1___closed__2;
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Quotation_precheckIdent___spec__1___rarg(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__2;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_throwEx___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_isMatchUnit_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -165,6 +166,7 @@ lean_object* lean_st_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_precheckMatch_match__3___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_generalize_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_nameToPattern___closed__17;
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1;
extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
extern lean_object* l_Lean_Parser_Term_nomatch___elambda__1___closed__1;
uint8_t lean_name_eq(lean_object*, lean_object*);
@ -218,6 +220,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_pr
extern lean_object* l_Array_getEvenElems___rarg___closed__1;
lean_object* l_Lean_MessageData_ofList(lean_object*);
lean_object* l_Lean_Meta_isTypeCorrect(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__4;
lean_object* l_Array_sequenceMap___at_Lean_Elab_Term_precheckMatch___spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_generalize_match__2(lean_object*);
lean_object* l_Lean_Elab_Term_ToDepElimPattern_main___closed__1;
@ -258,14 +261,12 @@ lean_object* l_Lean_Expr_replaceFVars(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldrMUnsafe_fold___at___private_Lean_Elab_Match_0__Lean_Elab_Term_generalize___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltView___closed__3;
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1;
lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_finalizePatternDecls___spec__1___closed__4;
lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_processCtorAppCore___lambda__2(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getMainModule___rarg(lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_1481____closed__8;
uint8_t l_USize_decLt(size_t, size_t);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__2;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_loop___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_processId_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_rootNamespace___closed__2;
@ -288,7 +289,6 @@ lean_object* l_Lean_Elab_Term_instToStringPatternVar_match__1(lean_object*);
lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*);
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltView___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Match_0__Lean_Elab_Term_generalize___spec__1(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__5;
lean_object* l_Lean_Elab_Term_precheckMatch___lambda__1(lean_object*, lean_object*);
lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkEqRefl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -345,7 +345,6 @@ extern lean_object* l___private_Lean_Util_Trace_0__Lean_addNode___rarg___lambda_
uint8_t l_Lean_Name_hasMacroScopes(lean_object*);
lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_withPatternVars_loop_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__4;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_getMVarSyntaxMVarId(lean_object*);
lean_object* l_Lean_Elab_throwIllFormedSyntax___at___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_quotedNameToPattern___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTermEnsuringType(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -389,6 +388,7 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_getPatternVarNames___
extern lean_object* l_List_forIn_loop___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_checkNextPatternTypes___spec__1___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_elabMatch(lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__5;
lean_object* l_Lean_Meta_Match_Pattern_toExpr_visit(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_precheckMatch___spec__5___closed__1;
lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_Match_0__Lean_Elab_Term_getIndicesToInclude___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -453,6 +453,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscr
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_nameToPattern___closed__12;
lean_object* l_Lean_throwError___at_Lean_Elab_Term_CollectPatternVars_collect_processCtorAppCore___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_instantiateLocalDeclMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__3;
lean_object* l_Lean_Elab_Term_mkMatcher(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_Quotation_precheckAttribute;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_isMatchUnit_x3f_match__2(lean_object*);
@ -478,7 +479,6 @@ uint8_t l_Lean_Option_get___at_Lean_ppExpr___spec__1(lean_object*, lean_object*)
lean_object* l_Lean_Elab_Term_elabMatch_elabMatchDefault___closed__1;
lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_processCtorAppContext_match__2(lean_object*);
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__3;
uint8_t l_Lean_LocalDecl_binderInfo(lean_object*);
lean_object* l_Lean_Elab_Term_expandMacrosInPatterns(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux_match__2(lean_object*);
@ -513,6 +513,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNonAtomicDiscrs
lean_object* l_Lean_throwError___at_Lean_Elab_Term_CollectPatternVars_collect_processCtorAppCore___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__2;
lean_object* l_Lean_Elab_Term_finalizePatternDecls_match__2(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__1;
lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_processCtor(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabPatterns___spec__2___lambda__1(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___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_loop___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*);
@ -536,7 +537,6 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_getPatternVarNames___
extern lean_object* l___private_Init_Meta_0__Lean_quoteName___closed__2;
lean_object* l_ReaderT_pure___at_Lean_Elab_liftMacroM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___spec__1___lambda__2___closed__3;
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__1;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__1(size_t, size_t, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_mkMVarSyntax___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mkStrLit(lean_object*, lean_object*);
@ -640,6 +640,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_mkUserNameFor___boxed
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_tryPostponeIfDiscrTypeIsMVar___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_nullKind___closed__2;
lean_object* l_Lean_Elab_Term_CollectPatternVars_collect(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2;
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_tryPostponeIfDiscrTypeIsMVar___spec__1___closed__1;
extern lean_object* l_Lean_Elab_Term_termElabAttribute;
lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_processId_match__2___rarg(lean_object*, lean_object*, lean_object*);
@ -648,7 +649,6 @@ extern lean_object* l_Lean_Elab_throwIllFormedSyntax___rarg___closed__2;
lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_processCtorAppContext(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_instToStringPatternVar(lean_object*);
lean_object* l_Lean_mkAtomFrom(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_waitExpectedType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNodeOf(lean_object*, lean_object*, lean_object*);
@ -988,9 +988,9 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux_match__3
lean_object* l_Lean_Elab_Term_isLocalIdent_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__4___lambda__1___closed__1;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Closure_mkBinding___spec__1(size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12038_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12040_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277_(lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_reportMatcherResultErrors___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkSimpleThunk(lean_object*);
@ -4490,7 +4490,7 @@ return x_11;
}
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__1() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__1() {
_start:
{
lean_object* x_1;
@ -4498,21 +4498,21 @@ x_1 = lean_mk_string("MVarWithIdKind");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275_(lean_object* x_1) {
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2;
x_3 = l_Lean_Parser_registerBuiltinNodeKind(x_2, x_1);
return x_3;
}
@ -4533,7 +4533,7 @@ lean_ctor_set(x_7, 0, x_5);
lean_ctor_set(x_7, 1, x_6);
x_8 = l_Lean_mkOptionalNode___closed__2;
x_9 = lean_array_push(x_8, x_7);
x_10 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2;
x_10 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2;
x_11 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_11, 1, x_9);
@ -4554,7 +4554,7 @@ lean_ctor_set(x_15, 0, x_12);
lean_ctor_set(x_15, 1, x_14);
x_16 = l_Lean_mkOptionalNode___closed__2;
x_17 = lean_array_push(x_16, x_15);
x_18 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2;
x_18 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2;
x_19 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_19, 0, x_18);
lean_ctor_set(x_19, 1, x_17);
@ -4656,7 +4656,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Elab_Term_termElabAttribute;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2;
x_4 = l___regBuiltin_Lean_Elab_Term_elabMVarWithIdKind___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
@ -31775,7 +31775,7 @@ lean_dec(x_5);
return x_12;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -31785,7 +31785,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__2() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__2() {
_start:
{
lean_object* x_1;
@ -31793,17 +31793,17 @@ x_1 = lean_mk_string("ignoreUnusedAlts");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__3() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__2;
x_1 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__2;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__4() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__4() {
_start:
{
lean_object* x_1;
@ -31811,13 +31811,13 @@ x_1 = lean_mk_string("if true, do not generate error if an alternative is not us
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__5() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__5() {
_start:
{
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = 0;
x_2 = l_Lean_instInhabitedParserDescr___closed__1;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__4;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__4;
x_4 = lean_box(x_1);
x_5 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_5, 0, x_4);
@ -31826,12 +31826,12 @@ lean_ctor_set(x_5, 2, x_3);
return x_5;
}
}
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327_(lean_object* x_1) {
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__3;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__5;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__3;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__5;
x_4 = l_Lean_Option_register___at_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_4____spec__1(x_2, x_3, x_1);
return x_4;
}
@ -36083,7 +36083,7 @@ x_31 = lean_ctor_get(x_29, 1);
lean_inc(x_31);
lean_dec(x_29);
x_32 = lean_array_get_size(x_25);
x_33 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1;
x_33 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1;
lean_inc(x_7);
x_34 = l_Lean_Elab_Term_mkAuxName(x_33, x_7, x_8, x_9, x_10, x_11, x_12, x_31);
if (lean_obj_tag(x_34) == 0)
@ -36489,7 +36489,7 @@ x_109 = lean_ctor_get(x_21, 1);
lean_inc(x_109);
lean_dec(x_21);
x_110 = lean_array_get_size(x_106);
x_111 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1;
x_111 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1;
lean_inc(x_7);
x_112 = l_Lean_Elab_Term_mkAuxName(x_111, x_7, x_8, x_9, x_10, x_11, x_12, x_105);
if (lean_obj_tag(x_112) == 0)
@ -40220,7 +40220,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12038_(lean_object* x_1) {
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12040_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -40529,11 +40529,11 @@ l_Lean_Elab_Term_expandMacrosInPatterns___boxed__const__1 = _init_l_Lean_Elab_Te
lean_mark_persistent(l_Lean_Elab_Term_expandMacrosInPatterns___boxed__const__1);
l_Lean_Elab_Term_instToStringPatternVar___closed__1 = _init_l_Lean_Elab_Term_instToStringPatternVar___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_instToStringPatternVar___closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275_(lean_io_mk_world());
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Term_elabMVarWithIdKind___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabMVarWithIdKind___closed__1();
@ -40749,17 +40749,17 @@ l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_collectDeps___cl
lean_mark_persistent(l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_collectDeps___closed__1);
l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_loop___boxed__const__1 = _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_loop___boxed__const__1();
lean_mark_persistent(l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_loop___boxed__const__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__2);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__3 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__3();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__3);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__4 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__4();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__4);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__5 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__5();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__5);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327_(lean_io_mk_world());
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__2);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__3 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__3();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__3);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__4 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__4();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__4);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__5 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__5();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__5);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_Elab_Term_match_ignoreUnusedAlts = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Elab_Term_match_ignoreUnusedAlts);
@ -40835,7 +40835,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabMatch___closed__1);
res = l___regBuiltin_Lean_Elab_Term_elabMatch(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12038_(lean_io_mk_world());
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12040_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_elabNoMatch___closed__1 = _init_l_Lean_Elab_Term_elabNoMatch___closed__1();

4
stage0/stdlib/Lean/Elab/Tactic/Match.c generated
View file

@ -42,6 +42,7 @@ size_t l_USize_sub(size_t, size_t);
extern lean_object* l_Array_empty___closed__1;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_15342____closed__8;
lean_object* lean_st_ref_get(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1;
lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTerm_match__1(lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_15342____closed__2;
@ -56,7 +57,6 @@ lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Match_0__Lea
size_t l_USize_shiftRight(size_t, size_t);
lean_object* lean_string_utf8_byte_size(lean_object*);
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTermAux___spec__1___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1;
lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Tactic_evalMatch___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getMainModule___rarg(lean_object*, lean_object*);
@ -1593,7 +1593,7 @@ lean_dec(x_277);
x_316 = lean_ctor_get(x_6, 0);
lean_inc(x_316);
lean_dec(x_6);
x_317 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1;
x_317 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1;
x_318 = l_Lean_Name_appendIndexAfter(x_317, x_316);
x_319 = l_Lean_Name_append(x_1, x_318);
x_320 = l_Lean_mkIdentFrom(x_30, x_319);

6
stage0/stdlib/Lean/Meta/IndPredBelow.c generated
View file

@ -299,7 +299,7 @@ lean_object* l_Lean_Meta_transform_visit_visitLambda___at_Lean_Meta_IndPredBelow
lean_object* l_Lean_Meta_IndPredBelow_proveBrecOn_closeGoal___rarg___closed__6;
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_processPostponedStep___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_IndPredBelow_initFn____x40_Lean_Meta_IndPredBelow___hyg_4_(lean_object*);
lean_object* l_Lean_Meta_IndPredBelow_initFn____x40_Lean_Meta_IndPredBelow___hyg_2916_(lean_object*);
lean_object* l_Lean_Meta_IndPredBelow_initFn____x40_Lean_Meta_IndPredBelow___hyg_2924_(lean_object*);
lean_object* l_Lean_Meta_forallTelescope___at_Lean_Meta_IndPredBelow_mkContext_mkHeader___spec__3(lean_object*);
lean_object* l_Lean_Meta_getLocalDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_IndPredBelow_mkCtorType_checkCount___spec__8___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -13308,7 +13308,7 @@ lean_dec(x_1);
return x_12;
}
}
lean_object* l_Lean_Meta_IndPredBelow_initFn____x40_Lean_Meta_IndPredBelow___hyg_2916_(lean_object* x_1) {
lean_object* l_Lean_Meta_IndPredBelow_initFn____x40_Lean_Meta_IndPredBelow___hyg_2924_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -13449,7 +13449,7 @@ l_Lean_Meta_IndPredBelow_mkBelow___closed__6 = _init_l_Lean_Meta_IndPredBelow_mk
lean_mark_persistent(l_Lean_Meta_IndPredBelow_mkBelow___closed__6);
l_Lean_Meta_IndPredBelow_mkBelow___closed__7 = _init_l_Lean_Meta_IndPredBelow_mkBelow___closed__7();
lean_mark_persistent(l_Lean_Meta_IndPredBelow_mkBelow___closed__7);
res = l_Lean_Meta_IndPredBelow_initFn____x40_Lean_Meta_IndPredBelow___hyg_2916_(lean_io_mk_world());
res = l_Lean_Meta_IndPredBelow_initFn____x40_Lean_Meta_IndPredBelow___hyg_2924_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));