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 2020-12-05 16:02:38 -08:00
parent 533192c369
commit 926c7f34ef
16 changed files with 1297 additions and 2362 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
stage0/src/Lean/Elab/Declaration.lean generated
View file

@ -39,20 +39,17 @@ def expandDeclNamespace? (stx : Syntax) : Option (Name × Syntax) :=
k == `Lean.Parser.Command.constant ||
k == `Lean.Parser.Command.axiom ||
k == `Lean.Parser.Command.inductive ||
k == `Lean.Parser.Command.classInductive ||
k == `Lean.Parser.Command.structure then
match expandDeclIdNamespace? decl[1] with
| some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 1 declId))
| none => none
else if k == `Lean.Parser.Command.instance then
let optDeclId := decl[1]
let optDeclId := decl[2]
if optDeclId.isNone then none
else match expandDeclIdNamespace? optDeclId[0] with
| some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 1 (optDeclId.setArg 0 declId)))
| some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 2 (optDeclId.setArg 0 declId)))
| none => none
else if k == `Lean.Parser.Command.classInductive then
match expandDeclIdNamespace? decl[2] with
| some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 2 declId))
| none => none
else
none

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

@ -135,17 +135,18 @@ def mkDefViewOfConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
}
def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
-- parser! "instance " >> optional declId >> declSig >> declVal
let (binders, type) := expandDeclSig (stx.getArg 2)
let modifiers := modifiers.addAttribute { name := `instance }
let declId ← match (stx.getArg 1).getOptional? with
-- parser! attrKind >> "instance " >> optional declId >> declSig >> declVal
let attrKind := toAttributeKind stx[0]
let (binders, type) := expandDeclSig stx[3]
let modifiers := modifiers.addAttribute { kind := attrKind, name := `instance }
let declId ← match stx[2].getOptional? with
| some declId => pure declId
| none =>
let id ← MkInstanceName.main type
pure <| Syntax.node `Lean.Parser.Command.declId #[mkIdentFrom stx id, mkNullNode]
return {
ref := stx, kind := DefKind.def, modifiers := modifiers,
declId := declId, binders := binders, type? := type, value := stx.getArg 3
declId := declId, binders := binders, type? := type, value := stx[4]
}
def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=

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

@ -489,7 +489,7 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
pure (info.isSubobject && decl.binderInfo.isInstImplicit)
let projInstances := instParents.toList.map fun info => info.declName
Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
projInstances.forM addGlobalInstance
projInstances.forM fun declName => addInstance declName AttributeKind.global
let lctx ← getLCtx
let fieldsWithDefault := fieldInfos.filter fun info => info.value?.isSome
let defaultAuxDecls ← fieldsWithDefault.mapM fun info => do

39
stage0/src/Lean/Meta/Instances.lean generated
View file

@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.ScopedEnvExtension
import Lean.Meta.DiscrTree
namespace Lean.Meta
@ -12,6 +13,9 @@ structure InstanceEntry where
val : Expr
globalName? : Option Name := none
instance : Inhabited InstanceEntry where
default := { keys := #[], val := arbitrary }
structure Instances where
discrTree : DiscrTree Expr := DiscrTree.empty
globalInstances : NameSet := {}
@ -27,11 +31,14 @@ def addInstanceEntry (d : Instances) (e : InstanceEntry) : Instances := {
| none => d.globalInstances
}
builtin_initialize instanceExtension : SimplePersistentEnvExtension InstanceEntry Instances ←
registerSimplePersistentEnvExtension {
builtin_initialize instanceExtension : ScopedEnvExtension InstanceEntry InstanceEntry Instances ←
registerScopedEnvExtension {
name := `instanceExt,
addEntryFn := addInstanceEntry,
addImportedFn := fun es => (mkStateFromImportedEntries addInstanceEntry {} es)
mkInitial := return {}
addEntry := addInstanceEntry
toOLeanEntry := id
ofOLeanEntry := fun s a => return a
eraseEntry := fun s _ => s
}
private def mkInstanceKey (e : Expr) : MetaM (Array DiscrTree.Key) := do
@ -40,28 +47,20 @@ private def mkInstanceKey (e : Expr) : MetaM (Array DiscrTree.Key) := do
let (_, _, type) ← forallMetaTelescopeReducing type
DiscrTree.mkPath type
@[export lean_add_instance]
def addGlobalInstanceImp (env : Environment) (constName : Name) : IO Environment := do
match env.find? constName with
| none => throw <| IO.userError s!"unknown constant '{constName}'"
| some cinfo =>
let c := mkConst constName (cinfo.lparams.map mkLevelParam)
let (keys, s, _) ← (mkInstanceKey c).toIO {} { env := env } {} {}
return instanceExtension.addEntry s.env { keys := keys, val := c, globalName? := constName }
def addGlobalInstance [Monad m] [MonadEnv m] [MonadLiftT IO m] (declName : Name) : m Unit := do
let env ← getEnv
let env ← Meta.addGlobalInstanceImp env declName
setEnv env
def addInstance (declName : Name) (attrKind : AttributeKind) : MetaM Unit := do
let cinfo ← getConstInfo declName
let c := mkConst declName (cinfo.lparams.map mkLevelParam)
let keys ← mkInstanceKey c
instanceExtension.add { keys := keys, val := c, globalName? := declName } attrKind
builtin_initialize
registerBuiltinAttribute {
name := `instance
descr := "type class instance"
add := fun declName args kind => do
add := fun declName args attrKind => do
if args.hasArgs then throwError "invalid attribute 'instance', unexpected argument"
unless kind == AttributeKind.global do throwError "invalid attribute 'instance', must be global"
addGlobalInstance declName
addInstance declName attrKind |>.run {} {}
return ()
}
@[export lean_is_instance]

5
stage0/src/Lean/Parser/Command.lean generated
View file

@ -42,10 +42,7 @@ def «abbrev» := parser! "abbrev " >> declId >> optDeclSig >> declVal
def «def» := parser! "def " >> declId >> optDeclSig >> declVal
def «theorem» := parser! "theorem " >> declId >> declSig >> declVal
def «constant» := parser! "constant " >> declId >> declSig >> optional declValSimple
def «instance» := parser!
(checkOutsideQuot >> "instance " >> optional declId >> declSig >> declVal)
<|>
(checkInsideQuot >> Term.attrKind >> "instance " >> optional declId >> declSig >> declVal)
def «instance» := parser! Term.attrKind >> "instance " >> optional declId >> declSig >> declVal
def «axiom» := parser! "axiom " >> declId >> declSig
def «example» := parser! "example " >> declSig >> declVal
def inferMod := parser! atomic (symbol "{" >> "}")

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

@ -141,7 +141,6 @@ lean_object* l_Lean_Elab_Command_expandBuiltinInitialize___boxed(lean_object*, l
lean_object* l_Lean_Elab_Command_expandDeclIdNamespace_x3f_match__2___rarg(lean_object*, lean_object*);
lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_isMutualDef___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_expandMutualNamespace___spec__1___closed__2;
lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f_match__3___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_List_map___at_Lean_resolveGlobalConstNoOverload___spec__1(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
@ -222,7 +221,6 @@ lean_object* l_Lean_setEnv___at___private_Lean_Elab_Declaration_0__Lean_Elab_Com
extern lean_object* l_Lean_KernelException_toMessageData___closed__3;
size_t lean_usize_of_nat(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_elabAttr___closed__2;
lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f_match__3(lean_object*);
lean_object* l_Lean_Elab_Command_elabAxiom___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*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabAxiom_match__2(lean_object*);
lean_object* l_Lean_Elab_expandDeclIdCore(lean_object*);
@ -771,42 +769,6 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Command_expandDeclNamespace_x3f_mat
return x_2;
}
}
lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f_match__3___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_4; lean_object* x_5;
lean_dec(x_2);
x_4 = lean_box(0);
x_5 = lean_apply_1(x_3, x_4);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
lean_dec(x_3);
x_6 = lean_ctor_get(x_1, 0);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_ctor_get(x_6, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_6, 1);
lean_inc(x_8);
lean_dec(x_6);
x_9 = lean_apply_2(x_2, x_7, x_8);
return x_9;
}
}
}
lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f_match__3(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Command_expandDeclNamespace_x3f_match__3___rarg), 3, 0);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__1() {
_start:
{
@ -838,19 +800,19 @@ return x_3;
static lean_object* _init_l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__3;
x_2 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
lean_object* x_1;
x_1 = lean_mk_string("classInductive");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("classInductive");
return x_1;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__3;
x_2 = l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__4;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__6() {
@ -858,7 +820,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__3;
x_2 = l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__5;
x_2 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -914,17 +876,17 @@ x_19 = lean_name_eq(x_7, x_18);
if (x_19 == 0)
{
lean_object* x_20; uint8_t x_21;
x_20 = l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__4;
x_20 = l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__5;
x_21 = lean_name_eq(x_7, x_20);
if (x_21 == 0)
{
lean_object* x_22; uint8_t x_23;
x_22 = l_Lean_Elab_Command_isDefLike___closed__7;
x_22 = l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__6;
x_23 = lean_name_eq(x_7, x_22);
if (x_23 == 0)
{
lean_object* x_24; uint8_t x_25;
x_24 = l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__6;
x_24 = l_Lean_Elab_Command_isDefLike___closed__7;
x_25 = lean_name_eq(x_7, x_24);
lean_dec(x_7);
if (x_25 == 0)
@ -937,190 +899,190 @@ return x_26;
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
lean_object* x_27; lean_object* x_28; uint8_t x_29;
x_27 = lean_unsigned_to_nat(2u);
x_28 = l_Lean_Syntax_getArg(x_6, x_27);
x_29 = l_Lean_Elab_Command_expandDeclIdNamespace_x3f(x_28);
if (lean_obj_tag(x_29) == 0)
x_29 = l_Lean_Syntax_isNone(x_28);
if (x_29 == 0)
{
lean_object* x_30;
lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_30 = lean_unsigned_to_nat(0u);
x_31 = l_Lean_Syntax_getArg(x_28, x_30);
x_32 = l_Lean_Elab_Command_expandDeclIdNamespace_x3f(x_31);
if (lean_obj_tag(x_32) == 0)
{
lean_object* x_33;
lean_dec(x_28);
lean_dec(x_6);
lean_dec(x_1);
x_30 = lean_box(0);
return x_30;
x_33 = lean_box(0);
return x_33;
}
else
{
uint8_t x_31;
x_31 = !lean_is_exclusive(x_29);
if (x_31 == 0)
uint8_t x_34;
x_34 = !lean_is_exclusive(x_32);
if (x_34 == 0)
{
lean_object* x_32; uint8_t x_33;
x_32 = lean_ctor_get(x_29, 0);
x_33 = !lean_is_exclusive(x_32);
if (x_33 == 0)
lean_object* x_35; uint8_t x_36;
x_35 = lean_ctor_get(x_32, 0);
x_36 = !lean_is_exclusive(x_35);
if (x_36 == 0)
{
lean_object* x_34; lean_object* x_35; lean_object* x_36;
x_34 = lean_ctor_get(x_32, 1);
x_35 = l_Lean_Syntax_setArg(x_6, x_27, x_34);
x_36 = l_Lean_Syntax_setArg(x_1, x_5, x_35);
lean_ctor_set(x_32, 1, x_36);
return x_29;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_37 = lean_ctor_get(x_32, 0);
x_38 = lean_ctor_get(x_32, 1);
lean_inc(x_38);
lean_inc(x_37);
lean_dec(x_32);
lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40;
x_37 = lean_ctor_get(x_35, 1);
x_38 = l_Lean_Syntax_setArg(x_28, x_30, x_37);
x_39 = l_Lean_Syntax_setArg(x_6, x_27, x_38);
x_40 = l_Lean_Syntax_setArg(x_1, x_5, x_39);
x_41 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_41, 0, x_37);
lean_ctor_set(x_41, 1, x_40);
lean_ctor_set(x_29, 0, x_41);
return x_29;
}
lean_ctor_set(x_35, 1, x_40);
return x_32;
}
else
{
lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49;
x_42 = lean_ctor_get(x_29, 0);
lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46;
x_41 = lean_ctor_get(x_35, 0);
x_42 = lean_ctor_get(x_35, 1);
lean_inc(x_42);
lean_dec(x_29);
x_43 = lean_ctor_get(x_42, 0);
lean_inc(x_43);
x_44 = lean_ctor_get(x_42, 1);
lean_inc(x_44);
if (lean_is_exclusive(x_42)) {
lean_ctor_release(x_42, 0);
lean_ctor_release(x_42, 1);
x_45 = x_42;
} else {
lean_dec_ref(x_42);
x_45 = lean_box(0);
}
x_46 = l_Lean_Syntax_setArg(x_6, x_27, x_44);
x_47 = l_Lean_Syntax_setArg(x_1, x_5, x_46);
if (lean_is_scalar(x_45)) {
x_48 = lean_alloc_ctor(0, 2, 0);
} else {
x_48 = x_45;
}
lean_ctor_set(x_48, 0, x_43);
lean_ctor_set(x_48, 1, x_47);
x_49 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_49, 0, x_48);
return x_49;
}
}
lean_inc(x_41);
lean_dec(x_35);
x_43 = l_Lean_Syntax_setArg(x_28, x_30, x_42);
x_44 = l_Lean_Syntax_setArg(x_6, x_27, x_43);
x_45 = l_Lean_Syntax_setArg(x_1, x_5, x_44);
x_46 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_46, 0, x_41);
lean_ctor_set(x_46, 1, x_45);
lean_ctor_set(x_32, 0, x_46);
return x_32;
}
}
else
{
lean_object* x_50; uint8_t x_51;
lean_dec(x_7);
x_50 = l_Lean_Syntax_getArg(x_6, x_5);
x_51 = l_Lean_Syntax_isNone(x_50);
if (x_51 == 0)
{
lean_object* x_52; lean_object* x_53; lean_object* x_54;
x_52 = lean_unsigned_to_nat(0u);
x_53 = l_Lean_Syntax_getArg(x_50, x_52);
x_54 = l_Lean_Elab_Command_expandDeclIdNamespace_x3f(x_53);
if (lean_obj_tag(x_54) == 0)
{
lean_object* x_55;
lean_dec(x_50);
lean_dec(x_6);
lean_dec(x_1);
x_55 = lean_box(0);
lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55;
x_47 = lean_ctor_get(x_32, 0);
lean_inc(x_47);
lean_dec(x_32);
x_48 = lean_ctor_get(x_47, 0);
lean_inc(x_48);
x_49 = lean_ctor_get(x_47, 1);
lean_inc(x_49);
if (lean_is_exclusive(x_47)) {
lean_ctor_release(x_47, 0);
lean_ctor_release(x_47, 1);
x_50 = x_47;
} else {
lean_dec_ref(x_47);
x_50 = lean_box(0);
}
x_51 = l_Lean_Syntax_setArg(x_28, x_30, x_49);
x_52 = l_Lean_Syntax_setArg(x_6, x_27, x_51);
x_53 = l_Lean_Syntax_setArg(x_1, x_5, x_52);
if (lean_is_scalar(x_50)) {
x_54 = lean_alloc_ctor(0, 2, 0);
} else {
x_54 = x_50;
}
lean_ctor_set(x_54, 0, x_48);
lean_ctor_set(x_54, 1, x_53);
x_55 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_55, 0, x_54);
return x_55;
}
else
{
uint8_t x_56;
x_56 = !lean_is_exclusive(x_54);
if (x_56 == 0)
{
lean_object* x_57; uint8_t x_58;
x_57 = lean_ctor_get(x_54, 0);
x_58 = !lean_is_exclusive(x_57);
if (x_58 == 0)
{
lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62;
x_59 = lean_ctor_get(x_57, 1);
x_60 = l_Lean_Syntax_setArg(x_50, x_52, x_59);
x_61 = l_Lean_Syntax_setArg(x_6, x_5, x_60);
x_62 = l_Lean_Syntax_setArg(x_1, x_5, x_61);
lean_ctor_set(x_57, 1, x_62);
return x_54;
}
else
{
lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68;
x_63 = lean_ctor_get(x_57, 0);
x_64 = lean_ctor_get(x_57, 1);
lean_inc(x_64);
lean_inc(x_63);
lean_dec(x_57);
x_65 = l_Lean_Syntax_setArg(x_50, x_52, x_64);
x_66 = l_Lean_Syntax_setArg(x_6, x_5, x_65);
x_67 = l_Lean_Syntax_setArg(x_1, x_5, x_66);
x_68 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_68, 0, x_63);
lean_ctor_set(x_68, 1, x_67);
lean_ctor_set(x_54, 0, x_68);
return x_54;
}
}
else
{
lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77;
x_69 = lean_ctor_get(x_54, 0);
lean_inc(x_69);
lean_dec(x_54);
x_70 = lean_ctor_get(x_69, 0);
lean_inc(x_70);
x_71 = lean_ctor_get(x_69, 1);
lean_inc(x_71);
if (lean_is_exclusive(x_69)) {
lean_ctor_release(x_69, 0);
lean_ctor_release(x_69, 1);
x_72 = x_69;
} else {
lean_dec_ref(x_69);
x_72 = lean_box(0);
}
x_73 = l_Lean_Syntax_setArg(x_50, x_52, x_71);
x_74 = l_Lean_Syntax_setArg(x_6, x_5, x_73);
x_75 = l_Lean_Syntax_setArg(x_1, x_5, x_74);
if (lean_is_scalar(x_72)) {
x_76 = lean_alloc_ctor(0, 2, 0);
} else {
x_76 = x_72;
}
lean_ctor_set(x_76, 0, x_70);
lean_ctor_set(x_76, 1, x_75);
x_77 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_77, 0, x_76);
return x_77;
}
}
}
else
{
lean_object* x_78;
lean_dec(x_50);
lean_object* x_56;
lean_dec(x_28);
lean_dec(x_6);
lean_dec(x_1);
x_78 = lean_box(0);
x_56 = lean_box(0);
return x_56;
}
}
}
else
{
lean_object* x_57; lean_object* x_58;
lean_dec(x_7);
x_57 = l_Lean_Syntax_getArg(x_6, x_5);
x_58 = l_Lean_Elab_Command_expandDeclIdNamespace_x3f(x_57);
if (lean_obj_tag(x_58) == 0)
{
lean_object* x_59;
lean_dec(x_6);
lean_dec(x_1);
x_59 = lean_box(0);
return x_59;
}
else
{
uint8_t x_60;
x_60 = !lean_is_exclusive(x_58);
if (x_60 == 0)
{
lean_object* x_61; uint8_t x_62;
x_61 = lean_ctor_get(x_58, 0);
x_62 = !lean_is_exclusive(x_61);
if (x_62 == 0)
{
lean_object* x_63; lean_object* x_64; lean_object* x_65;
x_63 = lean_ctor_get(x_61, 1);
x_64 = l_Lean_Syntax_setArg(x_6, x_5, x_63);
x_65 = l_Lean_Syntax_setArg(x_1, x_5, x_64);
lean_ctor_set(x_61, 1, x_65);
return x_58;
}
else
{
lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70;
x_66 = lean_ctor_get(x_61, 0);
x_67 = lean_ctor_get(x_61, 1);
lean_inc(x_67);
lean_inc(x_66);
lean_dec(x_61);
x_68 = l_Lean_Syntax_setArg(x_6, x_5, x_67);
x_69 = l_Lean_Syntax_setArg(x_1, x_5, x_68);
x_70 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_70, 0, x_66);
lean_ctor_set(x_70, 1, x_69);
lean_ctor_set(x_58, 0, x_70);
return x_58;
}
}
else
{
lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78;
x_71 = lean_ctor_get(x_58, 0);
lean_inc(x_71);
lean_dec(x_58);
x_72 = lean_ctor_get(x_71, 0);
lean_inc(x_72);
x_73 = lean_ctor_get(x_71, 1);
lean_inc(x_73);
if (lean_is_exclusive(x_71)) {
lean_ctor_release(x_71, 0);
lean_ctor_release(x_71, 1);
x_74 = x_71;
} else {
lean_dec_ref(x_71);
x_74 = lean_box(0);
}
x_75 = l_Lean_Syntax_setArg(x_6, x_5, x_73);
x_76 = l_Lean_Syntax_setArg(x_1, x_5, x_75);
if (lean_is_scalar(x_74)) {
x_77 = lean_alloc_ctor(0, 2, 0);
} else {
x_77 = x_74;
}
lean_ctor_set(x_77, 0, x_72);
lean_ctor_set(x_77, 1, x_76);
x_78 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_78, 0, x_77);
return x_78;
}
}
}
}
else
{
lean_object* x_79; lean_object* x_80;
@ -4457,12 +4419,12 @@ x_17 = lean_name_eq(x_13, x_16);
if (x_17 == 0)
{
lean_object* x_18; uint8_t x_19;
x_18 = l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__6;
x_18 = l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__5;
x_19 = lean_name_eq(x_13, x_18);
if (x_19 == 0)
{
lean_object* x_20; uint8_t x_21;
x_20 = l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__4;
x_20 = l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__6;
x_21 = lean_name_eq(x_13, x_20);
lean_dec(x_13);
if (x_21 == 0)

177
stage0/stdlib/Lean/Elab/DefView.c generated
View file

@ -13,8 +13,8 @@
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2;
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabCommand___spec__7___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2;
lean_object* l_Lean_Elab_Command_MkInstanceName_collect___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_DefView_0__Lean_Elab_Command_MkInstanceName_kindReplacements___closed__7;
lean_object* l_Lean_throwError___at___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -47,7 +47,6 @@ lean_object* l_Lean_Elab_mkUnusedBaseName___at_Lean_Elab_Command_MkInstanceName_
lean_object* lean_st_ref_get(lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__1;
lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_initFn____x40_Lean_ReducibilityAttrs___hyg_10____closed__4;
@ -64,8 +63,6 @@ lean_object* l_Lean_Elab_Command_MkInstanceName_collect___lambda__1(lean_object*
lean_object* l_Lean_Elab_DefKind_isExample_match__1(lean_object*);
extern lean_object* l___regBuiltin_Lean_Elab_Term_elabTypeStx___closed__2;
lean_object* l_Lean_Elab_Command_MkInstanceName_collect_match__3(lean_object*);
extern lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_272____closed__1;
extern lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_272____closed__2;
lean_object* l_Lean_Elab_Command_MkInstanceName_mkFreshInstanceName___rarg___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_DefView_0__Lean_Elab_Command_MkInstanceName_kindReplacements___closed__2;
lean_object* lean_string_utf8_byte_size(lean_object*);
@ -93,6 +90,7 @@ lean_object* l_Std_RBNode_setBlack___rarg(lean_object*);
lean_object* l_Lean_Elab_mkFreshInstanceName(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_mkDefViewOfConstant_match__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Array_forInUnsafe_loop___at___private_Init_NotationExtra_0__Lean_mkHintBody___spec__1___closed__2;
extern lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_201____closed__2;
lean_object* l_Lean_Elab_Command_mkDefViewOfConstant___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_DefView_0__Lean_Elab_Command_MkInstanceName_kindReplacements___closed__6;
@ -133,10 +131,10 @@ uint8_t l_Lean_Elab_Command_isDefLike(lean_object*);
lean_object* l_Lean_Elab_Command_MkInstanceName_mkFreshInstanceName___rarg(lean_object*, lean_object*);
lean_object* l_Std_RBNode_find___at_Lean_Elab_Command_MkInstanceName_collect___spec__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_mkDefViewOfConstant___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__1;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_MkInstanceName_collect___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ResolveName_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_mkDefViewOfConstant_match__2___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__1;
lean_object* l_Lean_Elab_DefKind_isDefOrAbbrevOrOpaque_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
uint8_t l_Lean_Elab_DefKind_isTheorem(uint8_t);
@ -158,7 +156,7 @@ lean_object* l_Lean_Name_append(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_mkDefViewOfConstant_match__1(lean_object*);
lean_object* l_Lean_Syntax_getKind(lean_object*);
lean_object* l_Lean_Elab_Command_MkInstanceName_collect_match__2(lean_object*);
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959_(lean_object*);
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963_(lean_object*);
lean_object* l___private_Lean_Elab_DefView_0__Lean_Elab_Command_MkInstanceName_kindReplacements___closed__10;
lean_object* l_Lean_Elab_Command_isDefLike___closed__6;
lean_object* l_Lean_Elab_Command_getMainModule___rarg(lean_object*, lean_object*);
@ -166,6 +164,7 @@ extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____close
lean_object* l_Lean_Elab_Command_mkDefViewOfDef_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_mkDefViewOfExample___closed__2;
lean_object* l_Lean_Elab_Command_getRef(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_201____closed__1;
lean_object* l_Lean_Elab_Command_MkInstanceName_main_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_expandDeclSig(lean_object*);
lean_object* l_Lean_Elab_Command_mkDefViewOfAbbrev_match__1___rarg(lean_object*, lean_object*);
@ -186,6 +185,7 @@ lean_object* l_Lean_Elab_Command_isDefLike___closed__5;
lean_object* l_Lean_Elab_DefKind_isExample___boxed(lean_object*);
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__3;
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
uint8_t l_Lean_Elab_toAttributeKind(lean_object*);
lean_object* l_Lean_Elab_DefKind_isTheorem_match__1___rarg(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_mkDefView(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_mkDefView___closed__1;
@ -4840,7 +4840,7 @@ _start:
lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12; lean_object* x_13; lean_object* x_14;
x_9 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_9, 0, x_1);
x_10 = lean_unsigned_to_nat(3u);
x_10 = lean_unsigned_to_nat(4u);
x_11 = l_Lean_Syntax_getArg(x_2, x_10);
x_12 = 0;
x_13 = lean_alloc_ctor(0, 6, 1);
@ -4857,103 +4857,98 @@ lean_ctor_set(x_14, 1, x_8);
return x_14;
}
}
static lean_object* _init_l_Lean_Elab_Command_mkDefViewOfInstance___closed__1() {
_start:
{
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = 0;
x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_272____closed__2;
x_3 = lean_box(0);
x_4 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
return x_4;
}
}
lean_object* l_Lean_Elab_Command_mkDefViewOfInstance(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_6 = lean_unsigned_to_nat(2u);
lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_6 = lean_unsigned_to_nat(0u);
x_7 = l_Lean_Syntax_getArg(x_2, x_6);
x_8 = l_Lean_Elab_expandDeclSig(x_7);
x_8 = l_Lean_Elab_toAttributeKind(x_7);
lean_dec(x_7);
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
x_10 = lean_ctor_get(x_8, 1);
lean_inc(x_10);
lean_dec(x_8);
x_11 = l_Lean_Elab_Command_mkDefViewOfInstance___closed__1;
x_12 = l_Lean_Elab_Modifiers_addAttribute(x_1, x_11);
x_13 = lean_unsigned_to_nat(1u);
x_14 = l_Lean_Syntax_getArg(x_2, x_13);
x_15 = l_Lean_Syntax_getOptional_x3f(x_14);
lean_dec(x_14);
if (lean_obj_tag(x_15) == 0)
x_9 = lean_unsigned_to_nat(3u);
x_10 = l_Lean_Syntax_getArg(x_2, x_9);
x_11 = l_Lean_Elab_expandDeclSig(x_10);
lean_dec(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_Meta_initFn____x40_Lean_Meta_Instances___hyg_201____closed__2;
x_15 = lean_box(0);
x_16 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_16, 0, x_14);
lean_ctor_set(x_16, 1, x_15);
lean_ctor_set_uint8(x_16, sizeof(void*)*2, x_8);
x_17 = l_Lean_Elab_Modifiers_addAttribute(x_1, x_16);
x_18 = lean_unsigned_to_nat(2u);
x_19 = l_Lean_Syntax_getArg(x_2, x_18);
x_20 = l_Lean_Syntax_getOptional_x3f(x_19);
lean_dec(x_19);
if (lean_obj_tag(x_20) == 0)
{
lean_object* x_16;
lean_object* x_21;
lean_inc(x_3);
lean_inc(x_10);
x_16 = l_Lean_Elab_Command_MkInstanceName_main(x_10, x_3, x_4, x_5);
if (lean_obj_tag(x_16) == 0)
lean_inc(x_13);
x_21 = l_Lean_Elab_Command_MkInstanceName_main(x_13, x_3, x_4, x_5);
if (lean_obj_tag(x_21) == 0)
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
x_18 = lean_ctor_get(x_16, 1);
lean_inc(x_18);
lean_dec(x_16);
x_19 = l_Lean_mkIdentFrom(x_2, x_17);
x_20 = l_Lean_Syntax_mkApp___closed__1;
x_21 = lean_array_push(x_20, x_19);
x_22 = l_Lean_mkOptionalNode___closed__1;
x_23 = lean_array_push(x_21, x_22);
x_24 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__25;
x_25 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_23);
x_26 = l_Lean_Elab_Command_mkDefViewOfInstance___lambda__1(x_10, x_2, x_12, x_9, x_25, x_3, x_4, x_18);
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_22 = lean_ctor_get(x_21, 0);
lean_inc(x_22);
x_23 = lean_ctor_get(x_21, 1);
lean_inc(x_23);
lean_dec(x_21);
x_24 = l_Lean_mkIdentFrom(x_2, x_22);
x_25 = l_Lean_Syntax_mkApp___closed__1;
x_26 = lean_array_push(x_25, x_24);
x_27 = l_Lean_mkOptionalNode___closed__1;
x_28 = lean_array_push(x_26, x_27);
x_29 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__25;
x_30 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_30, 0, x_29);
lean_ctor_set(x_30, 1, x_28);
x_31 = l_Lean_Elab_Command_mkDefViewOfInstance___lambda__1(x_13, x_2, x_17, x_12, x_30, x_3, x_4, x_23);
lean_dec(x_3);
return x_26;
return x_31;
}
else
{
uint8_t x_27;
uint8_t x_32;
lean_dec(x_17);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_3);
lean_dec(x_2);
x_27 = !lean_is_exclusive(x_16);
if (x_27 == 0)
x_32 = !lean_is_exclusive(x_21);
if (x_32 == 0)
{
return x_16;
return x_21;
}
else
{
lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_28 = lean_ctor_get(x_16, 0);
x_29 = lean_ctor_get(x_16, 1);
lean_inc(x_29);
lean_inc(x_28);
lean_dec(x_16);
x_30 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_30, 0, x_28);
lean_ctor_set(x_30, 1, x_29);
return x_30;
lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_33 = lean_ctor_get(x_21, 0);
x_34 = lean_ctor_get(x_21, 1);
lean_inc(x_34);
lean_inc(x_33);
lean_dec(x_21);
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_33);
lean_ctor_set(x_35, 1, x_34);
return x_35;
}
}
}
else
{
lean_object* x_31; lean_object* x_32;
x_31 = lean_ctor_get(x_15, 0);
lean_inc(x_31);
lean_dec(x_15);
x_32 = l_Lean_Elab_Command_mkDefViewOfInstance___lambda__1(x_10, x_2, x_12, x_9, x_31, x_3, x_4, x_5);
lean_object* x_36; lean_object* x_37;
x_36 = lean_ctor_get(x_20, 0);
lean_inc(x_36);
lean_dec(x_20);
x_37 = l_Lean_Elab_Command_mkDefViewOfInstance___lambda__1(x_13, x_2, x_17, x_12, x_36, x_3, x_4, x_5);
lean_dec(x_3);
return x_32;
return x_37;
}
}
}
@ -5113,7 +5108,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__3;
x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_272____closed__1;
x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_201____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -5364,7 +5359,7 @@ lean_dec(x_4);
return x_6;
}
}
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__1() {
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__1() {
_start:
{
lean_object* x_1;
@ -5372,21 +5367,21 @@ x_1 = lean_mk_string("definition");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2() {
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_893____closed__1;
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__1;
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959_(lean_object* x_1) {
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2;
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2;
x_3 = l_Lean_registerTraceClass(x_2, x_1);
return x_3;
}
@ -5482,8 +5477,6 @@ l_Lean_Elab_Command_mkDefViewOfConstant___closed__3 = _init_l_Lean_Elab_Command_
lean_mark_persistent(l_Lean_Elab_Command_mkDefViewOfConstant___closed__3);
l_Lean_Elab_Command_mkDefViewOfConstant___closed__4 = _init_l_Lean_Elab_Command_mkDefViewOfConstant___closed__4();
lean_mark_persistent(l_Lean_Elab_Command_mkDefViewOfConstant___closed__4);
l_Lean_Elab_Command_mkDefViewOfInstance___closed__1 = _init_l_Lean_Elab_Command_mkDefViewOfInstance___closed__1();
lean_mark_persistent(l_Lean_Elab_Command_mkDefViewOfInstance___closed__1);
l_Lean_Elab_Command_mkDefViewOfExample___closed__1 = _init_l_Lean_Elab_Command_mkDefViewOfExample___closed__1();
lean_mark_persistent(l_Lean_Elab_Command_mkDefViewOfExample___closed__1);
l_Lean_Elab_Command_mkDefViewOfExample___closed__2 = _init_l_Lean_Elab_Command_mkDefViewOfExample___closed__2();
@ -5512,11 +5505,11 @@ l_Lean_Elab_Command_mkDefView___closed__2 = _init_l_Lean_Elab_Command_mkDefView_
lean_mark_persistent(l_Lean_Elab_Command_mkDefView___closed__2);
l_Lean_Elab_Command_mkDefView___closed__3 = _init_l_Lean_Elab_Command_mkDefView___closed__3();
lean_mark_persistent(l_Lean_Elab_Command_mkDefView___closed__3);
l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__1();
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__1);
l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2();
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2);
res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959_(lean_io_mk_world());
l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__1();
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__1);
l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2();
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2);
res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));

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

@ -44,6 +44,7 @@ lean_object* l_Lean_mkSort(lean_object*);
lean_object* l_List_foldlM___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_collectUniverses___spec__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___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors_match__1(lean_object*);
lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabHeaderAux___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* l_List_map___at_Lean_Meta_addInstance___spec__1(lean_object*);
lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_levelMVarToParamAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkForallFVarsImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___rarg___closed__2;
@ -371,7 +372,6 @@ lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkAuxConstruct
lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_getResultingUniverse(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabInductiveViews___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_expr_eqv(lean_object*, lean_object*);
lean_object* l_List_map___at_Lean_Meta_addGlobalInstanceImp___spec__1(lean_object*);
lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___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_Inductive_0__Lean_Elab_Command_mkIndFVar2Const___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_309____closed__4;
@ -10840,7 +10840,7 @@ lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkIndFVar2Cons
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_4 = l_List_map___at_Lean_Meta_addGlobalInstanceImp___spec__1(x_3);
x_4 = l_List_map___at_Lean_Meta_addInstance___spec__1(x_3);
x_5 = lean_array_get_size(x_1);
x_6 = l_Std_HashMap_instInhabitedHashMap___closed__1;
lean_inc(x_5);

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

@ -13,11 +13,11 @@
#ifdef __cplusplus
extern "C" {
#endif
extern lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2;
lean_object* l_Lean_Elab_elabModifiers___at_Lean_Elab_Command_elabMutualDef___spec__1___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabFunType_match__1(lean_object*);
lean_object* lean_expr_update_forall(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabCommand___spec__7___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_removeUnused(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_extractMacroScopes(lean_object*);
@ -10236,7 +10236,7 @@ static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_Mutu
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2;
x_2 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkClosureForAux___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

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

@ -21,6 +21,7 @@ lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinition_Basic
extern lean_object* l_Lean_Syntax_strLitToAtom___closed__3;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_fixLevelParams___spec__4(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_addAsAxiom(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___at_Lean_Meta_addInstance___spec__1(lean_object*);
lean_object* l_Lean_addDecl___at_Lean_Elab_Term_declareTacticSyntax___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_instantiateMVarsAtPreDecls___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_name_mk_string(lean_object*, lean_object*);
@ -103,7 +104,6 @@ lean_object* l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_levelMVarToP
size_t lean_ptr_addr(lean_object*);
lean_object* l_Lean_Elab_fixLevelParams_match__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_CollectLevelParams_instInhabitedState___closed__1;
lean_object* l_List_map___at_Lean_Meta_addGlobalInstanceImp___spec__1(lean_object*);
lean_object* l_Lean_Meta_abstractNestedProofs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_addNonRec___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_addAsAxiom___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -2998,7 +2998,7 @@ if (x_13 == 0)
lean_object* x_14; lean_object* x_15; lean_object* x_16; size_t x_17; size_t x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_14 = lean_ctor_get(x_12, 0);
lean_inc(x_14);
x_15 = l_List_map___at_Lean_Meta_addGlobalInstanceImp___spec__1(x_14);
x_15 = l_List_map___at_Lean_Meta_addInstance___spec__1(x_14);
x_16 = lean_array_get_size(x_11);
x_17 = lean_usize_of_nat(x_16);
lean_dec(x_16);
@ -3020,7 +3020,7 @@ lean_inc(x_23);
lean_inc(x_22);
lean_dec(x_12);
lean_inc(x_22);
x_24 = l_List_map___at_Lean_Meta_addGlobalInstanceImp___spec__1(x_22);
x_24 = l_List_map___at_Lean_Meta_addInstance___spec__1(x_22);
x_25 = lean_array_get_size(x_11);
x_26 = lean_usize_of_nat(x_25);
lean_dec(x_25);

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

@ -14,8 +14,8 @@
extern "C" {
#endif
lean_object* l_List_reverse___rarg(lean_object*);
extern lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__8___lambda__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2;
size_t l_USize_add(size_t, size_t);
lean_object* l_Lean_SCC_scc___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__5(lean_object*, lean_object*);
lean_object* l_Lean_stringToMessageData(lean_object*);
@ -398,7 +398,7 @@ lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean
x_43 = lean_ctor_get(x_37, 1);
lean_inc(x_43);
lean_dec(x_37);
x_44 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2;
x_44 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2;
x_45 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(x_44, x_2, x_3, x_4, x_5, x_6, x_7, x_43);
x_46 = lean_ctor_get(x_45, 0);
lean_inc(x_46);
@ -416,7 +416,7 @@ block_24:
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_10 = lean_ctor_get(x_1, 3);
lean_inc(x_10);
x_11 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2;
x_11 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2;
lean_inc(x_10);
x_12 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__1___boxed), 12, 3);
lean_closure_set(x_12, 0, x_1);
@ -494,7 +494,7 @@ x_31 = l_Lean_KernelException_toMessageData___closed__15;
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 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2;
x_33 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2;
x_34 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_33, x_32, x_2, x_3, x_4, x_5, x_6, x_7, x_26);
x_35 = lean_ctor_get(x_34, 1);
lean_inc(x_35);
@ -2852,7 +2852,7 @@ static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefiniti
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2;
x_2 = l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -3534,7 +3534,7 @@ static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefiniti
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2;
x_2 = l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__8___lambda__3___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

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

@ -13,11 +13,11 @@
#ifdef __cplusplus
extern "C" {
#endif
extern lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Structural_addSmartUnfoldingDefAux_visit___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_binductionOnSuffix;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_replaceRecApps_loop___spec__12___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* lean_array_set(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2;
lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_hasBadParamDep_x3f_match__2___rarg(lean_object*, lean_object*, lean_object*);
size_t l_USize_add(size_t, size_t);
lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_withBelowDict___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -6380,7 +6380,7 @@ static lean_object* _init_l___private_Lean_Elab_PreDefinition_Structural_0__Lean
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_959____closed__2;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_963____closed__2;
x_2 = l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_toBelowAux___closed__10;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

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

@ -20,6 +20,7 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectLevelPa
lean_object* l_Lean_Elab_applyVisibility___at_Lean_Elab_Command_elabStructure___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_instInhabitedStructFieldInfo;
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__7(lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___rarg___closed__12;
lean_object* l_Lean_Elab_Command_elabStructure___lambda__1___boxed(lean_object**);
lean_object* l_Lean_Elab_Term_removeUnused(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -45,10 +46,10 @@ lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Ela
lean_object* l_Lean_stringToMessageData(lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__5___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_mk_empty_array_with_capacity(lean_object*);
lean_object* l_Lean_Meta_addGlobalInstance___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_checkResultingUniverse(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__3___closed__2;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_removeUnused___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___at_Lean_Meta_addInstance___spec__1(lean_object*);
lean_object* l_Lean_setReducibilityStatus___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults___spec__3(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_withIncRecDepth___rarg___lambda__2___closed__2;
lean_object* l_Lean_LocalDecl_userName(lean_object*);
@ -68,7 +69,6 @@ lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__4___closed__1
uint8_t l_USize_decEq(size_t, size_t);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__6___boxed(lean_object**);
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* lean_io_error_to_string(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__6___closed__2;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withUsed___rarg(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_checkValidFieldModifier___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -132,6 +132,7 @@ lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
uint8_t l_Lean_isInternalSubobjectFieldName(lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3___closed__2;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_levelMVarToParamAux_match__1(lean_object*);
lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Array_getEvenElems___rarg___closed__1;
@ -150,7 +151,6 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_11836____closed__14;
lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__4___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_Meta_assignLevelMVar___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_updateResultingUniverse___spec__1___boxed(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_mkAuxConstructions(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___closed__2;
lean_object* l_Lean_Elab_Term_getLevelNames___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1019____spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -159,12 +159,10 @@ lean_object* l_Lean_Elab_Command_shouldInferResultUniverse(lean_object*, lean_ob
lean_object* l_Lean_Elab_Command_accLevelAtCtor(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_addCtorFields_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_string_utf8_byte_size(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__2___closed__2;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUsed_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_withLevelNames___rarg(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_withParents___rarg___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_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_USize_decLt(size_t, size_t);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__7___lambda__4___closed__1;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___closed__2;
@ -182,7 +180,6 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addProjections
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__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_mkDeclName___at_Lean_Elab_Command_elabStructure___spec__3___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__7(lean_object*, size_t, size_t, lean_object*);
lean_object* l___private_Lean_Elab_Command_0__Lean_Elab_Command_getVarDecls(lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_checkParentIsStructure(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -232,18 +229,21 @@ lean_object* l_Lean_Elab_Command_StructFieldInfo_isSubobject_match__1___rarg___b
lean_object* l_Lean_Elab_elabDeclAttrs___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Elab_Command_StructFieldInfo_isSubobject(lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withParents___rarg___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*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__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_nat_sub(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__1___closed__4;
lean_object* l_List_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__1(lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabFieldTypeValue_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3___closed__1;
lean_object* l_Lean_Meta_mkProjection___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_processSubfields_loop___spec__1(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__5___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_addTrace___at_Lean_Meta_isLevelDefEqAux___spec__1(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__8___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_elabStructureView___lambda__1___boxed__const__1;
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__6___closed__3;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_mkProjections___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_removeUnused_match__1(lean_object*);
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_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* 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* l_Lean_mkNoConfusion___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkAuxConstructions___spec__5(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*, lean_object*);
@ -263,7 +263,6 @@ lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean
extern lean_object* l_Lean_Elab_Command_checkValidCtorModifier___rarg___lambda__3___closed__3;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_checkParentIsStructure_match__1(lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_forM___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__4___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_Lean_Meta_assignLevelMVar___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_updateResultingUniverse___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -277,7 +276,6 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureV
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___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_applyVisibility___at_Lean_Elab_Command_elabStructure___spec__4(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__3___closed__1;
lean_object* l_List_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__8(lean_object*);
lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__4___lambda__3(lean_object*, uint8_t, 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_expandFields___spec__7___lambda__2___closed__2;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields_match__2___rarg(lean_object*, lean_object*);
@ -291,14 +289,13 @@ uint8_t l_Lean_LocalDecl_binderInfo(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__7___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*);
extern lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__3___closed__2;
lean_object* lean_st_mk_ref(lean_object*, lean_object*);
lean_object* l_List_forM___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3___boxed(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_addDefaults___closed__1;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_getResultUniverse_match__1(lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addCtorFields_match__1(lean_object*);
extern lean_object* l_Lean_Elab_Command_checkValidCtorModifier___rarg___lambda__1___closed__3;
lean_object* l_Lean_Meta_mkId___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__10___boxed(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__4(lean_object*, size_t, size_t, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_processSubfields_loop___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*);
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*);
@ -306,6 +303,7 @@ lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__1___closed__3
lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars_loop(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_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_checkParentIsStructure___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_addInstance(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabFieldTypeValue_match__2(lean_object*);
extern lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___rarg___lambda__1___closed__3;
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -327,10 +325,10 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___b
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__7___lambda__4___closed__4;
lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__3(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_withParents___rarg___closed__1;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___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* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___closed__1;
lean_object* l_Lean_Meta_getLocalInstances___at_Lean_Elab_Term_removeUnused___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_forM___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__2(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_addCtorFields_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__1(lean_object*, 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_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -374,6 +372,7 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withParents(le
lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabBinders___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Lean_Elab_Structure_0__Lean_Elab_Command_containsFieldName(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_elabModifiers___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__1(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_addCtorFields_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields(lean_object*);
@ -397,7 +396,6 @@ lean_object* l_Lean_Elab_Term_resetMessageLog(lean_object*, lean_object*, lean_o
extern lean_object* l_Lean_Expr_instInhabitedExpr;
uint8_t l_List_elem___at_Lean_NameHashSet_insert___spec__2(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_elabAttr___rarg___closed__3;
lean_object* lean_add_instance(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Option_get_x21___rarg___closed__4;
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__7___lambda__4___closed__3;
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -411,9 +409,9 @@ lean_object* l_Lean_Elab_elabModifiers___at___private_Lean_Elab_Structure_0__Lea
lean_object* l_Lean_Syntax_getSepArgs(lean_object*);
uint8_t l_Lean_isAttribute(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectLevelParamsInFVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_addGlobalInstance___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__2___boxed(lean_object*, 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_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_BinderInfo_beq(uint8_t, uint8_t);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___at_Lean_Elab_Command_elabStructure___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getNumArgs(lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -421,7 +419,6 @@ extern lean_object* l_Lean_CollectLevelParams_instInhabitedState___closed__1;
extern lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkAuxConstructions___closed__2;
lean_object* l_Lean_Elab_Command_elabStructure___boxed(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_addDefaults___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___at_Lean_Meta_addGlobalInstanceImp___spec__1(lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults___boxed__const__1;
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__7___lambda__4___closed__5;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Syntax_getSepArgs___spec__1(lean_object*, size_t, size_t, lean_object*);
@ -496,6 +493,7 @@ extern lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___rarg___lam
lean_object* l_Lean_Elab_Term_elabType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_elabModifiers___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__1___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*);
lean_object* l_List_forM___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkForall(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_withParents___spec__1(lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_processSubfields___rarg(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*);
@ -509,13 +507,12 @@ extern lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkProjectionIm
lean_object* lean_set_reducibility_status(lean_object*, lean_object*, uint8_t);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_4072____closed__4;
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___at_Lean_Elab_Command_elabStructure___spec__1___lambda__2___boxed(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__10(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_Command_StructFieldInfo_isFromParent_match__1___rarg(uint8_t, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUsed___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_Structure_0__Lean_Elab_Command_withFields___rarg___closed__10;
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Term_Quotation_match__syntax_expand___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_expandDeclId___at_Lean_Elab_Command_elabStructure___spec__2___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_3623_(lean_object*);
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_3627_(lean_object*);
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6(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_elabStructureView___lambda__1___closed__1;
lean_object* lean_expr_abstract(lean_object*, lean_object*);
@ -560,7 +557,6 @@ uint8_t l_Lean_Elab_toAttributeKind(lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_levelMVarToParamFVar(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_expandFields___spec__7___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*);
extern lean_object* l_Lean_CollectFVars_instInhabitedState___closed__1;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___closed__1;
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__7___lambda__3___closed__2;
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__6(lean_object*, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, 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_Lean_Expr_getAppFn(lean_object*);
@ -578,12 +574,13 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields_mat
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___at_Lean_Elab_Command_elabStructure___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___lambda__2___closed__2;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_findFieldInfo_x3f(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__9(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_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__9(lean_object*, size_t, size_t, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withUsed_match__1___rarg(lean_object*, lean_object*);
uint8_t l_Lean_Elab_isFreshInstanceName(lean_object*);
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__40;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_levelMVarToParamFVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLetDeclImp___rarg(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_elabStructureView___spec__8(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6___lambda__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_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___boxed(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__2___closed__1;
@ -13219,7 +13216,7 @@ x_12 = lean_ctor_get(x_1, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_1, 4);
lean_inc(x_13);
x_14 = l_List_map___at_Lean_Meta_addGlobalInstanceImp___spec__1(x_2);
x_14 = l_List_map___at_Lean_Meta_addInstance___spec__1(x_2);
x_15 = l_Lean_mkConst(x_13, x_14);
x_16 = l_Lean_mkAppN(x_15, x_3);
x_17 = lean_array_get_size(x_4);
@ -14487,87 +14484,16 @@ return x_12;
}
}
}
lean_object* l_Lean_Meta_addGlobalInstance___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__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) {
_start:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_9 = lean_st_ref_get(x_7, x_8);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = lean_ctor_get(x_10, 0);
lean_inc(x_12);
lean_dec(x_10);
x_13 = lean_st_ref_get(x_7, x_11);
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = lean_ctor_get(x_6, 3);
x_16 = lean_add_instance(x_12, x_1, x_14);
if (lean_obj_tag(x_16) == 0)
{
lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
x_18 = lean_ctor_get(x_16, 1);
lean_inc(x_18);
lean_dec(x_16);
x_19 = l_Lean_setEnv___at_Lean_Elab_Term_declareTacticSyntax___spec__3(x_17, x_2, x_3, x_4, x_5, x_6, x_7, x_18);
return x_19;
}
else
{
uint8_t x_20;
x_20 = !lean_is_exclusive(x_16);
if (x_20 == 0)
{
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_21 = lean_ctor_get(x_16, 0);
x_22 = lean_io_error_to_string(x_21);
x_23 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_23, 0, x_22);
x_24 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_24, 0, x_23);
lean_inc(x_15);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_15);
lean_ctor_set(x_25, 1, x_24);
lean_ctor_set(x_16, 0, x_25);
return x_16;
}
else
{
lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_26 = lean_ctor_get(x_16, 0);
x_27 = lean_ctor_get(x_16, 1);
lean_inc(x_27);
lean_inc(x_26);
lean_dec(x_16);
x_28 = lean_io_error_to_string(x_26);
x_29 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_29, 0, x_28);
x_30 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_30, 0, x_29);
lean_inc(x_15);
x_31 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_31, 0, x_15);
lean_ctor_set(x_31, 1, x_30);
x_32 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_32, 0, x_31);
lean_ctor_set(x_32, 1, x_27);
return x_32;
}
}
}
}
lean_object* l_List_forM___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__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, lean_object* x_8) {
lean_object* l_List_forM___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__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) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_9; lean_object* x_10;
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
x_9 = lean_box(0);
x_10 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_10, 0, x_9);
@ -14576,50 +14502,59 @@ return x_10;
}
else
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14;
x_11 = lean_ctor_get(x_1, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_1, 1);
lean_inc(x_12);
lean_dec(x_1);
x_13 = l_Lean_Meta_addGlobalInstance___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__2(x_11, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
if (lean_obj_tag(x_13) == 0)
x_13 = 0;
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
x_14 = l_Lean_Meta_addInstance(x_11, x_13, x_4, x_5, x_6, x_7, x_8);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_14;
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
lean_object* x_15;
x_15 = lean_ctor_get(x_14, 1);
lean_inc(x_15);
lean_dec(x_14);
x_1 = x_12;
x_8 = x_14;
x_8 = x_15;
goto _start;
}
else
{
uint8_t x_16;
uint8_t x_17;
lean_dec(x_12);
x_16 = !lean_is_exclusive(x_13);
if (x_16 == 0)
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
x_17 = !lean_is_exclusive(x_14);
if (x_17 == 0)
{
return x_13;
return x_14;
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_17 = lean_ctor_get(x_13, 0);
x_18 = lean_ctor_get(x_13, 1);
lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_18 = lean_ctor_get(x_14, 0);
x_19 = lean_ctor_get(x_14, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_inc(x_17);
lean_dec(x_13);
x_19 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_19, 0, x_17);
lean_ctor_set(x_19, 1, x_18);
return x_19;
lean_dec(x_14);
x_20 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_20, 0, x_18);
lean_ctor_set(x_20, 1, x_19);
return x_20;
}
}
}
}
}
static lean_object* _init_l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___closed__1() {
static lean_object* _init_l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3___closed__1() {
_start:
{
lean_object* x_1;
@ -14627,17 +14562,17 @@ x_1 = lean_mk_string("_default");
return x_1;
}
}
static lean_object* _init_l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___closed__2() {
static lean_object* _init_l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___closed__1;
x_2 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4(size_t 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, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3(size_t 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, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
uint8_t x_11;
@ -14679,7 +14614,7 @@ lean_inc(x_21);
lean_dec(x_19);
x_22 = lean_ctor_get(x_17, 1);
lean_inc(x_22);
x_23 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___closed__2;
x_23 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3___closed__2;
x_24 = l_Lean_Name_append(x_22, x_23);
lean_dec(x_22);
x_25 = lean_ctor_get(x_17, 3);
@ -14759,7 +14694,7 @@ return x_47;
}
}
}
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__5(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
@ -14798,7 +14733,7 @@ return x_4;
}
}
}
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__6(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__5(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
@ -14823,7 +14758,7 @@ return x_4;
}
}
}
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__7(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__6(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
@ -14858,7 +14793,7 @@ return x_4;
}
}
}
lean_object* l_List_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__8(lean_object* x_1) {
lean_object* l_List_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__7(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 0)
@ -14883,7 +14818,7 @@ lean_dec(x_4);
x_8 = lean_alloc_ctor(0, 1, 1);
lean_ctor_set(x_8, 0, x_6);
lean_ctor_set_uint8(x_8, sizeof(void*)*1, x_7);
x_9 = l_List_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__8(x_5);
x_9 = l_List_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__7(x_5);
lean_ctor_set(x_1, 1, x_9);
lean_ctor_set(x_1, 0, x_8);
return x_1;
@ -14903,7 +14838,7 @@ lean_dec(x_10);
x_14 = lean_alloc_ctor(0, 1, 1);
lean_ctor_set(x_14, 0, x_12);
lean_ctor_set_uint8(x_14, sizeof(void*)*1, x_13);
x_15 = l_List_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__8(x_11);
x_15 = l_List_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__7(x_11);
x_16 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_16, 0, x_14);
lean_ctor_set(x_16, 1, x_15);
@ -14912,7 +14847,7 @@ return x_16;
}
}
}
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__9(lean_object* x_1, size_t x_2, size_t 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* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__8(lean_object* x_1, size_t x_2, size_t 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) {
_start:
{
uint8_t x_12;
@ -15027,7 +14962,7 @@ return x_35;
}
}
}
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__10(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__9(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
@ -15549,7 +15484,7 @@ size_t x_164; size_t x_165; lean_object* x_166;
x_164 = 0;
x_165 = lean_usize_of_nat(x_68);
lean_inc(x_5);
x_166 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__10(x_17, x_164, x_165, x_5);
x_166 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__9(x_17, x_164, x_165, x_5);
x_136 = x_166;
goto block_162;
}
@ -15574,7 +15509,11 @@ lean_object* x_76; lean_object* x_77;
x_76 = lean_ctor_get(x_75, 1);
lean_inc(x_76);
lean_dec(x_75);
x_77 = l_List_forM___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3(x_72, x_9, x_10, x_11, x_12, x_13, x_14, x_76);
lean_inc(x_14);
lean_inc(x_13);
lean_inc(x_12);
lean_inc(x_11);
x_77 = l_List_forM___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__2(x_72, x_9, x_10, x_11, x_12, x_13, x_14, x_76);
if (lean_obj_tag(x_77) == 0)
{
lean_object* x_78; lean_object* x_79; lean_object* x_80; uint8_t x_81; size_t x_82; lean_object* x_83;
@ -15604,7 +15543,7 @@ else
{
size_t x_122; lean_object* x_123;
x_122 = lean_usize_of_nat(x_68);
x_123 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__7(x_17, x_82, x_122, x_5);
x_123 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__6(x_17, x_82, x_122, x_5);
x_83 = x_123;
goto block_120;
}
@ -15618,7 +15557,7 @@ lean_dec(x_84);
x_86 = x_83;
x_87 = lean_box_usize(x_85);
x_88 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__1___boxed__const__1;
x_89 = lean_alloc_closure((void*)(l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___boxed), 10, 3);
x_89 = lean_alloc_closure((void*)(l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3___boxed), 10, 3);
lean_closure_set(x_89, 0, x_87);
lean_closure_set(x_89, 1, x_88);
lean_closure_set(x_89, 2, x_86);
@ -15668,7 +15607,7 @@ else
size_t x_98; lean_object* x_99; lean_object* x_100;
x_98 = lean_usize_of_nat(x_68);
lean_dec(x_68);
x_99 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__5(x_17, x_82, x_98, x_79);
x_99 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4(x_17, x_82, x_98, x_79);
lean_dec(x_17);
x_100 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults(x_99, x_92, x_9, x_10, x_11, x_12, x_13, x_14, x_93);
return x_100;
@ -15708,7 +15647,7 @@ else
size_t x_105; lean_object* x_106; lean_object* x_107;
x_105 = lean_usize_of_nat(x_68);
lean_dec(x_68);
x_106 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__5(x_17, x_82, x_105, x_79);
x_106 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4(x_17, x_82, x_105, x_79);
lean_dec(x_17);
x_107 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults(x_106, x_92, x_9, x_10, x_11, x_12, x_13, x_14, x_93);
return x_107;
@ -15720,7 +15659,7 @@ else
size_t x_108; lean_object* x_109;
x_108 = lean_usize_of_nat(x_59);
lean_dec(x_59);
x_109 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__6(x_45, x_82, x_108, x_79);
x_109 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__5(x_45, x_82, x_108, x_79);
lean_dec(x_45);
if (x_81 == 0)
{
@ -15747,7 +15686,7 @@ else
size_t x_113; lean_object* x_114; lean_object* x_115;
x_113 = lean_usize_of_nat(x_68);
lean_dec(x_68);
x_114 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__5(x_17, x_82, x_113, x_109);
x_114 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4(x_17, x_82, x_113, x_109);
lean_dec(x_17);
x_115 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults(x_114, x_92, x_9, x_10, x_11, x_12, x_13, x_14, x_93);
return x_115;
@ -15864,7 +15803,7 @@ block_162:
{
lean_object* x_137; lean_object* x_138; lean_object* x_139;
x_137 = lean_array_to_list(lean_box(0), x_136);
x_138 = l_List_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__8(x_137);
x_138 = l_List_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__7(x_137);
lean_inc(x_9);
lean_inc(x_55);
x_139 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addProjections(x_55, x_138, x_135, x_9, x_10, x_11, x_12, x_13, x_14, x_67);
@ -15916,7 +15855,7 @@ lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_5);
x_147 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__9(x_17, x_145, x_146, x_5, x_9, x_10, x_11, x_12, x_13, x_14, x_143);
x_147 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__8(x_17, x_145, x_146, x_5, x_9, x_10, x_11, x_12, x_13, x_14, x_143);
if (lean_obj_tag(x_147) == 0)
{
lean_object* x_148; lean_object* x_149;
@ -16684,35 +16623,17 @@ return x_25;
}
}
}
lean_object* l_Lean_Meta_addGlobalInstance___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__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* l_List_forM___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__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) {
_start:
{
lean_object* x_9;
x_9 = l_Lean_Meta_addGlobalInstance___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
x_9 = l_List_forM___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_3);
lean_dec(x_2);
return x_9;
}
}
lean_object* l_List_forM___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__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, lean_object* x_8) {
_start:
{
lean_object* x_9;
x_9 = l_List_forM___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_9;
}
}
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___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_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__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, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
size_t x_11; size_t x_12; lean_object* x_13;
@ -16720,12 +16641,25 @@ x_11 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_12 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_13 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4(x_11, x_12, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_13 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3(x_11, x_12, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_5);
lean_dec(x_4);
return x_13;
}
}
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7;
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = lean_unbox_usize(x_3);
lean_dec(x_3);
x_7 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4(x_1, x_5, x_6, x_4);
lean_dec(x_1);
return x_7;
}
}
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__5___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -16752,20 +16686,7 @@ lean_dec(x_1);
return x_7;
}
}
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__7___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7;
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = lean_unbox_usize(x_3);
lean_dec(x_3);
x_7 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__7(x_1, x_5, x_6, x_4);
lean_dec(x_1);
return x_7;
}
}
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__9___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* x_11) {
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__8___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* x_11) {
_start:
{
size_t x_12; size_t x_13; lean_object* x_14;
@ -16773,12 +16694,12 @@ x_12 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_13 = lean_unbox_usize(x_3);
lean_dec(x_3);
x_14 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__9(x_1, x_12, x_13, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
x_14 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__8(x_1, x_12, x_13, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
lean_dec(x_1);
return x_14;
}
}
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__10___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__9___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7;
@ -16786,7 +16707,7 @@ x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = lean_unbox_usize(x_3);
lean_dec(x_3);
x_7 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__10(x_1, x_5, x_6, x_4);
x_7 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__9(x_1, x_5, x_6, x_4);
lean_dec(x_1);
return x_7;
}
@ -18835,7 +18756,7 @@ lean_dec(x_4);
return x_6;
}
}
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_3623_(lean_object* x_1) {
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_3627_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -19035,10 +18956,10 @@ l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults___closed__1 = _
lean_mark_persistent(l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults___closed__1);
l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults___boxed__const__1 = _init_l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults___boxed__const__1();
lean_mark_persistent(l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults___boxed__const__1);
l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___closed__1 = _init_l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___closed__1();
lean_mark_persistent(l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___closed__1);
l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___closed__2 = _init_l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___closed__2();
lean_mark_persistent(l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4___closed__2);
l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3___closed__1 = _init_l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3___closed__1();
lean_mark_persistent(l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3___closed__1);
l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3___closed__2 = _init_l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3___closed__2();
lean_mark_persistent(l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__3___closed__2);
l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__1___closed__1 = _init_l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__1___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__1___closed__1);
l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__1___closed__2 = _init_l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__1___closed__2();
@ -19063,7 +18984,7 @@ l_Lean_Elab_Command_elabStructure___closed__2 = _init_l_Lean_Elab_Command_elabSt
lean_mark_persistent(l_Lean_Elab_Command_elabStructure___closed__2);
l_Lean_Elab_Command_elabStructure___closed__3 = _init_l_Lean_Elab_Command_elabStructure___closed__3();
lean_mark_persistent(l_Lean_Elab_Command_elabStructure___closed__3);
res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_3623_(lean_io_mk_world());
res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_3627_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));

31
stage0/stdlib/Lean/Elab/Term.c generated
View file

@ -132,6 +132,7 @@ lean_object* l_Lean_Elab_logTrace___at_Lean_Elab_Term_traceAtCmdPos___spec__1___
lean_object* l_Lean_Elab_Term_instInhabitedTermElabM___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_throwUnsupportedSyntax___rarg___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_elabRawNatLit(lean_object*);
extern lean_object* l_Lean_LocalContext_fvarIdToDecl___default___closed__1;
lean_object* l_Lean_getConstInfo___at_Lean_Elab_Term_mkConst___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resolveLocalName_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -437,7 +438,6 @@ lean_object* l_Lean_Elab_Term_elabProp___rarg(lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambdaAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_KernelException_toMessageData___closed__29;
lean_object* l_Lean_Syntax_isStrLit_x3f(lean_object*);
extern lean_object* l_Lean_Meta_addGlobalInstanceImp___closed__2;
lean_object* l___private_Lean_Util_Trace_0__Lean_getResetTraces___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_processPostponedStep___spec__6___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkTypeMismatchError___closed__1;
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -545,6 +545,7 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabOptLevel___boxed(l
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5882_(lean_object*);
lean_object* l_Lean_Elab_Term_setElabConfig(lean_object*);
lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__4;
lean_object* l_Lean_Elab_Term_getLetRecsToLift(lean_object*);
lean_object* l_Lean_Elab_Term_liftLevelM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1034_(lean_object*);
@ -37107,18 +37108,30 @@ return x_47;
static lean_object* _init_l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_LocalContext_fvarIdToDecl___default___closed__1;
x_2 = l_Std_PersistentArray_empty___closed__1;
x_3 = lean_alloc_ctor(0, 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_instMetaEvalTermElabM___rarg___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Context_config___default___closed__1;
x_2 = l_Lean_Elab_Term_setElabConfig(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__2() {
static lean_object* _init_l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__1;
x_2 = l_Lean_Meta_addGlobalInstanceImp___closed__2;
x_1 = l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__2;
x_2 = l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__1;
x_3 = l_Array_empty___closed__1;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
@ -37127,7 +37140,7 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3() {
static lean_object* _init_l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__4() {
_start:
{
lean_object* x_1;
@ -37189,7 +37202,7 @@ x_78 = lean_ctor_get(x_76, 1);
lean_inc(x_78);
lean_dec(x_76);
x_79 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkSomeContext;
x_80 = l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__2;
x_80 = l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3;
lean_inc(x_40);
lean_inc(x_34);
lean_inc(x_46);
@ -37216,7 +37229,7 @@ lean_dec(x_86);
x_89 = lean_ctor_get(x_87, 3);
lean_inc(x_89);
lean_dec(x_87);
x_90 = l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3;
x_90 = l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__4;
lean_inc(x_40);
lean_inc(x_34);
lean_inc(x_46);
@ -37306,7 +37319,7 @@ lean_dec(x_108);
x_111 = lean_ctor_get(x_109, 3);
lean_inc(x_111);
lean_dec(x_109);
x_112 = l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3;
x_112 = l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__4;
lean_inc(x_40);
lean_inc(x_34);
lean_inc(x_46);
@ -38365,6 +38378,8 @@ l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__2 = _init_l_Lean_Elab_Te
lean_mark_persistent(l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__2);
l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3 = _init_l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3);
l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__4 = _init_l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__4();
lean_mark_persistent(l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__4);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7622____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7622____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7622____closed__1);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7622_(lean_io_mk_world());

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

File diff suppressed because it is too large Load diff

282
stage0/stdlib/Lean/Parser/Command.c generated
View file

@ -58,7 +58,6 @@ lean_object* l_Lean_Parser_Command_printAxioms___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_structCtor___closed__8;
lean_object* l_Lean_Parser_Command_structExplicitBinder_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_quot_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Command_instance___elambda__1___closed__16;
lean_object* l_Lean_Parser_Command_structExplicitBinder___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_theorem___closed__9;
lean_object* l_Lean_Parser_Command_structure_formatter___closed__9;
@ -194,7 +193,6 @@ lean_object* l_Lean_Parser_Command_declModifiers___closed__1;
lean_object* l_Lean_Parser_Command_openRenaming___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_structCtor___closed__4;
lean_object* l_Lean_Parser_Command_visibility_formatter___closed__1;
lean_object* l_Lean_Parser_Command_instance_formatter___closed__12;
lean_object* l_Lean_Parser_many(lean_object*);
lean_object* l_Lean_Parser_Command_declModifiers_formatter___closed__3;
lean_object* l_Lean_Parser_Command_extends_parenthesizer___closed__2;
@ -291,7 +289,6 @@ extern lean_object* l_Lean_Parser_sepByScopeSuffixes_parenthesizer___closed__2;
lean_object* l___regBuiltinParser_Lean_Parser_Command_attribute(lean_object*);
lean_object* l_Lean_Parser_Command_section___closed__5;
lean_object* l_Lean_Parser_Command_openSimple___elambda__1___closed__3;
lean_object* l_Lean_PrettyPrinter_Formatter_checkInsideQuot_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__18;
lean_object* l_Lean_Parser_Command_ctor_parenthesizer___closed__5;
extern lean_object* l_Lean_Parser_Term_attributes_parenthesizer___closed__3;
@ -414,7 +411,6 @@ lean_object* l_Lean_Parser_Command_structFields___elambda__1___closed__22;
lean_object* l_Lean_Parser_Command_end_formatter___closed__1;
lean_object* l___regBuiltinParser_Lean_Parser_Command_export(lean_object*);
lean_object* l_Lean_Parser_Term_quot___closed__9;
lean_object* l_Lean_Parser_Command_instance___elambda__1___closed__15;
lean_object* l_Lean_Parser_Command_theorem_formatter___closed__5;
extern lean_object* l_Lean_Parser_Term_attributes___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_inductive___closed__5;
@ -541,7 +537,6 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_toggleInsideQuot_parenthesizer(l
lean_object* l_Lean_Parser_Command_printAxioms_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_init__quot___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_def_parenthesizer___closed__1;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_structure_parenthesizer___closed__8;
lean_object* l_Lean_Parser_Command_visibility_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_exit___closed__6;
@ -594,7 +589,6 @@ lean_object* l_Lean_Parser_Command_structFields___elambda__1___closed__17;
lean_object* l_Lean_Parser_Command_initialize_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_skip_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_structExplicitBinder___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_instance_parenthesizer___closed__8;
lean_object* l_Lean_Parser_Command_initialize___closed__7;
lean_object* l_Lean_Parser_Command_print_formatter___closed__4;
lean_object* l_Lean_Parser_Command_instance___closed__8;
@ -724,7 +718,6 @@ lean_object* l_Lean_Parser_Command_resolve__name___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_docComment_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_variables___closed__6;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_atomic_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_instance_parenthesizer___closed__11;
lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_declId___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_declaration_formatter___closed__13;
@ -860,7 +853,6 @@ lean_object* l_Lean_Parser_Command_universes___elambda__1___closed__10;
lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__7;
lean_object* l___regBuiltin_Lean_Parser_Command_synth_formatter(lean_object*);
extern lean_object* l_Lean_Parser_Term_binderDefault;
extern lean_object* l_Lean_Parser_checkOutsideQuot___closed__1;
lean_object* l_Lean_Parser_Command_structExplicitBinder___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_visibility_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Command_in_parenthesizer(lean_object*);
@ -993,7 +985,6 @@ lean_object* l_Lean_Parser_Command_export___closed__9;
lean_object* l_Lean_Parser_Command_check__failure___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__21;
lean_object* l_Lean_Parser_Command_printAxioms_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_instance___elambda__1___closed__14;
lean_object* l_Lean_Parser_Command_axiom_formatter___closed__4;
lean_object* l___regBuiltin_Lean_Parser_Command_printAxioms_formatter(lean_object*);
lean_object* l_Lean_Parser_Command_init__quot_parenthesizer___closed__1;
@ -1399,7 +1390,6 @@ lean_object* l_Lean_Parser_Command_structFields___closed__3;
lean_object* l_Lean_Parser_Term_quot___closed__5;
lean_object* l_Lean_Parser_Command_commentBody___elambda__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_in___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_instance_formatter___closed__8;
lean_object* l_Lean_Parser_Command_private___closed__6;
lean_object* l___regBuiltin_Lean_Parser_Command_init__quot_formatter___closed__1;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_many1Unbox_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1602,7 +1592,6 @@ lean_object* l_Lean_Parser_Command_declModifiers_parenthesizer___closed__9;
lean_object* l_Lean_Parser_Command_variables_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Command_classInductive___closed__8;
lean_object* l_Lean_Parser_Command_structCtor___closed__7;
extern lean_object* l_Lean_Parser_checkInsideQuot___closed__1;
lean_object* l_Lean_Parser_Command_openOnly___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_check_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_openRenaming___elambda__1___closed__9;
@ -1614,7 +1603,6 @@ lean_object* l_Lean_Parser_Command_printAxioms___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_noncomputable___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_quot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_instance___closed__10;
lean_object* l_Lean_Parser_Command_example_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_open___elambda__1___closed__11;
lean_object* l_Lean_Parser_Term_quot___closed__7;
@ -1724,7 +1712,6 @@ lean_object* l_Lean_Parser_Command_instance_formatter___closed__1;
lean_object* l_Lean_Parser_Command_init__quot___closed__2;
lean_object* l_Lean_Parser_Command_mutual___closed__2;
lean_object* l_Lean_Parser_Command_openSimple___closed__4;
lean_object* l_Lean_Parser_Command_instance_parenthesizer___closed__7;
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__6;
lean_object* l___regBuiltin_Lean_Parser_Command_synth_formatter___closed__1;
lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__8;
@ -1931,7 +1918,6 @@ extern lean_object* l_Lean_Parser_epsilonInfo;
lean_object* l_Lean_Parser_notSymbol_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_def___closed__1;
lean_object* l_Lean_Parser_Command_initialize___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_instance_parenthesizer___closed__10;
lean_object* l_Lean_Parser_Command_export___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_structCtor_formatter___closed__7;
lean_object* l_Lean_Parser_Command_docComment_parenthesizer___closed__4;
@ -2036,7 +2022,6 @@ lean_object* l_Lean_Parser_Command_openRenamingItem___elambda__1___closed__11;
lean_object* l_Lean_Parser_Command_openHiding___closed__2;
lean_object* l_Lean_Parser_Command_constant___closed__4;
lean_object* l_Lean_Parser_Command_declModifiers_formatter___closed__21;
lean_object* l_Lean_PrettyPrinter_Formatter_checkOutsideQuot_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_universe_formatter___closed__3;
lean_object* l_Lean_Parser_Command_partial___closed__2;
lean_object* l_Lean_Parser_Command_declModifiers_parenthesizer___closed__7;
@ -2161,7 +2146,6 @@ lean_object* l_Lean_Parser_Command_structFields___closed__5;
lean_object* l_Lean_Parser_Command_variable___closed__2;
lean_object* l_Lean_Parser_Command_section_formatter___closed__3;
lean_object* l_Lean_Parser_Command_unsafe___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_instance___closed__11;
lean_object* l_Lean_Parser_Command_synth___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_structImplicitBinder___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_inferMod_formatter___closed__2;
@ -2190,7 +2174,6 @@ lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_declModifiers_formatter___closed__13;
lean_object* l_Lean_Parser_Command_variables;
lean_object* l_Lean_Parser_Command_builtin__initialize___closed__1;
lean_object* l_Lean_Parser_Command_instance_formatter___closed__9;
lean_object* l_Lean_Parser_Command_export___elambda__1___closed__13;
lean_object* l_Lean_Parser_Command_set__option_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__10;
@ -2297,7 +2280,6 @@ lean_object* l_Lean_Parser_Command_axiom___closed__2;
lean_object* l_Lean_Parser_Command_constant___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_openOnly___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_inductive_formatter___closed__5;
lean_object* l_Lean_Parser_Command_instance_formatter___closed__10;
lean_object* l_Lean_Parser_Command_structure___elambda__1___closed__4;
extern lean_object* l_Lean_Parser_Term_dynamicQuot___elambda__1___closed__11;
lean_object* l_Lean_Parser_Command_check__failure_formatter___closed__3;
@ -2448,7 +2430,6 @@ lean_object* l_Lean_Parser_Command_inductive___closed__10;
lean_object* l_Lean_Parser_Command_example___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_exit___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_structure_parenthesizer___closed__11;
lean_object* l_Lean_Parser_Command_instance_parenthesizer___closed__9;
lean_object* l_Lean_Parser_Command_synth___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_structCtor_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Command_structureTk_parenthesizer___closed__1;
@ -2469,7 +2450,6 @@ lean_object* l_Lean_Parser_Command_declModifiers_formatter___closed__9;
lean_object* l_Lean_Parser_Command_constant___elambda__1___closed__13;
lean_object* l_Lean_Parser_Command_abbrev___closed__6;
lean_object* l_Lean_Parser_Command_open___closed__9;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_example___closed__2;
lean_object* l_Lean_Parser_Command_declValEqns_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_mutual___closed__5;
@ -2542,7 +2522,6 @@ lean_object* l_Lean_Parser_Command_openOnly_formatter___closed__5;
lean_object* l_Lean_Parser_Command_partial_formatter___closed__1;
extern lean_object* l_instReprChar___closed__1;
lean_object* l_Lean_Parser_Command_openHiding_formatter___closed__4;
lean_object* l_Lean_Parser_Command_instance_formatter___closed__11;
lean_object* l___regBuiltin_Lean_Parser_Command_initialize_parenthesizer(lean_object*);
extern lean_object* l_Lean_Parser_Term_haveAssign_formatter___closed__2;
extern lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_953____closed__19;
@ -2648,7 +2627,6 @@ lean_object* l_Lean_Parser_Command_instance___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_set__option___closed__11;
lean_object* l_Lean_Parser_Command_open___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_theorem___closed__2;
lean_object* l_Lean_Parser_Command_instance___closed__12;
lean_object* l_Lean_Parser_Command_check_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_declaration___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_declId___elambda__1___closed__2;
@ -6761,7 +6739,7 @@ static lean_object* _init_l_Lean_Parser_Command_instance___elambda__1___closed__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_checkOutsideQuot___closed__1;
x_1 = l_Lean_Parser_Term_attrKind___closed__4;
x_2 = l_Lean_Parser_Command_instance___elambda__1___closed__10;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
@ -6773,9 +6751,9 @@ static lean_object* _init_l_Lean_Parser_Command_instance___elambda__1___closed__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_attrKind___closed__4;
x_2 = l_Lean_Parser_Command_instance___elambda__1___closed__10;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
x_1 = l_Lean_Parser_Command_instance___elambda__1___closed__2;
x_2 = l_Lean_Parser_Command_instance___elambda__1___closed__11;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
@ -6785,44 +6763,8 @@ static lean_object* _init_l_Lean_Parser_Command_instance___elambda__1___closed__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_checkInsideQuot___closed__1;
x_2 = l_Lean_Parser_Command_instance___elambda__1___closed__12;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance___elambda__1___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_instance___elambda__1___closed__11;
x_2 = l_Lean_Parser_Command_instance___elambda__1___closed__13;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_orelseFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance___elambda__1___closed__15() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_instance___elambda__1___closed__2;
x_2 = l_Lean_Parser_Command_instance___elambda__1___closed__14;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance___elambda__1___closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_sepByScopeSuffixes___elambda__1___closed__11;
x_2 = l_Lean_Parser_Command_instance___elambda__1___closed__15;
x_2 = l_Lean_Parser_Command_instance___elambda__1___closed__12;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -6836,7 +6778,7 @@ lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; lean_object*
x_3 = l_Lean_Parser_Command_instance___elambda__1___closed__4;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
x_5 = l_Lean_Parser_Command_instance___elambda__1___closed__16;
x_5 = l_Lean_Parser_Command_instance___elambda__1___closed__13;
x_6 = 1;
x_7 = l_Lean_Parser_orelseFnCore(x_4, x_5, x_6, x_1, x_2);
return x_7;
@ -6876,16 +6818,6 @@ return x_3;
static lean_object* _init_l_Lean_Parser_Command_instance___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Command_instance___closed__3;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_attrKind;
x_2 = lean_ctor_get(x_1, 0);
@ -6895,6 +6827,16 @@ x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_instance___elambda__1___closed__2;
x_2 = l_Lean_Parser_Command_instance___closed__4;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance___closed__6() {
_start:
{
@ -6908,46 +6850,16 @@ return x_3;
static lean_object* _init_l_Lean_Parser_Command_instance___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_instance___closed__4;
x_2 = l_Lean_Parser_Command_instance___closed__6;
x_3 = l_Lean_Parser_orelseInfo(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_instance___elambda__1___closed__2;
x_2 = l_Lean_Parser_Command_instance___closed__7;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Command_instance___closed__8;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_instance___elambda__1___closed__4;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Command_instance___closed__9;
x_3 = l_Lean_Parser_Command_instance___closed__6;
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance___closed__11() {
static lean_object* _init_l_Lean_Parser_Command_instance___closed__8() {
_start:
{
lean_object* x_1;
@ -6955,12 +6867,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Command_instance___elambda__1), 2
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance___closed__12() {
static lean_object* _init_l_Lean_Parser_Command_instance___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_instance___closed__10;
x_2 = l_Lean_Parser_Command_instance___closed__11;
x_1 = l_Lean_Parser_Command_instance___closed__7;
x_2 = l_Lean_Parser_Command_instance___closed__8;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -6971,7 +6883,7 @@ static lean_object* _init_l_Lean_Parser_Command_instance() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Command_instance___closed__12;
x_1 = l_Lean_Parser_Command_instance___closed__9;
return x_1;
}
}
@ -11170,7 +11082,7 @@ static lean_object* _init_l_Lean_Parser_Command_declaration___elambda__1___close
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_instance___closed__11;
x_1 = l_Lean_Parser_Command_instance___closed__8;
x_2 = l_Lean_Parser_Command_declaration___elambda__1___closed__7;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_orelseFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
@ -12912,26 +12824,6 @@ return x_3;
static lean_object* _init_l_Lean_Parser_Command_instance_formatter___closed__6() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_checkOutsideQuot_formatter___boxed), 4, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance_formatter___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_instance_formatter___closed__6;
x_2 = l_Lean_Parser_Command_instance_formatter___closed__5;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance_formatter___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_attrInstance_formatter___closed__7;
x_2 = l_Lean_Parser_Command_instance_formatter___closed__5;
@ -12941,45 +12833,13 @@ lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance_formatter___closed__9() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_checkInsideQuot_formatter___boxed), 4, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance_formatter___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_instance_formatter___closed__9;
x_2 = l_Lean_Parser_Command_instance_formatter___closed__8;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance_formatter___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_instance_formatter___closed__7;
x_2 = l_Lean_Parser_Command_instance_formatter___closed__10;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_orelse_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance_formatter___closed__12() {
static lean_object* _init_l_Lean_Parser_Command_instance_formatter___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_instance___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Command_instance_formatter___closed__11;
x_3 = l_Lean_Parser_Command_instance_formatter___closed__6;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -12992,7 +12852,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Command_instance_formatter___closed__1;
x_7 = l_Lean_Parser_Command_instance_formatter___closed__12;
x_7 = l_Lean_Parser_Command_instance_formatter___closed__7;
x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -16177,26 +16037,6 @@ return x_3;
static lean_object* _init_l_Lean_Parser_Command_instance_parenthesizer___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___boxed), 4, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance_parenthesizer___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_instance_parenthesizer___closed__5;
x_2 = l_Lean_Parser_Command_instance_parenthesizer___closed__4;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance_parenthesizer___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_attrInstance_parenthesizer___closed__7;
x_2 = l_Lean_Parser_Command_instance_parenthesizer___closed__4;
@ -16206,45 +16046,13 @@ lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance_parenthesizer___closed__8() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___boxed), 4, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance_parenthesizer___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_instance_parenthesizer___closed__8;
x_2 = l_Lean_Parser_Command_instance_parenthesizer___closed__7;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance_parenthesizer___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_instance_parenthesizer___closed__6;
x_2 = l_Lean_Parser_Command_instance_parenthesizer___closed__9;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_instance_parenthesizer___closed__11() {
static lean_object* _init_l_Lean_Parser_Command_instance_parenthesizer___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_instance___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Command_instance_parenthesizer___closed__10;
x_3 = l_Lean_Parser_Command_instance_parenthesizer___closed__5;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -16257,7 +16065,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Command_instance_parenthesizer___closed__1;
x_7 = l_Lean_Parser_Command_instance_parenthesizer___closed__11;
x_7 = l_Lean_Parser_Command_instance_parenthesizer___closed__6;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -29885,12 +29693,6 @@ l_Lean_Parser_Command_instance___elambda__1___closed__12 = _init_l_Lean_Parser_C
lean_mark_persistent(l_Lean_Parser_Command_instance___elambda__1___closed__12);
l_Lean_Parser_Command_instance___elambda__1___closed__13 = _init_l_Lean_Parser_Command_instance___elambda__1___closed__13();
lean_mark_persistent(l_Lean_Parser_Command_instance___elambda__1___closed__13);
l_Lean_Parser_Command_instance___elambda__1___closed__14 = _init_l_Lean_Parser_Command_instance___elambda__1___closed__14();
lean_mark_persistent(l_Lean_Parser_Command_instance___elambda__1___closed__14);
l_Lean_Parser_Command_instance___elambda__1___closed__15 = _init_l_Lean_Parser_Command_instance___elambda__1___closed__15();
lean_mark_persistent(l_Lean_Parser_Command_instance___elambda__1___closed__15);
l_Lean_Parser_Command_instance___elambda__1___closed__16 = _init_l_Lean_Parser_Command_instance___elambda__1___closed__16();
lean_mark_persistent(l_Lean_Parser_Command_instance___elambda__1___closed__16);
l_Lean_Parser_Command_instance___closed__1 = _init_l_Lean_Parser_Command_instance___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_instance___closed__1);
l_Lean_Parser_Command_instance___closed__2 = _init_l_Lean_Parser_Command_instance___closed__2();
@ -29909,12 +29711,6 @@ l_Lean_Parser_Command_instance___closed__8 = _init_l_Lean_Parser_Command_instanc
lean_mark_persistent(l_Lean_Parser_Command_instance___closed__8);
l_Lean_Parser_Command_instance___closed__9 = _init_l_Lean_Parser_Command_instance___closed__9();
lean_mark_persistent(l_Lean_Parser_Command_instance___closed__9);
l_Lean_Parser_Command_instance___closed__10 = _init_l_Lean_Parser_Command_instance___closed__10();
lean_mark_persistent(l_Lean_Parser_Command_instance___closed__10);
l_Lean_Parser_Command_instance___closed__11 = _init_l_Lean_Parser_Command_instance___closed__11();
lean_mark_persistent(l_Lean_Parser_Command_instance___closed__11);
l_Lean_Parser_Command_instance___closed__12 = _init_l_Lean_Parser_Command_instance___closed__12();
lean_mark_persistent(l_Lean_Parser_Command_instance___closed__12);
l_Lean_Parser_Command_instance = _init_l_Lean_Parser_Command_instance();
lean_mark_persistent(l_Lean_Parser_Command_instance);
l_Lean_Parser_Command_axiom___elambda__1___closed__1 = _init_l_Lean_Parser_Command_axiom___elambda__1___closed__1();
@ -30926,16 +30722,6 @@ l_Lean_Parser_Command_instance_formatter___closed__6 = _init_l_Lean_Parser_Comma
lean_mark_persistent(l_Lean_Parser_Command_instance_formatter___closed__6);
l_Lean_Parser_Command_instance_formatter___closed__7 = _init_l_Lean_Parser_Command_instance_formatter___closed__7();
lean_mark_persistent(l_Lean_Parser_Command_instance_formatter___closed__7);
l_Lean_Parser_Command_instance_formatter___closed__8 = _init_l_Lean_Parser_Command_instance_formatter___closed__8();
lean_mark_persistent(l_Lean_Parser_Command_instance_formatter___closed__8);
l_Lean_Parser_Command_instance_formatter___closed__9 = _init_l_Lean_Parser_Command_instance_formatter___closed__9();
lean_mark_persistent(l_Lean_Parser_Command_instance_formatter___closed__9);
l_Lean_Parser_Command_instance_formatter___closed__10 = _init_l_Lean_Parser_Command_instance_formatter___closed__10();
lean_mark_persistent(l_Lean_Parser_Command_instance_formatter___closed__10);
l_Lean_Parser_Command_instance_formatter___closed__11 = _init_l_Lean_Parser_Command_instance_formatter___closed__11();
lean_mark_persistent(l_Lean_Parser_Command_instance_formatter___closed__11);
l_Lean_Parser_Command_instance_formatter___closed__12 = _init_l_Lean_Parser_Command_instance_formatter___closed__12();
lean_mark_persistent(l_Lean_Parser_Command_instance_formatter___closed__12);
l_Lean_Parser_Command_axiom_formatter___closed__1 = _init_l_Lean_Parser_Command_axiom_formatter___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_axiom_formatter___closed__1);
l_Lean_Parser_Command_axiom_formatter___closed__2 = _init_l_Lean_Parser_Command_axiom_formatter___closed__2();
@ -31425,16 +31211,6 @@ l_Lean_Parser_Command_instance_parenthesizer___closed__5 = _init_l_Lean_Parser_C
lean_mark_persistent(l_Lean_Parser_Command_instance_parenthesizer___closed__5);
l_Lean_Parser_Command_instance_parenthesizer___closed__6 = _init_l_Lean_Parser_Command_instance_parenthesizer___closed__6();
lean_mark_persistent(l_Lean_Parser_Command_instance_parenthesizer___closed__6);
l_Lean_Parser_Command_instance_parenthesizer___closed__7 = _init_l_Lean_Parser_Command_instance_parenthesizer___closed__7();
lean_mark_persistent(l_Lean_Parser_Command_instance_parenthesizer___closed__7);
l_Lean_Parser_Command_instance_parenthesizer___closed__8 = _init_l_Lean_Parser_Command_instance_parenthesizer___closed__8();
lean_mark_persistent(l_Lean_Parser_Command_instance_parenthesizer___closed__8);
l_Lean_Parser_Command_instance_parenthesizer___closed__9 = _init_l_Lean_Parser_Command_instance_parenthesizer___closed__9();
lean_mark_persistent(l_Lean_Parser_Command_instance_parenthesizer___closed__9);
l_Lean_Parser_Command_instance_parenthesizer___closed__10 = _init_l_Lean_Parser_Command_instance_parenthesizer___closed__10();
lean_mark_persistent(l_Lean_Parser_Command_instance_parenthesizer___closed__10);
l_Lean_Parser_Command_instance_parenthesizer___closed__11 = _init_l_Lean_Parser_Command_instance_parenthesizer___closed__11();
lean_mark_persistent(l_Lean_Parser_Command_instance_parenthesizer___closed__11);
l_Lean_Parser_Command_axiom_parenthesizer___closed__1 = _init_l_Lean_Parser_Command_axiom_parenthesizer___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_axiom_parenthesizer___closed__1);
l_Lean_Parser_Command_axiom_parenthesizer___closed__2 = _init_l_Lean_Parser_Command_axiom_parenthesizer___closed__2();