max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-07 13:29:50 -07:00
parent d991c20859
commit 61976c4e56
15 changed files with 3009 additions and 917 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
stage0/src/Lean/Elab/DeclModifiers.lean generated
View file

@ -145,11 +145,22 @@ def applyVisibility (visibility : Visibility) (declName : Name) : m Name := do
checkNotAlreadyDeclared declName
pure declName
def checkIfShadowingStructureField (declName : Name) : m Unit := do
match declName with
| Name.str pre .. =>
if isStructure (← getEnv) pre then
let fieldNames := getStructureFieldsFlattened (← getEnv) pre
for fieldName in fieldNames do
if pre ++ fieldName == declName then
throwError "invalid declaration name '{declName}', structure '{pre}' has field '{fieldName}'"
| _ => pure ()
def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name) : m (Name × Name) := do
let name := (extractMacroScopes shortName).name
unless name.isAtomic || isFreshInstanceName name do
throwError "atomic identifier expected '{shortName}'"
let declName := currNamespace ++ shortName
checkIfShadowingStructureField declName
let declName ← applyVisibility modifiers.visibility declName
match modifiers.visibility with
| Visibility.protected =>

2
stage0/src/Lean/Elab/Extra.lean generated
View file

@ -228,7 +228,7 @@ where
withRef ref <| return Tree.term ref (← mkCoe maxType type e)
@[builtinTermElab binop]
def elabBinOp' : TermElab := fun stx expectedType? => do
def elabBinOp : TermElab := fun stx expectedType? => do
let tree ← toTree stx
let r ← analyze tree expectedType?
trace[Elab.binop] "hasUncomparable: {r.hasUncomparable}, maxType: {r.max?}"

1
stage0/src/Lean/Parser/Term.lean generated
View file

@ -203,6 +203,7 @@ def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
@[builtinTermParser] def binrel := leading_parser "binrel% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def binop := leading_parser "binop% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def binop_lazy := leading_parser "binop_lazy% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def forInMacro := leading_parser "forIn% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec

16
stage0/stdlib/Lean/Elab/BuiltinCommand.c generated
View file

@ -198,7 +198,6 @@ lean_object* l_Lean_Elab_OpenDecl_resolveId___at_Lean_Elab_Command_elabExport___
static lean_object* l_Lean_Elab_Command_elabCheckFailure___closed__1;
lean_object* l_Lean_Elab_Command_elabOpen___lambda__1(lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___spec__2___lambda__2___closed__11;
lean_object* l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ResolveName_resolveNamespace_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_runTermElabM___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Command_elabCheckFailure___closed__2;
@ -218,6 +217,7 @@ lean_object* l_Lean_Elab_Command_elabCheck___boxed(lean_object*, lean_object*, l
lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda_loop___spec__1___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabEvalUnsafe_match__4___rarg(lean_object*, lean_object*);
lean_object* l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__7(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_elabCheck___closed__5;
lean_object* lean_st_ref_take(lean_object*, lean_object*);
lean_object* l_Lean_getOptionDecl(lean_object*, lean_object*);
@ -4228,7 +4228,7 @@ lean_object* x_19; lean_object* x_20;
x_19 = lean_ctor_get(x_9, 0);
lean_inc(x_19);
lean_dec(x_9);
x_20 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__5(x_19, x_1, x_2, x_6);
x_20 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__7(x_19, x_1, x_2, x_6);
lean_dec(x_1);
return x_20;
}
@ -11254,7 +11254,7 @@ lean_inc(x_25);
x_26 = lean_ctor_get(x_24, 1);
lean_inc(x_26);
lean_dec(x_24);
x_27 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__5(x_15, x_2, x_3, x_26);
x_27 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__7(x_15, x_2, x_3, x_26);
lean_dec(x_2);
x_28 = !lean_is_exclusive(x_27);
if (x_28 == 0)
@ -11285,7 +11285,7 @@ lean_inc(x_32);
x_33 = lean_ctor_get(x_24, 1);
lean_inc(x_33);
lean_dec(x_24);
x_34 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__5(x_15, x_2, x_3, x_33);
x_34 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__7(x_15, x_2, x_3, x_33);
lean_dec(x_2);
x_35 = !lean_is_exclusive(x_34);
if (x_35 == 0)
@ -12157,7 +12157,7 @@ lean_inc(x_25);
x_26 = lean_ctor_get(x_24, 1);
lean_inc(x_26);
lean_dec(x_24);
x_27 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__5(x_15, x_2, x_3, x_26);
x_27 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__7(x_15, x_2, x_3, x_26);
lean_dec(x_2);
x_28 = !lean_is_exclusive(x_27);
if (x_28 == 0)
@ -12188,7 +12188,7 @@ lean_inc(x_32);
x_33 = lean_ctor_get(x_24, 1);
lean_inc(x_33);
lean_dec(x_24);
x_34 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__5(x_15, x_2, x_3, x_33);
x_34 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__7(x_15, x_2, x_3, x_33);
lean_dec(x_2);
x_35 = !lean_is_exclusive(x_34);
if (x_35 == 0)
@ -16121,7 +16121,7 @@ lean_inc(x_20);
x_21 = lean_ctor_get(x_19, 1);
lean_inc(x_21);
lean_dec(x_19);
x_22 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__5(x_10, x_2, x_3, x_21);
x_22 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__7(x_10, x_2, x_3, x_21);
lean_dec(x_2);
x_23 = !lean_is_exclusive(x_22);
if (x_23 == 0)
@ -16152,7 +16152,7 @@ lean_inc(x_27);
x_28 = lean_ctor_get(x_19, 1);
lean_inc(x_28);
lean_dec(x_19);
x_29 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__5(x_10, x_2, x_3, x_28);
x_29 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__7(x_10, x_2, x_3, x_28);
lean_dec(x_2);
x_30 = !lean_is_exclusive(x_29);
if (x_30 == 0)

846
stage0/stdlib/Lean/Elab/Command.c generated
View file

File diff suppressed because it is too large Load diff

562
stage0/stdlib/Lean/Elab/DeclModifiers.c generated
View file

@ -17,6 +17,7 @@ lean_object* l_List_reverse___rarg(lean_object*);
lean_object* l_Lean_Elab_instToFormatModifiers_match__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_RecKind_noConfusion___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Visibility_noConfusion___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkDeclName___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instToStringVisibility___closed__3;
static lean_object* l_Lean_Elab_Visibility_noConfusion___rarg___closed__1;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_expandDeclId___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
@ -30,6 +31,7 @@ lean_object* lean_mk_empty_array_with_capacity(lean_object*);
static lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__3___closed__2;
lean_object* l_Lean_Elab_expandOptDocComment_x3f(lean_object*);
static lean_object* l_List_mapTRAux___at_Lean_Elab_instToFormatModifiers___spec__1___closed__8;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__2(lean_object*, lean_object*);
extern lean_object* l_Lean_nullKind;
lean_object* l_Lean_addDocString_x27___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__3___closed__1;
@ -45,6 +47,7 @@ uint8_t l_USize_decEq(size_t, size_t);
lean_object* lean_array_uget(lean_object*, size_t);
uint8_t l_Lean_Elab_Modifiers_isProtected(lean_object*);
static lean_object* l_List_mapTRAux___at_Lean_Elab_instToFormatModifiers___spec__1___closed__9;
lean_object* l_Lean_Elab_mkDeclName_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Format_defWidth;
static lean_object* l_List_mapTRAux___at_Lean_Elab_instToFormatModifiers___spec__1___closed__4;
lean_object* l_Lean_Elab_mkDeclName(lean_object*);
@ -54,18 +57,22 @@ static lean_object* l_Lean_Elab_instToFormatModifiers___closed__18;
static lean_object* l_Lean_Elab_instToFormatModifiers___closed__6;
lean_object* l_Lean_Elab_Visibility_toCtorIdx___boxed(lean_object*);
lean_object* l_Lean_Elab_applyVisibility___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_RecKind_noConfusion(lean_object*);
lean_object* l_Lean_Elab_applyVisibility___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Modifiers_isPartial___boxed(lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkDeclName___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkDeclName___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkIfShadowingStructureField___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_private_to_user_name(lean_object*);
lean_object* l_Lean_Elab_RecKind_toCtorIdx(uint8_t);
lean_object* l_Lean_Elab_Visibility_noConfusion___rarg___lambda__1(lean_object*);
static lean_object* l_Lean_Elab_instToStringModifiers___closed__3;
lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__1;
lean_object* l_Lean_Elab_checkNotAlreadyDeclared_match__1(lean_object*);
lean_object* l_Lean_Elab_instToFormatModifiers_match__3___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__4;
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
uint8_t l_Lean_Elab_instInhabitedRecKind;
@ -76,6 +83,8 @@ lean_object* l_Lean_Elab_Modifiers_docString_x3f___default;
static lean_object* l_Lean_Elab_instToFormatModifiers___closed__25;
lean_object* l_Lean_Elab_instToStringVisibility(uint8_t);
lean_object* l_Lean_Elab_Modifiers_isNonrec_match__1(lean_object*);
uint8_t l_USize_decLt(size_t, size_t);
lean_object* l_Lean_Elab_checkIfShadowingStructureField___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Modifiers_isPartial_match__1(lean_object*);
lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__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*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_applyVisibility_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -83,6 +92,7 @@ static lean_object* l_Lean_Elab_instToFormatModifiers___closed__8;
static lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__3___closed__4;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_expandDeclId___spec__1___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Modifiers_isNonrec___boxed(lean_object*);
lean_object* l_Lean_Elab_checkIfShadowingStructureField___rarg___lambda__1___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instToFormatModifiers___closed__23;
lean_object* l_Lean_Elab_applyVisibility_match__1(lean_object*);
uint8_t l_Lean_Elab_Modifiers_isNoncomputable___default;
@ -90,6 +100,7 @@ lean_object* l_Lean_Elab_expandDeclId___rarg(lean_object*, lean_object*, lean_ob
lean_object* l_Lean_Elab_expandDeclId_match__1(lean_object*);
lean_object* l_Lean_Elab_expandDeclId_match__2(lean_object*);
static lean_object* l_Lean_Elab_mkDeclName___rarg___closed__2;
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__6;
lean_object* l_Lean_Elab_instToFormatModifiers_match__3(lean_object*);
lean_object* l_Lean_Elab_expandOptDocComment_x3f_match__2(lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
@ -97,12 +108,17 @@ static lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__3___closed__9;
static lean_object* l_Lean_Elab_instToFormatModifiers___closed__21;
static lean_object* l_Lean_Elab_instToFormatModifiers___closed__13;
lean_object* l_Lean_Elab_applyVisibility_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__2___closed__1;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_expandDeclId___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__3(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getStructureFieldsFlattened(lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_Elab_mkDeclName___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__3___closed__8;
static lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__3___closed__3;
lean_object* l_Lean_Name_toString(lean_object*, uint8_t);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__5;
lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_instToStringVisibility_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_instToStringVisibility_match__1(lean_object*);
@ -130,7 +146,7 @@ static lean_object* l_Lean_Elab_instToFormatModifiers___closed__11;
extern lean_object* l_Lean_protectedExt;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_expandDeclId___spec__1(lean_object*);
static lean_object* l_Lean_Elab_instToFormatModifiers___closed__27;
lean_object* l_Lean_Elab_mkDeclName_match__2___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__1(lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
lean_object* l_Lean_Elab_instToFormatModifiers_match__2___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instToFormatModifiers___closed__10;
@ -139,16 +155,18 @@ static lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__3___closed__3;
lean_object* l_Lean_Elab_Modifiers_attrs___default;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_expandDeclId___spec__1___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Visibility_noConfusion(lean_object*);
lean_object* l_Lean_Elab_mkDeclName___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkDeclName___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instToFormatModifiers___closed__20;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_expandDeclId___spec__1___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
static lean_object* l_List_mapTRAux___at_Lean_Elab_instToFormatModifiers___spec__1___closed__7;
lean_object* l_Lean_Elab_checkIfShadowingStructureField___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_throwErrorAt___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkDeclName_match__2___rarg(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Elab_expandDeclId___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkIfShadowingStructureField_match__1(lean_object*);
lean_object* l_Lean_Elab_Visibility_noConfusion___rarg(uint8_t, uint8_t, lean_object*);
static lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__3___closed__6;
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__3(lean_object*, lean_object*);
lean_object* l_Lean_Elab_expandDeclIdCore(lean_object*);
static lean_object* l_Lean_Elab_instToStringModifiers___closed__1;
lean_object* l_Lean_Elab_expandDeclId_match__1___rarg(lean_object*, lean_object*);
@ -178,6 +196,7 @@ static lean_object* l_Lean_Elab_instInhabitedModifiers___closed__1;
lean_object* l_Lean_Syntax_getArgs(lean_object*);
lean_object* l_Lean_Name_append(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_mkDeclName___rarg___lambda__1___closed__1;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_instToFormatModifiers_match__1(lean_object*);
lean_object* l_Lean_Syntax_getKind(lean_object*);
lean_object* l_Lean_Elab_expandOptDocComment_x3f_match__1(lean_object*);
@ -185,13 +204,15 @@ lean_object* l_Lean_Elab_mkDeclName___rarg___lambda__1___boxed(lean_object*, lea
lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__1___closed__3;
lean_object* l_Lean_Elab_expandDeclId___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1(lean_object*);
uint8_t l_Lean_Elab_instInhabitedVisibility;
lean_object* l_Lean_Elab_Modifiers_isPrivate___boxed(lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__3;
lean_object* l_Lean_Elab_Modifiers_isNonrec_match__1___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instToFormatModifiers___closed__12;
lean_object* l_Lean_Elab_applyVisibility___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Elab_Modifiers_visibility___default;
lean_object* l_Lean_Elab_mkDeclName_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkDeclName_match__1___rarg(uint8_t, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instToFormatModifiers___closed__22;
static lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__1___closed__1;
lean_object* l_Lean_throwError___rarg(lean_object*, lean_object*, lean_object*);
@ -206,6 +227,7 @@ uint8_t l_Lean_Elab_Modifiers_isNonrec(lean_object*);
lean_object* l_Lean_Elab_Modifiers_addAttribute(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__3___closed__10;
lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, uint8_t, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__3___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instToFormatModifiers___closed__28;
static lean_object* l_Lean_Elab_instToFormatModifiers___closed__14;
lean_object* l_Lean_Elab_expandOptDocComment_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -214,8 +236,10 @@ lean_object* l_Lean_Elab_applyVisibility___rarg___lambda__1(lean_object*, lean_o
lean_object* l_Lean_Elab_mkDeclName_match__1(lean_object*);
lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__3___closed__7;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_instToFormatModifiers_match__2(lean_object*);
lean_object* l_Lean_Elab_Visibility_toCtorIdx(uint8_t);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__2;
static lean_object* l_Lean_Elab_instToFormatModifiers___closed__7;
lean_object* l_Lean_Elab_applyVisibility___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_instToStringVisibility_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -223,6 +247,7 @@ lean_object* l_Lean_Elab_Modifiers_isPartial_match__1___rarg(lean_object*, lean_
lean_object* lean_string_length(lean_object*);
lean_object* l_Lean_indentD(lean_object*);
lean_object* l_Lean_Elab_elabModifiers___rarg___boxed(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_checkIfShadowingStructureField___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Elab_Modifiers_isUnsafe___default;
static lean_object* l_Lean_Elab_elabModifiers___rarg___closed__1;
uint8_t l_Lean_Elab_Modifiers_isPrivate(lean_object*);
@ -230,6 +255,7 @@ lean_object* l_Lean_Elab_Modifiers_isPrivate_match__1___rarg(lean_object*, lean_
static lean_object* l_Lean_Elab_expandDeclIdCore___closed__1;
static lean_object* l_Lean_Elab_mkDeclName___rarg___closed__1;
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkIfShadowingStructureField(lean_object*);
static lean_object* l_Lean_Elab_expandOptDocComment_x3f___rarg___closed__1;
lean_object* l_Lean_Elab_expandOptDocComment_x3f___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkNotAlreadyDeclared(lean_object*);
@ -239,6 +265,7 @@ lean_object* l_Lean_Elab_expandDeclId(lean_object*);
static lean_object* l_Lean_Elab_instToFormatModifiers___closed__15;
static lean_object* l_Lean_Elab_Modifiers_attrs___default___closed__1;
uint8_t l_Lean_Elab_isFreshInstanceName(lean_object*);
lean_object* l_Lean_Elab_checkIfShadowingStructureField_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkNotAlreadyDeclared_match__1___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_List_mapTRAux___at_Lean_Elab_instToFormatModifiers___spec__1___closed__5;
static lean_object* l_Lean_Elab_instToFormatModifiers___closed__29;
@ -255,9 +282,9 @@ static lean_object* l_Lean_Elab_instToStringVisibility___closed__2;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Syntax_SepArray_getElems___spec__1(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_applyVisibility___rarg(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* l_Lean_Elab_Visibility_noConfusion___rarg___lambda__1___boxed(lean_object*);
uint8_t l_Lean_isStructure(lean_object*, lean_object*);
lean_object* l_Lean_Elab_expandDeclId___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__1___closed__2;
lean_object* l_Lean_Elab_mkDeclName_match__2(lean_object*);
lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_Elab_instToStringVisibility___boxed(lean_object*);
lean_object* l_Lean_Elab_mkDeclName___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -3369,7 +3396,7 @@ x_7 = l_Lean_Elab_applyVisibility___rarg(x_1, x_2, x_3, x_6, x_5);
return x_7;
}
}
lean_object* l_Lean_Elab_mkDeclName_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Elab_checkIfShadowingStructureField_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 1)
@ -3395,15 +3422,434 @@ return x_9;
}
}
}
lean_object* l_Lean_Elab_mkDeclName_match__1(lean_object* x_1) {
lean_object* l_Lean_Elab_checkIfShadowingStructureField_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_mkDeclName_match__1___rarg), 3, 0);
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_checkIfShadowingStructureField_match__1___rarg), 3, 0);
return x_2;
}
}
lean_object* l_Lean_Elab_mkDeclName_match__2___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__1(lean_object* x_1, size_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, size_t x_8, lean_object* x_9) {
_start:
{
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
lean_dec(x_9);
x_11 = lean_ctor_get(x_1, 0);
lean_inc(x_11);
lean_dec(x_1);
x_12 = lean_ctor_get(x_11, 1);
lean_inc(x_12);
lean_dec(x_11);
x_13 = lean_apply_2(x_12, lean_box(0), x_10);
return x_13;
}
else
{
lean_object* x_14; size_t x_15; size_t x_16; lean_object* x_17;
x_14 = lean_ctor_get(x_9, 0);
lean_inc(x_14);
lean_dec(x_9);
x_15 = 1;
x_16 = x_2 + x_15;
x_17 = l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg(x_1, x_3, x_4, x_5, x_6, x_7, x_8, x_16, x_14);
return x_17;
}
}
}
static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__2___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_box(0);
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__2(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__2___closed__1;
x_4 = lean_apply_2(x_1, lean_box(0), x_3);
return x_4;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__3(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
lean_dec(x_1);
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__2___closed__1;
x_6 = lean_apply_2(x_4, lean_box(0), x_5);
return x_6;
}
}
static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("invalid declaration name '");
return x_1;
}
}
static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__1;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("', structure '");
return x_1;
}
}
static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__3;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("' has field '");
return x_1;
}
}
static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__5;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, size_t x_7, size_t x_8, lean_object* x_9) {
_start:
{
uint8_t x_10;
x_10 = x_8 < x_7;
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_11 = lean_ctor_get(x_1, 0);
lean_inc(x_11);
lean_dec(x_1);
x_12 = lean_ctor_get(x_11, 1);
lean_inc(x_12);
lean_dec(x_11);
x_13 = lean_apply_2(x_12, lean_box(0), x_9);
return x_13;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_dec(x_9);
x_14 = lean_array_uget(x_6, x_8);
x_15 = lean_ctor_get(x_1, 1);
lean_inc(x_15);
lean_inc(x_14);
x_16 = l_Lean_Name_append(x_4, x_14);
x_17 = lean_name_eq(x_16, x_3);
lean_dec(x_16);
x_18 = lean_box_usize(x_8);
x_19 = lean_box_usize(x_7);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_1);
x_20 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__1___boxed), 9, 8);
lean_closure_set(x_20, 0, x_1);
lean_closure_set(x_20, 1, x_18);
lean_closure_set(x_20, 2, x_2);
lean_closure_set(x_20, 3, x_3);
lean_closure_set(x_20, 4, x_4);
lean_closure_set(x_20, 5, x_5);
lean_closure_set(x_20, 6, x_6);
lean_closure_set(x_20, 7, x_19);
if (x_17 == 0)
{
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_dec(x_14);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_21 = lean_ctor_get(x_1, 0);
lean_inc(x_21);
lean_dec(x_1);
x_22 = lean_ctor_get(x_21, 1);
lean_inc(x_22);
lean_dec(x_21);
x_23 = lean_box(0);
lean_inc(x_22);
x_24 = lean_apply_2(x_22, lean_box(0), x_23);
x_25 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__2___boxed), 2, 1);
lean_closure_set(x_25, 0, x_22);
x_26 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_24, x_25);
x_27 = lean_apply_4(x_15, lean_box(0), lean_box(0), x_26, x_20);
return x_27;
}
else
{
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;
x_28 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_28, 0, x_3);
x_29 = l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__2;
x_30 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_30, 0, x_29);
lean_ctor_set(x_30, 1, x_28);
x_31 = l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__4;
x_32 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_32, 0, x_30);
lean_ctor_set(x_32, 1, x_31);
x_33 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_33, 0, x_4);
x_34 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_34, 0, x_32);
lean_ctor_set(x_34, 1, x_33);
x_35 = l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__6;
x_36 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_36, 0, x_34);
lean_ctor_set(x_36, 1, x_35);
x_37 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_37, 0, x_14);
x_38 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_38, 0, x_36);
lean_ctor_set(x_38, 1, x_37);
x_39 = l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__3___closed__2;
x_40 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_40, 0, x_38);
lean_ctor_set(x_40, 1, x_39);
lean_inc(x_1);
x_41 = l_Lean_throwError___rarg(x_1, x_2, x_40);
x_42 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__3___boxed), 2, 1);
lean_closure_set(x_42, 0, x_1);
x_43 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_41, x_42);
x_44 = lean_apply_4(x_15, lean_box(0), lean_box(0), x_43, x_20);
return x_44;
}
}
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___boxed), 9, 0);
return x_2;
}
}
lean_object* l_Lean_Elab_checkIfShadowingStructureField___rarg___lambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
lean_dec(x_1);
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = lean_box(0);
x_6 = lean_apply_2(x_4, lean_box(0), x_5);
return x_6;
}
}
lean_object* l_Lean_Elab_checkIfShadowingStructureField___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
uint8_t x_7; lean_object* x_8; lean_object* x_9; size_t x_10; size_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_7 = 1;
lean_inc(x_1);
x_8 = l_Lean_getStructureFieldsFlattened(x_6, x_1, x_7);
x_9 = lean_array_get_size(x_8);
x_10 = lean_usize_of_nat(x_9);
lean_dec(x_9);
x_11 = 0;
x_12 = lean_box(0);
lean_inc(x_5);
lean_inc(x_2);
x_13 = l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg(x_2, x_3, x_4, x_1, x_5, x_8, x_10, x_11, x_12);
x_14 = lean_alloc_closure((void*)(l_Lean_Elab_checkIfShadowingStructureField___rarg___lambda__1___boxed), 2, 1);
lean_closure_set(x_14, 0, x_2);
x_15 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_13, x_14);
return x_15;
}
}
lean_object* l_Lean_Elab_checkIfShadowingStructureField___rarg___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
uint8_t x_8;
lean_inc(x_1);
x_8 = l_Lean_isStructure(x_7, x_1);
if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_9 = lean_ctor_get(x_2, 0);
lean_inc(x_9);
lean_dec(x_2);
x_10 = lean_ctor_get(x_9, 1);
lean_inc(x_10);
lean_dec(x_9);
x_11 = lean_box(0);
x_12 = lean_apply_2(x_10, lean_box(0), x_11);
return x_12;
}
else
{
lean_object* x_13; lean_object* x_14;
lean_inc(x_5);
x_13 = lean_alloc_closure((void*)(l_Lean_Elab_checkIfShadowingStructureField___rarg___lambda__2), 6, 5);
lean_closure_set(x_13, 0, x_1);
lean_closure_set(x_13, 1, x_2);
lean_closure_set(x_13, 2, x_3);
lean_closure_set(x_13, 3, x_4);
lean_closure_set(x_13, 4, x_5);
x_14 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_6, x_13);
return x_14;
}
}
}
lean_object* l_Lean_Elab_checkIfShadowingStructureField___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
if (lean_obj_tag(x_4) == 1)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_5 = lean_ctor_get(x_4, 0);
lean_inc(x_5);
x_6 = lean_ctor_get(x_1, 1);
lean_inc(x_6);
x_7 = lean_ctor_get(x_2, 0);
lean_inc(x_7);
lean_dec(x_2);
lean_inc(x_7);
lean_inc(x_6);
x_8 = lean_alloc_closure((void*)(l_Lean_Elab_checkIfShadowingStructureField___rarg___lambda__3), 7, 6);
lean_closure_set(x_8, 0, x_5);
lean_closure_set(x_8, 1, x_1);
lean_closure_set(x_8, 2, x_3);
lean_closure_set(x_8, 3, x_4);
lean_closure_set(x_8, 4, x_6);
lean_closure_set(x_8, 5, x_7);
x_9 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_7, x_8);
return x_9;
}
else
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_10 = lean_ctor_get(x_1, 0);
lean_inc(x_10);
lean_dec(x_1);
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
x_12 = lean_box(0);
x_13 = lean_apply_2(x_11, lean_box(0), x_12);
return x_13;
}
}
}
lean_object* l_Lean_Elab_checkIfShadowingStructureField(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_checkIfShadowingStructureField___rarg), 4, 0);
return x_2;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__1___boxed(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) {
_start:
{
size_t x_10; size_t x_11; lean_object* x_12;
x_10 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_11 = lean_unbox_usize(x_8);
lean_dec(x_8);
x_12 = l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__1(x_1, x_10, x_3, x_4, x_5, x_6, x_7, x_11, x_9);
return x_12;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__2___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__2(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__3___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__3(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___boxed(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) {
_start:
{
size_t x_10; size_t x_11; lean_object* x_12;
x_10 = lean_unbox_usize(x_7);
lean_dec(x_7);
x_11 = lean_unbox_usize(x_8);
lean_dec(x_8);
x_12 = l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_10, x_11, x_9);
return x_12;
}
}
lean_object* l_Lean_Elab_checkIfShadowingStructureField___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Elab_checkIfShadowingStructureField___rarg___lambda__1(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_mkDeclName_match__1___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
@ -3427,21 +3873,21 @@ return x_8;
}
}
}
lean_object* l_Lean_Elab_mkDeclName_match__2(lean_object* x_1) {
lean_object* l_Lean_Elab_mkDeclName_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_mkDeclName_match__2___rarg___boxed), 3, 0);
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_mkDeclName_match__1___rarg___boxed), 3, 0);
return x_2;
}
}
lean_object* l_Lean_Elab_mkDeclName_match__2___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Elab_mkDeclName_match__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = lean_unbox(x_1);
lean_dec(x_1);
x_5 = l_Lean_Elab_mkDeclName_match__2___rarg(x_4, x_2, x_3);
x_5 = l_Lean_Elab_mkDeclName_match__1___rarg(x_4, x_2, x_3);
return x_5;
}
}
@ -3523,27 +3969,50 @@ return x_21;
}
}
}
lean_object* l_Lean_Elab_mkDeclName___rarg___lambda__2(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* l_Lean_Elab_mkDeclName___rarg___lambda__2(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) {
_start:
{
lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
uint8_t x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_10 = lean_ctor_get_uint8(x_1, sizeof(void*)*2);
lean_inc(x_4);
lean_inc(x_2);
x_11 = l_Lean_Elab_applyVisibility___rarg(x_2, x_3, x_4, x_10, x_5);
x_12 = lean_box(x_10);
x_13 = lean_alloc_closure((void*)(l_Lean_Elab_mkDeclName___rarg___lambda__1___boxed), 6, 5);
lean_closure_set(x_13, 0, x_12);
lean_closure_set(x_13, 1, x_2);
lean_closure_set(x_13, 2, x_6);
lean_closure_set(x_13, 3, x_7);
lean_closure_set(x_13, 4, x_4);
x_14 = lean_apply_4(x_8, lean_box(0), lean_box(0), x_11, x_13);
return x_14;
}
}
lean_object* l_Lean_Elab_mkDeclName___rarg___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
lean_inc(x_2);
x_8 = l_Lean_Name_append(x_1, x_2);
x_9 = lean_ctor_get(x_3, 1);
lean_inc(x_9);
x_10 = lean_ctor_get_uint8(x_4, sizeof(void*)*2);
lean_inc(x_6);
lean_inc(x_8);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_11 = l_Lean_Elab_applyVisibility___rarg(x_3, x_5, x_6, x_10, x_8);
x_12 = lean_box(x_10);
x_13 = lean_alloc_closure((void*)(l_Lean_Elab_mkDeclName___rarg___lambda__1___boxed), 6, 5);
lean_closure_set(x_13, 0, x_12);
lean_closure_set(x_13, 1, x_3);
lean_closure_set(x_13, 2, x_2);
lean_closure_set(x_13, 3, x_1);
lean_closure_set(x_13, 4, x_6);
x_14 = lean_apply_4(x_9, lean_box(0), lean_box(0), x_11, x_13);
return x_14;
x_10 = l_Lean_Elab_checkIfShadowingStructureField___rarg(x_3, x_4, x_5, x_8);
lean_inc(x_9);
x_11 = lean_alloc_closure((void*)(l_Lean_Elab_mkDeclName___rarg___lambda__2___boxed), 9, 8);
lean_closure_set(x_11, 0, x_6);
lean_closure_set(x_11, 1, x_3);
lean_closure_set(x_11, 2, x_4);
lean_closure_set(x_11, 3, x_5);
lean_closure_set(x_11, 4, x_8);
lean_closure_set(x_11, 5, x_2);
lean_closure_set(x_11, 6, x_1);
lean_closure_set(x_11, 7, x_9);
x_12 = lean_apply_4(x_9, lean_box(0), lean_box(0), x_10, x_11);
return x_12;
}
}
static lean_object* _init_l_Lean_Elab_mkDeclName___rarg___closed__1() {
@ -3575,13 +4044,13 @@ lean_dec(x_7);
lean_inc(x_3);
lean_inc(x_1);
lean_inc(x_6);
x_9 = lean_alloc_closure((void*)(l_Lean_Elab_mkDeclName___rarg___lambda__2___boxed), 7, 6);
x_9 = lean_alloc_closure((void*)(l_Lean_Elab_mkDeclName___rarg___lambda__3___boxed), 7, 6);
lean_closure_set(x_9, 0, x_4);
lean_closure_set(x_9, 1, x_6);
lean_closure_set(x_9, 2, x_1);
lean_closure_set(x_9, 3, x_5);
lean_closure_set(x_9, 4, x_2);
lean_closure_set(x_9, 5, x_3);
lean_closure_set(x_9, 3, x_2);
lean_closure_set(x_9, 4, x_3);
lean_closure_set(x_9, 5, x_5);
x_10 = l_Lean_Name_isAtomic(x_8);
if (x_10 == 0)
{
@ -3665,13 +4134,22 @@ x_8 = l_Lean_Elab_mkDeclName___rarg___lambda__1(x_7, x_2, x_3, x_4, x_5, x_6);
return x_8;
}
}
lean_object* l_Lean_Elab_mkDeclName___rarg___lambda__2___boxed(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* l_Lean_Elab_mkDeclName___rarg___lambda__2___boxed(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) {
_start:
{
lean_object* x_10;
x_10 = l_Lean_Elab_mkDeclName___rarg___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_9);
lean_dec(x_1);
return x_10;
}
}
lean_object* l_Lean_Elab_mkDeclName___rarg___lambda__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8;
x_8 = l_Lean_Elab_mkDeclName___rarg___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
x_8 = l_Lean_Elab_mkDeclName___rarg___lambda__3(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_7);
lean_dec(x_4);
return x_8;
}
}
@ -4348,6 +4826,20 @@ l_Lean_Elab_elabModifiers___rarg___lambda__3___closed__10 = _init_l_Lean_Elab_el
lean_mark_persistent(l_Lean_Elab_elabModifiers___rarg___lambda__3___closed__10);
l_Lean_Elab_elabModifiers___rarg___closed__1 = _init_l_Lean_Elab_elabModifiers___rarg___closed__1();
lean_mark_persistent(l_Lean_Elab_elabModifiers___rarg___closed__1);
l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__2___closed__1 = _init_l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__2___closed__1();
lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___lambda__2___closed__1);
l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__1 = _init_l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__1();
lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__1);
l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__2 = _init_l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__2();
lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__2);
l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__3 = _init_l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__3();
lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__3);
l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__4 = _init_l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__4();
lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__4);
l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__5 = _init_l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__5();
lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__5);
l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__6 = _init_l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__6();
lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Elab_checkIfShadowingStructureField___spec__1___rarg___closed__6);
l_Lean_Elab_mkDeclName___rarg___lambda__1___closed__1 = _init_l_Lean_Elab_mkDeclName___rarg___lambda__1___closed__1();
lean_mark_persistent(l_Lean_Elab_mkDeclName___rarg___lambda__1___closed__1);
l_Lean_Elab_mkDeclName___rarg___lambda__1___closed__2 = _init_l_Lean_Elab_mkDeclName___rarg___lambda__1___closed__2();

10
stage0/stdlib/Lean/Elab/Declaration.c generated
View file

@ -25,6 +25,7 @@ static lean_object* l_Lean_Elab_Command_expandInitCmd___lambda__1___closed__32;
static lean_object* l___regBuiltin_Lean_Elab_Command_elabDeclaration___closed__4;
static lean_object* l_Lean_Elab_Command_expandInitCmd___closed__20;
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_myMacro____x40_Init_Notation___hyg_72____spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_applyVisibility___at_Lean_Elab_Command_expandDeclId___spec__5(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_compileDecl___at_Lean_Elab_Term_evalExpr___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_extractMacroScopes(lean_object*);
static lean_object* l_Lean_Elab_Command_elabDeclaration___closed__9;
@ -149,7 +150,6 @@ static lean_object* l_Lean_Elab_Command_expandInitCmd___closed__19;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_expandMutualNamespace___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_addDeclarationRanges___at_Lean_Elab_Command_elabAxiom___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ConstantInfo_levelParams(lean_object*);
lean_object* l_Lean_Elab_applyVisibility___at_Lean_Elab_Command_expandDeclId___spec__3(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_expandDeclIdNamespace_x3f_match__2___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange___at_Lean_Elab_Command_elabAxiom___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -383,7 +383,6 @@ lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_expandInitCmd___lambda__1___closed__52;
static lean_object* l_Lean_Elab_Command_elabDeclaration___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Command_expandMutualNamespace___closed__4;
lean_object* l_Lean_addDocString_x27___at_Lean_Elab_Command_expandDeclId___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__5;
static lean_object* l___regBuiltin_Lean_Elab_Command_expandBuiltinInitialize___closed__3;
static lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__3___closed__2;
@ -427,6 +426,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Command_elabMutual___closed__1;
static lean_object* l_Lean_Elab_Command_expandInitCmd___lambda__1___closed__42;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__3___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabAxiom_match__1(lean_object*);
lean_object* l_Lean_addDocString_x27___at_Lean_Elab_Command_expandDeclId___spec__9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_expandInitCmd___closed__1;
lean_object* l_Lean_Elab_Command_expandInitCmd___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_expandInitCmd___lambda__1___closed__37;
@ -3554,7 +3554,7 @@ lean_ctor_set(x_25, 4, x_23);
lean_ctor_set(x_25, 5, x_24);
lean_ctor_set(x_25, 6, x_18);
lean_inc(x_6);
x_26 = l_Lean_Elab_applyVisibility___at_Lean_Elab_Command_expandDeclId___spec__3(x_14, x_12, x_25, x_6, x_17);
x_26 = l_Lean_Elab_applyVisibility___at_Lean_Elab_Command_expandDeclId___spec__5(x_14, x_12, x_25, x_6, x_17);
if (lean_obj_tag(x_26) == 0)
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34;
@ -3582,7 +3582,7 @@ lean_dec(x_34);
x_37 = lean_ctor_get(x_1, 0);
lean_inc(x_37);
lean_inc(x_27);
x_38 = l_Lean_addDocString_x27___at_Lean_Elab_Command_expandDeclId___spec__7(x_27, x_37, x_5, x_6, x_28);
x_38 = l_Lean_addDocString_x27___at_Lean_Elab_Command_expandDeclId___spec__9(x_27, x_37, x_5, x_6, x_28);
x_39 = lean_ctor_get(x_38, 1);
lean_inc(x_39);
lean_dec(x_38);
@ -3639,7 +3639,7 @@ lean_dec(x_34);
x_51 = lean_ctor_get(x_1, 0);
lean_inc(x_51);
lean_inc(x_27);
x_52 = l_Lean_addDocString_x27___at_Lean_Elab_Command_expandDeclId___spec__7(x_27, x_51, x_5, x_6, x_28);
x_52 = l_Lean_addDocString_x27___at_Lean_Elab_Command_expandDeclId___spec__9(x_27, x_51, x_5, x_6, x_28);
x_53 = lean_ctor_get(x_52, 1);
lean_inc(x_53);
lean_dec(x_52);

6
stage0/stdlib/Lean/Elab/Deriving/Basic.c generated
View file

@ -90,6 +90,7 @@ lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_getOptDerivingClasses___spe
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_elabDeriving___spec__5___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_elabDeriving___closed__2;
lean_object* l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__12(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_elabDeriving___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1299_(lean_object*);
@ -121,7 +122,6 @@ lean_object* l_Lean_addMessageContextPartial___at_Lean_Elab_Command_instAddMessa
lean_object* lean_array_to_list(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_elabDeriving___closed__9;
lean_object* l_Std_RBNode_find___at_Lean_Elab_applyDerivingHandlers___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__10(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_resolveGlobalConstNoOverloadWithInfo___at_Lean_Elab_elabDeriving___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_registerBuiltinDerivingHandlerWithArgs___lambda__2___closed__2;
static lean_object* l_Lean_Elab_elabDeriving___closed__6;
@ -1112,7 +1112,7 @@ lean_object* x_11; lean_object* x_12;
x_11 = lean_ctor_get(x_3, 6);
lean_dec(x_11);
lean_ctor_set(x_3, 6, x_9);
x_12 = l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__10(x_2, x_3, x_4, x_8);
x_12 = l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__12(x_2, x_3, x_4, x_8);
return x_12;
}
else
@ -1139,7 +1139,7 @@ lean_ctor_set(x_19, 3, x_16);
lean_ctor_set(x_19, 4, x_17);
lean_ctor_set(x_19, 5, x_18);
lean_ctor_set(x_19, 6, x_9);
x_20 = l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__10(x_2, x_19, x_4, x_8);
x_20 = l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__12(x_2, x_19, x_4, x_8);
return x_20;
}
}

334
stage0/stdlib/Lean/Elab/Extra.c generated
View file

@ -13,9 +13,9 @@
#ifdef __cplusplus
extern "C" {
#endif
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__13;
lean_object* l_Lean_Elab_Term_elabForIn_getMonad_match__1___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_toTree_go___closed__2;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__8;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabBinRel___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__1___closed__1;
@ -30,18 +30,15 @@ static lean_object* l_Lean_Elab_Term_elabForIn___lambda__1___closed__1;
lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabForIn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabForIn_getMonad___closed__4;
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__5;
lean_object* l_Lean_stringToMessageData(lean_object*);
lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___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_mk_empty_array_with_capacity(lean_object*);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__2___closed__7;
lean_object* l_Lean_mkSort(lean_object*);
static lean_object* l_Lean_Elab_Term_elabForIn___closed__10;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__17;
static lean_object* l_Lean_Elab_Term_elabForIn___lambda__1___closed__4;
lean_object* l_Lean_Elab_Term_BinOp_elabBinCalc_match__6___rarg(lean_object*, lean_object*);
extern lean_object* l_Lean_nullKind;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__21;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__12;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__2___closed__3;
lean_object* lean_array_uget(lean_object*, size_t);
@ -52,36 +49,36 @@ static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc
lean_object* l_Lean_Meta_mkAppM(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_elabForIn___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel___closed__8;
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__3;
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go___closed__2;
lean_object* l_Lean_Elab_Term_elabBinRel_match__1(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel___closed__14;
static lean_object* l_Lean_Elab_Term_elabForIn___closed__16;
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_applyCoe_go___closed__2;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__2;
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_toTree_go___closed__1;
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__1___closed__9;
static lean_object* l_Lean_Elab_Term_elabForIn___lambda__1___closed__3;
lean_object* l_Lean_addTrace_addTraceOptions(lean_object*);
uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__21;
lean_object* l_Lean_throwError___at___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_toTree_go___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__8;
lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___lambda__1(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_Elab_Term_elabForIn___lambda__1___closed__5;
lean_object* l_Lean_Expr_appFn_x21(lean_object*);
static lean_object* l_Lean_Elab_Term_elabForIn_getMonad___closed__5;
lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_BinOp_elabBinCalc_match__2___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__13;
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel___closed__3;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__6;
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel___closed__12;
static lean_object* l___regBuiltin_Lean_Elab_Term_elabForIn___closed__1;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__1___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*);
static lean_object* l_Lean_Elab_Term_elabForIn_getMonad___closed__3;
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp(lean_object*);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__2___closed__10;
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__1;
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_isUnknow___boxed(lean_object*);
lean_object* l_Lean_Expr_appArg_x21(lean_object*);
static lean_object* l_Lean_Elab_Term_elabForIn_throwFailure___closed__2;
@ -90,12 +87,15 @@ lean_object* l_Lean_Elab_Term_instInhabitedTermElabM(lean_object*);
lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getMainModule___rarg(lean_object*, lean_object*);
uint8_t l_USize_decLt(size_t, size_t);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__17;
lean_object* l_Lean_Elab_Term_BinOp_elabBinCalc_match__6(lean_object*);
lean_object* l_Lean_Elab_Term_BinOp_elabBinCalc_match__1___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_applyCoe_go___lambda__2___closed__5;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__1;
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__1___closed__11;
extern lean_object* l_Lean_levelZero;
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2(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_Elab_Term_elabForIn___closed__19;
lean_object* l_Lean_Elab_Term_elabBinRel___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_toTree_go___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -113,11 +113,11 @@ static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc
lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabForIn_getMonad(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addTrace___at___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go___spec__2___boxed(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_Elab_Term_BinOp_elabBinOp_x27___closed__18;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__15;
lean_object* l_Lean_Elab_Term_BinOp_elabBinOp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_addTrace___at___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go___spec__2___closed__2;
lean_object* l_Lean_Elab_Term_elabForIn_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateRefT_x27_lift___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_addTrace___at___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go___spec__2___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinCalc___closed__4;
@ -125,18 +125,17 @@ lean_object* l_Lean_Elab_Term_elabForIn_getMonad_match__2___rarg(lean_object*, l
lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinCalc___closed__1;
static lean_object* l_Lean_Elab_Term_elabForIn___lambda__1___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27(lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__10;
static lean_object* l_Lean_Elab_Term_elabForIn___closed__11;
lean_object* l_Lean_Elab_Term_elabTermEnsuringType(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Option_get___at_Lean_initFn____x40_Lean_Util_PPExt___hyg_218____spec__1(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__14;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__5;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_toTree(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabForIn_match__1(lean_object*);
static lean_object* l_Lean_Elab_Term_elabForIn___closed__12;
lean_object* l_Lean_Elab_Term_BinOp_elabBinCalc___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_applyCoe_go___closed__1;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__11;
lean_object* l_Lean_Elab_Term_BinOp_elabBinCalc_match__4___rarg(lean_object*, lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__1___closed__6;
@ -145,6 +144,7 @@ static lean_object* l_Lean_addTrace___at___private_Lean_Elab_Extra_0__Lean_Elab_
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_toExpr_match__1(lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__2___lambda__1(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_Elab_Term_BinOp_elabBinOp___closed__19;
lean_object* l_Lean_throwUnknownConstant___at___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_toTree_go___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinCalc___closed__1;
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__2___closed__8;
@ -154,7 +154,6 @@ static lean_object* l_Lean_Elab_Term_elabForIn___closed__17;
lean_object* l_Lean_Expr_headBeta(lean_object*);
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_applyCoe_go___lambda__2___closed__4;
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, 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_Elab_Term_BinOp_elabBinOp_x27___closed__3;
lean_object* l_Lean_addTrace___at___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkCoe(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -169,12 +168,13 @@ lean_object* l_Lean_Elab_Term_BinOp_elabBinCalc_match__3(lean_object*);
lean_object* l_Lean_Elab_Term_elabAppArgs(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_relation_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__2___closed__11;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__20;
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Term_elabBinRel___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabBinRel___closed__1;
lean_object* l_Lean_Elab_Term_elabBinRel___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_applyCoe_go___closed__4;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__7;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2___closed__1;
lean_object* l_Array_back___at_Lean_Meta_DiscrTree_mkPathAux___spec__1(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel___closed__10;
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinCalc___closed__2;
@ -183,19 +183,17 @@ static lean_object* l_Lean_Elab_Term_elabBinRel___lambda__2___closed__1;
lean_object* l_Lean_Elab_Term_BinOp_elabBinCalc_match__4(lean_object*);
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l_Lean_Elab_addMacroStack___at_Lean_Elab_Term_instAddErrorMessageContextTermElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__1;
lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars_loop(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isExprDefEqGuarded(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getCurrMacroScope(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__2___closed__13;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2___closed__2;
uint8_t l_Lean_Environment_contains(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabBinRel___lambda__2___closed__4;
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go___closed__6;
lean_object* l_Lean_Elab_Term_BinOp_elabBinCalc_match__5___rarg(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2___closed__1;
lean_object* l_Lean_Elab_Term_BinOp_elabBinCalc_match__5(lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2___closed__2;
static lean_object* l_Lean_Elab_Term_elabForIn___closed__23;
uint8_t l_Lean_Expr_isAppOfArity(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resolveId_x3f(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -211,7 +209,6 @@ lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_toExpr(lean_obj
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_isUnknow_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_BinOp_initFn____x40_Lean_Elab_Extra___hyg_3845_(lean_object*);
lean_object* l_Lean_Elab_Term_elabBinRel(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__16;
uint8_t l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_isUnknow(lean_object*);
lean_object* l_Lean_Elab_Term_elabBinRel_match__2(lean_object*);
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_applyCoe(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -219,11 +216,11 @@ lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze(lean_ob
static lean_object* l_Lean_Elab_Term_elabForIn___closed__2;
size_t lean_usize_of_nat(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinCalc(lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__10;
lean_object* l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabForIn___closed__9;
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_mkOp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__4;
lean_object* l_Lean_Elab_Term_mkConst(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_BinOp_elabBinCalc_match__3___rarg(lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__1___closed__7;
@ -234,7 +231,6 @@ lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec
lean_object* l_Lean_Elab_Term_elabForIn_throwFailure___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNodeOf(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabForIn___closed__4;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__20;
static lean_object* l_Lean_Elab_Term_elabForIn_throwFailure___closed__1;
static lean_object* l_Lean_Elab_Term_elabForIn___closed__8;
static lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Term_elabBinRel___spec__1___closed__3;
@ -245,6 +241,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Term_elabForIn___closed__3;
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__2___closed__4;
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel___closed__4;
lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__16;
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinCalc___closed__3;
lean_object* l_Lean_Meta_trySynthInstance(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
@ -259,12 +256,12 @@ lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_relation_x3f(le
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_toTree_go_match__1(lean_object*);
lean_object* l_Lean_Meta_withNewMCtxDepth___at___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__12;
lean_object* l___regBuiltin_Lean_Elab_Term_elabForIn(lean_object*);
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_hasCoe_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_SavedState_restore(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArgs(lean_object*);
lean_object* l_Lean_Name_append(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__7;
lean_object* l_Lean_Elab_Term_elabBinRel_match__1___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___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*, lean_object*);
@ -293,17 +290,18 @@ lean_object* l_Lean_Elab_Term_elabType(lean_object*, lean_object*, lean_object*,
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go_match__1(lean_object*);
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_isUnknow_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__9;
static lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Term_elabBinRel___spec__1___closed__4;
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkArrow(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel(lean_object*);
lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__4;
lean_object* l_Lean_expandMacros(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__1___closed__8;
static lean_object* l_Lean_Elab_Term_elabForIn___closed__22;
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_applyCoe_go___lambda__2___closed__6;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__11;
lean_object* l_Lean_Elab_Term_BinOp_elabBinCalc_match__1(lean_object*);
static lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Term_elabBinRel___spec__1___closed__2;
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -324,29 +322,33 @@ lean_object* l_Lean_Meta_mkFreshLevelMVar___rarg(lean_object*, lean_object*, lea
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabBinRel___lambda__2___closed__5;
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__2;
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel___closed__13;
static lean_object* l_Lean_addTrace___at___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go___spec__2___closed__3;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__18;
lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Term_elabLetDeclCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2(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_addTrace___at___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go___spec__2___closed__5;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__5;
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__2___closed__12;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__4;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__3;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__15;
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__2___closed__14;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__14;
lean_object* l_Lean_Elab_Term_elabForIn_getMonad_match__2(lean_object*);
lean_object* l_Lean_Elab_Term_BinOp_elabBinCalc_match__2(lean_object*);
lean_object* l_Lean_indentExpr(lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__2;
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_toTree_go___closed__4;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__19;
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_toTree_go(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_isLocalIdent_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__6;
static lean_object* l_Lean_Elab_Term_elabForIn___closed__7;
lean_object* l_Lean_Elab_Term_saveState___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__4;
static lean_object* l_Lean_Elab_Term_elabForIn___closed__24;
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__3;
static lean_object* l_Lean_Elab_Term_elabForIn_getMonad___closed__1;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__9;
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_toTree_go_match__1___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_hasCoe___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel___closed__1;
@ -354,16 +356,14 @@ lean_object* l_Lean_Elab_Term_elabForIn_throwFailure(lean_object*, lean_object*,
lean_object* l_Lean_Elab_Term_elabForIn_getMonad___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Term_synthesizeInst___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabForIn___closed__5;
lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_hasCoe___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__5;
static lean_object* l_Lean_Elab_Term_elabForIn___closed__15;
static lean_object* l_Lean_Elab_Term_elabForIn___closed__18;
lean_object* l_Lean_Elab_getBetterRef(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel___closed__7;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__1;
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_hasCoe___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__2;
lean_object* l_Lean_Elab_Term_elabBinRel_match__1___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -9386,7 +9386,7 @@ x_10 = l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_applyCoe_go(x_2, x_1,
return x_10;
}
}
lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_12;
@ -9395,7 +9395,7 @@ x_12 = l_Lean_Elab_Term_ensureHasType(x_1, x_2, x_11, x_4, x_5, x_6, x_7, x_8, x
return x_12;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2___closed__1() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2___closed__1() {
_start:
{
lean_object* x_1;
@ -9403,16 +9403,16 @@ x_1 = lean_mk_string("result: ");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2___closed__2() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2___closed__1;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2___closed__1;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2(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, lean_object* x_11, lean_object* x_12) {
lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2(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, lean_object* x_11, lean_object* x_12) {
_start:
{
uint8_t x_13;
@ -9558,7 +9558,7 @@ if (x_31 == 0)
lean_object* x_33; lean_object* x_34;
lean_dec(x_4);
x_33 = lean_box(0);
x_34 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__1(x_3, x_29, x_33, x_6, x_7, x_8, x_9, x_10, x_11, x_32);
x_34 = l_Lean_Elab_Term_BinOp_elabBinOp___lambda__1(x_3, x_29, x_33, x_6, x_7, x_8, x_9, x_10, x_11, x_32);
return x_34;
}
else
@ -9567,7 +9567,7 @@ lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean
lean_inc(x_29);
x_35 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_35, 0, x_29);
x_36 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2___closed__2;
x_36 = l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2___closed__2;
x_37 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_37, 0, x_36);
lean_ctor_set(x_37, 1, x_35);
@ -9581,7 +9581,7 @@ lean_inc(x_41);
x_42 = lean_ctor_get(x_40, 1);
lean_inc(x_42);
lean_dec(x_40);
x_43 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__1(x_3, x_29, x_41, x_6, x_7, x_8, x_9, x_10, x_11, x_42);
x_43 = l_Lean_Elab_Term_BinOp_elabBinOp___lambda__1(x_3, x_29, x_41, x_6, x_7, x_8, x_9, x_10, x_11, x_42);
lean_dec(x_41);
return x_43;
}
@ -9706,7 +9706,7 @@ return x_72;
}
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__1() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__1() {
_start:
{
lean_object* x_1;
@ -9714,16 +9714,16 @@ x_1 = lean_mk_string("hasUncomparable: ");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__2() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__1;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__1;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__3() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__3() {
_start:
{
lean_object* x_1;
@ -9731,16 +9731,16 @@ x_1 = lean_mk_string(", maxType: ");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__4() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__3;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__3;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__5() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__5() {
_start:
{
lean_object* x_1;
@ -9748,51 +9748,51 @@ x_1 = lean_mk_string("false");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__6() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__5;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__5;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__7() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__6;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__6;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__8() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__2;
x_2 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__7;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__2;
x_2 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__7;
x_3 = lean_alloc_ctor(10, 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_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__9() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__8;
x_2 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__4;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__8;
x_2 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__4;
x_3 = lean_alloc_ctor(10, 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_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__10() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__10() {
_start:
{
lean_object* x_1;
@ -9800,43 +9800,43 @@ x_1 = lean_mk_string("<not-available>");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__11() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__10;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__10;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__12() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__11;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__11;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__13() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__13() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__9;
x_2 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__12;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__9;
x_2 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__12;
x_3 = lean_alloc_ctor(10, 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_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__14() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__13;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__13;
x_2 = l_Lean_Elab_Term_elabForIn_getMonad___closed__6;
x_3 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -9844,7 +9844,7 @@ lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__15() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__15() {
_start:
{
lean_object* x_1;
@ -9852,67 +9852,67 @@ x_1 = lean_mk_string("true");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__16() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__15;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__15;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__17() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__17() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__16;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__16;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__18() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__2;
x_2 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__17;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__2;
x_2 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__17;
x_3 = lean_alloc_ctor(10, 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_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__19() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__19() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__18;
x_2 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__4;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__18;
x_2 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__4;
x_3 = lean_alloc_ctor(10, 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_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__20() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__20() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__19;
x_2 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__12;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__19;
x_2 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__12;
x_3 = lean_alloc_ctor(10, 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_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__21() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__21() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__20;
x_1 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__20;
x_2 = l_Lean_Elab_Term_elabForIn_getMonad___closed__6;
x_3 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -9920,7 +9920,7 @@ lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27(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* l_Lean_Elab_Term_BinOp_elabBinOp(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) {
_start:
{
lean_object* x_10;
@ -10000,7 +10000,7 @@ if (x_17 == 0)
{
lean_object* x_19; lean_object* x_20;
x_19 = lean_box(0);
x_20 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2(x_14, x_11, x_2, x_16, x_19, x_3, x_4, x_5, x_6, x_7, x_8, x_18);
x_20 = l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2(x_14, x_11, x_2, x_16, x_19, x_3, x_4, x_5, x_6, x_7, x_8, x_18);
return x_20;
}
else
@ -10015,14 +10015,14 @@ lean_inc(x_22);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_23 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__14;
x_23 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__14;
x_24 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_16, x_23, x_3, x_4, x_5, x_6, x_7, x_8, x_18);
x_25 = lean_ctor_get(x_24, 0);
lean_inc(x_25);
x_26 = lean_ctor_get(x_24, 1);
lean_inc(x_26);
lean_dec(x_24);
x_27 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2(x_14, x_11, x_2, x_16, x_25, x_3, x_4, x_5, x_6, x_7, x_8, x_26);
x_27 = l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2(x_14, x_11, x_2, x_16, x_25, x_3, x_4, x_5, x_6, x_7, x_8, x_26);
return x_27;
}
else
@ -10033,7 +10033,7 @@ lean_inc(x_28);
lean_dec(x_22);
x_29 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_29, 0, x_28);
x_30 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__9;
x_30 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__9;
x_31 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_29);
@ -10047,7 +10047,7 @@ lean_inc(x_35);
x_36 = lean_ctor_get(x_34, 1);
lean_inc(x_36);
lean_dec(x_34);
x_37 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2(x_14, x_11, x_2, x_16, x_35, x_3, x_4, x_5, x_6, x_7, x_8, x_36);
x_37 = l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2(x_14, x_11, x_2, x_16, x_35, x_3, x_4, x_5, x_6, x_7, x_8, x_36);
return x_37;
}
}
@ -10059,14 +10059,14 @@ lean_inc(x_38);
if (lean_obj_tag(x_38) == 0)
{
lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_39 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__21;
x_39 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__21;
x_40 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_16, x_39, x_3, x_4, x_5, x_6, x_7, x_8, x_18);
x_41 = lean_ctor_get(x_40, 0);
lean_inc(x_41);
x_42 = lean_ctor_get(x_40, 1);
lean_inc(x_42);
lean_dec(x_40);
x_43 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2(x_14, x_11, x_2, x_16, x_41, x_3, x_4, x_5, x_6, x_7, x_8, x_42);
x_43 = l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2(x_14, x_11, x_2, x_16, x_41, x_3, x_4, x_5, x_6, x_7, x_8, x_42);
return x_43;
}
else
@ -10077,7 +10077,7 @@ lean_inc(x_44);
lean_dec(x_38);
x_45 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_45, 0, x_44);
x_46 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__19;
x_46 = l_Lean_Elab_Term_BinOp_elabBinOp___closed__19;
x_47 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_47, 0, x_46);
lean_ctor_set(x_47, 1, x_45);
@ -10091,7 +10091,7 @@ lean_inc(x_51);
x_52 = lean_ctor_get(x_50, 1);
lean_inc(x_52);
lean_dec(x_50);
x_53 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2(x_14, x_11, x_2, x_16, x_51, x_3, x_4, x_5, x_6, x_7, x_8, x_52);
x_53 = l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2(x_14, x_11, x_2, x_16, x_51, x_3, x_4, x_5, x_6, x_7, x_8, x_52);
return x_53;
}
}
@ -10160,16 +10160,16 @@ return x_73;
}
}
}
lean_object* l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__1___boxed(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) {
lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___lambda__1___boxed(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;
x_11 = l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_11 = l_Lean_Elab_Term_BinOp_elabBinOp___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_3);
return x_11;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__1() {
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__1() {
_start:
{
lean_object* x_1;
@ -10177,50 +10177,50 @@ x_1 = lean_mk_string("BinOp");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__2() {
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Term_elabBinRel___closed__11;
x_2 = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__1;
x_2 = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__3() {
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("elabBinOp'");
x_1 = lean_mk_string("elabBinOp");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__4() {
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__2;
x_2 = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__3;
x_1 = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__2;
x_2 = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__5() {
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_BinOp_elabBinOp_x27), 9, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_BinOp_elabBinOp), 9, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27(lean_object* x_1) {
lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp(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_Elab_Term_termElabAttribute;
x_3 = l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_toTree_go___closed__2;
x_4 = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__4;
x_5 = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__5;
x_4 = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__4;
x_5 = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__5;
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
@ -14523,7 +14523,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinCalc___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__2;
x_1 = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__2;
x_2 = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinCalc___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -14772,63 +14772,63 @@ l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_applyCoe_go___closed__3 = _i
lean_mark_persistent(l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_applyCoe_go___closed__3);
l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_applyCoe_go___closed__4 = _init_l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_applyCoe_go___closed__4();
lean_mark_persistent(l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_applyCoe_go___closed__4);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2___closed__1 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2___closed__1);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2___closed__2 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___lambda__2___closed__2);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__1 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__1);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__2 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__2);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__3 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__3);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__4 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__4();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__4);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__5 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__5();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__5);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__6 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__6();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__6);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__7 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__7();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__7);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__8 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__8();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__8);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__9 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__9();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__9);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__10 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__10();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__10);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__11 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__11();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__11);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__12 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__12();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__12);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__13 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__13();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__13);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__14 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__14();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__14);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__15 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__15();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__15);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__16 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__16();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__16);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__17 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__17();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__17);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__18 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__18();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__18);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__19 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__19();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__19);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__20 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__20();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__20);
l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__21 = _init_l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__21();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__21);
l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__1);
l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__2);
l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__3 = _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__3);
l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__4 = _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__4();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__4);
l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__5 = _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__5();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27___closed__5);
res = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_x27(lean_io_mk_world());
l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2___closed__1 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2___closed__1);
l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2___closed__2 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___lambda__2___closed__2);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__1 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__1);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__2 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__2);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__3 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__3);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__4 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__4();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__4);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__5 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__5();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__5);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__6 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__6();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__6);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__7 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__7();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__7);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__8 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__8();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__8);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__9 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__9();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__9);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__10 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__10();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__10);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__11 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__11();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__11);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__12 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__12();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__12);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__13 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__13();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__13);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__14 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__14();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__14);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__15 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__15();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__15);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__16 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__16();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__16);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__17 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__17();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__17);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__18 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__18();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__18);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__19 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__19();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__19);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__20 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__20();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__20);
l_Lean_Elab_Term_BinOp_elabBinOp___closed__21 = _init_l_Lean_Elab_Term_BinOp_elabBinOp___closed__21();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabBinOp___closed__21);
l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__1);
l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__2);
l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__3 = _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__3);
l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__4 = _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__4();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__4);
l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__5 = _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__5();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp___closed__5);
res = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Array_forInUnsafe_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__1___closed__1 = _init_l_Array_forInUnsafe_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__1___closed__1();

6
stage0/stdlib/Lean/Elab/GenInjective.c generated
View file

@ -42,6 +42,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___
static lean_object* l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___closed__4;
lean_object* l_Lean_resolveGlobalConstCore___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mapTRAux___at_Lean_resolveGlobalConstNoOverload___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__12(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__2___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___closed__9;
@ -53,7 +54,6 @@ static lean_object* l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___
lean_object* lean_format_pretty(lean_object*, lean_object*);
lean_object* l_Lean_addMessageContextPartial___at_Lean_Elab_Command_instAddMessageContextCommandElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__6(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__10(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_resolveGlobalConstCore___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__4___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___closed__14;
lean_object* l_Lean_ResolveName_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*);
@ -103,7 +103,7 @@ lean_object* x_11; lean_object* x_12;
x_11 = lean_ctor_get(x_3, 6);
lean_dec(x_11);
lean_ctor_set(x_3, 6, x_9);
x_12 = l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__10(x_2, x_3, x_4, x_8);
x_12 = l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__12(x_2, x_3, x_4, x_8);
return x_12;
}
else
@ -130,7 +130,7 @@ lean_ctor_set(x_19, 3, x_16);
lean_ctor_set(x_19, 4, x_17);
lean_ctor_set(x_19, 5, x_18);
lean_ctor_set(x_19, 6, x_9);
x_20 = l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__10(x_2, x_19, x_4, x_8);
x_20 = l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__12(x_2, x_19, x_4, x_8);
return x_20;
}
}

1022
stage0/stdlib/Lean/Elab/MutualDef.c generated
View file

File diff suppressed because it is too large Load diff

6
stage0/stdlib/Lean/Elab/Print.c generated
View file

@ -106,6 +106,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Command_elabPrintAxioms___closed__1
static lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader___closed__9;
lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_levelParamsToMessageData_match__1(lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__12(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_pushInfoTree___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printId___spec__9(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Command_elabPrintAxioms___closed__2;
@ -138,7 +139,6 @@ static lean_object* l_Lean_getConstInfo___at___private_Lean_Elab_Print_0__Lean_E
extern lean_object* l_Lean_protectedExt;
lean_object* l_List_forIn_loop___at___private_Lean_Elab_Print_0__Lean_Elab_Command_levelParamsToMessageData___spec__1___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_elabPrint___closed__11;
lean_object* l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__10(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_throwUnknownId___closed__2;
lean_object* l_Lean_Elab_Command_CollectAxioms_State_axioms___default;
lean_object* l_Lean_resolveGlobalConst___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printId___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
@ -2364,7 +2364,7 @@ lean_object* x_11; lean_object* x_12;
x_11 = lean_ctor_get(x_3, 6);
lean_dec(x_11);
lean_ctor_set(x_3, 6, x_9);
x_12 = l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__10(x_2, x_3, x_4, x_8);
x_12 = l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__12(x_2, x_3, x_4, x_8);
return x_12;
}
else
@ -2391,7 +2391,7 @@ lean_ctor_set(x_19, 3, x_16);
lean_ctor_set(x_19, 4, x_17);
lean_ctor_set(x_19, 5, x_18);
lean_ctor_set(x_19, 6, x_9);
x_20 = l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__10(x_2, x_19, x_4, x_8);
x_20 = l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__12(x_2, x_19, x_4, x_8);
return x_20;
}
}

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

@ -297,7 +297,6 @@ lean_object* l_Lean_Meta_mkSizeOfInstances(lean_object*, lean_object*, lean_obje
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_levelMVarToParamAux___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_updateResultingUniverse(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getFieldInfo_x3f(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_applyVisibility___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__3(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTermEnsuringType(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
@ -336,6 +335,7 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_removeUnused_m
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabStructure___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*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUsed___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__13(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__11(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_mkAuxConstructions___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_defaultCtorName;
@ -346,7 +346,6 @@ lean_object* l_Lean_getStructureFieldsFlattened(lean_object*, lean_object*, uint
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_getFieldType___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_elabStructure___closed__8;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__11(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__5___lambda__3___closed__10;
static lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__5___lambda__5___closed__2;
static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_getFieldType___lambda__1___closed__2;
@ -433,6 +432,7 @@ static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_findFie
static uint8_t l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___closed__2;
lean_object* l_Lean_mkRecOn___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkAuxConstructions___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars_loop(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addDeclarationRanges___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__14(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_instInhabitedStructFieldInfo___closed__3;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectLevelParamsInFVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_copyDefaultValue_x3f_go_x3f_match__1(lean_object*);
@ -444,10 +444,10 @@ static lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withParents_go___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__1___boxed(lean_object**);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__11___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_addDeclarationRanges___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabStructure___lambda__2___boxed(lean_object**);
lean_object* l_Lean_getStructureFields(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_StructFieldInfo_isSubobject___boxed(lean_object*);
lean_object* l_Lean_Elab_addDeclarationRanges___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__12(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getCurrMacroScope(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_to_list(lean_object*, lean_object*);
uint8_t l_Lean_Name_isAtomic(lean_object*);
@ -524,7 +524,6 @@ static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFie
uint8_t l_Lean_Expr_isForall(lean_object*);
uint8_t l_Lean_BinderInfo_isInstImplicit(uint8_t);
lean_object* lean_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addDeclarationRanges___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__12(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addAndCompile___at_Lean_mkNoConfusionEnum_mkToCtorIdx___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_copyNewFieldsFrom_processOveriddenDefaultValues_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults___spec__2___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -544,6 +543,7 @@ lean_object* l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_pos
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_mkCoercionToCopiedParent___lambda__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*, lean_object*);
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__5___closed__5;
lean_object* l_Lean_addDocString_x27___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__5___lambda__3___closed__12;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectLevelParamsInStructure___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_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -666,7 +666,6 @@ static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandC
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_removeUnused(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_findFieldInfo_x3f___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_elabModifiers___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__1___lambda__3(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addDocString_x27___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_copyNewFieldsFrom_copyFields_copy___rarg___closed__6;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_mkAuxConstructions___lambda__1(uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_elabStructure___closed__1;
@ -777,6 +776,7 @@ lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Ela
lean_object* l_Lean_Elab_Term_withoutAutoBoundImplicit___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields(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_Command_checkValidInductiveModifier___at_Lean_Elab_Command_elabStructure___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_applyVisibility___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__5(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__4___lambda__2___closed__1;
static lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__5___lambda__3___closed__7;
lean_object* l_Lean_Elab_Term_elabBinders___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -3593,13 +3593,13 @@ lean_object* l_Lean_Elab_addAuxDeclarationRanges___at___private_Lean_Elab_Struct
_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;
x_11 = l_Lean_Elab_getDeclarationRange___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__11(x_2, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_11 = l_Lean_Elab_getDeclarationRange___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__13(x_2, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l_Lean_Elab_getDeclarationRange___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__11(x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_13);
x_14 = l_Lean_Elab_getDeclarationRange___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__13(x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_13);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_ctor_get(x_14, 1);
@ -3608,7 +3608,7 @@ lean_dec(x_14);
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_12);
lean_ctor_set(x_17, 1, x_15);
x_18 = l_Lean_addDeclarationRanges___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__12(x_1, x_17, x_4, x_5, x_6, x_7, x_8, x_9, x_16);
x_18 = l_Lean_addDeclarationRanges___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__14(x_1, x_17, x_4, x_5, x_6, x_7, x_8, x_9, x_16);
return x_18;
}
}
@ -3632,7 +3632,7 @@ lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_20 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__3(x_19, x_18, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
x_20 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__5(x_19, x_18, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
if (x_14 == 0)
{
if (lean_obj_tag(x_20) == 0)
@ -3646,7 +3646,7 @@ lean_dec(x_20);
x_23 = lean_ctor_get(x_3, 0);
lean_inc(x_23);
lean_inc(x_21);
x_24 = l_Lean_addDocString_x27___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__6(x_21, x_23, x_5, x_6, x_7, x_8, x_9, x_10, x_22);
x_24 = l_Lean_addDocString_x27___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__8(x_21, x_23, x_5, x_6, x_7, x_8, x_9, x_10, x_22);
x_25 = lean_ctor_get(x_24, 1);
lean_inc(x_25);
lean_dec(x_24);
@ -3740,7 +3740,7 @@ lean_dec(x_20);
x_41 = lean_ctor_get(x_3, 0);
lean_inc(x_41);
lean_inc(x_39);
x_42 = l_Lean_addDocString_x27___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__6(x_39, x_41, x_5, x_6, x_7, x_8, x_9, x_10, x_40);
x_42 = l_Lean_addDocString_x27___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__8(x_39, x_41, x_5, x_6, x_7, x_8, x_9, x_10, x_40);
x_43 = lean_ctor_get(x_42, 1);
lean_inc(x_43);
lean_dec(x_42);
@ -5047,7 +5047,7 @@ lean_inc(x_15);
lean_inc(x_14);
lean_inc(x_13);
lean_inc(x_12);
x_21 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__3(x_20, x_19, x_12, x_13, x_14, x_15, x_16, x_17, x_18);
x_21 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__5(x_20, x_19, x_12, x_13, x_14, x_15, x_16, x_17, x_18);
if (lean_obj_tag(x_21) == 0)
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26;
@ -5059,7 +5059,7 @@ lean_dec(x_21);
x_24 = lean_ctor_get(x_3, 0);
lean_inc(x_24);
lean_inc(x_22);
x_25 = l_Lean_addDocString_x27___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__6(x_22, x_24, x_12, x_13, x_14, x_15, x_16, x_17, x_23);
x_25 = l_Lean_addDocString_x27___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__8(x_22, x_24, x_12, x_13, x_14, x_15, x_16, x_17, x_23);
lean_dec(x_17);
lean_dec(x_16);
lean_dec(x_15);
@ -12244,7 +12244,7 @@ lean_inc(x_18);
lean_inc(x_17);
lean_inc(x_16);
lean_inc(x_15);
x_27 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__3(x_26, x_22, x_15, x_16, x_17, x_18, x_19, x_20, x_25);
x_27 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__5(x_26, x_22, x_15, x_16, x_17, x_18, x_19, x_20, x_25);
if (lean_obj_tag(x_27) == 0)
{
lean_object* x_28; lean_object* x_29; uint8_t 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;
@ -28692,7 +28692,7 @@ lean_inc(x_25);
lean_dec(x_22);
lean_inc(x_3);
lean_inc(x_24);
x_26 = l_Lean_Elab_addDeclarationRanges___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__10(x_24, x_3, x_10, x_11, x_12, x_13, x_14, x_15, x_23);
x_26 = l_Lean_Elab_addDeclarationRanges___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__12(x_24, x_3, x_10, x_11, x_12, x_13, x_14, x_15, x_23);
x_27 = lean_ctor_get(x_26, 1);
lean_inc(x_27);
lean_dec(x_26);

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

@ -232,7 +232,6 @@ static lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyn
static lean_object* l_Lean_Elab_Term_toParserDescr_processAtom___lambda__1___closed__5;
lean_object* l_Lean_ConstantInfo_levelParams(lean_object*);
static lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__67;
lean_object* l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__40;
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabSyntax___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_toParserDescr_processNonReserved___closed__4;
@ -264,6 +263,7 @@ static lean_object* l_Lean_Elab_Term_toParserDescr_processNullaryOrCat___closed_
static lean_object* l_Lean_addTrace___at_Lean_Elab_Term_checkLeftRec___spec__3___closed__2;
static lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__51;
lean_object* l_Lean_Elab_expandMacroImpl_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__7(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_elabSyntaxAbbrev(lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_elabSyntax___spec__1___boxed(lean_object*, lean_object*);
@ -14188,7 +14188,7 @@ lean_inc(x_19);
x_20 = lean_ctor_get(x_18, 1);
lean_inc(x_20);
lean_dec(x_18);
x_21 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__5(x_19, x_2, x_3, x_20);
x_21 = l_Lean_setEnv___at_Lean_Elab_Command_expandDeclId___spec__7(x_19, x_2, x_3, x_20);
x_22 = lean_ctor_get(x_21, 1);
lean_inc(x_22);
lean_dec(x_21);

1070
stage0/stdlib/Lean/Parser/Term.c generated
View file

File diff suppressed because it is too large Load diff