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:
Joachim Breitner 2024-07-03 12:27:41 +02:00 • committed by Sebastian Ullrich
parent 15a41ffc1c
commit f6deaa8fb2
7 changed files with 1178 additions and 1223 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/PreDefinition/Structural/Eqns.lean
View file

@ -63,12 +63,12 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
let us := info.levelParams.map mkLevelParam
let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
let goal ← mkFreshExprSyntheticOpaqueMVar target
mkEqnTypes (tryRefl := true) info.declNames goal.mvarId!
mkEqnTypes (tryRefl := true) #[info.declName] goal.mvarId!
let baseName := info.declName
let mut thmNames := #[]
for i in [: eqnTypes.size] do
let type := eqnTypes[i]!
trace[Elab.definition.structural.eqns] "eqnType {i}: {type}"
trace[Elab.definition.structural.eqns] "{eqnTypes[i]!}"
let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
thmNames := thmNames.push name
let value ← mkProof info.declName type

4
stage0/stdlib/Lake/Toml/ParserUtil.c generated
View file

@ -163,6 +163,7 @@ lean_object* l_Lean_Parser_withAntiquotSpliceAndSuffix(lean_object*, lean_object
LEAN_EXPORT lean_object* l_Lake_Toml_getInfoExprPos_x3f(lean_object*);
LEAN_EXPORT lean_object* l_Lake_Toml_strAtom_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lake_Toml_dynamicNode_parenthesizer___boxed(lean_object*);
lean_object* l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lake_Toml_litWithAntiquot(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
LEAN_EXPORT lean_object* l_Lake_Toml_skipInsideQuotFn(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
@ -176,7 +177,6 @@ lean_object* l_Lean_Parser_atomicFn(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lake_Toml_epsilon_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_string_utf8_next_fast(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lake_Toml_trailing(lean_object*);
lean_object* l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lake_Toml_isBinDigit(uint32_t);
LEAN_EXPORT lean_object* l_Lake_Toml_pushLit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lake_Toml_extendTrailingFn(lean_object*, lean_object*, lean_object*);
@ -1424,7 +1424,7 @@ lean_object* x_14; lean_object* x_15;
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__2___rarg(x_2, x_3, x_4, x_14);
x_15 = l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__4___rarg(x_2, x_3, x_4, x_14);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);

2
stage0/stdlib/Lean/Elab/PreDefinition/Main.c generated
View file

@ -10753,6 +10753,7 @@ lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_1);
x_18 = l_Lean_Elab_Structural_structuralRecursion(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_16);
if (lean_obj_tag(x_18) == 0)
{
@ -12873,6 +12874,7 @@ lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_1);
x_206 = l_Lean_Elab_Structural_structuralRecursion(x_1, x_166, x_4, x_5, x_6, x_7, x_8, x_9, x_167);
if (lean_obj_tag(x_206) == 0)
{

677
stage0/stdlib/Lean/Elab/PreDefinition/Structural/Eqns.c generated
View file

File diff suppressed because it is too large Load diff

732
stage0/stdlib/Lean/Elab/PreDefinition/Structural/Main.c generated
View file

File diff suppressed because it is too large Load diff

13
stage0/stdlib/Lean/Parser/Extra.c generated
View file

@ -402,6 +402,7 @@ static lean_object* l_Lean_Parser___aux__Lean__Parser__Extra______macroRules__Le
LEAN_EXPORT lean_object* l_Lean_Parser_withResetCache_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkLinebreakBefore_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_ppSpace;
lean_object* l_Lean_PrettyPrinter_Formatter_optionalNoAntiquot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_optional_parenthesizer___closed__1;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_1790____closed__78;
LEAN_EXPORT lean_object* l_Lean_Parser_nameLit_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -664,6 +665,7 @@ LEAN_EXPORT lean_object* l_Lean_ppAllowUngrouped_formatter___rarg___boxed(lean_o
LEAN_EXPORT lean_object* l_Lean_Parser_patternIgnore(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_dbgTraceState_parenthesizer(lean_object*);
static lean_object* l_Lean_Parser_identWithPartialTrailingDot___closed__6;
lean_object* l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_ppSpace_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_1790____closed__97;
static lean_object* l_Lean_Parser_mkAntiquotSplice_parenthesizer___closed__2;
@ -717,7 +719,6 @@ LEAN_EXPORT lean_object* l_Lean_Parser_many1Indent_parenthesizer(lean_object*, l
static lean_object* l_Lean_Parser___aux__Lean__Parser__Extra______macroRules__Lean__Parser__termRegister__parser__alias_x28Kind_x3a_x3d___x29______________1___lambda__1___closed__35;
static lean_object* l_Lean_Parser_identWithPartialTrailingDot___closed__3;
LEAN_EXPORT lean_object* l_Lean_Parser_mkAntiquotSplice_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_String_intercalate(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_mkAntiquot_formatter___closed__7;
static lean_object* l_Lean_Parser_identWithPartialTrailingDot___closed__1;
@ -2952,7 +2953,7 @@ x_9 = lean_alloc_closure((void*)(l_Lean_Parser_withAntiquotSpliceAndSuffix_forma
lean_closure_set(x_9, 0, x_7);
lean_closure_set(x_9, 1, x_1);
lean_closure_set(x_9, 2, x_8);
x_10 = l_Lean_PrettyPrinter_Formatter_visitArgs(x_9, x_2, x_3, x_4, x_5, x_6);
x_10 = l_Lean_PrettyPrinter_Formatter_optionalNoAntiquot_formatter(x_9, x_2, x_3, x_4, x_5, x_6);
return x_10;
}
}
@ -4744,7 +4745,7 @@ x_43 = l_Lean_PrettyPrinter_Formatter_pushWhitespace(x_42, x_6, x_7, x_8, x_9, x
x_44 = lean_ctor_get(x_43, 1);
lean_inc(x_44);
lean_dec(x_43);
x_45 = l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__2___rarg(x_7, x_8, x_9, x_44);
x_45 = l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__4___rarg(x_7, x_8, x_9, x_44);
x_46 = lean_ctor_get(x_45, 1);
lean_inc(x_46);
lean_dec(x_45);
@ -4756,7 +4757,7 @@ goto block_18;
else
{
lean_object* x_48; lean_object* x_49; lean_object* x_50;
x_48 = l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__2___rarg(x_7, x_8, x_9, x_38);
x_48 = l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__4___rarg(x_7, x_8, x_9, x_38);
x_49 = lean_ctor_get(x_48, 1);
lean_inc(x_49);
lean_dec(x_48);
@ -4865,7 +4866,7 @@ x_66 = l_Lean_PrettyPrinter_Formatter_pushWhitespace(x_65, x_6, x_7, x_8, x_9, x
x_67 = lean_ctor_get(x_66, 1);
lean_inc(x_67);
lean_dec(x_66);
x_68 = l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__2___rarg(x_7, x_8, x_9, x_67);
x_68 = l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__4___rarg(x_7, x_8, x_9, x_67);
x_69 = lean_ctor_get(x_68, 1);
lean_inc(x_69);
lean_dec(x_68);
@ -4877,7 +4878,7 @@ goto block_18;
else
{
lean_object* x_71; lean_object* x_72; lean_object* x_73;
x_71 = l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__2___rarg(x_7, x_8, x_9, x_61);
x_71 = l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__4___rarg(x_7, x_8, x_9, x_61);
x_72 = lean_ctor_get(x_71, 1);
lean_inc(x_72);
lean_dec(x_71);

969
stage0/stdlib/Lean/PrettyPrinter/Formatter.c generated
View file

File diff suppressed because it is too large Load diff