chore: update stage0
This commit is contained in:
parent
e1c176543a
commit
855a762bcb
5 changed files with 1713 additions and 7 deletions
95
stage0/stdlib/Init/Tactics.c
generated
95
stage0/stdlib/Init/Tactics.c
generated
|
|
@ -682,6 +682,7 @@ static lean_object* l_Lean_Parser_Tactic_rwRule___closed__14;
|
|||
static lean_object* l_Lean_Parser_Tactic_tacticStop_____closed__4;
|
||||
static lean_object* l_Lean_Parser_Tactic_simpTrace___closed__10;
|
||||
static lean_object* l_Lean_Parser_Tactic_simpAll___closed__13;
|
||||
static lean_object* l_Lean_Parser_Tactic_normCastAddElim___closed__4;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_simpa;
|
||||
static lean_object* l_Lean_Parser_Tactic_discharger___closed__13;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_injection;
|
||||
|
|
@ -698,6 +699,7 @@ static lean_object* l_Lean_Parser_Tactic_tacticSimpa_x3f_x21_____closed__3;
|
|||
static lean_object* l_Lean_Parser_Tactic_pushCast___closed__11;
|
||||
static lean_object* l_Lean_Parser_Tactic_rwRule___closed__3;
|
||||
static lean_object* l_Lean_Parser_Tactic_first___closed__23;
|
||||
static lean_object* l_Lean_Parser_Tactic_normCastAddElim___closed__5;
|
||||
static lean_object* l_Lean_Parser_Tactic_tacticHave_____closed__9;
|
||||
static lean_object* l_Lean_Parser_Tactic_split___closed__7;
|
||||
static lean_object* l_Lean_Parser_Tactic_rotateLeft___closed__11;
|
||||
|
|
@ -922,6 +924,7 @@ static lean_object* l_Lean_Parser_Tactic_tacticSimp_x3f_x21_____closed__5;
|
|||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_simpPre;
|
||||
static lean_object* l_Lean_Parser_Tactic_first___closed__21;
|
||||
static lean_object* l_Lean_Parser_Tactic_unfold___closed__6;
|
||||
static lean_object* l_Lean_Parser_Tactic_normCastAddElim___closed__1;
|
||||
static lean_object* l_Lean_Parser_Tactic_rotateRight___closed__4;
|
||||
static lean_object* l_Lean_Parser_Tactic_traceState___closed__5;
|
||||
static lean_object* l_Lean_Parser_Tactic_simp___closed__1;
|
||||
|
|
@ -1085,6 +1088,7 @@ static lean_object* l_Lean_Parser_Tactic_simpa___closed__6;
|
|||
static lean_object* l_Lean_Parser_Tactic_cases___closed__2;
|
||||
static lean_object* l_Lean_Parser_Tactic_locationHyp___closed__17;
|
||||
static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticShow____1___closed__2;
|
||||
static lean_object* l_Lean_Parser_Tactic_normCastAddElim___closed__6;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_simp;
|
||||
static lean_object* l_Lean_Parser_Tactic_pushCast___closed__9;
|
||||
static lean_object* l_Lean_Parser_Tactic_split___closed__8;
|
||||
|
|
@ -1122,6 +1126,7 @@ static lean_object* l_Lean_Parser_Tactic_withAnnotateState___closed__1;
|
|||
static lean_object* l_Lean_Parser_Tactic_contradiction___closed__2;
|
||||
static lean_object* l_Lean_Parser_Tactic_discharger___closed__2;
|
||||
static lean_object* l_Lean_Parser_Tactic_letrec___closed__12;
|
||||
static lean_object* l_Lean_Parser_Tactic_normCastAddElim___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticRfl__1(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_Tactic_simpTraceArgsRest___closed__1;
|
||||
static lean_object* l_Lean_Parser_Tactic_simpLemma___closed__3;
|
||||
|
|
@ -1263,6 +1268,7 @@ static lean_object* l_Lean_Parser_Tactic_rwRuleSeq___closed__3;
|
|||
static lean_object* l_Lean_Parser_Tactic_focus___closed__6;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticSimpa_x3f_x21____1(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_omega;
|
||||
static lean_object* l_Lean_Parser_Tactic_normCastAddElim___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_clear;
|
||||
static lean_object* l_Lean_Parser_Tactic_locationHyp___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_traceState;
|
||||
|
|
@ -1278,6 +1284,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_exact;
|
|||
static lean_object* l_Lean_Parser_Tactic_traceMessage___closed__2;
|
||||
static lean_object* l_Lean_Parser_Tactic_tacticTry_____closed__3;
|
||||
static lean_object* l_Lean_Parser_Tactic_omega___closed__5;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_normCastAddElim;
|
||||
static lean_object* l_Lean_Parser_Tactic_paren___closed__2;
|
||||
static lean_object* l_Lean_Parser_Tactic_discharger___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_simpArgs;
|
||||
|
|
@ -19977,6 +19984,80 @@ x_1 = l_Lean_Parser_Tactic_pushCast___closed__14;
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Tactic_normCastAddElim___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string_from_bytes("normCastAddElim", 15);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Tactic_normCastAddElim___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_1 = l_Lean_Parser_Tactic_withAnnotateState___closed__1;
|
||||
x_2 = l_Lean_Parser_Tactic_withAnnotateState___closed__2;
|
||||
x_3 = l_Lean_Parser_Tactic_withAnnotateState___closed__3;
|
||||
x_4 = l_Lean_Parser_Tactic_normCastAddElim___closed__1;
|
||||
x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Tactic_normCastAddElim___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string_from_bytes("norm_cast_add_elim", 18);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Tactic_normCastAddElim___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Parser_Tactic_normCastAddElim___closed__3;
|
||||
x_2 = lean_alloc_ctor(5, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Tactic_normCastAddElim___closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Parser_Tactic_withAnnotateState___closed__7;
|
||||
x_2 = l_Lean_Parser_Tactic_normCastAddElim___closed__4;
|
||||
x_3 = l_Lean_Parser_Tactic_intros___closed__8;
|
||||
x_4 = lean_alloc_ctor(2, 3, 0);
|
||||
lean_ctor_set(x_4, 0, x_1);
|
||||
lean_ctor_set(x_4, 1, x_2);
|
||||
lean_ctor_set(x_4, 2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Tactic_normCastAddElim___closed__6() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Parser_Tactic_normCastAddElim___closed__2;
|
||||
x_2 = lean_unsigned_to_nat(1022u);
|
||||
x_3 = l_Lean_Parser_Tactic_normCastAddElim___closed__5;
|
||||
x_4 = lean_alloc_ctor(3, 3, 0);
|
||||
lean_ctor_set(x_4, 0, x_1);
|
||||
lean_ctor_set(x_4, 1, x_2);
|
||||
lean_ctor_set(x_4, 2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Tactic_normCastAddElim() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = l_Lean_Parser_Tactic_normCastAddElim___closed__6;
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Attr_simp___closed__1() {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -24353,6 +24434,20 @@ l_Lean_Parser_Tactic_pushCast___closed__14 = _init_l_Lean_Parser_Tactic_pushCast
|
|||
lean_mark_persistent(l_Lean_Parser_Tactic_pushCast___closed__14);
|
||||
l_Lean_Parser_Tactic_pushCast = _init_l_Lean_Parser_Tactic_pushCast();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_pushCast);
|
||||
l_Lean_Parser_Tactic_normCastAddElim___closed__1 = _init_l_Lean_Parser_Tactic_normCastAddElim___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_normCastAddElim___closed__1);
|
||||
l_Lean_Parser_Tactic_normCastAddElim___closed__2 = _init_l_Lean_Parser_Tactic_normCastAddElim___closed__2();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_normCastAddElim___closed__2);
|
||||
l_Lean_Parser_Tactic_normCastAddElim___closed__3 = _init_l_Lean_Parser_Tactic_normCastAddElim___closed__3();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_normCastAddElim___closed__3);
|
||||
l_Lean_Parser_Tactic_normCastAddElim___closed__4 = _init_l_Lean_Parser_Tactic_normCastAddElim___closed__4();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_normCastAddElim___closed__4);
|
||||
l_Lean_Parser_Tactic_normCastAddElim___closed__5 = _init_l_Lean_Parser_Tactic_normCastAddElim___closed__5();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_normCastAddElim___closed__5);
|
||||
l_Lean_Parser_Tactic_normCastAddElim___closed__6 = _init_l_Lean_Parser_Tactic_normCastAddElim___closed__6();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_normCastAddElim___closed__6);
|
||||
l_Lean_Parser_Tactic_normCastAddElim = _init_l_Lean_Parser_Tactic_normCastAddElim();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_normCastAddElim);
|
||||
l_Lean_Parser_Attr_simp___closed__1 = _init_l_Lean_Parser_Attr_simp___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_Attr_simp___closed__1);
|
||||
l_Lean_Parser_Attr_simp___closed__2 = _init_l_Lean_Parser_Attr_simp___closed__2();
|
||||
|
|
|
|||
10
stage0/stdlib/Lean/Data/Position.c
generated
10
stage0/stdlib/Lean/Data/Position.c
generated
|
|
@ -25,7 +25,6 @@ lean_object* lean_mk_empty_array_with_capacity(lean_object*);
|
|||
lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_176____closed__2;
|
||||
static lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_176____closed__13;
|
||||
lean_object* l_String_Iterator_pos(lean_object*);
|
||||
static lean_object* l_Lean_Position_instToFormatPosition___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Position_lt___closed__2;
|
||||
|
|
@ -1182,7 +1181,8 @@ x_14 = lean_alloc_ctor(0, 2, 0);
|
|||
lean_ctor_set(x_14, 0, x_6);
|
||||
lean_ctor_set(x_14, 1, x_13);
|
||||
x_15 = l_String_Iterator_nextn(x_14, x_10);
|
||||
x_16 = l_String_Iterator_pos(x_15);
|
||||
x_16 = lean_ctor_get(x_15, 1);
|
||||
lean_inc(x_16);
|
||||
lean_dec(x_15);
|
||||
return x_16;
|
||||
}
|
||||
|
|
@ -1195,7 +1195,8 @@ x_18 = lean_alloc_ctor(0, 2, 0);
|
|||
lean_ctor_set(x_18, 0, x_6);
|
||||
lean_ctor_set(x_18, 1, x_17);
|
||||
x_19 = l_String_Iterator_nextn(x_18, x_10);
|
||||
x_20 = l_String_Iterator_pos(x_19);
|
||||
x_20 = lean_ctor_get(x_19, 1);
|
||||
lean_inc(x_20);
|
||||
lean_dec(x_19);
|
||||
return x_20;
|
||||
}
|
||||
|
|
@ -1213,7 +1214,8 @@ x_23 = lean_alloc_ctor(0, 2, 0);
|
|||
lean_ctor_set(x_23, 0, x_6);
|
||||
lean_ctor_set(x_23, 1, x_22);
|
||||
x_24 = l_String_Iterator_nextn(x_23, x_21);
|
||||
x_25 = l_String_Iterator_pos(x_24);
|
||||
x_25 = lean_ctor_get(x_24, 1);
|
||||
lean_inc(x_25);
|
||||
lean_dec(x_24);
|
||||
return x_25;
|
||||
}
|
||||
|
|
|
|||
1556
stage0/stdlib/Lean/Elab/Tactic/NormCast.c
generated
1556
stage0/stdlib/Lean/Elab/Tactic/NormCast.c
generated
File diff suppressed because it is too large
Load diff
4
stage0/stdlib/Lean/Meta/Tactic/NormCast.c
generated
4
stage0/stdlib/Lean/Meta/Tactic/NormCast.c
generated
|
|
@ -5677,12 +5677,12 @@ l_Lean_Meta_NormCast_initFn____x40_Lean_Meta_Tactic_NormCast___hyg_1586____close
|
|||
lean_mark_persistent(l_Lean_Meta_NormCast_initFn____x40_Lean_Meta_Tactic_NormCast___hyg_1586____closed__7);
|
||||
l_Lean_Meta_NormCast_initFn____x40_Lean_Meta_Tactic_NormCast___hyg_1586____closed__8 = _init_l_Lean_Meta_NormCast_initFn____x40_Lean_Meta_Tactic_NormCast___hyg_1586____closed__8();
|
||||
lean_mark_persistent(l_Lean_Meta_NormCast_initFn____x40_Lean_Meta_Tactic_NormCast___hyg_1586____closed__8);
|
||||
res = l_Lean_Meta_NormCast_initFn____x40_Lean_Meta_Tactic_NormCast___hyg_1586_(lean_io_mk_world());
|
||||
if (builtin) {res = l_Lean_Meta_NormCast_initFn____x40_Lean_Meta_Tactic_NormCast___hyg_1586_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
l_Lean_Meta_NormCast_pushCastExt = lean_io_result_get_value(res);
|
||||
lean_mark_persistent(l_Lean_Meta_NormCast_pushCastExt);
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__1___closed__1 = _init_l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__1___closed__1();
|
||||
}l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__1___closed__1 = _init_l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__1___closed__1();
|
||||
l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__1___closed__2 = _init_l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__1___closed__2();
|
||||
lean_mark_persistent(l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__1___closed__2);
|
||||
l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__3___closed__1 = _init_l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__3___closed__1();
|
||||
|
|
|
|||
55
stage0/stdlib/Lean/Meta/Tactic/TryThis.c
generated
55
stage0/stdlib/Lean/Meta/Tactic/TryThis.c
generated
|
|
@ -91,6 +91,7 @@ lean_object* l_Lean_Elab_pushInfoLeaf___at_Lean_Widget_savePanelWidgetInfo___spe
|
|||
static lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Tactic_TryThis_addRewriteSuggestion___spec__1___closed__6;
|
||||
static lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Tactic_TryThis_addRewriteSuggestion___spec__1___closed__7;
|
||||
static lean_object* l_Lean_Meta_Tactic_TryThis_SuggestionStyle_asHypothesis___closed__2;
|
||||
static lean_object* l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__2;
|
||||
static lean_object* l_Std_Range_forIn_x27_loop___at_Lean_Meta_Tactic_TryThis_tryThisProvider___spec__1___closed__3;
|
||||
static lean_object* l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisWidget___closed__4;
|
||||
lean_object* l_Lean_logAt___at_Lean_Meta_computeSynthOrder___spec__7(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -143,6 +144,7 @@ static lean_object* l_Lean_Meta_Tactic_TryThis_addHaveSuggestion___closed__3;
|
|||
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonCommand____x40_Lean_Data_Lsp_Basic___hyg_1545____spec__2(size_t, size_t, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Tactic_TryThis_instInhabitedSuggestionText___closed__1;
|
||||
static lean_object* l_Lean_Meta_Tactic_TryThis_SuggestionStyle_value___closed__8;
|
||||
static lean_object* l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Tactic_TryThis_addExactSuggestions___spec__1(uint8_t, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Tactic_TryThis_getInputWidth___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Syntax_replaceM___at_Lean_Meta_Tactic_TryThis_delabToRefinableSyntax___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -250,6 +252,7 @@ lean_object* l_Lean_Syntax_node2(lean_object*, lean_object*, lean_object*, lean_
|
|||
static lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Tactic_TryThis_addSuggestions___spec__2___closed__1;
|
||||
static lean_object* l_Lean_Syntax_replaceM___at_Lean_Meta_Tactic_TryThis_replaceMVarsByUnderscores___spec__1___rarg___lambda__3___closed__4;
|
||||
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Server_addBuiltinCodeActionProvider(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Tactic_TryThis_0__Lean_Meta_Tactic_TryThis_addExactSuggestionCore___closed__4;
|
||||
static lean_object* l_Lean_Meta_Tactic_TryThis_addRewriteSuggestion___closed__11;
|
||||
static lean_object* l_Lean_Meta_Tactic_TryThis_addHaveSuggestion___closed__36;
|
||||
|
|
@ -258,6 +261,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Tactic_TryThis_addExactSuggestion___boxed(l
|
|||
LEAN_EXPORT lean_object* l_Lean_Meta_Tactic_TryThis_Suggestion_toCodeActionTitle_x3f___default;
|
||||
static lean_object* l_Lean_Meta_Tactic_TryThis_addRewriteSuggestion___closed__10;
|
||||
static lean_object* l_Lean_Meta_Tactic_TryThis_addRewriteSuggestion___lambda__2___closed__5;
|
||||
static lean_object* l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Tactic_TryThis_SuggestionStyle_warning___boxed(lean_object*);
|
||||
static lean_object* l_Lean_Meta_Tactic_TryThis_addHaveSuggestion___closed__44;
|
||||
LEAN_EXPORT lean_object* l_Lean_throwErrorAt___at_Lean_Meta_Tactic_TryThis_addSuggestions___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -442,6 +446,7 @@ uint8_t lean_nat_dec_le(lean_object*, lean_object*);
|
|||
static lean_object* l_Lean_Meta_Tactic_TryThis_SuggestionStyle_warning___closed__14;
|
||||
uint8_t lean_usize_dec_lt(size_t, size_t);
|
||||
static lean_object* l_Lean_Meta_Tactic_TryThis_SuggestionStyle_warning___closed__2;
|
||||
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Tactic_TryThis_replaceMVarsByUnderscores___spec__2___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Tactic_TryThis_addRewriteSuggestion___spec__1___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Meta_Tactic_TryThis_0__Lean_Meta_Tactic_TryThis_addSuggestionCore___spec__2___boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -1191,6 +1196,45 @@ lean_dec(x_3);
|
|||
return x_5;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string_from_bytes("tryThisProvider", 15);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
||||
x_1 = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisWidget___closed__1;
|
||||
x_2 = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisWidget___closed__2;
|
||||
x_3 = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisWidget___closed__3;
|
||||
x_4 = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisWidget___closed__4;
|
||||
x_5 = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1;
|
||||
x_6 = l_Lean_Name_mkStr5(x_1, x_2, x_3, x_4, x_5);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Meta_Tactic_TryThis_tryThisProvider___boxed), 4, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_2 = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__2;
|
||||
x_3 = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__3;
|
||||
x_4 = l_Lean_Server_addBuiltinCodeActionProvider(x_2, x_3, x_1);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT uint8_t l_Lean_Meta_Tactic_TryThis_getIndentAndColumn___lambda__1(uint32_t x_1) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -9391,7 +9435,16 @@ l_Std_Range_forIn_x27_loop___at_Lean_Meta_Tactic_TryThis_tryThisProvider___spec_
|
|||
lean_mark_persistent(l_Std_Range_forIn_x27_loop___at_Lean_Meta_Tactic_TryThis_tryThisProvider___spec__1___closed__4);
|
||||
l_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1 = _init_l_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1();
|
||||
lean_mark_persistent(l_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1);
|
||||
l_Lean_Meta_Tactic_TryThis_getIndentAndColumn___closed__1 = _init_l_Lean_Meta_Tactic_TryThis_getIndentAndColumn___closed__1();
|
||||
l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1 = _init_l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1);
|
||||
l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__2 = _init_l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__2();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__2);
|
||||
l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__3 = _init_l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__3();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__3);
|
||||
if (builtin) {res = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
}l_Lean_Meta_Tactic_TryThis_getIndentAndColumn___closed__1 = _init_l_Lean_Meta_Tactic_TryThis_getIndentAndColumn___closed__1();
|
||||
lean_mark_persistent(l_Lean_Meta_Tactic_TryThis_getIndentAndColumn___closed__1);
|
||||
l_Lean_Syntax_replaceM___at_Lean_Meta_Tactic_TryThis_replaceMVarsByUnderscores___spec__1___rarg___lambda__3___closed__1 = _init_l_Lean_Syntax_replaceM___at_Lean_Meta_Tactic_TryThis_replaceMVarsByUnderscores___spec__1___rarg___lambda__3___closed__1();
|
||||
lean_mark_persistent(l_Lean_Syntax_replaceM___at_Lean_Meta_Tactic_TryThis_replaceMVarsByUnderscores___spec__1___rarg___lambda__3___closed__1);
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue