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:
Gabriel Ebner 2022-09-16 14:35:09 +02:00 • committed by Leonardo de Moura
parent 193a18e4e3
commit ca4dfa5627
32 changed files with 11711 additions and 14082 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
stage0/src/Init/Conv.lean generated
View file

@ -17,8 +17,8 @@ It is mainly used for doing targeted term transformations, for example rewriting
only on the left side of an equality. -/
declare_syntax_cat conv (behavior := both)
syntax convSeq1Indented := withPosition((colGe conv ";"?)+)
syntax convSeqBracketed := "{" (conv ";"?)* "}"
syntax convSeq1Indented := sepBy1IndentSemicolon(conv)
syntax convSeqBracketed := "{" sepByIndentSemicolon(conv) "}"
-- Order is important: a missing `conv` proof should not be parsed as `{ <missing> }`,
-- automatically closing goals
syntax convSeq := convSeqBracketed <|> convSeq1Indented

12
stage0/src/Lean/Elab/Tactic/BuiltinTactic.lean generated
View file

@ -69,12 +69,6 @@ where
/-- Evaluate `sepByIndent tactic "; " -/
def evalSepByIndentTactic (stx : Syntax) : TacticM Unit := do
-- HACK: bootstrapping hack to support (group tac ";") nodes
if stx[0].getKind == groupKind then
for seqElem in stx.getArgs do
evalTactic seqElem
return
for seqElem in (← addCheckpoints (stx.getSepArgs.map (⟨·⟩))) do
evalTactic seqElem
@ -380,10 +374,4 @@ where
| none => throwIllFormedSyntax
| some ms => IO.sleep ms.toUInt32
-- HACK: support (group tac ";") quotations from the previous stage.
-- Unfortuntely, parseQuotWithCurrentStage is not powerful enough to make this
-- unnecessary as it does not affect parser aliases.
@[builtinTactic group] def evalGroup : Tactic := fun stx =>
evalTactic stx[0]
end Lean.Elab.Tactic

8
stage0/src/Lean/Elab/Tactic/Conv/Basic.lean generated
View file

@ -86,16 +86,16 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
changeLhs (← zetaReduce (← getLhs))
@[builtinTactic Lean.Parser.Tactic.Conv.convSeq1Indented] def evalConvSeq1Indented : Tactic := fun stx => do
for seqElem in stx[0].getArgs do
evalTactic seqElem[0]
for seqElem in stx[0].getSepArgs do
evalTactic seqElem
@[builtinTactic Lean.Parser.Tactic.Conv.convSeqBracketed] def evalConvSeqBracketed : Tactic := fun stx => do
let initInfo ← mkInitialTacticInfo stx[0]
withRef stx[2] <| closeUsingOrAdmit do
-- save state before/after entering focus on `{`
withInfoContext (pure ()) initInfo
for seqElem in stx[1].getArgs do
evalTactic seqElem[0]
for seqElem in stx[1].getSepArgs do
evalTactic seqElem
evalTactic (← `(tactic| all_goals (try rfl)))
@[builtinTactic Lean.Parser.Tactic.Conv.nestedConv] def evalNestedConv : Tactic := fun stx => do

3394
stage0/stdlib/Init/Conv.c generated
View file

File diff suppressed because it is too large Load diff

800
stage0/stdlib/Init/Data/Array/Mem.c generated
View file

@ -790,7 +790,7 @@ x_8 = l_Lean_MonadRef_mkInfoFromRefPos___at___aux__Init__Notation______macroRule
x_9 = !lean_is_exclusive(x_8);
if (x_9 == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125;
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116;
x_10 = lean_ctor_get(x_8, 0);
x_11 = lean_ctor_get(x_2, 2);
lean_inc(x_11);
@ -845,510 +845,458 @@ lean_ctor_set(x_31, 2, x_30);
x_32 = lean_array_push(x_24, x_28);
lean_inc(x_31);
x_33 = lean_array_push(x_32, x_31);
x_34 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__14;
lean_inc(x_10);
x_35 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_35, 0, x_10);
lean_ctor_set(x_35, 1, x_34);
lean_ctor_set(x_35, 2, x_33);
x_36 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__31;
x_37 = lean_array_push(x_36, x_35);
x_34 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_34, 0, x_10);
lean_ctor_set(x_34, 1, x_29);
lean_ctor_set(x_34, 2, x_33);
x_35 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__31;
x_36 = lean_array_push(x_35, x_34);
x_37 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__19;
lean_inc(x_10);
x_38 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_38, 0, x_10);
lean_ctor_set(x_38, 1, x_29);
lean_ctor_set(x_38, 2, x_37);
x_39 = lean_array_push(x_36, x_38);
x_40 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__19;
lean_ctor_set(x_38, 1, x_37);
lean_ctor_set(x_38, 2, x_36);
x_39 = lean_array_push(x_35, x_38);
x_40 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__17;
lean_inc(x_10);
x_41 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_41, 0, x_10);
lean_ctor_set(x_41, 1, x_40);
lean_ctor_set(x_41, 2, x_39);
x_42 = lean_array_push(x_36, x_41);
x_43 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__17;
x_42 = lean_array_push(x_24, x_16);
lean_inc(x_42);
x_43 = lean_array_push(x_42, x_41);
x_44 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__14;
lean_inc(x_10);
x_44 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_44, 0, x_10);
lean_ctor_set(x_44, 1, x_43);
lean_ctor_set(x_44, 2, x_42);
x_45 = lean_array_push(x_24, x_16);
lean_inc(x_45);
x_46 = lean_array_push(x_45, x_44);
x_45 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_45, 0, x_10);
lean_ctor_set(x_45, 1, x_44);
lean_ctor_set(x_45, 2, x_43);
x_46 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__42;
x_47 = l_Lean_addMacroScope(x_12, x_46, x_11);
x_48 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__38;
x_49 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__44;
lean_inc(x_10);
x_47 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_47, 0, x_10);
lean_ctor_set(x_47, 1, x_34);
lean_ctor_set(x_47, 2, x_46);
x_48 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__42;
x_49 = l_Lean_addMacroScope(x_12, x_48, x_11);
x_50 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__38;
x_51 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__44;
x_50 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_50, 0, x_10);
lean_ctor_set(x_50, 1, x_48);
lean_ctor_set(x_50, 2, x_47);
lean_ctor_set(x_50, 3, x_49);
x_51 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__47;
lean_inc(x_10);
x_52 = lean_alloc_ctor(3, 4, 0);
x_52 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_52, 0, x_10);
lean_ctor_set(x_52, 1, x_50);
lean_ctor_set(x_52, 2, x_49);
lean_ctor_set(x_52, 3, x_51);
x_53 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__47;
lean_ctor_set(x_52, 1, x_51);
x_53 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__50;
lean_inc(x_10);
x_54 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_54, 0, x_10);
lean_ctor_set(x_54, 1, x_53);
x_55 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__50;
x_55 = lean_array_push(x_35, x_54);
x_56 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__49;
lean_inc(x_10);
x_56 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_56, 0, x_10);
lean_ctor_set(x_56, 1, x_55);
x_57 = lean_array_push(x_36, x_56);
x_58 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__49;
x_57 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_57, 0, x_10);
lean_ctor_set(x_57, 1, x_56);
lean_ctor_set(x_57, 2, x_55);
x_58 = lean_array_push(x_35, x_57);
lean_inc(x_10);
x_59 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_59, 0, x_10);
lean_ctor_set(x_59, 1, x_58);
lean_ctor_set(x_59, 2, x_57);
x_60 = lean_array_push(x_36, x_59);
lean_ctor_set(x_59, 1, x_29);
lean_ctor_set(x_59, 2, x_58);
x_60 = lean_array_push(x_24, x_23);
x_61 = lean_array_push(x_60, x_59);
x_62 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__35;
lean_inc(x_10);
x_61 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_61, 0, x_10);
lean_ctor_set(x_61, 1, x_29);
lean_ctor_set(x_61, 2, x_60);
x_62 = lean_array_push(x_24, x_23);
x_63 = lean_array_push(x_62, x_61);
x_64 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__35;
lean_inc(x_10);
x_65 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_65, 0, x_10);
lean_ctor_set(x_65, 1, x_64);
lean_ctor_set(x_65, 2, x_63);
x_66 = lean_array_push(x_24, x_65);
x_63 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_63, 0, x_10);
lean_ctor_set(x_63, 1, x_62);
lean_ctor_set(x_63, 2, x_61);
x_64 = lean_array_push(x_24, x_63);
lean_inc(x_31);
x_67 = lean_array_push(x_66, x_31);
x_65 = lean_array_push(x_64, x_31);
lean_inc(x_10);
x_68 = lean_alloc_ctor(1, 3, 0);
x_66 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_66, 0, x_10);
lean_ctor_set(x_66, 1, x_29);
lean_ctor_set(x_66, 2, x_65);
x_67 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__51;
lean_inc(x_10);
x_68 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_68, 0, x_10);
lean_ctor_set(x_68, 1, x_29);
lean_ctor_set(x_68, 2, x_67);
x_69 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__51;
lean_ctor_set(x_68, 1, x_67);
x_69 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__52;
x_70 = lean_array_push(x_69, x_52);
x_71 = lean_array_push(x_70, x_66);
x_72 = lean_array_push(x_71, x_68);
x_73 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__46;
lean_inc(x_10);
x_70 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_70, 0, x_10);
lean_ctor_set(x_70, 1, x_69);
x_71 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__52;
x_72 = lean_array_push(x_71, x_54);
x_73 = lean_array_push(x_72, x_68);
x_74 = lean_array_push(x_73, x_70);
x_75 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__46;
x_74 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_74, 0, x_10);
lean_ctor_set(x_74, 1, x_73);
lean_ctor_set(x_74, 2, x_72);
x_75 = lean_array_push(x_35, x_74);
lean_inc(x_10);
x_76 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_76, 0, x_10);
lean_ctor_set(x_76, 1, x_75);
lean_ctor_set(x_76, 2, x_74);
x_77 = lean_array_push(x_36, x_76);
lean_ctor_set(x_76, 1, x_29);
lean_ctor_set(x_76, 2, x_75);
x_77 = lean_array_push(x_24, x_50);
x_78 = lean_array_push(x_77, x_76);
lean_inc(x_10);
x_78 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_78, 0, x_10);
lean_ctor_set(x_78, 1, x_29);
lean_ctor_set(x_78, 2, x_77);
x_79 = lean_array_push(x_24, x_52);
x_80 = lean_array_push(x_79, x_78);
x_79 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_79, 0, x_10);
lean_ctor_set(x_79, 1, x_62);
lean_ctor_set(x_79, 2, x_78);
x_80 = lean_array_push(x_25, x_79);
lean_inc(x_10);
x_81 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_81, 0, x_10);
lean_ctor_set(x_81, 1, x_64);
lean_ctor_set(x_81, 1, x_27);
lean_ctor_set(x_81, 2, x_80);
x_82 = lean_array_push(x_25, x_81);
x_82 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__53;
lean_inc(x_10);
x_83 = lean_alloc_ctor(1, 3, 0);
x_83 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_83, 0, x_10);
lean_ctor_set(x_83, 1, x_27);
lean_ctor_set(x_83, 2, x_82);
x_84 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__53;
lean_ctor_set(x_83, 1, x_82);
x_84 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__56;
lean_inc(x_10);
x_85 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_85, 0, x_10);
lean_ctor_set(x_85, 1, x_84);
x_86 = lean_array_push(x_36, x_85);
x_86 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__57;
x_87 = lean_array_push(x_86, x_85);
lean_inc(x_31);
x_88 = lean_array_push(x_87, x_31);
lean_inc(x_31);
x_89 = lean_array_push(x_88, x_31);
lean_inc(x_31);
x_90 = lean_array_push(x_89, x_31);
lean_inc(x_31);
x_91 = lean_array_push(x_90, x_31);
x_92 = lean_array_push(x_91, x_31);
x_93 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__55;
lean_inc(x_10);
x_87 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_87, 0, x_10);
lean_ctor_set(x_87, 1, x_29);
lean_ctor_set(x_87, 2, x_86);
x_88 = lean_array_push(x_24, x_83);
x_89 = lean_array_push(x_88, x_87);
x_94 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_94, 0, x_10);
lean_ctor_set(x_94, 1, x_93);
lean_ctor_set(x_94, 2, x_92);
x_95 = lean_array_push(x_69, x_81);
x_96 = lean_array_push(x_95, x_83);
x_97 = lean_array_push(x_96, x_94);
lean_inc(x_10);
x_90 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_90, 0, x_10);
lean_ctor_set(x_90, 1, x_34);
lean_ctor_set(x_90, 2, x_89);
x_91 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__56;
x_98 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_98, 0, x_10);
lean_ctor_set(x_98, 1, x_29);
lean_ctor_set(x_98, 2, x_97);
x_99 = lean_array_push(x_35, x_98);
lean_inc(x_10);
x_92 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_92, 0, x_10);
lean_ctor_set(x_92, 1, x_91);
x_93 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__57;
x_94 = lean_array_push(x_93, x_92);
lean_inc(x_31);
x_95 = lean_array_push(x_94, x_31);
lean_inc(x_31);
x_96 = lean_array_push(x_95, x_31);
lean_inc(x_31);
x_97 = lean_array_push(x_96, x_31);
lean_inc(x_31);
x_98 = lean_array_push(x_97, x_31);
lean_inc(x_31);
x_99 = lean_array_push(x_98, x_31);
x_100 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__55;
x_100 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_100, 0, x_10);
lean_ctor_set(x_100, 1, x_37);
lean_ctor_set(x_100, 2, x_99);
x_101 = lean_array_push(x_35, x_100);
lean_inc(x_10);
x_101 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_101, 0, x_10);
lean_ctor_set(x_101, 1, x_100);
lean_ctor_set(x_101, 2, x_99);
x_102 = lean_array_push(x_24, x_101);
x_103 = lean_array_push(x_102, x_31);
x_102 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_102, 0, x_10);
lean_ctor_set(x_102, 1, x_40);
lean_ctor_set(x_102, 2, x_101);
x_103 = lean_array_push(x_42, x_102);
lean_inc(x_10);
x_104 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_104, 0, x_10);
lean_ctor_set(x_104, 1, x_34);
lean_ctor_set(x_104, 1, x_44);
lean_ctor_set(x_104, 2, x_103);
x_105 = lean_array_push(x_24, x_90);
x_105 = lean_array_push(x_24, x_45);
x_106 = lean_array_push(x_105, x_104);
lean_inc(x_10);
x_107 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_107, 0, x_10);
lean_ctor_set(x_107, 1, x_29);
lean_ctor_set(x_107, 2, x_106);
x_108 = lean_array_push(x_36, x_107);
lean_inc(x_10);
x_109 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_109, 0, x_10);
lean_ctor_set(x_109, 1, x_40);
lean_ctor_set(x_109, 2, x_108);
x_110 = lean_array_push(x_36, x_109);
x_108 = lean_array_push(x_24, x_14);
x_109 = lean_array_push(x_108, x_107);
x_110 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__12;
lean_inc(x_10);
x_111 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_111, 0, x_10);
lean_ctor_set(x_111, 1, x_43);
lean_ctor_set(x_111, 2, x_110);
x_112 = lean_array_push(x_45, x_111);
lean_ctor_set(x_111, 1, x_110);
lean_ctor_set(x_111, 2, x_109);
x_112 = lean_array_push(x_35, x_111);
lean_inc(x_10);
x_113 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_113, 0, x_10);
lean_ctor_set(x_113, 1, x_34);
lean_ctor_set(x_113, 1, x_29);
lean_ctor_set(x_113, 2, x_112);
x_114 = lean_array_push(x_24, x_47);
x_115 = lean_array_push(x_114, x_113);
lean_inc(x_10);
x_114 = lean_array_push(x_35, x_113);
x_115 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__8;
x_116 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_116, 0, x_10);
lean_ctor_set(x_116, 1, x_29);
lean_ctor_set(x_116, 2, x_115);
x_117 = lean_array_push(x_24, x_14);
x_118 = lean_array_push(x_117, x_116);
x_119 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__12;
lean_inc(x_10);
x_120 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_120, 0, x_10);
lean_ctor_set(x_120, 1, x_119);
lean_ctor_set(x_120, 2, x_118);
x_121 = lean_array_push(x_36, x_120);
lean_inc(x_10);
x_122 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_122, 0, x_10);
lean_ctor_set(x_122, 1, x_29);
lean_ctor_set(x_122, 2, x_121);
x_123 = lean_array_push(x_36, x_122);
x_124 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__8;
x_125 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_125, 0, x_10);
lean_ctor_set(x_125, 1, x_124);
lean_ctor_set(x_125, 2, x_123);
lean_ctor_set(x_8, 0, x_125);
lean_ctor_set(x_116, 1, x_115);
lean_ctor_set(x_116, 2, x_114);
lean_ctor_set(x_8, 0, x_116);
return x_8;
}
else
{
lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166; lean_object* x_167; lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_171; lean_object* x_172; lean_object* x_173; lean_object* x_174; lean_object* x_175; lean_object* x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; lean_object* x_180; lean_object* x_181; lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_185; lean_object* x_186; lean_object* x_187; lean_object* x_188; lean_object* x_189; lean_object* x_190; lean_object* x_191; lean_object* x_192; lean_object* x_193; lean_object* x_194; lean_object* x_195; lean_object* x_196; lean_object* x_197; lean_object* x_198; lean_object* x_199; lean_object* x_200; lean_object* x_201; lean_object* x_202; lean_object* x_203; lean_object* x_204; lean_object* x_205; lean_object* x_206; lean_object* x_207; lean_object* x_208; lean_object* x_209; lean_object* x_210; lean_object* x_211; lean_object* x_212; lean_object* x_213; lean_object* x_214; lean_object* x_215; lean_object* x_216; lean_object* x_217; lean_object* x_218; lean_object* x_219; lean_object* x_220; lean_object* x_221; lean_object* x_222; lean_object* x_223; lean_object* x_224; lean_object* x_225; lean_object* x_226; lean_object* x_227; lean_object* x_228; lean_object* x_229; lean_object* x_230; lean_object* x_231; lean_object* x_232; lean_object* x_233; lean_object* x_234; lean_object* x_235; lean_object* x_236; lean_object* x_237; lean_object* x_238; lean_object* x_239; lean_object* x_240; lean_object* x_241; lean_object* x_242; lean_object* x_243;
x_126 = lean_ctor_get(x_8, 0);
x_127 = lean_ctor_get(x_8, 1);
lean_inc(x_127);
lean_inc(x_126);
lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166; lean_object* x_167; lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_171; lean_object* x_172; lean_object* x_173; lean_object* x_174; lean_object* x_175; lean_object* x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; lean_object* x_180; lean_object* x_181; lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_185; lean_object* x_186; lean_object* x_187; lean_object* x_188; lean_object* x_189; lean_object* x_190; lean_object* x_191; lean_object* x_192; lean_object* x_193; lean_object* x_194; lean_object* x_195; lean_object* x_196; lean_object* x_197; lean_object* x_198; lean_object* x_199; lean_object* x_200; lean_object* x_201; lean_object* x_202; lean_object* x_203; lean_object* x_204; lean_object* x_205; lean_object* x_206; lean_object* x_207; lean_object* x_208; lean_object* x_209; lean_object* x_210; lean_object* x_211; lean_object* x_212; lean_object* x_213; lean_object* x_214; lean_object* x_215; lean_object* x_216; lean_object* x_217; lean_object* x_218; lean_object* x_219; lean_object* x_220; lean_object* x_221; lean_object* x_222; lean_object* x_223; lean_object* x_224; lean_object* x_225;
x_117 = lean_ctor_get(x_8, 0);
x_118 = lean_ctor_get(x_8, 1);
lean_inc(x_118);
lean_inc(x_117);
lean_dec(x_8);
x_128 = lean_ctor_get(x_2, 2);
lean_inc(x_128);
x_129 = lean_ctor_get(x_2, 1);
lean_inc(x_129);
x_119 = lean_ctor_get(x_2, 2);
lean_inc(x_119);
x_120 = lean_ctor_get(x_2, 1);
lean_inc(x_120);
lean_dec(x_2);
x_130 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__11;
lean_inc(x_126);
x_131 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_131, 0, x_126);
lean_ctor_set(x_131, 1, x_130);
x_132 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__15;
lean_inc(x_126);
x_133 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_133, 0, x_126);
lean_ctor_set(x_133, 1, x_132);
x_134 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__20;
lean_inc(x_126);
x_135 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_135, 0, x_126);
lean_ctor_set(x_135, 1, x_134);
x_136 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__25;
lean_inc(x_128);
lean_inc(x_129);
x_137 = l_Lean_addMacroScope(x_129, x_136, x_128);
x_138 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__24;
x_139 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__28;
lean_inc(x_126);
x_140 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_140, 0, x_126);
lean_ctor_set(x_140, 1, x_138);
lean_ctor_set(x_140, 2, x_137);
lean_ctor_set(x_140, 3, x_139);
x_141 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__29;
x_142 = lean_array_push(x_141, x_135);
lean_inc(x_140);
lean_inc(x_142);
x_143 = lean_array_push(x_142, x_140);
x_144 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__21;
lean_inc(x_126);
x_145 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_145, 0, x_126);
lean_ctor_set(x_145, 1, x_144);
lean_ctor_set(x_145, 2, x_143);
x_146 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__10;
x_147 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__30;
lean_inc(x_126);
x_148 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_148, 0, x_126);
lean_ctor_set(x_148, 1, x_146);
lean_ctor_set(x_148, 2, x_147);
x_149 = lean_array_push(x_141, x_145);
lean_inc(x_148);
x_150 = lean_array_push(x_149, x_148);
x_151 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__14;
lean_inc(x_126);
x_152 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_152, 0, x_126);
lean_ctor_set(x_152, 1, x_151);
lean_ctor_set(x_152, 2, x_150);
x_153 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__31;
x_154 = lean_array_push(x_153, x_152);
lean_inc(x_126);
x_155 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_155, 0, x_126);
lean_ctor_set(x_155, 1, x_146);
lean_ctor_set(x_155, 2, x_154);
x_156 = lean_array_push(x_153, x_155);
x_157 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__19;
lean_inc(x_126);
x_158 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_158, 0, x_126);
lean_ctor_set(x_158, 1, x_157);
lean_ctor_set(x_158, 2, x_156);
x_159 = lean_array_push(x_153, x_158);
x_160 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__17;
lean_inc(x_126);
x_161 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_161, 0, x_126);
lean_ctor_set(x_161, 1, x_160);
lean_ctor_set(x_161, 2, x_159);
x_162 = lean_array_push(x_141, x_133);
lean_inc(x_162);
x_163 = lean_array_push(x_162, x_161);
lean_inc(x_126);
x_164 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_164, 0, x_126);
lean_ctor_set(x_164, 1, x_151);
lean_ctor_set(x_164, 2, x_163);
x_165 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__42;
x_166 = l_Lean_addMacroScope(x_129, x_165, x_128);
x_167 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__38;
x_168 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__44;
lean_inc(x_126);
x_169 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_169, 0, x_126);
lean_ctor_set(x_169, 1, x_167);
lean_ctor_set(x_169, 2, x_166);
lean_ctor_set(x_169, 3, x_168);
x_170 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__47;
lean_inc(x_126);
x_171 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_171, 0, x_126);
x_121 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__11;
lean_inc(x_117);
x_122 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_122, 0, x_117);
lean_ctor_set(x_122, 1, x_121);
x_123 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__15;
lean_inc(x_117);
x_124 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_124, 0, x_117);
lean_ctor_set(x_124, 1, x_123);
x_125 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__20;
lean_inc(x_117);
x_126 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_126, 0, x_117);
lean_ctor_set(x_126, 1, x_125);
x_127 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__25;
lean_inc(x_119);
lean_inc(x_120);
x_128 = l_Lean_addMacroScope(x_120, x_127, x_119);
x_129 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__24;
x_130 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__28;
lean_inc(x_117);
x_131 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_131, 0, x_117);
lean_ctor_set(x_131, 1, x_129);
lean_ctor_set(x_131, 2, x_128);
lean_ctor_set(x_131, 3, x_130);
x_132 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__29;
x_133 = lean_array_push(x_132, x_126);
lean_inc(x_131);
lean_inc(x_133);
x_134 = lean_array_push(x_133, x_131);
x_135 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__21;
lean_inc(x_117);
x_136 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_136, 0, x_117);
lean_ctor_set(x_136, 1, x_135);
lean_ctor_set(x_136, 2, x_134);
x_137 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__10;
x_138 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__30;
lean_inc(x_117);
x_139 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_139, 0, x_117);
lean_ctor_set(x_139, 1, x_137);
lean_ctor_set(x_139, 2, x_138);
x_140 = lean_array_push(x_132, x_136);
lean_inc(x_139);
x_141 = lean_array_push(x_140, x_139);
lean_inc(x_117);
x_142 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_142, 0, x_117);
lean_ctor_set(x_142, 1, x_137);
lean_ctor_set(x_142, 2, x_141);
x_143 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__31;
x_144 = lean_array_push(x_143, x_142);
x_145 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__19;
lean_inc(x_117);
x_146 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_146, 0, x_117);
lean_ctor_set(x_146, 1, x_145);
lean_ctor_set(x_146, 2, x_144);
x_147 = lean_array_push(x_143, x_146);
x_148 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__17;
lean_inc(x_117);
x_149 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_149, 0, x_117);
lean_ctor_set(x_149, 1, x_148);
lean_ctor_set(x_149, 2, x_147);
x_150 = lean_array_push(x_132, x_124);
lean_inc(x_150);
x_151 = lean_array_push(x_150, x_149);
x_152 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__14;
lean_inc(x_117);
x_153 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_153, 0, x_117);
lean_ctor_set(x_153, 1, x_152);
lean_ctor_set(x_153, 2, x_151);
x_154 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__42;
x_155 = l_Lean_addMacroScope(x_120, x_154, x_119);
x_156 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__38;
x_157 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__44;
lean_inc(x_117);
x_158 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_158, 0, x_117);
lean_ctor_set(x_158, 1, x_156);
lean_ctor_set(x_158, 2, x_155);
lean_ctor_set(x_158, 3, x_157);
x_159 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__47;
lean_inc(x_117);
x_160 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_160, 0, x_117);
lean_ctor_set(x_160, 1, x_159);
x_161 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__50;
lean_inc(x_117);
x_162 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_162, 0, x_117);
lean_ctor_set(x_162, 1, x_161);
x_163 = lean_array_push(x_143, x_162);
x_164 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__49;
lean_inc(x_117);
x_165 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_165, 0, x_117);
lean_ctor_set(x_165, 1, x_164);
lean_ctor_set(x_165, 2, x_163);
x_166 = lean_array_push(x_143, x_165);
lean_inc(x_117);
x_167 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_167, 0, x_117);
lean_ctor_set(x_167, 1, x_137);
lean_ctor_set(x_167, 2, x_166);
x_168 = lean_array_push(x_132, x_131);
x_169 = lean_array_push(x_168, x_167);
x_170 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__35;
lean_inc(x_117);
x_171 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_171, 0, x_117);
lean_ctor_set(x_171, 1, x_170);
x_172 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__50;
lean_inc(x_126);
x_173 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_173, 0, x_126);
lean_ctor_set(x_173, 1, x_172);
x_174 = lean_array_push(x_153, x_173);
x_175 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__49;
lean_inc(x_126);
x_176 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_176, 0, x_126);
lean_ctor_set(x_171, 2, x_169);
x_172 = lean_array_push(x_132, x_171);
lean_inc(x_139);
x_173 = lean_array_push(x_172, x_139);
lean_inc(x_117);
x_174 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_174, 0, x_117);
lean_ctor_set(x_174, 1, x_137);
lean_ctor_set(x_174, 2, x_173);
x_175 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__51;
lean_inc(x_117);
x_176 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_176, 0, x_117);
lean_ctor_set(x_176, 1, x_175);
lean_ctor_set(x_176, 2, x_174);
x_177 = lean_array_push(x_153, x_176);
lean_inc(x_126);
x_178 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_178, 0, x_126);
lean_ctor_set(x_178, 1, x_146);
lean_ctor_set(x_178, 2, x_177);
x_179 = lean_array_push(x_141, x_140);
x_180 = lean_array_push(x_179, x_178);
x_181 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__35;
lean_inc(x_126);
x_177 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__52;
x_178 = lean_array_push(x_177, x_160);
x_179 = lean_array_push(x_178, x_174);
x_180 = lean_array_push(x_179, x_176);
x_181 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__46;
lean_inc(x_117);
x_182 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_182, 0, x_126);
lean_ctor_set(x_182, 0, x_117);
lean_ctor_set(x_182, 1, x_181);
lean_ctor_set(x_182, 2, x_180);
x_183 = lean_array_push(x_141, x_182);
lean_inc(x_148);
x_184 = lean_array_push(x_183, x_148);
lean_inc(x_126);
x_185 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_185, 0, x_126);
lean_ctor_set(x_185, 1, x_146);
lean_ctor_set(x_185, 2, x_184);
x_186 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__51;
lean_inc(x_126);
x_187 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_187, 0, x_126);
lean_ctor_set(x_187, 1, x_186);
x_188 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__52;
x_189 = lean_array_push(x_188, x_171);
x_190 = lean_array_push(x_189, x_185);
x_191 = lean_array_push(x_190, x_187);
x_192 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__46;
lean_inc(x_126);
x_193 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_193, 0, x_126);
x_183 = lean_array_push(x_143, x_182);
lean_inc(x_117);
x_184 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_184, 0, x_117);
lean_ctor_set(x_184, 1, x_137);
lean_ctor_set(x_184, 2, x_183);
x_185 = lean_array_push(x_132, x_158);
x_186 = lean_array_push(x_185, x_184);
lean_inc(x_117);
x_187 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_187, 0, x_117);
lean_ctor_set(x_187, 1, x_170);
lean_ctor_set(x_187, 2, x_186);
x_188 = lean_array_push(x_133, x_187);
lean_inc(x_117);
x_189 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_189, 0, x_117);
lean_ctor_set(x_189, 1, x_135);
lean_ctor_set(x_189, 2, x_188);
x_190 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__53;
lean_inc(x_117);
x_191 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_191, 0, x_117);
lean_ctor_set(x_191, 1, x_190);
x_192 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__56;
lean_inc(x_117);
x_193 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_193, 0, x_117);
lean_ctor_set(x_193, 1, x_192);
lean_ctor_set(x_193, 2, x_191);
x_194 = lean_array_push(x_153, x_193);
lean_inc(x_126);
x_195 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_195, 0, x_126);
lean_ctor_set(x_195, 1, x_146);
lean_ctor_set(x_195, 2, x_194);
x_196 = lean_array_push(x_141, x_169);
x_197 = lean_array_push(x_196, x_195);
lean_inc(x_126);
x_198 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_198, 0, x_126);
lean_ctor_set(x_198, 1, x_181);
lean_ctor_set(x_198, 2, x_197);
x_199 = lean_array_push(x_142, x_198);
lean_inc(x_126);
x_200 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_200, 0, x_126);
lean_ctor_set(x_200, 1, x_144);
lean_ctor_set(x_200, 2, x_199);
x_201 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__53;
lean_inc(x_126);
x_202 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_202, 0, x_126);
x_194 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__57;
x_195 = lean_array_push(x_194, x_193);
lean_inc(x_139);
x_196 = lean_array_push(x_195, x_139);
lean_inc(x_139);
x_197 = lean_array_push(x_196, x_139);
lean_inc(x_139);
x_198 = lean_array_push(x_197, x_139);
lean_inc(x_139);
x_199 = lean_array_push(x_198, x_139);
x_200 = lean_array_push(x_199, x_139);
x_201 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__55;
lean_inc(x_117);
x_202 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_202, 0, x_117);
lean_ctor_set(x_202, 1, x_201);
x_203 = lean_array_push(x_153, x_202);
lean_inc(x_126);
x_204 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_204, 0, x_126);
lean_ctor_set(x_204, 1, x_146);
lean_ctor_set(x_204, 2, x_203);
x_205 = lean_array_push(x_141, x_200);
x_206 = lean_array_push(x_205, x_204);
lean_inc(x_126);
x_207 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_207, 0, x_126);
lean_ctor_set(x_207, 1, x_151);
lean_ctor_set(x_207, 2, x_206);
x_208 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__56;
lean_inc(x_126);
x_209 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_209, 0, x_126);
lean_ctor_set(x_209, 1, x_208);
x_210 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__57;
x_211 = lean_array_push(x_210, x_209);
lean_inc(x_148);
x_212 = lean_array_push(x_211, x_148);
lean_inc(x_148);
x_213 = lean_array_push(x_212, x_148);
lean_inc(x_148);
x_214 = lean_array_push(x_213, x_148);
lean_inc(x_148);
x_215 = lean_array_push(x_214, x_148);
lean_inc(x_148);
x_216 = lean_array_push(x_215, x_148);
x_217 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__55;
lean_inc(x_126);
x_218 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_218, 0, x_126);
lean_ctor_set(x_218, 1, x_217);
lean_ctor_set(x_218, 2, x_216);
x_219 = lean_array_push(x_141, x_218);
x_220 = lean_array_push(x_219, x_148);
lean_inc(x_126);
lean_ctor_set(x_202, 2, x_200);
x_203 = lean_array_push(x_177, x_189);
x_204 = lean_array_push(x_203, x_191);
x_205 = lean_array_push(x_204, x_202);
lean_inc(x_117);
x_206 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_206, 0, x_117);
lean_ctor_set(x_206, 1, x_137);
lean_ctor_set(x_206, 2, x_205);
x_207 = lean_array_push(x_143, x_206);
lean_inc(x_117);
x_208 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_208, 0, x_117);
lean_ctor_set(x_208, 1, x_145);
lean_ctor_set(x_208, 2, x_207);
x_209 = lean_array_push(x_143, x_208);
lean_inc(x_117);
x_210 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_210, 0, x_117);
lean_ctor_set(x_210, 1, x_148);
lean_ctor_set(x_210, 2, x_209);
x_211 = lean_array_push(x_150, x_210);
lean_inc(x_117);
x_212 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_212, 0, x_117);
lean_ctor_set(x_212, 1, x_152);
lean_ctor_set(x_212, 2, x_211);
x_213 = lean_array_push(x_132, x_153);
x_214 = lean_array_push(x_213, x_212);
lean_inc(x_117);
x_215 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_215, 0, x_117);
lean_ctor_set(x_215, 1, x_137);
lean_ctor_set(x_215, 2, x_214);
x_216 = lean_array_push(x_132, x_122);
x_217 = lean_array_push(x_216, x_215);
x_218 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__12;
lean_inc(x_117);
x_219 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_219, 0, x_117);
lean_ctor_set(x_219, 1, x_218);
lean_ctor_set(x_219, 2, x_217);
x_220 = lean_array_push(x_143, x_219);
lean_inc(x_117);
x_221 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_221, 0, x_126);
lean_ctor_set(x_221, 1, x_151);
lean_ctor_set(x_221, 0, x_117);
lean_ctor_set(x_221, 1, x_137);
lean_ctor_set(x_221, 2, x_220);
x_222 = lean_array_push(x_141, x_207);
x_223 = lean_array_push(x_222, x_221);
lean_inc(x_126);
x_222 = lean_array_push(x_143, x_221);
x_223 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__8;
x_224 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_224, 0, x_126);
lean_ctor_set(x_224, 1, x_146);
lean_ctor_set(x_224, 2, x_223);
x_225 = lean_array_push(x_153, x_224);
lean_inc(x_126);
x_226 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_226, 0, x_126);
lean_ctor_set(x_226, 1, x_157);
lean_ctor_set(x_226, 2, x_225);
x_227 = lean_array_push(x_153, x_226);
lean_inc(x_126);
x_228 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_228, 0, x_126);
lean_ctor_set(x_228, 1, x_160);
lean_ctor_set(x_228, 2, x_227);
x_229 = lean_array_push(x_162, x_228);
lean_inc(x_126);
x_230 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_230, 0, x_126);
lean_ctor_set(x_230, 1, x_151);
lean_ctor_set(x_230, 2, x_229);
x_231 = lean_array_push(x_141, x_164);
x_232 = lean_array_push(x_231, x_230);
lean_inc(x_126);
x_233 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_233, 0, x_126);
lean_ctor_set(x_233, 1, x_146);
lean_ctor_set(x_233, 2, x_232);
x_234 = lean_array_push(x_141, x_131);
x_235 = lean_array_push(x_234, x_233);
x_236 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__12;
lean_inc(x_126);
x_237 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_237, 0, x_126);
lean_ctor_set(x_237, 1, x_236);
lean_ctor_set(x_237, 2, x_235);
x_238 = lean_array_push(x_153, x_237);
lean_inc(x_126);
x_239 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_239, 0, x_126);
lean_ctor_set(x_239, 1, x_146);
lean_ctor_set(x_239, 2, x_238);
x_240 = lean_array_push(x_153, x_239);
x_241 = l_Array___aux__Init__Data__Array__Mem______macroRules__Array__tacticArray__get__dec__1___closed__8;
x_242 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_242, 0, x_126);
lean_ctor_set(x_242, 1, x_241);
lean_ctor_set(x_242, 2, x_240);
x_243 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_243, 0, x_242);
lean_ctor_set(x_243, 1, x_127);
return x_243;
lean_ctor_set(x_224, 0, x_117);
lean_ctor_set(x_224, 1, x_223);
lean_ctor_set(x_224, 2, x_222);
x_225 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_225, 0, x_224);
lean_ctor_set(x_225, 1, x_118);
return x_225;
}
}
}

1346
stage0/stdlib/Init/Data/List/BasicAux.c generated
View file

File diff suppressed because it is too large Load diff

872
stage0/stdlib/Init/NotationExtra.c generated
View file

File diff suppressed because it is too large Load diff

922
stage0/stdlib/Init/System/IO.c generated
View file

File diff suppressed because it is too large Load diff

4913
stage0/stdlib/Init/Tactics.c generated
View file

File diff suppressed because it is too large Load diff

2444
stage0/stdlib/Init/WFTactics.c generated
View file

File diff suppressed because it is too large Load diff

493
stage0/stdlib/Lean/Attributes.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/Class.c generated
View file

@ -68,7 +68,7 @@ static lean_object* l_Lean_addClass___lambda__2___closed__3;
LEAN_EXPORT lean_object* l_Lean_addClass___lambda__2(lean_object*, lean_object*, lean_object*);
uint64_t l_Lean_Name_hash___override(lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(uint8_t, uint8_t);
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_187_(uint8_t, uint8_t);
static lean_object* l_Lean_initFn____x40_Lean_Class___hyg_588____closed__3;
static lean_object* l_Lean_initFn____x40_Lean_Class___hyg_588____closed__15;
LEAN_EXPORT lean_object* l_Lean_SMap_insert___at_Lean_ClassState_addEntry___spec__1(lean_object*, lean_object*, lean_object*);
@ -2893,7 +2893,7 @@ x_12 = lean_ctor_get(x_11, 1);
lean_inc(x_12);
lean_dec(x_11);
x_13 = 0;
x_14 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(x_3, x_13);
x_14 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_187_(x_3, x_13);
if (x_14 == 0)
{
lean_object* x_15; lean_object* x_16; uint8_t x_17;

296
stage0/stdlib/Lean/Compiler/InitAttr.c generated
View file

@ -19,8 +19,8 @@ lean_object* l_Lean_addMessageContextPartial___at_Lean_Core_instAddMessageContex
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_registerInitAttrUnsafe___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_registerInitAttrUnsafe(lean_object*, uint8_t, lean_object*, lean_object*);
static lean_object* l_Lean_setEnv___at_Lean_declareBuiltin___spec__3___closed__1;
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__1;
size_t lean_usize_add(size_t, size_t);
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__38;
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__21;
LEAN_EXPORT lean_object* l___private_Lean_Compiler_InitAttr_0__Lean_isUnitType___boxed(lean_object*);
lean_object* l_Lean_stringToMessageData(lean_object*);
@ -41,7 +41,6 @@ LEAN_EXPORT lean_object* l_Lean_mkConstWithLevelParams___at_Lean_registerInitAtt
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__2;
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* lean_io_error_to_string(lean_object*);
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__34;
lean_object* l_List_mapTRAux___at_Lean_resolveGlobalConstCore___spec__2(lean_object*, lean_object*);
extern lean_object* l_Std_Format_defWidth;
LEAN_EXPORT lean_object* l_Lean_setBuiltinInitAttr(lean_object*, lean_object*, lean_object*);
@ -80,43 +79,37 @@ lean_object* lean_run_mod_init(lean_object*, lean_object*);
static lean_object* l_Lean_resolveGlobalConst___at_Lean_registerInitAttrUnsafe___spec__6___closed__2;
static lean_object* l_Lean_registerInitAttrUnsafe___closed__2;
uint8_t lean_usize_dec_lt(size_t, size_t);
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__37;
static lean_object* l_Lean_declareBuiltin___closed__4;
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__24;
LEAN_EXPORT lean_object* l___private_Lean_Compiler_InitAttr_0__Lean_getIOTypeArg___boxed(lean_object*);
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__19;
lean_object* lean_nat_add(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_registerInitAttrUnsafe___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__4;
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__7;
LEAN_EXPORT lean_object* l_Lean_registerInitAttrUnsafe___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__1;
LEAN_EXPORT lean_object* l_Lean_resolveGlobalConst___at_Lean_registerInitAttrUnsafe___spec__6(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_LocalContext_empty;
lean_object* l_List_mapTRAux___at_Lean_resolveGlobalConstNoOverload___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_registerInitAttrUnsafe___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863_(lean_object*);
lean_object* l_Lean_ConstantInfo_levelParams(lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__2;
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__3;
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__4;
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__33;
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__1;
lean_object* lean_array_fget(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_resolveGlobalConstNoOverloadWithInfo___at_Lean_registerInitAttrUnsafe___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* lean_get_init_fn_name_for(lean_object*, lean_object*);
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__39;
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__4;
lean_object* l_Lean_MessageData_toString(lean_object*, lean_object*);
lean_object* l_Lean_ParametricAttribute_getParam_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_isIOUnitInitFnCore(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_setEnv___at_Lean_declareBuiltin___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_registerInitAttrUnsafe___lambda__1___closed__3;
lean_object* lean_st_ref_take(lean_object*, lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__2;
static lean_object* l_Lean_declareBuiltin___closed__1;
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__31;
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Compiler_InitAttr_0__Lean_isIOUnit___boxed(lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__3;
LEAN_EXPORT lean_object* l_Lean_registerInitAttrUnsafe___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_KernelException_toMessageData(lean_object*, lean_object*);
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__11;
@ -124,12 +117,13 @@ lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_pushInfoLeaf___at_Lean_registerInitAttrUnsafe___spec__15___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_declareBuiltin___closed__2;
static lean_object* l_Lean_declareBuiltin___closed__12;
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__3;
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__4;
static lean_object* l_Lean_Elab_pushInfoLeaf___at_Lean_registerInitAttrUnsafe___spec__15___closed__3;
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__25;
LEAN_EXPORT lean_object* l_Lean_Elab_resolveGlobalConstNoOverloadWithInfo___at_Lean_registerInitAttrUnsafe___spec__4___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_pushInfoLeaf___at_Lean_registerInitAttrUnsafe___spec__15___closed__1;
lean_object* l_Lean_isInitializerExecutionEnabled(lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__3;
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__29;
static lean_object* l_Lean_registerInitAttrUnsafe___lambda__1___closed__5;
lean_object* l_Lean_Attribute_Builtin_getIdent_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
@ -145,6 +139,7 @@ static lean_object* l_Lean_registerInitAttrUnsafe___closed__1;
LEAN_EXPORT lean_object* l_Lean_runModInit___boxed(lean_object*, lean_object*);
lean_object* lean_eval_const(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_hasInitAttr___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__2;
LEAN_EXPORT lean_object* lean_get_regular_init_fn_name_for(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_declareBuiltin___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_registerInitAttrUnsafe___spec__5___closed__3;
@ -181,9 +176,9 @@ LEAN_EXPORT lean_object* l_Lean_getConstInfo___at_Lean_registerInitAttrUnsafe___
static lean_object* l_Lean_getConstInfo___at_Lean_registerInitAttrUnsafe___spec__1___closed__1;
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__1;
LEAN_EXPORT lean_object* l_Lean_isIOUnitRegularInitFn___boxed(lean_object*, lean_object*);
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__36;
lean_object* l_Lean_Name_append(lean_object*, lean_object*);
lean_object* l_Lean_Environment_addAndCompile(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__1;
uint8_t l_Lean_Name_isAnonymous(lean_object*);
LEAN_EXPORT lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791_;
LEAN_EXPORT lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_registerInitAttrUnsafe___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
@ -194,7 +189,6 @@ static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__
LEAN_EXPORT lean_object* l_Lean_Elab_pushInfoTree___at_Lean_registerInitAttrUnsafe___spec__16(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_regularInitAttr;
LEAN_EXPORT uint8_t l_Lean_isIOUnitInitFn(lean_object*, lean_object*);
static lean_object* l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__35;
static lean_object* l___private_Lean_Compiler_InitAttr_0__Lean_getIOTypeArg___closed__1;
LEAN_EXPORT lean_object* l_Lean_declareBuiltin(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mapTRAux___at_Lean_mkConstWithLevelParams___spec__1(lean_object*, lean_object*);
@ -3173,7 +3167,7 @@ static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____cl
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("group", 5);
x_1 = lean_mk_string_from_bytes("exact", 5);
return x_1;
}
}
@ -3181,7 +3175,7 @@ static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__6;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__14;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
@ -3190,44 +3184,26 @@ return x_3;
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__16() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("exact", 5);
return x_1;
}
}
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__17() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__6;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__16;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__16;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__14;
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__19() {
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__17() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__9;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__18;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__16;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__20() {
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__18() {
_start:
{
lean_object* x_1;
@ -3235,11 +3211,29 @@ x_1 = lean_mk_string_from_bytes("Term", 4);
return x_1;
}
}
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__21() {
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__19() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__4;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__18;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__20() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("declName", 8);
return x_1;
}
}
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__21() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__19;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__20;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
@ -3249,7 +3243,7 @@ static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____cl
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("declName", 8);
x_1 = lean_mk_string_from_bytes("decl_name%", 10);
return x_1;
}
}
@ -3257,37 +3251,43 @@ static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__21;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__22;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__24() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("decl_name%", 10);
return x_1;
}
}
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__25() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__24;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__22;
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__26() {
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__24() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__9;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__23;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__25() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__21;
x_3 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__24;
x_4 = lean_alloc_ctor(1, 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___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__26() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__17;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__25;
x_3 = lean_array_push(x_1, x_2);
return x_3;
@ -3298,7 +3298,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__23;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__15;
x_3 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__26;
x_4 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_4, 0, x_1);
@ -3311,7 +3311,7 @@ static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__19;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__9;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__27;
x_3 = lean_array_push(x_1, x_2);
return x_3;
@ -3322,7 +3322,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__17;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__13;
x_3 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__28;
x_4 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_4, 0, x_1);
@ -3346,8 +3346,8 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__13;
x_3 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__9;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__11;
x_3 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__30;
x_4 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -3359,7 +3359,7 @@ static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__30;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__9;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__31;
x_3 = lean_array_push(x_1, x_2);
return x_3;
@ -3370,80 +3370,8 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__15;
x_3 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__32;
x_4 = lean_alloc_ctor(1, 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___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__34() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__9;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__33;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__35() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__13;
x_3 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__34;
x_4 = lean_alloc_ctor(1, 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___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__36() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__9;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__35;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__37() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__11;
x_3 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__36;
x_4 = lean_alloc_ctor(1, 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___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__38() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__9;
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__37;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__39() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__8;
x_3 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__38;
x_3 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__32;
x_4 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -3455,7 +3383,7 @@ static lean_object* _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791_() {
_start:
{
lean_object* x_1;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__39;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__33;
return x_1;
}
}
@ -3477,7 +3405,7 @@ x_6 = l_Lean_registerInitAttr(x_1, x_5, x_3, x_4);
return x_6;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__1() {
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__1() {
_start:
{
lean_object* x_1;
@ -3485,17 +3413,17 @@ x_1 = lean_mk_string_from_bytes("init", 4);
return x_1;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__2() {
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__1;
x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__1;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__3() {
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__3() {
_start:
{
lean_object* x_1;
@ -3503,28 +3431,28 @@ x_1 = lean_mk_string_from_bytes("regularInitAttr", 15);
return x_1;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__4() {
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__2;
x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__3;
x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__3;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__2;
x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__2;
x_3 = 1;
x_4 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__4;
x_4 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__4;
x_5 = l_Lean_registerInitAttrUnsafe(x_2, x_3, x_4, x_1);
return x_5;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__1() {
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__1() {
_start:
{
lean_object* x_1;
@ -3532,17 +3460,17 @@ x_1 = lean_mk_string_from_bytes("builtinInit", 11);
return x_1;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__2() {
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__1;
x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__1;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__3() {
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__3() {
_start:
{
lean_object* x_1;
@ -3550,23 +3478,23 @@ x_1 = lean_mk_string_from_bytes("builtinInitAttr", 15);
return x_1;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__4() {
static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__2;
x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__3;
x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__3;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__2;
x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__2;
x_3 = 0;
x_4 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__4;
x_4 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__4;
x_5 = l_Lean_registerInitAttrUnsafe(x_2, x_3, x_4, x_1);
return x_5;
}
@ -4526,42 +4454,30 @@ l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__32 = _init_l___auto_
lean_mark_persistent(l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__32);
l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__33 = _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__33();
lean_mark_persistent(l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__33);
l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__34 = _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__34();
lean_mark_persistent(l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__34);
l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__35 = _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__35();
lean_mark_persistent(l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__35);
l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__36 = _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__36();
lean_mark_persistent(l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__36);
l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__37 = _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__37();
lean_mark_persistent(l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__37);
l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__38 = _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__38();
lean_mark_persistent(l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__38);
l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__39 = _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__39();
lean_mark_persistent(l___auto____x40_Lean_Compiler_InitAttr___hyg_791____closed__39);
l___auto____x40_Lean_Compiler_InitAttr___hyg_791_ = _init_l___auto____x40_Lean_Compiler_InitAttr___hyg_791_();
lean_mark_persistent(l___auto____x40_Lean_Compiler_InitAttr___hyg_791_);
l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__1 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__1();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__1);
l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__2 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__2();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__2);
l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__3 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__3();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__3);
l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__4 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__4();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845____closed__4);
if (builtin) {res = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_845_(lean_io_mk_world());
l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__1 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__1();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__1);
l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__2 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__2();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__2);
l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__3 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__3();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__3);
l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__4 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__4();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835____closed__4);
if (builtin) {res = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_835_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_regularInitAttr = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_regularInitAttr);
lean_dec_ref(res);
}l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__1 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__1();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__1);
l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__2 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__2();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__2);
l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__3 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__3();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__3);
l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__4 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__4();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873____closed__4);
if (builtin) {res = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_873_(lean_io_mk_world());
}l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__1 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__1();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__1);
l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__2 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__2();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__2);
l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__3 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__3();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__3);
l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__4 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__4();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863____closed__4);
if (builtin) {res = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_863_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_builtinInitAttr = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_builtinInitAttr);

4
stage0/stdlib/Lean/Compiler/LCNF/PassManager.c generated
View file

@ -108,7 +108,7 @@ lean_object* l_Array_push___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_LCNF_PassInstaller_installAfter___elambda__1___closed__6;
static lean_object* l_Lean_Compiler_LCNF_PassInstaller_initFn____x40_Lean_Compiler_LCNF_PassManager___hyg_1339____closed__2;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(uint8_t, uint8_t);
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_187_(uint8_t, uint8_t);
uint8_t l_instDecidableNot___rarg(uint8_t);
static lean_object* l_Lean_throwError___at_Lean_Compiler_LCNF_PassManager_validate___spec__1___closed__4;
LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Compiler_LCNF_PassManager_0__Lean_Compiler_LCNF_PassInstaller_getPassInstallerUnsafe___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -3079,7 +3079,7 @@ x_8 = lean_ctor_get(x_7, 1);
lean_inc(x_8);
lean_dec(x_7);
x_9 = 0;
x_10 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(x_3, x_9);
x_10 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_187_(x_3, x_9);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12; uint8_t x_13;

8
stage0/stdlib/Lean/Data/Lsp/Capabilities.c generated
View file

@ -41,7 +41,7 @@ static lean_object* l_Lean_Lsp_instToJsonTextDocumentClientCapabilities___closed
static lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_607____closed__4;
LEAN_EXPORT lean_object* l_Lean_Lsp_instFromJsonServerCapabilities;
static lean_object* l_Lean_Lsp_instToJsonCompletionClientCapabilities___closed__1;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5317_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5320_(lean_object*);
LEAN_EXPORT uint8_t l_Lean_Lsp_ServerCapabilities_workspaceSymbolProvider___default;
LEAN_EXPORT uint8_t l_Lean_Lsp_ServerCapabilities_hoverProvider___default;
lean_object* l_List_join___rarg(lean_object*);
@ -55,7 +55,7 @@ LEAN_EXPORT lean_object* l_Lean_Lsp_instToJsonCompletionClientCapabilities;
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonWindowClientCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_324____spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonCompletionOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_119_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonTextDocumentClientCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_191____spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5241_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5244_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Lsp_ClientCapabilities_textDocument_x3f___default;
static lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_607____closed__3;
LEAN_EXPORT lean_object* l_Lean_Lsp_instFromJsonTextDocumentClientCapabilities;
@ -1777,7 +1777,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_obj
x_4 = lean_ctor_get(x_2, 0);
lean_inc(x_4);
lean_dec(x_2);
x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5317_(x_4);
x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5320_(x_4);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_5);
@ -2192,7 +2192,7 @@ return x_4;
else
{
lean_object* x_5;
x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5241_(x_3);
x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5244_(x_3);
lean_dec(x_3);
if (lean_obj_tag(x_5) == 0)
{

4386
stage0/stdlib/Lean/Data/Lsp/LanguageFeatures.c generated
View file

File diff suppressed because it is too large Load diff

819
stage0/stdlib/Lean/Elab/Deriving/DecEq.c generated
View file

File diff suppressed because one or more lines are too long

4
stage0/stdlib/Lean/Elab/InheritDoc.c generated
View file

@ -59,7 +59,7 @@ static lean_object* l_Lean_initFn____x40_Lean_Elab_InheritDoc___hyg_4____closed_
LEAN_EXPORT lean_object* l_Lean_getConstInfo___at_Lean_initFn____x40_Lean_Elab_InheritDoc___hyg_4____spec__13(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Option_get___at_Lean_getSanitizeNames___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_MapDeclarationExtension_insert___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(uint8_t, uint8_t);
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_187_(uint8_t, uint8_t);
static lean_object* l_Lean_initFn____x40_Lean_Elab_InheritDoc___hyg_4____closed__2;
uint8_t l_Lean_Syntax_matchesNull(lean_object*, lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
@ -3057,7 +3057,7 @@ _start:
{
uint8_t x_9; uint8_t x_10;
x_9 = 0;
x_10 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(x_5, x_9);
x_10 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_187_(x_5, x_9);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12; uint8_t x_13;

618
stage0/stdlib/Lean/Elab/Structure.c generated
View file

File diff suppressed because it is too large Load diff

1294
stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c generated
View file

File diff suppressed because it is too large Load diff

724
stage0/stdlib/Lean/Elab/Tactic/Conv/Basic.c generated
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

226
stage0/stdlib/Lean/Elab/Tactic/Simp.c generated
View file

@ -86,7 +86,6 @@ lean_object* l_Std_PersistentArray_append___rarg(lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_elabSimpArgs___spec__20___closed__5;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_simpLocation___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*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_tacticToDischarge___closed__22;
static lean_object* l_Lean_Elab_Tactic_tacticToDischarge___lambda__3___closed__4;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSimp(lean_object*);
uint8_t l_Lean_Meta_SimpTheorems_isDeclToUnfold(lean_object*, lean_object*);
@ -368,7 +367,6 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_elabSimpCo
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_dsimpLocation(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_Tactic_replaceMainGoal(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_unsupportedSyntaxExceptionId;
static lean_object* l_Lean_Elab_Tactic_tacticToDischarge___closed__21;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_SimpKind_toCtorIdx___boxed(lean_object*);
static lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_elabSimpArgs___spec__3___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSimpAll_declRange___closed__5;
@ -3259,7 +3257,7 @@ static lean_object* _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__14() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("group", 5);
x_1 = lean_mk_string_from_bytes("paren", 5);
return x_1;
}
}
@ -3267,7 +3265,7 @@ static lean_object* _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__15() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_1 = l_Lean_Elab_Tactic_tacticToDischarge___closed__4;
x_2 = l_Lean_Elab_Tactic_tacticToDischarge___closed__14;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
@ -3277,29 +3275,11 @@ static lean_object* _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__16() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("paren", 5);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__17() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Tactic_tacticToDischarge___closed__4;
x_2 = l_Lean_Elab_Tactic_tacticToDischarge___closed__16;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__18() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("(", 1);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__19() {
static lean_object* _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__17() {
_start:
{
lean_object* x_1;
@ -3307,7 +3287,7 @@ x_1 = lean_mk_string_from_bytes(")", 1);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__20() {
static lean_object* _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -3316,16 +3296,7 @@ x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__21() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(2u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__22() {
static lean_object* _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__19() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -3334,10 +3305,19 @@ x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__20() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(2u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_tacticToDischarge(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; uint8_t x_57;
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; uint8_t x_51;
x_11 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Tactic_tacticToDischarge___spec__1___rarg(x_8, x_9, x_10);
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
@ -3353,121 +3333,107 @@ lean_inc(x_12);
x_17 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_17, 0, x_12);
lean_ctor_set(x_17, 1, x_16);
x_18 = l_Lean_Elab_Tactic_tacticToDischarge___closed__18;
x_18 = l_Lean_Elab_Tactic_tacticToDischarge___closed__16;
lean_inc(x_12);
x_19 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_19, 0, x_12);
lean_ctor_set(x_19, 1, x_18);
x_20 = l_Lean_Elab_Tactic_tacticToDischarge___closed__19;
x_20 = l_Lean_Elab_Tactic_tacticToDischarge___closed__17;
lean_inc(x_12);
x_21 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_21, 0, x_12);
lean_ctor_set(x_21, 1, x_20);
x_22 = l_Lean_Elab_Tactic_tacticToDischarge___closed__20;
x_22 = l_Lean_Elab_Tactic_tacticToDischarge___closed__18;
x_23 = lean_array_push(x_22, x_19);
x_24 = lean_array_push(x_23, x_1);
x_25 = lean_array_push(x_24, x_21);
x_26 = l_Lean_Elab_Tactic_tacticToDischarge___closed__17;
x_26 = l_Lean_Elab_Tactic_tacticToDischarge___closed__15;
lean_inc(x_12);
x_27 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_27, 0, x_12);
lean_ctor_set(x_27, 1, x_26);
lean_ctor_set(x_27, 2, x_25);
x_28 = l_Lean_Elab_Tactic_tacticToDischarge___closed__13;
x_29 = l_Lean_Elab_Tactic_elabSimpConfigCore___closed__8;
x_28 = l_Lean_Elab_Tactic_tacticToDischarge___closed__19;
x_29 = lean_array_push(x_28, x_27);
x_30 = l_Lean_Elab_Tactic_tacticToDischarge___closed__13;
lean_inc(x_12);
x_30 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_30, 0, x_12);
lean_ctor_set(x_30, 1, x_28);
lean_ctor_set(x_30, 2, x_29);
x_31 = l_Lean_Elab_Tactic_tacticToDischarge___closed__21;
x_32 = lean_array_push(x_31, x_27);
x_33 = lean_array_push(x_32, x_30);
x_34 = l_Lean_Elab_Tactic_tacticToDischarge___closed__15;
x_31 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_31, 0, x_12);
lean_ctor_set(x_31, 1, x_30);
lean_ctor_set(x_31, 2, x_29);
x_32 = lean_array_push(x_28, x_31);
x_33 = l_Lean_Elab_Tactic_tacticToDischarge___closed__11;
lean_inc(x_12);
x_35 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_35, 0, x_12);
lean_ctor_set(x_35, 1, x_34);
lean_ctor_set(x_35, 2, x_33);
x_36 = l_Lean_Elab_Tactic_tacticToDischarge___closed__22;
x_37 = lean_array_push(x_36, x_35);
x_34 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_34, 0, x_12);
lean_ctor_set(x_34, 1, x_33);
lean_ctor_set(x_34, 2, x_32);
x_35 = lean_array_push(x_28, x_34);
x_36 = l_Lean_Elab_Tactic_tacticToDischarge___closed__9;
lean_inc(x_12);
x_38 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_38, 0, x_12);
lean_ctor_set(x_38, 1, x_28);
lean_ctor_set(x_38, 2, x_37);
x_39 = lean_array_push(x_36, x_38);
x_40 = l_Lean_Elab_Tactic_tacticToDischarge___closed__11;
lean_inc(x_12);
x_41 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_41, 0, x_12);
lean_ctor_set(x_41, 1, x_40);
lean_ctor_set(x_41, 2, x_39);
x_42 = lean_array_push(x_36, x_41);
x_43 = l_Lean_Elab_Tactic_tacticToDischarge___closed__9;
lean_inc(x_12);
x_44 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_44, 0, x_12);
lean_ctor_set(x_44, 1, x_43);
lean_ctor_set(x_44, 2, x_42);
x_45 = lean_array_push(x_31, x_17);
x_46 = lean_array_push(x_45, x_44);
x_47 = l_Lean_Elab_Tactic_tacticToDischarge___closed__6;
x_48 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_48, 0, x_12);
lean_ctor_set(x_48, 1, x_47);
lean_ctor_set(x_48, 2, x_46);
x_49 = lean_st_ref_get(x_9, x_15);
x_50 = lean_ctor_get(x_49, 1);
lean_inc(x_50);
lean_dec(x_49);
x_51 = lean_st_ref_get(x_5, x_50);
x_52 = lean_ctor_get(x_51, 0);
lean_inc(x_52);
x_53 = lean_ctor_get(x_51, 1);
lean_inc(x_53);
lean_dec(x_51);
x_54 = lean_st_ref_get(x_9, x_53);
x_55 = lean_ctor_get(x_54, 1);
lean_inc(x_55);
lean_dec(x_54);
x_56 = lean_st_mk_ref(x_52, x_55);
x_57 = !lean_is_exclusive(x_56);
if (x_57 == 0)
x_37 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_37, 0, x_12);
lean_ctor_set(x_37, 1, x_36);
lean_ctor_set(x_37, 2, x_35);
x_38 = l_Lean_Elab_Tactic_tacticToDischarge___closed__20;
x_39 = lean_array_push(x_38, x_17);
x_40 = lean_array_push(x_39, x_37);
x_41 = l_Lean_Elab_Tactic_tacticToDischarge___closed__6;
x_42 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_42, 0, x_12);
lean_ctor_set(x_42, 1, x_41);
lean_ctor_set(x_42, 2, x_40);
x_43 = lean_st_ref_get(x_9, x_15);
x_44 = lean_ctor_get(x_43, 1);
lean_inc(x_44);
lean_dec(x_43);
x_45 = lean_st_ref_get(x_5, x_44);
x_46 = lean_ctor_get(x_45, 0);
lean_inc(x_46);
x_47 = lean_ctor_get(x_45, 1);
lean_inc(x_47);
lean_dec(x_45);
x_48 = lean_st_ref_get(x_9, x_47);
x_49 = lean_ctor_get(x_48, 1);
lean_inc(x_49);
lean_dec(x_48);
x_50 = lean_st_mk_ref(x_46, x_49);
x_51 = !lean_is_exclusive(x_50);
if (x_51 == 0)
{
lean_object* x_58; lean_object* x_59; lean_object* x_60;
x_58 = lean_ctor_get(x_56, 0);
lean_inc(x_58);
x_59 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_tacticToDischarge___lambda__3___boxed), 11, 3);
lean_closure_set(x_59, 0, x_58);
lean_closure_set(x_59, 1, x_48);
lean_closure_set(x_59, 2, x_4);
x_60 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_60, 0, x_58);
lean_ctor_set(x_60, 1, x_59);
lean_ctor_set(x_56, 0, x_60);
return x_56;
lean_object* x_52; lean_object* x_53; lean_object* x_54;
x_52 = lean_ctor_get(x_50, 0);
lean_inc(x_52);
x_53 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_tacticToDischarge___lambda__3___boxed), 11, 3);
lean_closure_set(x_53, 0, x_52);
lean_closure_set(x_53, 1, x_42);
lean_closure_set(x_53, 2, x_4);
x_54 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_54, 0, x_52);
lean_ctor_set(x_54, 1, x_53);
lean_ctor_set(x_50, 0, x_54);
return x_50;
}
else
{
lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65;
x_61 = lean_ctor_get(x_56, 0);
x_62 = lean_ctor_get(x_56, 1);
lean_inc(x_62);
lean_inc(x_61);
lean_dec(x_56);
lean_inc(x_61);
x_63 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_tacticToDischarge___lambda__3___boxed), 11, 3);
lean_closure_set(x_63, 0, x_61);
lean_closure_set(x_63, 1, x_48);
lean_closure_set(x_63, 2, x_4);
x_64 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_64, 0, x_61);
lean_ctor_set(x_64, 1, x_63);
x_65 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_65, 0, x_64);
lean_ctor_set(x_65, 1, x_62);
return x_65;
lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59;
x_55 = lean_ctor_get(x_50, 0);
x_56 = lean_ctor_get(x_50, 1);
lean_inc(x_56);
lean_inc(x_55);
lean_dec(x_50);
lean_inc(x_55);
x_57 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_tacticToDischarge___lambda__3___boxed), 11, 3);
lean_closure_set(x_57, 0, x_55);
lean_closure_set(x_57, 1, x_42);
lean_closure_set(x_57, 2, x_4);
x_58 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_58, 0, x_55);
lean_ctor_set(x_58, 1, x_57);
x_59 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_59, 0, x_58);
lean_ctor_set(x_59, 1, x_56);
return x_59;
}
}
}
@ -9385,7 +9351,7 @@ lean_inc(x_23);
lean_dec(x_21);
x_24 = lean_unsigned_to_nat(4u);
x_25 = l_Lean_Syntax_getArg(x_1, x_24);
x_26 = l_Lean_Elab_Tactic_tacticToDischarge___closed__22;
x_26 = l_Lean_Elab_Tactic_tacticToDischarge___closed__19;
x_27 = lean_array_push(x_26, x_6);
x_28 = lean_box(0);
x_29 = lean_unsigned_to_nat(0u);
@ -11969,10 +11935,6 @@ l_Lean_Elab_Tactic_tacticToDischarge___closed__19 = _init_l_Lean_Elab_Tactic_tac
lean_mark_persistent(l_Lean_Elab_Tactic_tacticToDischarge___closed__19);
l_Lean_Elab_Tactic_tacticToDischarge___closed__20 = _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__20();
lean_mark_persistent(l_Lean_Elab_Tactic_tacticToDischarge___closed__20);
l_Lean_Elab_Tactic_tacticToDischarge___closed__21 = _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__21();
lean_mark_persistent(l_Lean_Elab_Tactic_tacticToDischarge___closed__21);
l_Lean_Elab_Tactic_tacticToDischarge___closed__22 = _init_l_Lean_Elab_Tactic_tacticToDischarge___closed__22();
lean_mark_persistent(l_Lean_Elab_Tactic_tacticToDischarge___closed__22);
l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_addDeclToUnfoldOrTheorem___closed__1 = _init_l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_addDeclToUnfoldOrTheorem___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_addDeclToUnfoldOrTheorem___closed__1);
l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_addDeclToUnfoldOrTheorem___closed__2 = _init_l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_addDeclToUnfoldOrTheorem___closed__2();

4
stage0/stdlib/Lean/KeyedDeclsAttribute.c generated
View file

@ -139,7 +139,7 @@ LEAN_EXPORT lean_object* l_Lean_KeyedDeclsAttribute_init___rarg___lambda__7(lean
static lean_object* l_Lean_KeyedDeclsAttribute_init___rarg___lambda__9___closed__11;
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at___private_Lean_KeyedDeclsAttribute_0__Lean_KeyedDeclsAttribute_Table_insert___spec__26___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(uint8_t, uint8_t);
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_187_(uint8_t, uint8_t);
static lean_object* l_Lean_KeyedDeclsAttribute_instInhabitedDef___lambda__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_KeyedDeclsAttribute_instInhabitedDef___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_AssocList_find_x3f___at_Lean_KeyedDeclsAttribute_getEntries___spec__10___rarg(lean_object*, lean_object*);
@ -5951,7 +5951,7 @@ _start:
{
uint8_t x_12; uint8_t x_13;
x_12 = 0;
x_13 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(x_8, x_12);
x_13 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_187_(x_8, x_12);
if (x_13 == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20;

6
stage0/stdlib/Lean/Linter/MissingDocs.c generated
View file

@ -172,7 +172,7 @@ LEAN_EXPORT lean_object* l___regBuiltin_Lean_Linter_MissingDocs_checkSimpLike(le
static lean_object* l_Lean_Linter_MissingDocs_lintDeclHead___closed__4;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Array_anyMUnsafe_any___at_Lean_Linter_MissingDocs_hasInheritDoc___spec__1___closed__8;
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(uint8_t, uint8_t);
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_187_(uint8_t, uint8_t);
static lean_object* l_Lean_Linter_MissingDocs_initFn____x40_Lean_Linter_MissingDocs___hyg_757____closed__5;
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Linter_MissingDocs_initFn____x40_Lean_Linter_MissingDocs___hyg_356____spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Linter_MissingDocs_checkNotation___closed__4;
@ -2599,7 +2599,7 @@ _start:
{
uint8_t x_9; uint8_t x_10;
x_9 = 0;
x_10 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(x_5, x_9);
x_10 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_187_(x_5, x_9);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17;
@ -3100,7 +3100,7 @@ _start:
{
uint8_t x_9; uint8_t x_10;
x_9 = 0;
x_10 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(x_5, x_9);
x_10 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_187_(x_5, x_9);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17;

4
stage0/stdlib/Lean/Linter/UnusedVariables.c generated
View file

@ -182,7 +182,7 @@ lean_object* lean_array_fget(lean_object*, lean_object*);
static lean_object* l_Lean_MessageData_isUnusedVariableWarning___closed__1;
LEAN_EXPORT lean_object* l_Lean_MessageData_isUnusedVariableWarning___boxed(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(uint8_t, uint8_t);
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_187_(uint8_t, uint8_t);
LEAN_EXPORT uint8_t l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1620____lambda__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Linter_collectMacroExpansions_x3f_go___at_Lean_Linter_unusedVariables___spec__22(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Option_register___at_Lean_initFn____x40_Lean_PrettyPrinter_Delaborator_Options___hyg_6____spec__1(lean_object*, lean_object*, lean_object*);
@ -4268,7 +4268,7 @@ x_9 = lean_ctor_get(x_8, 1);
lean_inc(x_9);
lean_dec(x_8);
x_10 = 0;
x_11 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(x_4, x_10);
x_11 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_187_(x_4, x_10);
if (x_11 == 0)
{
lean_object* x_12; lean_object* x_13; uint8_t x_14;

4
stage0/stdlib/Lean/Meta/Instances.c generated
View file

@ -123,7 +123,7 @@ lean_object* lean_array_fget(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_944____spec__1(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_500____closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(uint8_t, uint8_t);
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_187_(uint8_t, uint8_t);
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_944_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_308_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_500_(lean_object*);
@ -8294,7 +8294,7 @@ x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = 0;
x_13 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(x_3, x_12);
x_13 = l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_187_(x_3, x_12);
if (x_13 == 0)
{
lean_object* x_14; lean_object* x_15; uint8_t x_16;

422
stage0/stdlib/Lean/Meta/Tactic/LinearArith/Solver.c generated
View file

File diff suppressed because it is too large Load diff

348
stage0/stdlib/Lean/Meta/Tactic/Simp/SimpTheorems.c generated
View file

@ -17,7 +17,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorem_getName___boxed(lean_object*);
lean_object* l_List_reverse___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_SimpTheorems_addDeclToUnfold___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_SimpTheorems_erase___rarg___closed__2;
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__2;
static lean_object* l_Lean_Meta_mkSimpAttr___lambda__1___closed__2;
LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_pre___default;
static lean_object* l_Lean_Parser_Command_registerSimpAttr___closed__12;
@ -28,7 +27,6 @@ lean_object* l_Lean_Meta_mkPropExt(lean_object*, lean_object*, lean_object*, lea
static lean_object* l_Lean_Meta_SimpTheorems_toUnfoldThms___default___closed__2;
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__5;
LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_erase___at_Lean_Meta_mkSimpAttr___spec__3___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__4;
size_t lean_usize_add(size_t, size_t);
LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_isLemma___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_erase___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -64,16 +62,16 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Meta_Tactic_Simp_
static lean_object* l_Lean_Meta_mkSimpAttr___lambda__1___closed__13;
LEAN_EXPORT lean_object* l_Lean_Meta_SimpExtension_getTheorems(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__42;
LEAN_EXPORT lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4704_;
LEAN_EXPORT lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4694_;
LEAN_EXPORT lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087_;
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__53;
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__100;
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__9;
static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___closed__6;
LEAN_EXPORT lean_object* l_Lean_Meta_addSimpTheoremEntry_updateLemmaNames(lean_object*, lean_object*);
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__91;
lean_object* l_Lean_Meta_mkAppM(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__26;
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__9;
static lean_object* l_Lean_Meta_SimpTheorems_erase___rarg___closed__1;
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__103;
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
@ -111,10 +109,8 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__102;
uint8_t lean_name_eq(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isApp(lean_object*);
static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__36;
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_addSimpTheoremEntry___spec__12(lean_object*, lean_object*, size_t, size_t);
lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__35;
static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___closed__2;
lean_object* l_Lean_Expr_appFn_x21(lean_object*);
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at___aux__Init__Notation______macroRules__precMax__1___spec__1(lean_object*, lean_object*);
@ -142,6 +138,7 @@ static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems___
uint8_t l_ptrEqList___rarg(lean_object*, lean_object*);
static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__11;
static lean_object* l_Lean_Meta_mkSimpAttr___lambda__1___closed__1;
LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4658____spec__1___boxed(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__62;
LEAN_EXPORT lean_object* l_Lean_Meta_mkSimpAttr___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -160,6 +157,7 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpAttr___sp
lean_object* lean_string_utf8_byte_size(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_isRflProof(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_shouldPreprocess___closed__1;
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__4;
LEAN_EXPORT lean_object* l_Std_AssocList_contains___at_Lean_Meta_registerSimpAttr___spec__2___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__87;
static lean_object* l_Lean_Meta_instInhabitedSimpTheorems___closed__2;
@ -241,7 +239,6 @@ lean_object* l_Lean_Meta_mkEqSymm(lean_object*, lean_object*, lean_object*, lean
LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_add___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_EXPORT lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Meta_addSimpTheoremEntry___spec__2(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_simpExtension;
static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__34;
static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_mkSimpTheoremCore___lambda__2___closed__1;
static size_t l_Std_PersistentHashMap_findAux___at_Lean_Meta_addSimpTheoremEntry___spec__3___closed__1;
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__40;
@ -322,8 +319,8 @@ static lean_object* l_Lean_Meta_instToFormatSimpTheorem___closed__5;
LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_isDeclToUnfold___boxed(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isConstOf(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_SimpExtension_getTheorems___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4668_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4658_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798_(lean_object*);
size_t lean_usize_mul(size_t, size_t);
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__75;
lean_object* l_Lean_Expr_bvar___override(lean_object*);
@ -336,17 +333,16 @@ static lean_object* l_Lean_Meta_DiscrTree_insertCore___at_Lean_Meta_addSimpTheor
uint8_t l_Lean_Expr_isForall(lean_object*);
LEAN_EXPORT lean_object* l_Array_contains___at_Lean_Meta_addSimpTheoremEntry___spec__11___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__12;
static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__33;
lean_object* lean_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_containsAtAux___at_Lean_Meta_SimpTheorems_erase___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__22;
LEAN_EXPORT lean_object* l_Lean_Meta_instInhabitedSimpTheorems;
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__3;
static lean_object* l_Lean_Meta_SimpTheorem_getValue___closed__1;
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__81;
LEAN_EXPORT lean_object* l_Lean_Meta_isRflProofCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__39;
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__7;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_SimpTheorems_addDeclToUnfold___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_DiscrTree_insertCore___at_Lean_Meta_addSimpTheoremEntry___spec__1(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_PersistentHashMap_empty___at_Lean_Meta_Instances_instanceNames___default___spec__1;
@ -382,6 +378,7 @@ static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems___
LEAN_EXPORT lean_object* l_Lean_Meta_mkSimpAttr___lambda__2(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_mkSimpTheoremCore___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_erased___default;
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__3;
static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__14;
static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_checkTypeIsProp___closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -412,12 +409,10 @@ uint8_t lean_expr_eqv(lean_object*, lean_object*);
lean_object* l_Lean_Meta_getEqnsFor_x3f(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__23;
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__96;
static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__37;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__8(lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__72;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__88;
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__7;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
uint8_t lean_usize_dec_le(size_t, size_t);
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__38;
@ -434,7 +429,6 @@ lean_object* l_Lean_Syntax_getKind(lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__2___closed__3;
static lean_object* l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_insertAux___at_Lean_Meta_addSimpTheoremEntry___spec__9___closed__1;
lean_object* l_Lean_quoteNameMk(lean_object*);
static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__38;
lean_object* l_Lean_TSyntax_getDocString(lean_object*);
static lean_object* l_Lean_Parser_Command_registerSimpAttr___closed__14;
static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__21;
@ -446,7 +440,6 @@ static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAux___at_Lean_Meta_addSimpTheoremEntry___spec__3(lean_object*, size_t, lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_checkBadRewrite___closed__2;
lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Meta_SynthInstance_0__Lean_Meta_SynthInstance_removeUnusedArguments_x3f___spec__2___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__5;
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__80;
static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__3;
static lean_object* l_Lean_Parser_Command_registerSimpAttr___closed__21;
@ -484,12 +477,12 @@ static lean_object* l_Lean_Meta_mkSimpAttr___lambda__1___closed__15;
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Command_registerSimpAttr___closed__17;
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__8;
static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_checkBadRewrite___closed__3;
lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_SimpTheoremsArray_isDeclToUnfold___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__60;
uint8_t l_Lean_Syntax_isNone(lean_object*);
LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4668____spec__1(lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__3___closed__6;
lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1(lean_object*, lean_object*, lean_object*);
@ -529,11 +522,11 @@ LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_toUnfold___default;
static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__2___closed__1;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpAttr___spec__2___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*);
static lean_object* l_Lean_Meta_instToFormatSimpTheorem___closed__1;
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__1;
static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__3___closed__10;
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__48;
extern lean_object* l_Lean_Expr_instBEqExpr;
static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___closed__9;
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__6;
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_Meta_addSimpTheoremEntry___spec__6(lean_object*, size_t, size_t, lean_object*, lean_object*);
static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__7;
static lean_object* l_Lean_Meta_DiscrTree_insertCore___at_Lean_Meta_addSimpTheoremEntry___spec__1___closed__5;
@ -562,6 +555,7 @@ static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems___
static lean_object* l_Lean_Meta_DiscrTree_insertCore___at_Lean_Meta_addSimpTheoremEntry___spec__1___closed__3;
static lean_object* l_Lean_Parser_Command_registerSimpAttr___closed__4;
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4658____spec__1(lean_object*);
static lean_object* l_Lean_Meta_instToFormatSimpTheorem___closed__4;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_isRflProofCore___closed__3;
@ -606,9 +600,10 @@ static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems___
static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__12;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_mkSimpTheoremCore(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_indentExpr(lean_object*);
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__6;
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_addSimpTheoremEntry(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__2;
static lean_object* l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__76;
LEAN_EXPORT lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Meta_hasSmartUnfoldingDecl(lean_object*, lean_object*);
@ -640,13 +635,12 @@ static lean_object* l_Lean_Meta_instInhabitedSimpEntry___closed__1;
static lean_object* l_Lean_Parser_Command_registerSimpAttr___closed__2;
LEAN_EXPORT lean_object* l_Lean_Meta_mkSimpAttr___lambda__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Meta_DiscrTree_instInhabitedTrie(lean_object*);
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__5;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_shouldPreprocess___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_DiscrTree_insertCore___at_Lean_Meta_addSimpTheoremEntry___spec__1___closed__4;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_addSimpTheorem___spec__2(lean_object*, uint8_t, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4668____spec__1___boxed(lean_object*);
lean_object* l_Lean_Meta_DiscrTree_empty(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheoremsArray_isErased___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__8;
LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorem_levelParams___default;
lean_object* l_Std_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_DiscrTree_insertCore___at_Lean_Meta_addSimpTheoremEntry___spec__1___closed__8;
@ -11003,7 +10997,7 @@ static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___h
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("group", 5);
x_1 = lean_mk_string_from_bytes("exact", 5);
return x_1;
}
}
@ -11011,7 +11005,7 @@ static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___h
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__6;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__13;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
@ -11020,44 +11014,26 @@ return x_3;
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__15() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("exact", 5);
return x_1;
}
}
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__6;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__15;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__17() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__15;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__13;
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__18() {
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_SimpTheorem_keys___default___closed__1;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__17;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__15;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__19() {
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__17() {
_start:
{
lean_object* x_1;
@ -11065,11 +11041,29 @@ x_1 = lean_mk_string_from_bytes("Term", 4);
return x_1;
}
}
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__20() {
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__4;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__17;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__19() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("declName", 8);
return x_1;
}
}
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__20() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__18;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__19;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
@ -11079,7 +11073,7 @@ static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___h
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("declName", 8);
x_1 = lean_mk_string_from_bytes("decl_name%", 10);
return x_1;
}
}
@ -11087,37 +11081,43 @@ static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___h
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__20;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__21;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__23() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("decl_name%", 10);
return x_1;
}
}
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__24() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__23;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__21;
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__25() {
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__23() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_SimpTheorem_keys___default___closed__1;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__22;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__24() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__20;
x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__23;
x_4 = lean_alloc_ctor(1, 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___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__25() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__16;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__24;
x_3 = lean_array_push(x_1, x_2);
return x_3;
@ -11128,7 +11128,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__22;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__14;
x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__25;
x_4 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_4, 0, x_1);
@ -11141,7 +11141,7 @@ static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___h
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__18;
x_1 = l_Lean_Meta_SimpTheorem_keys___default___closed__1;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__26;
x_3 = lean_array_push(x_1, x_2);
return x_3;
@ -11152,7 +11152,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__16;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__12;
x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__27;
x_4 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_4, 0, x_1);
@ -11176,8 +11176,8 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__12;
x_3 = l_Lean_Meta_SimpTheorem_keys___default___closed__1;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__10;
x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__29;
x_4 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -11189,7 +11189,7 @@ static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___h
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__29;
x_1 = l_Lean_Meta_SimpTheorem_keys___default___closed__1;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__30;
x_3 = lean_array_push(x_1, x_2);
return x_3;
@ -11200,80 +11200,8 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__14;
x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__31;
x_4 = lean_alloc_ctor(1, 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___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__33() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_SimpTheorem_keys___default___closed__1;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__32;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__34() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__12;
x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__33;
x_4 = lean_alloc_ctor(1, 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___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__35() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_SimpTheorem_keys___default___closed__1;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__34;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__36() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__10;
x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__35;
x_4 = lean_alloc_ctor(1, 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___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__37() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_SimpTheorem_keys___default___closed__1;
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__36;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__38() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__8;
x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__37;
x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__31;
x_4 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -11285,7 +11213,7 @@ static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___h
_start:
{
lean_object* x_1;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__38;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__32;
return x_1;
}
}
@ -13076,7 +13004,7 @@ x_7 = l_Lean_registerSimpleScopedEnvExtension___rarg(x_6, x_2);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4668____spec__1(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4658____spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
@ -13084,7 +13012,7 @@ x_2 = l_Std_mkHashMapImp___rarg(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4668_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4658_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5;
@ -13111,20 +13039,20 @@ return x_8;
}
}
}
LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4668____spec__1___boxed(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4658____spec__1___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Std_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4668____spec__1(x_1);
x_2 = l_Std_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4658____spec__1(x_1);
lean_dec(x_1);
return x_2;
}
}
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4704_() {
static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4694_() {
_start:
{
lean_object* x_1;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__38;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__32;
return x_1;
}
}
@ -13572,7 +13500,7 @@ x_4 = lean_box(x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__1() {
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__1() {
_start:
{
lean_object* x_1;
@ -13580,17 +13508,17 @@ x_1 = lean_mk_string_from_bytes("simp", 4);
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__2() {
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__1;
x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__1;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__3() {
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__3() {
_start:
{
lean_object* x_1;
@ -13598,17 +13526,17 @@ x_1 = lean_mk_string_from_bytes("Meta", 4);
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__4() {
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__2;
x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__3;
x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__3;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__5() {
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__5() {
_start:
{
lean_object* x_1;
@ -13616,17 +13544,17 @@ x_1 = lean_mk_string_from_bytes("simpExtension", 13);
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__6() {
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__4;
x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__5;
x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__4;
x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__5;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__7() {
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__7() {
_start:
{
lean_object* x_1;
@ -13634,17 +13562,17 @@ x_1 = lean_mk_string_from_bytes("Ext", 3);
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__8() {
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__2;
x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__7;
x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__2;
x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__7;
x_3 = lean_name_append_after(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__9() {
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__9() {
_start:
{
lean_object* x_1;
@ -13652,14 +13580,14 @@ x_1 = lean_mk_string_from_bytes("simplification theorem", 22);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__2;
x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__9;
x_4 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__6;
x_5 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__8;
x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__2;
x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__9;
x_4 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__6;
x_5 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__8;
x_6 = l_Lean_Meta_registerSimpAttr(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
@ -16210,7 +16138,7 @@ static lean_object* _init_l_Lean_Parser_Command_registerSimpAttr___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__4;
x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__4;
x_2 = l_Lean_Parser_Command_registerSimpAttr___closed__1;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
@ -16568,7 +16496,7 @@ static lean_object* _init_l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheor
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__20;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__18;
x_2 = l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__16;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
@ -16619,7 +16547,7 @@ static lean_object* _init_l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheor
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__4;
x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__4;
x_2 = l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__18;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
@ -16709,7 +16637,7 @@ static lean_object* _init_l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheor
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__20;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__18;
x_2 = l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__30;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
@ -16727,7 +16655,7 @@ static lean_object* _init_l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheor
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__20;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__18;
x_2 = l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__32;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
@ -16745,7 +16673,7 @@ static lean_object* _init_l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheor
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__20;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__18;
x_2 = l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__34;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
@ -16763,7 +16691,7 @@ static lean_object* _init_l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheor
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__20;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__18;
x_2 = l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__36;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
@ -16806,7 +16734,7 @@ static lean_object* _init_l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheor
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__4;
x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__4;
x_2 = l_Lean_Parser_Command_registerSimpAttr___closed__7;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
@ -16897,7 +16825,7 @@ static lean_object* _init_l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheor
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__20;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__18;
x_2 = l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__49;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
@ -17391,7 +17319,7 @@ static lean_object* _init_l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheor
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__20;
x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__18;
x_2 = l_Lean_Meta___aux__Lean__Meta__Tactic__Simp__SimpTheorems______macroRules__Lean__Meta____root____Lean__Parser__Command__registerSimpAttr__1___closed__100;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
@ -18226,18 +18154,6 @@ l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__31 = _i
lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__31);
l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__32 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__32();
lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__32);
l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__33 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__33();
lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__33);
l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__34 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__34();
lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__34);
l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__35 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__35();
lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__35);
l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__36 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__36();
lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__36);
l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__37 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__37();
lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__37);
l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__38 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__38();
lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087____closed__38);
l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087_ = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087_();
lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4087_);
l_Lean_Meta_mkSimpAttr___lambda__1___closed__1 = _init_l_Lean_Meta_mkSimpAttr___lambda__1___closed__1();
@ -18276,34 +18192,34 @@ l_Lean_Meta_mkSimpExt___closed__2 = _init_l_Lean_Meta_mkSimpExt___closed__2();
lean_mark_persistent(l_Lean_Meta_mkSimpExt___closed__2);
l_Lean_Meta_mkSimpExt___closed__3 = _init_l_Lean_Meta_mkSimpExt___closed__3();
lean_mark_persistent(l_Lean_Meta_mkSimpExt___closed__3);
if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4668_(lean_io_mk_world());
if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4658_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_Meta_simpExtensionMapRef = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Meta_simpExtensionMapRef);
lean_dec_ref(res);
}l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4704_ = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4704_();
lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4704_);
}l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4694_ = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4694_();
lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4694_);
l_Lean_Meta_registerSimpAttr___closed__1 = _init_l_Lean_Meta_registerSimpAttr___closed__1();
lean_mark_persistent(l_Lean_Meta_registerSimpAttr___closed__1);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__1();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__1);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__2();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__2);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__3();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__3);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__4();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__4);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__5 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__5();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__5);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__6 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__6();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__6);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__7 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__7();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__7);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__8 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__8();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__8);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__9 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__9();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818____closed__9);
if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4818_(lean_io_mk_world());
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__1();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__1);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__2();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__2);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__3();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__3);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__4();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__4);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__5 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__5();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__5);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__6 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__6();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__6);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__7 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__7();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__7);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__8 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__8();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__8);
l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__9 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__9();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798____closed__9);
if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4798_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_Meta_simpExtension = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Meta_simpExtension);

506
stage0/stdlib/Lean/Parser/Extension.c generated
View file

File diff suppressed because it is too large Load diff

48
stage0/stdlib/Lean/Server/FileWorker/RequestHandling.c generated
View file

@ -60,7 +60,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleDocumentHighlight___lamb
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* lean_io_error_to_string(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_getInteractiveTermGoal___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1908_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1911_(lean_object*);
static lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___lambda__3___closed__7;
static lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__4___lambda__2___closed__1;
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonPlainGoalParams____x40_Lean_Data_Lsp_Extra___hyg_516_(lean_object*);
@ -205,7 +205,7 @@ LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Server_FileWorker_handleSem
static lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__31___lambda__3___closed__1;
LEAN_EXPORT lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__1___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Except_map___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1806_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1809_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonWaitForDiagnosticsParams____x40_Lean_Data_Lsp_Extra___hyg_24_(lean_object*);
static lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___closed__3;
static lean_object* l_Lean_Server_FileWorker_handleFoldingRange_addCommandRange___closed__1;
@ -248,7 +248,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleFoldingRange_addRanges(l
static lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___closed__10;
static lean_object* l_List_mapM_loop___at_Lean_Server_FileWorker_getInteractiveGoals___spec__5___closed__7;
lean_object* l_Lean_Syntax_findStack_x3f(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokens____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5645_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokens____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5648_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__1___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleFoldingRange_addCommandRange___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_toString(lean_object*, uint8_t);
@ -259,7 +259,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleFoldingRange___rarg___la
lean_object* l_Lean_Meta_withPPShowLetValuesImp___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_insert___at_Lean_Server_registerLspRequestHandler___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Widget_InteractiveTermGoal_toInteractiveGoal(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonFoldingRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5689_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonFoldingRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5692_(lean_object*);
lean_object* l_IO_AsyncList_waitAll___rarg(lean_object*, lean_object*);
static lean_object* l_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____closed__20;
LEAN_EXPORT lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__10___lambda__1(lean_object*);
@ -271,7 +271,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleDocumentHighlight___lamb
static lean_object* l_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____closed__10;
static lean_object* l_Lean_Server_FileWorker_handleSemanticTokensFull___rarg___closed__1;
LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_locationLinksOfInfo___lambda__3(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5467_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5470_(lean_object*);
LEAN_EXPORT lean_object* l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__29___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleSemanticTokensFull(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleSemanticTokens_highlightId___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -303,7 +303,7 @@ static lean_object* l_Lean_Server_FileWorker_noHighlightKinds___closed__12;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_FileWorker_handlePlainGoal___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_to_list(lean_object*, lean_object*);
static lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___lambda__3___closed__3;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5379_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5382_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handlePlainGoal(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Environment_contains(lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_RefInfo_instCoeRefInfoRefInfo___spec__1(size_t, size_t, lean_object*);
@ -324,9 +324,9 @@ LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleCompletion(lean_object*,
static lean_object* l_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____closed__12;
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonPlainGoal____x40_Lean_Data_Lsp_Extra___hyg_692_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_locationLinksOfInfo___lambda__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* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2845_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2848_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_getInteractiveTermGoal___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentHighlight____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2797_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentHighlight____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2800_(lean_object*);
lean_object* lean_local_ctx_pop(lean_object*);
static lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__10___lambda__4___closed__1;
static lean_object* l_List_mapM_loop___at_Lean_Server_FileWorker_getInteractiveGoals___spec__5___closed__5;
@ -347,7 +347,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Serve
lean_object* l_Lean_Elab_Info_toElabInfo_x3f(lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDocumentHighlight_highlightReturn_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDocumentHighlight_highlightReturn_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonCompletionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1687_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonCompletionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1690_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__27___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Task_Priority_default;
lean_object* l_Lean_Elab_Info_range_x3f(lean_object*);
@ -368,7 +368,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_getInteractiveTermGoal___lambd
LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__25(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_FileWorker_noHighlightKinds___closed__5;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonCompletionList____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1636_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonCompletionList____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1639_(lean_object*);
static lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___lambda__3___closed__4;
static lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__21___lambda__2___closed__1;
LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleFoldingRange_addCommandRange(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -554,7 +554,7 @@ static lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_Fil
LEAN_EXPORT lean_object* l_List_spanAux___at_Lean_Server_FileWorker_handleFoldingRange_addRanges___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__26___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_Server_FileWorker_handleSemanticTokens___lambda__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonFoldingRange____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5815_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonFoldingRange____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5818_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__7___lambda__1(lean_object*);
static lean_object* l_Lean_Server_FileWorker_handleDocumentHighlight_highlightReturn_x3f___closed__8;
LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_locationLinksOfInfo___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -633,7 +633,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_handleDocumentHighlight_highli
LEAN_EXPORT lean_object* l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__16___boxed(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDocumentHighlight___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentHighlightParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2650_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentHighlightParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2653_(lean_object*);
static lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__2___closed__2;
static lean_object* l_Lean_Server_FileWorker_locationLinksOfInfo___lambda__2___closed__3;
LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_9653____spec__15(lean_object*);
@ -16436,7 +16436,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileW
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonCompletionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1687_(x_1);
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonCompletionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1690_(x_1);
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_3;
@ -16592,7 +16592,7 @@ static lean_object* _init_l_Lean_Server_registerLspRequestHandler___at_Lean_Serv
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonCompletionList____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1636_), 1, 0);
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonCompletionList____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1639_), 1, 0);
return x_1;
}
}
@ -16889,7 +16889,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileW
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1908_(x_1);
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1911_(x_1);
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_3;
@ -17056,7 +17056,7 @@ lean_object* x_3; lean_object* x_4;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
lean_dec(x_1);
x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1806_(x_3);
x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_LanguageFeatures___hyg_1809_(x_3);
return x_4;
}
}
@ -17854,7 +17854,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileW
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentHighlightParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2650_(x_1);
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentHighlightParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2653_(x_1);
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_3;
@ -17967,7 +17967,7 @@ lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; size_t x
x_5 = lean_array_uget(x_3, x_2);
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_array_uset(x_3, x_2, x_6);
x_8 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentHighlight____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2797_(x_5);
x_8 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentHighlight____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2800_(x_5);
x_9 = 1;
x_10 = lean_usize_add(x_2, x_9);
x_11 = lean_array_uset(x_7, x_2, x_8);
@ -18346,7 +18346,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileW
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2845_(x_1);
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2848_(x_1);
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_3;
@ -18804,7 +18804,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileW
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5379_(x_1);
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5382_(x_1);
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_3;
@ -18951,7 +18951,7 @@ static lean_object* _init_l_Lean_Server_registerLspRequestHandler___at_Lean_Serv
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokens____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5645_), 1, 0);
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokens____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5648_), 1, 0);
return x_1;
}
}
@ -19248,7 +19248,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileW
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5467_(x_1);
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5470_(x_1);
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_3;
@ -19683,7 +19683,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileW
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonFoldingRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5689_(x_1);
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonFoldingRangeParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5692_(x_1);
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_3;
@ -19796,7 +19796,7 @@ lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; size_t x
x_5 = lean_array_uget(x_3, x_2);
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_array_uset(x_3, x_2, x_6);
x_8 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonFoldingRange____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5815_(x_5);
x_8 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonFoldingRange____x40_Lean_Data_Lsp_LanguageFeatures___hyg_5818_(x_5);
x_9 = 1;
x_10 = lean_usize_add(x_2, x_9);
x_11 = lean_array_uset(x_7, x_2, x_8);

12
stage0/stdlib/Lean/Server/Watchdog.c generated
View file

@ -313,7 +313,7 @@ static lean_object* l_Lean_Server_Watchdog_mkLeanServerCapabilities___closed__6;
lean_object* lean_get_prefix(lean_object*);
static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__11;
lean_object* l_Lean_FileMap_ofString(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSymbolInformation____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3319_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSymbolInformation____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3322_(lean_object*);
lean_object* l_Std_RBNode_balLeft___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_FileWorker_errorPendingRequests___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_mainLoop(lean_object*, lean_object*, lean_object*);
@ -532,7 +532,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol(lean_objec
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handleWorkspaceSymbol___spec__2___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_IO_FS_Stream_readLspRequestAs___at_Lean_Server_Watchdog_initAndRunWatchdog___spec__1___closed__1;
static lean_object* l_Lean_Server_Watchdog_findFileWorker_x21___closed__2;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonReferenceParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2432_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonReferenceParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2435_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handleNotification___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_References_definitionOf_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_to_int(lean_object*);
@ -542,7 +542,7 @@ lean_object* l___private_Lean_Data_Lsp_Internal_0__Lean_Lsp_fromJsonLeanIleanInf
lean_object* l_List_appendTR___rarg(lean_object*, lean_object*);
static lean_object* l_Lean_Server_Watchdog_forwardRequestToWorker___closed__1;
static uint8_t l_Lean_Server_Watchdog_tryWriteMessage___lambda__1___closed__1;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonWorkspaceSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2570_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonWorkspaceSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2573_(lean_object*);
LEAN_EXPORT lean_object* l_Std_RBNode_ins___at_Lean_Server_Watchdog_forwardRequestToWorker___spec__3(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_Watchdog_handleNotification___closed__3;
lean_object* l___private_Lean_Data_Lsp_InitShutdown_0__Lean_Lsp_toJsonInitializeResult____x40_Lean_Data_Lsp_InitShutdown___hyg_708_(lean_object*);
@ -14124,7 +14124,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Wat
_start:
{
lean_object* x_4;
x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonWorkspaceSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2570_(x_1);
x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonWorkspaceSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2573_(x_1);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
@ -14173,7 +14173,7 @@ lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; size_t x
x_5 = lean_array_uget(x_3, x_2);
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_array_uset(x_3, x_2, x_6);
x_8 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSymbolInformation____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3319_(x_5);
x_8 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSymbolInformation____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3322_(x_5);
x_9 = 1;
x_10 = lean_usize_add(x_2, x_9);
x_11 = lean_array_uset(x_7, x_2, x_8);
@ -14211,7 +14211,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Wat
_start:
{
lean_object* x_4;
x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonReferenceParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2432_(x_1);
x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonReferenceParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2435_(x_1);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;