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 2022-01-20 17:11:09 -08:00
parent b0083e0dd0
commit 893b816f82
18 changed files with 1534 additions and 4316 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
stage0/src/Init/Coe.lean generated
View file

@ -97,21 +97,11 @@ instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α wh
/- Coe bridge -/
-- TODO: delete
@[inline] def liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do
let a ← liftM x
pure (CoeT.coe a)
-- Helper definition used by the elaborator. It is not meant to be used directly by users
@[inline] def Lean.Internal.liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do
let a ← liftM x
pure (CoeT.coe a)
-- TODO: delete
@[inline] def coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do
let a ← x
pure <| CoeT.coe a
-- Helper definition used by the elaborator. It is not meant to be used directly by users
@[inline] def Lean.Internal.coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do
let a ← x

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

@ -7,6 +7,7 @@ import Std.ShareCommon
import Lean.Parser.Command
import Lean.Util.CollectLevelParams
import Lean.Util.FoldConsts
import Lean.Meta.ForEachExpr
import Lean.Meta.CollectFVars
import Lean.Elab.Command
import Lean.Elab.SyntheticMVars
@ -68,63 +69,57 @@ def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView :=
{ ref := stx, kind := DefKind.theorem, modifiers,
declId := stx[1], binders, type? := some type, value := stx[3] }
namespace MkInstanceName
-- Table for `mkInstanceName`
private def kindReplacements : NameMap String :=
Std.RBMap.ofList [
(``Parser.Term.depArrow, "DepArrow"),
(``Parser.Term.«forall», "Forall"),
(``Parser.Term.arrow, "Arrow"),
(``Parser.Term.prop, "Prop"),
(``Parser.Term.sort, "Sort"),
(``Parser.Term.type, "Type")
]
abbrev M := StateRefT String CommandElabM
def isFirst : M Bool :=
return (← get) == ""
def append (str : String) : M Unit :=
modify fun s => s ++ str
partial def collect (stx : Syntax) : M Unit := do
match stx with
| Syntax.node _ k args =>
unless (← isFirst) do
match kindReplacements.find? k with
| some r => append r
| none => pure ()
for arg in args do
collect arg
| Syntax.ident (preresolved := preresolved) .. =>
unless preresolved.isEmpty && (← resolveGlobalName stx.getId).isEmpty do
match stx.getId.eraseMacroScopes with
| Name.str _ str _ =>
if str[0].isLower then
append str.capitalize
else
append str
| _ => pure ()
| _ => pure ()
def mkFreshInstanceName : CommandElabM Name := do
let s ← get
let idx := s.nextInstIdx
modify fun s => { s with nextInstIdx := s.nextInstIdx + 1 }
return Lean.Elab.mkFreshInstanceName s.env idx
partial def main (type : Syntax) : CommandElabM Name := do
/- We use `expandMacros` to expand notation such as `x < y` into `LT.lt x y` -/
let type ← liftMacroM <| expandMacros type
let (_, str) ← collect type |>.run ""
if str.isEmpty then
/--
Generate a name for an instance with the given type.
Note that we elaborate the type twice. Once for producing the name, and another when elaborating the declaration. -/
def mkInstanceName (binders : Array Syntax) (type : Syntax) : CommandElabM Name := do
let savedState ← get
try
let result ← runTermElabM `inst fun _ => Term.withAutoBoundImplicit <| Term.elabBinders binders fun _ => Term.withoutErrToSorry do
let type ← instantiateMVars (← Term.elabType type)
let ref ← IO.mkRef ""
Meta.forEachExpr type fun e => do
if e.isForall then ref.modify (. ++ "ForAll")
else if e.isProp then ref.modify (. ++ "Prop")
else if e.isType then ref.modify (. ++ "Type")
else if e.isSort then ref.modify (. ++ "Sort")
else if e.isConst then
match e.constName!.eraseMacroScopes with
| Name.str _ str _ =>
if str[0].isLower then
ref.modify (. ++ str.capitalize)
else
ref.modify (. ++ str)
| _ => pure ()
ref.get
set savedState
liftMacroM <| mkUnusedBaseName <| Name.mkSimple ("inst" ++ result)
catch ex =>
set savedState
mkFreshInstanceName
else
liftMacroM <| mkUnusedBaseName <| Name.mkSimple ("inst" ++ str)
end MkInstanceName
def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
-- leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal
let attrKind ← liftMacroM <| toAttributeKind stx[0]
let prio ← liftMacroM <| expandOptNamedPrio stx[2]
let attrStx ← `(attr| instance $(quote prio):numLit)
let (binders, type) := expandDeclSig stx[4]
let modifiers := modifiers.addAttribute { kind := attrKind, name := `instance, stx := attrStx }
let declId ← match stx[3].getOptional? with
| some declId => pure declId
| none =>
let id ← mkInstanceName binders.getArgs type
pure <| mkNode ``Parser.Command.declId #[mkIdentFrom stx id, mkNullNode]
return {
ref := stx, kind := DefKind.def, modifiers := modifiers,
declId := declId, binders := binders, type? := type, value := stx[5]
}
def mkDefViewOfConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
-- leading_parser "constant " >> declId >> declSig >> optional declValSimple
@ -139,23 +134,6 @@ def mkDefViewOfConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
declId := stx[1], binders := binders, type? := some type, value := val
}
def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
-- leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal
let attrKind ← liftMacroM <| toAttributeKind stx[0]
let prio ← liftMacroM <| expandOptNamedPrio stx[2]
let attrStx ← `(attr| instance $(quote prio):numLit)
let (binders, type) := expandDeclSig stx[4]
let modifiers := modifiers.addAttribute { kind := attrKind, name := `instance, stx := attrStx }
let declId ← match stx[3].getOptional? with
| some declId => pure declId
| none =>
let id ← MkInstanceName.main type
pure <| mkNode ``Parser.Command.declId #[mkIdentFrom stx id, mkNullNode]
return {
ref := stx, kind := DefKind.def, modifiers := modifiers,
declId := declId, binders := binders, type? := type, value := stx[5]
}
def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=
-- leading_parser "example " >> declSig >> declVal
let (binders, type) := expandDeclSig stx[1]

4
stage0/src/Lean/Expr.lean generated
View file

@ -446,6 +446,10 @@ def isSort : Expr → Bool
| sort _ _ => true
| _ => false
def isType : Expr → Bool
| sort (Level.succ ..) _ => true
| _ => false
def isProp : Expr → Bool
| sort (Level.zero ..) _ => true
| _ => false

55
stage0/stdlib/Init/Coe.c generated
View file

@ -35,6 +35,7 @@ LEAN_EXPORT lean_object* l_coeOfTail(lean_object*, lean_object*);
static lean_object* l_coeNotation___closed__5;
LEAN_EXPORT lean_object* l_coeOfHeadOfTC___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_coeNotation___closed__8;
LEAN_EXPORT lean_object* l_Lean_Internal_liftCoeM___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_decPropToBool___rarg___boxed(lean_object*);
static lean_object* l_coeNotation___closed__4;
LEAN_EXPORT lean_object* l_instCoeDep(lean_object*, lean_object*);
@ -42,7 +43,6 @@ LEAN_EXPORT lean_object* l_coeNotation;
LEAN_EXPORT lean_object* l_coeSortToCoeTail___rarg___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Internal_liftCoeM(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_coeNotation___closed__3;
LEAN_EXPORT lean_object* l_liftCoeM___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Internal_coeM___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_coeOfHTCT(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_boolToSort;
@ -55,7 +55,6 @@ LEAN_EXPORT lean_object* l_coeOfHead(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_optionCoe___rarg(lean_object*);
LEAN_EXPORT lean_object* l_coeOfDep___rarg(lean_object*);
LEAN_EXPORT lean_object* l_coeOfTC(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_liftCoeM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_coeOfTail___rarg(lean_object*, lean_object*);
static lean_object* l_coeNotation___closed__7;
LEAN_EXPORT lean_object* l_instCoeTail__1(lean_object*, lean_object*);
@ -63,13 +62,10 @@ LEAN_EXPORT lean_object* l_coeOfDep___boxed(lean_object*, lean_object*, lean_obj
static lean_object* l_coeNotation___closed__11;
LEAN_EXPORT lean_object* l_coeTrans___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_optionCoe(lean_object*);
LEAN_EXPORT lean_object* l_coeM(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_coeId(lean_object*);
LEAN_EXPORT lean_object* l_subtypeCoe___rarg(lean_object*);
LEAN_EXPORT lean_object* l_subtypeCoe(lean_object*, lean_object*);
static lean_object* l_coeNotation___closed__6;
LEAN_EXPORT lean_object* l_coeM___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_liftCoeM(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_coeOfHeafOfTCOfTail___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_boolToProp;
LEAN_EXPORT lean_object* l_coeId___rarg(lean_object*);
@ -507,7 +503,7 @@ lean_dec(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_liftCoeM___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
LEAN_EXPORT lean_object* l_Lean_Internal_liftCoeM___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
@ -522,28 +518,6 @@ x_7 = lean_apply_2(x_5, lean_box(0), x_6);
return x_7;
}
}
LEAN_EXPORT lean_object* l_liftCoeM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_5 = lean_ctor_get(x_3, 1);
lean_inc(x_5);
x_6 = lean_apply_2(x_1, lean_box(0), x_4);
x_7 = lean_alloc_closure((void*)(l_liftCoeM___rarg___lambda__1), 3, 2);
lean_closure_set(x_7, 0, x_3);
lean_closure_set(x_7, 1, x_2);
x_8 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_6, x_7);
return x_8;
}
}
LEAN_EXPORT lean_object* l_liftCoeM(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_alloc_closure((void*)(l_liftCoeM___rarg), 4, 0);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Lean_Internal_liftCoeM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -551,7 +525,7 @@ lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_5 = lean_ctor_get(x_3, 1);
lean_inc(x_5);
x_6 = lean_apply_2(x_1, lean_box(0), x_4);
x_7 = lean_alloc_closure((void*)(l_liftCoeM___rarg___lambda__1), 3, 2);
x_7 = lean_alloc_closure((void*)(l_Lean_Internal_liftCoeM___rarg___lambda__1), 3, 2);
lean_closure_set(x_7, 0, x_3);
lean_closure_set(x_7, 1, x_2);
x_8 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_6, x_7);
@ -566,34 +540,13 @@ x_5 = lean_alloc_closure((void*)(l_Lean_Internal_liftCoeM___rarg), 4, 0);
return x_5;
}
}
LEAN_EXPORT lean_object* l_coeM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
x_5 = lean_alloc_closure((void*)(l_liftCoeM___rarg___lambda__1), 3, 2);
lean_closure_set(x_5, 0, x_2);
lean_closure_set(x_5, 1, x_1);
x_6 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_3, x_5);
return x_6;
}
}
LEAN_EXPORT lean_object* l_coeM(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_coeM___rarg), 3, 0);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Internal_coeM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
x_5 = lean_alloc_closure((void*)(l_liftCoeM___rarg___lambda__1), 3, 2);
x_5 = lean_alloc_closure((void*)(l_Lean_Internal_liftCoeM___rarg___lambda__1), 3, 2);
lean_closure_set(x_5, 0, x_2);
lean_closure_set(x_5, 1, x_1);
x_6 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_3, x_5);

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

@ -267,6 +267,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_
static lean_object* l_Lean_Elab_Command_elabMutual___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Command_elabDeclaration_declRange___closed__3;
static lean_object* l___regBuiltin_Lean_Elab_Command_elabAttr___closed__4;
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfInstance___spec__9(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_expandInitCmd___lambda__1___closed__17;
static lean_object* l_Lean_Elab_Command_elabAttr___closed__1;
size_t lean_usize_of_nat(lean_object*);
@ -488,7 +489,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Command_expandInitCmd___boxed(lean_object*,
static lean_object* l_Lean_Elab_Command_expandInitCmd___lambda__1___closed__37;
static lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__3___lambda__2___closed__2;
static lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__25;
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfConstant___spec__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_expandInitCmd___closed__5;
static lean_object* l_Lean_Elab_Command_checkValidCtorModifier___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___lambda__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_Command_expandBuiltinInitialize(lean_object*, lean_object*, lean_object*);
@ -4817,7 +4817,7 @@ lean_inc(x_39);
lean_dec(x_37);
lean_inc(x_1);
x_40 = l_Lean_mkIdentFrom(x_1, x_38);
x_41 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfConstant___spec__1(x_2, x_3, x_4);
x_41 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfInstance___spec__9(x_2, x_3, x_4);
x_42 = lean_ctor_get(x_41, 0);
lean_inc(x_42);
x_43 = lean_ctor_get(x_41, 1);

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

File diff suppressed because it is too large Load diff

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

@ -19,6 +19,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_derivingHandlersRef;
size_t lean_usize_add(size_t, size_t);
lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_defaultHandler___closed__4;
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_mkInstanceName___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_stringToMessageData(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_elabDeriving_declRange___closed__3;
LEAN_EXPORT lean_object* l_Lean_Elab_registerBuiltinDerivingHandlerWithArgs___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
@ -136,7 +137,6 @@ static lean_object* l_Lean_Elab_elabDeriving___closed__6;
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_elabDeriving___spec__15(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ResolveName_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_MkInstanceName_main___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_elabDeriving___spec__18___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_mkConstWithLevelParams___at_Lean_Elab_elabDeriving___spec__13___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_elabDeriving___spec__19(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1324,7 +1324,7 @@ x_24 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_24, 0, x_23);
x_25 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_25, 0, x_24);
x_26 = l_Lean_throwErrorAt___at_Lean_Elab_Command_MkInstanceName_main___spec__2(x_1, x_25, x_2, x_3, x_7);
x_26 = l_Lean_throwErrorAt___at_Lean_Elab_Command_mkInstanceName___spec__2(x_1, x_25, x_2, x_3, x_7);
return x_26;
}
else
@ -1395,7 +1395,7 @@ x_51 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_51, 0, x_50);
x_52 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_52, 0, x_51);
x_53 = l_Lean_throwErrorAt___at_Lean_Elab_Command_MkInstanceName_main___spec__2(x_1, x_52, x_2, x_3, x_34);
x_53 = l_Lean_throwErrorAt___at_Lean_Elab_Command_mkInstanceName___spec__2(x_1, x_52, x_2, x_3, x_34);
return x_53;
}
}

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

@ -243,6 +243,7 @@ lean_object* l_Lean_Elab_Deriving_mkHeader___rarg(lean_object*, lean_object*, le
static lean_object* l_Lean_Elab_Deriving_DecEq_mkAuxFunction___closed__10;
static lean_object* l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__11;
static lean_object* l_Lean_Elab_Deriving_DecEq_mkDecEqCmds___closed__10;
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfInstance___spec__9(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Deriving_mkContext(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
static lean_object* l_Lean_Elab_Deriving_DecEq_mkMatch_mkSameCtorRhs___lambda__1___closed__48;
@ -411,7 +412,6 @@ static lean_object* l_Lean_Elab_Deriving_DecEq_mkDecEqCmds___closed__4;
static lean_object* l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__1;
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Deriving_DecEq_mkMatch_mkAlts___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Deriving_DecEq_mkMatch_mkSameCtorRhs___lambda__1___closed__64;
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfConstant___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Deriving_mkInductiveApp___spec__2___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_List_forIn_loop___at_Lean_Elab_Deriving_DecEq_mkMatch_mkAlts___spec__6___closed__5;
static lean_object* l_Lean_Elab_Deriving_DecEq_mkMatch_mkSameCtorRhs___lambda__1___closed__34;
@ -8484,7 +8484,7 @@ lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean
x_19 = lean_ctor_get(x_18, 1);
lean_inc(x_19);
lean_dec(x_18);
x_20 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfConstant___spec__1(x_2, x_3, x_19);
x_20 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfInstance___spec__9(x_2, x_3, x_19);
x_21 = lean_ctor_get(x_20, 0);
lean_inc(x_21);
x_22 = lean_ctor_get(x_20, 1);

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

@ -28,6 +28,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_isMul
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereStructInst___spec__3(lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* lean_erase_macro_scopes(lean_object*);
lean_object* l_Lean_CollectMVars_visit(lean_object*, lean_object*);
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_mkInstanceName___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withLCtx___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunBinderViews___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_stringToMessageData(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_check(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -437,7 +438,6 @@ lean_object* l_Lean_replaceFVarIdAtLocalDecl(lean_object*, lean_object*, lean_ob
uint8_t l_Lean_Elab_DefKind_isTheorem(uint8_t);
static lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_isMultiConstant_x3f___spec__3___closed__6;
static lean_object* l_Lean_Elab_elabAttr___at_Lean_Elab_Command_elabMutualDef___spec__4___closed__6;
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_MkInstanceName_main___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MetavarContext_getDelayedRoot(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_getMax_x3f___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_pickMaxFVar_x3f___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_isExample___spec__1___boxed(lean_object*, lean_object*, lean_object*);
@ -26831,7 +26831,7 @@ lean_object* x_25; lean_object* x_26; uint8_t x_27;
lean_dec(x_17);
lean_dec(x_9);
x_25 = l_Lean_Elab_elabAttr___at_Lean_Elab_Command_elabMutualDef___spec__4___closed__6;
x_26 = l_Lean_throwErrorAt___at_Lean_Elab_Command_MkInstanceName_main___spec__2(x_15, x_25, x_2, x_3, x_16);
x_26 = l_Lean_throwErrorAt___at_Lean_Elab_Command_mkInstanceName___spec__2(x_15, x_25, x_2, x_3, x_16);
x_27 = !lean_is_exclusive(x_26);
if (x_27 == 0)
{

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

@ -479,6 +479,7 @@ uint8_t l_Lean_Expr_isForall(lean_object*);
uint8_t l_Lean_BinderInfo_isInstImplicit(uint8_t);
lean_object* lean_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__4___closed__6;
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfInstance___spec__9(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults___spec__2___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -853,7 +854,6 @@ lean_object* l_panic___at_Lean_ResolveName_resolveNamespaceUsingScope___spec__1(
lean_object* l_Lean_Meta_instInhabitedMetaM___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabFieldTypeValue___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_elabStructure___lambda__3___boxed(lean_object**);
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfConstant___spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_elabModifiers___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___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*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__5___lambda__2___closed__4;
LEAN_EXPORT lean_object* l_Lean_Elab_elabAttrs___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -28103,7 +28103,7 @@ else
{
lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59;
lean_dec(x_22);
x_35 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfConstant___spec__1(x_3, x_4, x_30);
x_35 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfInstance___spec__9(x_3, x_4, x_30);
x_36 = lean_ctor_get(x_35, 0);
lean_inc(x_36);
x_37 = lean_ctor_get(x_35, 1);

90
stage0/stdlib/Lean/Expr.c generated
View file

@ -397,6 +397,7 @@ LEAN_EXPORT lean_object* l_Lean_mkAppRange___boxed(lean_object*, lean_object*, l
LEAN_EXPORT uint8_t l_Lean_Expr_approxDepth(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Expr_setAppPPExplicitForExposingMVars(lean_object*);
static lean_object* l_Lean_Expr_fvarId_x21___closed__1;
LEAN_EXPORT lean_object* l_Lean_Expr_isType___boxed(lean_object*);
static lean_object* l_Lean_Expr_updateConst_x21___closed__2;
LEAN_EXPORT lean_object* lean_expr_mk_bvar(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Expr_instHashableExpr;
@ -541,6 +542,7 @@ static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Exp
LEAN_EXPORT lean_object* l_Lean_instInhabitedFVarId;
static lean_object* l_Lean_Expr_updateProj_x21___closed__1;
static lean_object* l___private_Lean_Expr_0__Lean_reprExpr____x40_Lean_Expr___hyg_2203____closed__30;
LEAN_EXPORT uint8_t l_Lean_Expr_isType(lean_object*);
lean_object* lean_level_update_imax(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_mkNatLit___closed__3;
static lean_object* l___private_Lean_Expr_0__Lean_reprExpr____x40_Lean_Expr___hyg_2203____closed__18;
@ -9604,6 +9606,44 @@ x_3 = lean_box(x_2);
return x_3;
}
}
LEAN_EXPORT uint8_t l_Lean_Expr_isType(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 3)
{
lean_object* x_2;
x_2 = lean_ctor_get(x_1, 0);
if (lean_obj_tag(x_2) == 1)
{
uint8_t x_3;
x_3 = 1;
return x_3;
}
else
{
uint8_t x_4;
x_4 = 0;
return x_4;
}
}
else
{
uint8_t x_5;
x_5 = 0;
return x_5;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Expr_isType___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Expr_isType(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
LEAN_EXPORT uint8_t l_Lean_Expr_isProp(lean_object* x_1) {
_start:
{
@ -10379,7 +10419,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_getRevArg_x21___closed__1;
x_3 = lean_unsigned_to_nat(561u);
x_3 = lean_unsigned_to_nat(565u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Expr_getRevArg_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -10600,7 +10640,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_appFn_x21___closed__1;
x_3 = lean_unsigned_to_nat(581u);
x_3 = lean_unsigned_to_nat(585u);
x_4 = lean_unsigned_to_nat(17u);
x_5 = l_Lean_Expr_appFn_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -10649,7 +10689,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_appArg_x21___closed__1;
x_3 = lean_unsigned_to_nat(585u);
x_3 = lean_unsigned_to_nat(589u);
x_4 = lean_unsigned_to_nat(17u);
x_5 = l_Lean_Expr_appFn_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -10883,7 +10923,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_constName_x21___closed__1;
x_3 = lean_unsigned_to_nat(604u);
x_3 = lean_unsigned_to_nat(608u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_constName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -10970,7 +11010,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_constLevels_x21___closed__1;
x_3 = lean_unsigned_to_nat(612u);
x_3 = lean_unsigned_to_nat(616u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_constName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11020,7 +11060,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_bvarIdx_x21___closed__1;
x_3 = lean_unsigned_to_nat(616u);
x_3 = lean_unsigned_to_nat(620u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l_Lean_Expr_bvarIdx_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11086,7 +11126,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_fvarId_x21___closed__1;
x_3 = lean_unsigned_to_nat(620u);
x_3 = lean_unsigned_to_nat(624u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_Expr_fvarId_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11136,7 +11176,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_mvarId_x21___closed__1;
x_3 = lean_unsigned_to_nat(624u);
x_3 = lean_unsigned_to_nat(628u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_Expr_mvarId_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11193,7 +11233,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_bindingName_x21___closed__1;
x_3 = lean_unsigned_to_nat(629u);
x_3 = lean_unsigned_to_nat(633u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_bindingName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11251,7 +11291,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_bindingDomain_x21___closed__1;
x_3 = lean_unsigned_to_nat(634u);
x_3 = lean_unsigned_to_nat(638u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_bindingName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11309,7 +11349,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_bindingBody_x21___closed__1;
x_3 = lean_unsigned_to_nat(639u);
x_3 = lean_unsigned_to_nat(643u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_bindingName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11377,7 +11417,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_bindingInfo_x21___closed__1;
x_3 = lean_unsigned_to_nat(644u);
x_3 = lean_unsigned_to_nat(648u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_bindingName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11439,7 +11479,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_letName_x21___closed__1;
x_3 = lean_unsigned_to_nat(648u);
x_3 = lean_unsigned_to_nat(652u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Expr_letName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11522,7 +11562,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_mdataExpr_x21___closed__1;
x_3 = lean_unsigned_to_nat(656u);
x_3 = lean_unsigned_to_nat(660u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_mdataExpr_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11579,7 +11619,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_projExpr_x21___closed__1;
x_3 = lean_unsigned_to_nat(660u);
x_3 = lean_unsigned_to_nat(664u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_projExpr_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -13276,7 +13316,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_updateApp_x21___closed__1;
x_3 = lean_unsigned_to_nat(937u);
x_3 = lean_unsigned_to_nat(941u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_appFn_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -13347,7 +13387,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_updateConst_x21___closed__1;
x_3 = lean_unsigned_to_nat(946u);
x_3 = lean_unsigned_to_nat(950u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_constName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -13425,7 +13465,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_updateSort_x21___closed__1;
x_3 = lean_unsigned_to_nat(955u);
x_3 = lean_unsigned_to_nat(959u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_Expr_updateSort_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -13508,7 +13548,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_updateMData_x21___closed__1;
x_3 = lean_unsigned_to_nat(972u);
x_3 = lean_unsigned_to_nat(976u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_updateMData_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -13578,7 +13618,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_updateProj_x21___closed__1;
x_3 = lean_unsigned_to_nat(977u);
x_3 = lean_unsigned_to_nat(981u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_updateProj_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -13661,7 +13701,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_updateForall_x21___closed__1;
x_3 = lean_unsigned_to_nat(986u);
x_3 = lean_unsigned_to_nat(990u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_updateForall_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -13737,7 +13777,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_updateForallE_x21___closed__1;
x_3 = lean_unsigned_to_nat(991u);
x_3 = lean_unsigned_to_nat(995u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_updateForall_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -13824,7 +13864,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_updateLambda_x21___closed__1;
x_3 = lean_unsigned_to_nat(1000u);
x_3 = lean_unsigned_to_nat(1004u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_updateLambda_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -13900,7 +13940,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_updateLambdaE_x21___closed__1;
x_3 = lean_unsigned_to_nat(1005u);
x_3 = lean_unsigned_to_nat(1009u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_updateLambda_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -13977,7 +14017,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_mkData___closed__2;
x_2 = l_Lean_Expr_updateLet_x21___closed__1;
x_3 = lean_unsigned_to_nat(1014u);
x_3 = lean_unsigned_to_nat(1018u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Expr_letName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

12
stage0/stdlib/Lean/Meta/Closure.c generated
View file

@ -3930,7 +3930,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__2;
x_3 = lean_unsigned_to_nat(972u);
x_3 = lean_unsigned_to_nat(976u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -3959,7 +3959,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__5;
x_3 = lean_unsigned_to_nat(977u);
x_3 = lean_unsigned_to_nat(981u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__6;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -3988,7 +3988,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__8;
x_3 = lean_unsigned_to_nat(937u);
x_3 = lean_unsigned_to_nat(941u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__9;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -4017,7 +4017,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__11;
x_3 = lean_unsigned_to_nat(1005u);
x_3 = lean_unsigned_to_nat(1009u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__12;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -4046,7 +4046,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__14;
x_3 = lean_unsigned_to_nat(991u);
x_3 = lean_unsigned_to_nat(995u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__15;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -4075,7 +4075,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__17;
x_3 = lean_unsigned_to_nat(1014u);
x_3 = lean_unsigned_to_nat(1018u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__18;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

10
stage0/stdlib/Lean/Meta/ExprDefEq.c generated
View file

@ -15577,7 +15577,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_CheckAssignment_check___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_check___closed__2;
x_3 = lean_unsigned_to_nat(972u);
x_3 = lean_unsigned_to_nat(976u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Meta_CheckAssignment_check___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -15606,7 +15606,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_CheckAssignment_check___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_check___closed__5;
x_3 = lean_unsigned_to_nat(977u);
x_3 = lean_unsigned_to_nat(981u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Meta_CheckAssignment_check___closed__6;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -15635,7 +15635,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_CheckAssignment_check___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_check___closed__8;
x_3 = lean_unsigned_to_nat(1005u);
x_3 = lean_unsigned_to_nat(1009u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Meta_CheckAssignment_check___closed__9;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -15664,7 +15664,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_CheckAssignment_check___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_check___closed__11;
x_3 = lean_unsigned_to_nat(991u);
x_3 = lean_unsigned_to_nat(995u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Meta_CheckAssignment_check___closed__12;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -15693,7 +15693,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_CheckAssignment_check___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_check___closed__14;
x_3 = lean_unsigned_to_nat(1014u);
x_3 = lean_unsigned_to_nat(1018u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Meta_CheckAssignment_check___closed__15;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Meta/Tactic/Simp/Main.c generated
View file

@ -21379,7 +21379,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Simp_simp_simpProj___lambda__1___closed__1;
x_2 = l_Lean_Meta_Simp_simp_simpProj___lambda__1___closed__2;
x_3 = lean_unsigned_to_nat(977u);
x_3 = lean_unsigned_to_nat(981u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Meta_Simp_simp_simpProj___lambda__1___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Meta/Tactic/Simp/SimpLemmas.c generated
View file

@ -11950,7 +11950,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_SimpLemma_getValue___closed__1;
x_2 = l_Lean_Meta_SimpLemma_getValue___closed__2;
x_3 = lean_unsigned_to_nat(946u);
x_3 = lean_unsigned_to_nat(950u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Meta_SimpLemma_getValue___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

10
stage0/stdlib/Lean/Meta/Transform.c generated
View file

@ -636,7 +636,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__2;
x_3 = lean_unsigned_to_nat(1005u);
x_3 = lean_unsigned_to_nat(1009u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -742,7 +742,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__4___closed__1;
x_3 = lean_unsigned_to_nat(991u);
x_3 = lean_unsigned_to_nat(995u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__4___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -848,7 +848,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__6___closed__1;
x_3 = lean_unsigned_to_nat(1014u);
x_3 = lean_unsigned_to_nat(1018u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__6___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -985,7 +985,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__9___closed__1;
x_3 = lean_unsigned_to_nat(972u);
x_3 = lean_unsigned_to_nat(976u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__9___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -1058,7 +1058,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__10___closed__1;
x_3 = lean_unsigned_to_nat(977u);
x_3 = lean_unsigned_to_nat(981u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__10___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

14
stage0/stdlib/Lean/MetavarContext.c generated
View file

@ -15609,7 +15609,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__2;
x_3 = lean_unsigned_to_nat(955u);
x_3 = lean_unsigned_to_nat(959u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -15691,7 +15691,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__11___closed__1;
x_3 = lean_unsigned_to_nat(946u);
x_3 = lean_unsigned_to_nat(950u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__11___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -15776,7 +15776,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__12___closed__1;
x_3 = lean_unsigned_to_nat(1005u);
x_3 = lean_unsigned_to_nat(1009u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__12___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -15882,7 +15882,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__14___closed__1;
x_3 = lean_unsigned_to_nat(991u);
x_3 = lean_unsigned_to_nat(995u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__14___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -15988,7 +15988,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__16___closed__1;
x_3 = lean_unsigned_to_nat(1014u);
x_3 = lean_unsigned_to_nat(1018u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__16___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -16121,7 +16121,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__19___closed__1;
x_3 = lean_unsigned_to_nat(972u);
x_3 = lean_unsigned_to_nat(976u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__19___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -16206,7 +16206,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__20___closed__1;
x_3 = lean_unsigned_to_nat(977u);
x_3 = lean_unsigned_to_nat(981u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__20___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

4
stage0/stdlib/Lean/Server/Rpc/Deriving.c generated
View file

@ -285,6 +285,7 @@ static lean_object* l___private_Lean_Server_Rpc_Deriving_0__Lean_Server_RpcEncod
static lean_object* l___private_Lean_Server_Rpc_Deriving_0__Lean_Server_RpcEncoding_deriveInstance___lambda__1___closed__51;
LEAN_EXPORT lean_object* l___private_Lean_Server_Rpc_Deriving_0__Lean_Server_RpcEncoding_deriveInstance___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Server_Rpc_Deriving_0__Lean_Server_RpcEncoding_deriveWithRefInstance___closed__157;
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfInstance___spec__9(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Server_Rpc_Deriving_0__Lean_Server_RpcEncoding_dispatchDeriveInstanceUnsafe___lambda__3___closed__2;
static lean_object* l___private_Lean_Server_Rpc_Deriving_0__Lean_Server_RpcEncoding_deriveInstance___lambda__1___closed__17;
lean_object* l_Lean_Elab_Command_liftCoreM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -480,7 +481,6 @@ lean_object* l_Lean_throwError___at_Lean_Elab_Term_synthesizeInst___spec__1(lean
static lean_object* l___private_Lean_Server_Rpc_Deriving_0__Lean_Server_RpcEncoding_deriveWithRefInstance___closed__194;
LEAN_EXPORT lean_object* l_Lean_Server_RpcEncoding_initFn____x40_Lean_Server_Rpc_Deriving___hyg_4692_(lean_object*);
static lean_object* l___private_Lean_Server_Rpc_Deriving_0__Lean_Server_RpcEncoding_deriveInstance___lambda__1___closed__37;
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfConstant___spec__1(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_isStructure(lean_object*, lean_object*);
static lean_object* l___private_Lean_Server_Rpc_Deriving_0__Lean_Server_RpcEncoding_deriveWithRefInstance___closed__122;
static lean_object* l___private_Lean_Server_Rpc_Deriving_0__Lean_Server_RpcEncoding_deriveWithRefInstance___closed__44;
@ -2952,7 +2952,7 @@ lean_inc(x_6);
lean_dec(x_5);
lean_inc(x_1);
x_7 = lean_mk_syntax_ident(x_1);
x_8 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfConstant___spec__1(x_2, x_3, x_6);
x_8 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfInstance___spec__9(x_2, x_3, x_6);
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
x_10 = lean_ctor_get(x_8, 1);