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-08-04 15:57:45 -07:00
parent 0717bdb66d
commit 7cb67bb123
12 changed files with 992 additions and 825 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
stage0/src/Lean/DocString.lean generated
View file

@ -60,7 +60,13 @@ def addDocString' [Monad m] [MonadEnv m] (declName : Name) (docString? : Option
| none => return ()
def findDocString? (env : Environment) (declName : Name) : IO (Option String) :=
return (← builtinDocStrings.get).find? declName |>.orElse fun _ => docStringExt.find? env declName
/-
`docStringExt` should have precedence over `builtinDocStrings`, otherwise
we would not be able to update the doc strings for builtin elaborators, parsers, macros, ...
-/
match docStringExt.find? env declName with
| some docStr => return some docStr
| none => return (← builtinDocStrings.get).find? declName
structure ModuleDoc where
doc : String

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

@ -922,10 +922,11 @@ inductive LValResolution where
private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α :=
throwError "{msg}{indentExpr e}\nhas type{indentExpr eType}"
/-- `findMethod? env S fName`.
1- If `env` contains `S ++ fName`, return `(S, S++fName)`
2- Otherwise if `env` contains private name `prv` for `S ++ fName`, return `(S, prv)`, o
3- Otherwise for each parent structure `S'` of `S`, we try `findMethod? env S' fname`
/--
`findMethod? env S fName`.
- If `env` contains `S ++ fName`, return `(S, S++fName)`
- Otherwise if `env` contains private name `prv` for `S ++ fName`, return `(S, prv)`, o
- Otherwise for each parent structure `S'` of `S`, we try `findMethod? env S' fname`
-/
private partial def findMethod? (env : Environment) (structName fieldName : Name) : Option (Name × Name) :=
let fullName := structName ++ fieldName

18
stage0/src/Lean/Elab/BuiltinNotation.lean generated
View file

@ -243,13 +243,17 @@ where
/--
Try to expand `·` notation.
Recall that in Lean the `·` notation must be surrounded by parentheses.
We may change this is the future, but right now, here are valid examples
- `(· + 1)`
- `(f ⟨·, 1⟩ ·)`
- `(· + ·)`
- `(f · a b)` -/
You can use parentheses for
- Grouping expressions, e.g., `a * (b + c)`.
- Creating tuples, e.g., `(a, b, c)` is notation for `Prod.mk a (Prod.mk b c)`.
- Performing type ascription, e.g., `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.
- Creating `Unit.unit`, `()` is just a shorthand for `Unit.unit`.
- Creating simple functions when combined with `·`. Here are some examples:
- `(· + 1)` is shorthand for `fun x => x + 1`
- `(· + ·)` is shorthand for `fun x y => x + y`
- `(f · a b)` is shorthand for `fun x => f x a b`
- `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`
-/
@[builtinMacro Lean.Parser.Term.paren] def expandParen : Macro
| `(()) => `(Unit.unit)
| `(($e : $type)) => do

20
stage0/src/Lean/Elab/Do.lean generated
View file

@ -863,12 +863,24 @@ Example: suppose we want to support `repeat doSeq`. Assuming we have `repeat : m
/--
Helper method for annotating `term` with the raw syntax `ref`.
We use this method to implement finer-grained term infos for `do`-blocks.
Note that we attach `term` position to token `with_annotate_term`. We do that
to make sure if a coercion is created for `with_annotate_term ref term`, we
get the position information for `term`.
We use `withRef term` to make sure the synthetic position for the `with_annotate_term` is equal
to the one for `term`. This is important for producing error messages when there is a type mismatch.
Consider the following example:
```
opaque f : IO Nat
def g : IO String := do
f
```
There is at type mismatch at `f`, but it is detected when elaborating the expanded term
containing the `with_annotate_term .. f`. The current `getRef` when this `annotate` is invoked
is not necessarily `f`. Actually, it is the whole `do`-block. By using `withRef` we ensure
the synthetic position for the `with_annotate_term ..` is equal to `term`.
Recall that synthetic positions are used when generating error messages.
-/
def annotate [Monad m] [MonadRef m] [MonadQuotation m] (ref : Syntax) (term : Syntax) : m Syntax :=
`(with_annotate_term%$term $ref $term)
withRef term <| `(with_annotate_term $ref $term)
namespace ToTerm

32
stage0/src/Lean/Meta/ExprDefEq.lean generated
View file

@ -1250,21 +1250,29 @@ private def unfoldReducibeDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : Meta
unfoldDefEq tInfo sInfo t s
/--
If `t` is a projection function application and `s` is not ==> `isDefEqRight t (unfold s)`
If `s` is a projection function application and `t` is not ==> `isDefEqRight (unfold t) s`
This is an auxiliary method for isDefEqDelta.
If `t` is a (non-class) projection function application and `s` is not ==> `isDefEqRight t (unfold s)`
If `s` is a (non-class) projection function application and `t` is not ==> `isDefEqRight (unfold t) s`
Otherwise, use `unfoldReducibeDefEq`
Auxiliary method for isDefEqDelta -/
The motivation for the heuristic above is unification problems such as
```
id (?m.1) =?= (a, b).1
```
We want to reduce the lhs instead of the rhs, and eventually assign `?m := (a, b)`.
For class projections we do the opposite because the `?m` can always be synthesized using
type class resolution. See issue #1419 for an example for motivating this behavior.
-/
private def unfoldNonProjFnDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : MetaM LBool := do
let tProj? ← isProjectionFn tInfo.name
let sProj? ← isProjectionFn sInfo.name
if tProj? && !sProj? then
unfold s (unfoldDefEq tInfo sInfo t s) fun s => isDefEqRight sInfo.name t s
else if !tProj? && sProj? then
unfold t (unfoldDefEq tInfo sInfo t s) fun t => isDefEqLeft tInfo.name t s
else
unfoldReducibeDefEq tInfo sInfo t s
let tProjInfo? ← getProjectionFnInfo? tInfo.name
let sProjInfo? ← getProjectionFnInfo? sInfo.name
match tProjInfo?, sProjInfo? with
| some { fromClass := false, .. }, none | none, some { fromClass := true, ..}
=> unfold s (unfoldDefEq tInfo sInfo t s) fun s => isDefEqRight sInfo.name t s
| some { fromClass := true, .. }, none | none, some { fromClass := false, ..}
=> unfold t (unfoldDefEq tInfo sInfo t s) fun t => isDefEqLeft tInfo.name t s
| _, _ => unfoldReducibeDefEq tInfo sInfo t s
/--
isDefEq by lazy delta reduction.

7
stage0/src/Lean/Server/InfoUtils.lean generated
View file

@ -231,7 +231,12 @@ where
else
let eFmt ← Meta.ppExpr e
-- Try not to show too scary internals
let fmt := if isAtomicFormat eFmt then f!"{eFmt} : {tpFmt}" else f!"{tpFmt}"
let showTerm := if let .fvar id := e then
if let some ldecl := (← getLCtx).findFVar? e then
!ldecl.userName.hasMacroScopes
else false
else isAtomicFormat eFmt
let fmt := if showTerm then f!"{eFmt} : {tpFmt}" else tpFmt
return some f!"```lean
{fmt}
```"

239
stage0/stdlib/Lean/DocString.c generated
View file

@ -16,7 +16,6 @@ extern "C" {
lean_object* lean_string_push(lean_object*, uint32_t);
LEAN_EXPORT lean_object* l___private_Lean_DocString_0__Lean_findLeadingSpacesSize_consumeSpaces___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_addMainModuleDoc(lean_object*, lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__1;
static lean_object* l_Lean_addMainModuleDoc___closed__1;
lean_object* l_Lean_stringToMessageData(lean_object*);
extern lean_object* l_String_instInhabitedString;
@ -26,47 +25,48 @@ lean_object* l_Lean_PersistentEnvExtension_getModuleEntries___rarg(lean_object*,
LEAN_EXPORT lean_object* l_Lean_addDocString_x27___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_getDocStringText___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_DocString_0__Lean_docStringExt;
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__5;
LEAN_EXPORT lean_object* l___private_Lean_DocString_0__Lean_removeNumLeadingSpaces_consumeSpaces(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_DocString_0__Lean_findLeadingSpacesSize_findNextLine(lean_object*, lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_DocString_0__Lean_removeNumLeadingSpaces(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___boxed(lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__1;
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__1;
lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__3;
LEAN_EXPORT lean_object* l_Lean_addDocString___rarg(lean_object*, lean_object*, lean_object*);
uint8_t l_String_Iterator_atEnd(lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__5;
LEAN_EXPORT lean_object* l_Lean_addDocString___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* lean_string_utf8_byte_size(lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__6;
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1(lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_DocString_0__Lean_findLeadingSpacesSize(lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__2;
LEAN_EXPORT lean_object* l_Lean_addDocString(lean_object*);
lean_object* l_Lean_MapDeclarationExtension_find_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_getDocStringText(lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__4;
lean_object* l_Lean_MapDeclarationExtension_insert___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__4;
lean_object* lean_nat_sub(lean_object*, lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__2;
uint8_t l_Lean_Name_quickCmp(lean_object*, lean_object*);
lean_object* l_Lean_mkMapDeclarationExtension___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__6;
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__2;
lean_object* lean_st_mk_ref(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1(lean_object*);
static lean_object* l___private_Lean_DocString_0__Lean_removeNumLeadingSpaces___closed__1;
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_44____closed__2;
LEAN_EXPORT lean_object* l___private_Lean_DocString_0__Lean_removeNumLeadingSpaces_saveLine(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_DocString_0__Lean_findLeadingSpacesSize_consumeSpaces(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_Iterator_find___at___private_Lean_DocString_0__Lean_findLeadingSpacesSize___spec__1(lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__2;
lean_object* l_String_Iterator_next(lean_object*);
lean_object* l_Lean_throwErrorAt___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_getMainModuleDoc(lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__3;
lean_object* l_Std_instInhabitedPersistentArray(lean_object*);
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___boxed(lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__1;
lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SimplePersistentEnvExtension_getState___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_getDocStringText___rarg___closed__3;
@ -88,17 +88,17 @@ static lean_object* l_Lean_getDocStringText___rarg___closed__1;
LEAN_EXPORT lean_object* l_Lean_addDocString_x27(lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1534_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1555_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_4_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_44_(lean_object*);
LEAN_EXPORT lean_object* l_Std_RBNode_find___at_Lean_findDocString_x3f___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_indentD(lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__3;
LEAN_EXPORT lean_object* l_Lean_addBuiltinDocString(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l_Nat_min(lean_object*, lean_object*);
lean_object* l_Lean_Environment_getModuleIdx_x3f(lean_object*, lean_object*);
static lean_object* l_Lean_addBuiltinDocString___closed__1;
static lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__3;
LEAN_EXPORT lean_object* l_Std_RBNode_find___at_Lean_findDocString_x3f___spec__1___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_DocString_0__Lean_builtinDocStrings;
LEAN_EXPORT lean_object* l_String_Iterator_foldUntil___at___private_Lean_DocString_0__Lean_findLeadingSpacesSize___spec__2(lean_object*, lean_object*);
@ -677,94 +677,69 @@ goto _start;
LEAN_EXPORT lean_object* l_Lean_findDocString_x3f(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; uint8_t x_6;
x_4 = l_Lean_addBuiltinDocString___closed__1;
x_5 = lean_st_ref_get(x_4, x_3);
x_6 = !lean_is_exclusive(x_5);
if (x_6 == 0)
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = l_String_instInhabitedString;
x_5 = l_Lean_addDocString___rarg___lambda__1___closed__1;
lean_inc(x_2);
x_6 = l_Lean_MapDeclarationExtension_find_x3f___rarg(x_4, x_5, x_1, x_2);
if (lean_obj_tag(x_6) == 0)
{
lean_object* x_7; lean_object* x_8;
x_7 = lean_ctor_get(x_5, 0);
x_8 = l_Std_RBNode_find___at_Lean_findDocString_x3f___spec__1(x_7, x_2);
lean_dec(x_7);
if (lean_obj_tag(x_8) == 0)
lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_7 = l_Lean_addBuiltinDocString___closed__1;
x_8 = lean_st_ref_get(x_7, x_3);
x_9 = !lean_is_exclusive(x_8);
if (x_9 == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = l_String_instInhabitedString;
x_10 = l_Lean_addDocString___rarg___lambda__1___closed__1;
x_11 = l_Lean_MapDeclarationExtension_find_x3f___rarg(x_9, x_10, x_1, x_2);
lean_ctor_set(x_5, 0, x_11);
return x_5;
}
else
{
uint8_t x_12;
lean_object* x_10; lean_object* x_11;
x_10 = lean_ctor_get(x_8, 0);
x_11 = l_Std_RBNode_find___at_Lean_findDocString_x3f___spec__1(x_10, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_12 = !lean_is_exclusive(x_8);
if (x_12 == 0)
{
lean_ctor_set(x_5, 0, x_8);
return x_5;
lean_dec(x_10);
lean_ctor_set(x_8, 0, x_11);
return x_8;
}
else
{
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_8, 0);
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_12 = lean_ctor_get(x_8, 0);
x_13 = lean_ctor_get(x_8, 1);
lean_inc(x_13);
lean_inc(x_12);
lean_dec(x_8);
x_14 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_5, 0, x_14);
return x_5;
}
}
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_ctor_get(x_5, 0);
x_16 = lean_ctor_get(x_5, 1);
lean_inc(x_16);
lean_inc(x_15);
lean_dec(x_5);
x_17 = l_Std_RBNode_find___at_Lean_findDocString_x3f___spec__1(x_15, x_2);
lean_dec(x_15);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_18 = l_String_instInhabitedString;
x_19 = l_Lean_addDocString___rarg___lambda__1___closed__1;
x_20 = l_Lean_MapDeclarationExtension_find_x3f___rarg(x_18, x_19, x_1, x_2);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_16);
return x_21;
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_14 = l_Std_RBNode_find___at_Lean_findDocString_x3f___spec__1(x_12, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_22 = lean_ctor_get(x_17, 0);
lean_inc(x_22);
if (lean_is_exclusive(x_17)) {
lean_ctor_release(x_17, 0);
x_23 = x_17;
} else {
lean_dec_ref(x_17);
x_23 = lean_box(0);
lean_dec(x_12);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_13);
return x_15;
}
if (lean_is_scalar(x_23)) {
x_24 = lean_alloc_ctor(1, 1, 0);
} else {
x_24 = x_23;
}
lean_ctor_set(x_24, 0, x_22);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_16);
return x_25;
else
{
uint8_t x_16;
lean_dec(x_2);
x_16 = !lean_is_exclusive(x_6);
if (x_16 == 0)
{
lean_object* x_17;
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_6);
lean_ctor_set(x_17, 1, x_3);
return x_17;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_18 = lean_ctor_get(x_6, 0);
lean_inc(x_18);
lean_dec(x_6);
x_19 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_19, 0, x_18);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_3);
return x_20;
}
}
}
@ -779,7 +754,7 @@ lean_dec(x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__1() {
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -788,23 +763,23 @@ x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__2() {
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__1;
x_1 = l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__1;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__3() {
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__3() {
_start:
{
size_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = 5;
x_2 = l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__2;
x_3 = l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__1;
x_2 = l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__2;
x_3 = l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__1;
x_4 = lean_unsigned_to_nat(0u);
x_5 = lean_alloc_ctor(0, 4, sizeof(size_t)*1);
lean_ctor_set(x_5, 0, x_2);
@ -815,15 +790,15 @@ lean_ctor_set_usize(x_5, 4, x_1);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__3;
x_2 = l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__3;
return x_2;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__1() {
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__1() {
_start:
{
lean_object* x_1;
@ -831,17 +806,17 @@ x_1 = lean_mk_string_from_bytes("moduleDocExt", 12);
return x_1;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__2() {
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__1;
x_2 = l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__1;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__3() {
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__3() {
_start:
{
lean_object* x_1;
@ -850,7 +825,7 @@ lean_closure_set(x_1, 0, lean_box(0));
return x_1;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__4() {
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__4() {
_start:
{
lean_object* x_1;
@ -858,22 +833,22 @@ x_1 = lean_alloc_closure((void*)(l_Std_PersistentArray_push___rarg), 2, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__5() {
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___boxed), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__6() {
static lean_object* _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__2;
x_2 = l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__4;
x_3 = l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__5;
x_4 = l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__3;
x_1 = l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__2;
x_2 = l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__4;
x_3 = l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__5;
x_4 = l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__3;
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -882,20 +857,20 @@ lean_ctor_set(x_5, 3, x_4);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1534_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1555_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__6;
x_2 = l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__6;
x_3 = l_Lean_registerSimplePersistentEnvExtension___rarg(x_2, x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___boxed(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1(x_1);
x_2 = l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1(x_1);
lean_dec(x_1);
return x_2;
}
@ -1138,25 +1113,25 @@ l_Lean_addBuiltinDocString___closed__1 = _init_l_Lean_addBuiltinDocString___clos
lean_mark_persistent(l_Lean_addBuiltinDocString___closed__1);
l_Lean_addDocString___rarg___lambda__1___closed__1 = _init_l_Lean_addDocString___rarg___lambda__1___closed__1();
lean_mark_persistent(l_Lean_addDocString___rarg___lambda__1___closed__1);
l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__1 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__1();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__1);
l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__2 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__2();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__2);
l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__3 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__3();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1534____lambda__1___closed__3);
l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__1 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__1();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__1);
l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__2 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__2();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__2);
l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__3 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__3();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__3);
l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__4 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__4();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__4);
l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__5 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__5();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__5);
l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__6 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__6();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1534____closed__6);
if (builtin) {res = l_Lean_initFn____x40_Lean_DocString___hyg_1534_(lean_io_mk_world());
l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__1 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__1();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__1);
l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__2 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__2();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__2);
l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__3 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__3();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1555____lambda__1___closed__3);
l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__1 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__1();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__1);
l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__2 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__2();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__2);
l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__3 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__3();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__3);
l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__4 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__4();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__4);
l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__5 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__5();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__5);
l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__6 = _init_l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__6();
lean_mark_persistent(l_Lean_initFn____x40_Lean_DocString___hyg_1555____closed__6);
if (builtin) {res = l_Lean_initFn____x40_Lean_DocString___hyg_1555_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l___private_Lean_DocString_0__Lean_moduleDocExt = lean_io_result_get_value(res);
lean_mark_persistent(l___private_Lean_DocString_0__Lean_moduleDocExt);

78
stage0/stdlib/Lean/Elab/App.c generated
View file

@ -37433,7 +37433,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_Elab_Term_ElabElim_finalize___lambda__6___closed__4;
x_2 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___lambda__3___closed__1;
x_3 = lean_unsigned_to_nat(1156u);
x_3 = lean_unsigned_to_nat(1157u);
x_4 = lean_unsigned_to_nat(8u);
x_5 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___lambda__3___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -46511,7 +46511,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_Elab_Term_ElabElim_finalize___lambda__6___closed__4;
x_2 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_App_0__Lean_Elab_Term_mergeFailures___spec__1___closed__1;
x_3 = lean_unsigned_to_nat(1355u);
x_3 = lean_unsigned_to_nat(1356u);
x_4 = lean_unsigned_to_nat(57u);
x_5 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___lambda__3___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -47347,7 +47347,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_Elab_Term_ElabElim_finalize___lambda__6___closed__4;
x_2 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppAux___spec__4___closed__1;
x_3 = lean_unsigned_to_nat(1370u);
x_3 = lean_unsigned_to_nat(1371u);
x_4 = lean_unsigned_to_nat(21u);
x_5 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___lambda__3___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -48282,7 +48282,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabApp_declRange___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1392u);
x_1 = lean_unsigned_to_nat(1393u);
x_2 = lean_unsigned_to_nat(23u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48294,7 +48294,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabApp_declRange___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1395u);
x_1 = lean_unsigned_to_nat(1396u);
x_2 = lean_unsigned_to_nat(90u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48322,7 +48322,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabApp_declRange___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1392u);
x_1 = lean_unsigned_to_nat(1393u);
x_2 = lean_unsigned_to_nat(27u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48334,7 +48334,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabApp_declRange___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1392u);
x_1 = lean_unsigned_to_nat(1393u);
x_2 = lean_unsigned_to_nat(34u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48491,7 +48491,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabIdent_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1400u);
x_1 = lean_unsigned_to_nat(1401u);
x_2 = lean_unsigned_to_nat(25u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48503,7 +48503,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabIdent_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1400u);
x_1 = lean_unsigned_to_nat(1401u);
x_2 = lean_unsigned_to_nat(61u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48531,7 +48531,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabIdent_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1400u);
x_1 = lean_unsigned_to_nat(1401u);
x_2 = lean_unsigned_to_nat(29u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48543,7 +48543,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabIdent_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1400u);
x_1 = lean_unsigned_to_nat(1401u);
x_2 = lean_unsigned_to_nat(38u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48667,7 +48667,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNamedPattern_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1402u);
x_1 = lean_unsigned_to_nat(1403u);
x_2 = lean_unsigned_to_nat(32u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48679,7 +48679,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNamedPattern_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1402u);
x_1 = lean_unsigned_to_nat(1403u);
x_2 = lean_unsigned_to_nat(75u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48707,7 +48707,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNamedPattern_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1402u);
x_1 = lean_unsigned_to_nat(1403u);
x_2 = lean_unsigned_to_nat(36u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48719,7 +48719,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNamedPattern_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1402u);
x_1 = lean_unsigned_to_nat(1403u);
x_2 = lean_unsigned_to_nat(52u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48815,7 +48815,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabDotIdent_declRange__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1403u);
x_1 = lean_unsigned_to_nat(1404u);
x_2 = lean_unsigned_to_nat(28u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48827,7 +48827,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabDotIdent_declRange__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1403u);
x_1 = lean_unsigned_to_nat(1404u);
x_2 = lean_unsigned_to_nat(67u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48855,7 +48855,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabDotIdent_declRange__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1403u);
x_1 = lean_unsigned_to_nat(1404u);
x_2 = lean_unsigned_to_nat(32u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48867,7 +48867,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabDotIdent_declRange__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1403u);
x_1 = lean_unsigned_to_nat(1404u);
x_2 = lean_unsigned_to_nat(44u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48981,7 +48981,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicitUniv_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1405u);
x_1 = lean_unsigned_to_nat(1406u);
x_2 = lean_unsigned_to_nat(32u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -48993,7 +48993,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicitUniv_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1405u);
x_1 = lean_unsigned_to_nat(1406u);
x_2 = lean_unsigned_to_nat(75u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49021,7 +49021,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicitUniv_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1405u);
x_1 = lean_unsigned_to_nat(1406u);
x_2 = lean_unsigned_to_nat(36u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49033,7 +49033,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicitUniv_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1405u);
x_1 = lean_unsigned_to_nat(1406u);
x_2 = lean_unsigned_to_nat(52u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49315,7 +49315,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabPipeProj_declRange__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1407u);
x_1 = lean_unsigned_to_nat(1408u);
x_2 = lean_unsigned_to_nat(28u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49327,7 +49327,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabPipeProj_declRange__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1412u);
x_1 = lean_unsigned_to_nat(1413u);
x_2 = lean_unsigned_to_nat(34u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49355,7 +49355,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabPipeProj_declRange__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1407u);
x_1 = lean_unsigned_to_nat(1408u);
x_2 = lean_unsigned_to_nat(32u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49367,7 +49367,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabPipeProj_declRange__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1407u);
x_1 = lean_unsigned_to_nat(1408u);
x_2 = lean_unsigned_to_nat(44u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49620,7 +49620,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicit_declRange__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1417u);
x_1 = lean_unsigned_to_nat(1418u);
x_2 = lean_unsigned_to_nat(28u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49632,7 +49632,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicit_declRange__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1423u);
x_1 = lean_unsigned_to_nat(1424u);
x_2 = lean_unsigned_to_nat(50u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49660,7 +49660,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicit_declRange__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1417u);
x_1 = lean_unsigned_to_nat(1418u);
x_2 = lean_unsigned_to_nat(32u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49672,7 +49672,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicit_declRange__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1417u);
x_1 = lean_unsigned_to_nat(1418u);
x_2 = lean_unsigned_to_nat(44u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49768,7 +49768,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabChoice_declRange___c
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1425u);
x_1 = lean_unsigned_to_nat(1426u);
x_2 = lean_unsigned_to_nat(26u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49780,7 +49780,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabChoice_declRange___c
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1425u);
x_1 = lean_unsigned_to_nat(1426u);
x_2 = lean_unsigned_to_nat(63u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49808,7 +49808,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabChoice_declRange___c
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1425u);
x_1 = lean_unsigned_to_nat(1426u);
x_2 = lean_unsigned_to_nat(30u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49820,7 +49820,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabChoice_declRange___c
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1425u);
x_1 = lean_unsigned_to_nat(1426u);
x_2 = lean_unsigned_to_nat(40u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49916,7 +49916,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabProj_declRange___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1426u);
x_1 = lean_unsigned_to_nat(1427u);
x_2 = lean_unsigned_to_nat(24u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49928,7 +49928,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabProj_declRange___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1426u);
x_1 = lean_unsigned_to_nat(1427u);
x_2 = lean_unsigned_to_nat(59u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49956,7 +49956,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabProj_declRange___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1426u);
x_1 = lean_unsigned_to_nat(1427u);
x_2 = lean_unsigned_to_nat(28u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -49968,7 +49968,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabProj_declRange___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1426u);
x_1 = lean_unsigned_to_nat(1427u);
x_2 = lean_unsigned_to_nat(36u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);

40
stage0/stdlib/Lean/Elab/BuiltinNotation.c generated
View file

@ -16534,7 +16534,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandParen_declRange___
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(253u);
x_1 = lean_unsigned_to_nat(257u);
x_2 = lean_unsigned_to_nat(39u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -16546,7 +16546,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandParen_declRange___
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(268u);
x_1 = lean_unsigned_to_nat(272u);
x_2 = lean_unsigned_to_nat(74u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -16574,7 +16574,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandParen_declRange___
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(253u);
x_1 = lean_unsigned_to_nat(257u);
x_2 = lean_unsigned_to_nat(43u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -16586,7 +16586,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandParen_declRange___
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(253u);
x_1 = lean_unsigned_to_nat(257u);
x_2 = lean_unsigned_to_nat(54u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -16880,7 +16880,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabParen_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(270u);
x_1 = lean_unsigned_to_nat(274u);
x_2 = lean_unsigned_to_nat(25u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -16892,7 +16892,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabParen_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(276u);
x_1 = lean_unsigned_to_nat(280u);
x_2 = lean_unsigned_to_nat(31u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -16920,7 +16920,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabParen_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(270u);
x_1 = lean_unsigned_to_nat(274u);
x_2 = lean_unsigned_to_nat(29u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -16932,7 +16932,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabParen_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(270u);
x_1 = lean_unsigned_to_nat(274u);
x_2 = lean_unsigned_to_nat(38u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -19883,7 +19883,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabSubst_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(303u);
x_1 = lean_unsigned_to_nat(307u);
x_2 = lean_unsigned_to_nat(25u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -19895,7 +19895,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabSubst_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(368u);
x_1 = lean_unsigned_to_nat(372u);
x_2 = lean_unsigned_to_nat(31u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -19923,7 +19923,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabSubst_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(303u);
x_1 = lean_unsigned_to_nat(307u);
x_2 = lean_unsigned_to_nat(29u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -19935,7 +19935,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabSubst_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(303u);
x_1 = lean_unsigned_to_nat(307u);
x_2 = lean_unsigned_to_nat(38u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -20371,7 +20371,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT_declRange_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(370u);
x_1 = lean_unsigned_to_nat(374u);
x_2 = lean_unsigned_to_nat(29u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -20383,7 +20383,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT_declRange_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(379u);
x_1 = lean_unsigned_to_nat(383u);
x_2 = lean_unsigned_to_nat(32u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -20411,7 +20411,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT_declRange_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(370u);
x_1 = lean_unsigned_to_nat(374u);
x_2 = lean_unsigned_to_nat(33u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -20423,7 +20423,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT_declRange_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(370u);
x_1 = lean_unsigned_to_nat(374u);
x_2 = lean_unsigned_to_nat(46u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -20597,7 +20597,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNoindex_declRange___
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(381u);
x_1 = lean_unsigned_to_nat(385u);
x_2 = lean_unsigned_to_nat(27u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -20609,7 +20609,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNoindex_declRange___
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(383u);
x_1 = lean_unsigned_to_nat(387u);
x_2 = lean_unsigned_to_nat(40u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -20637,7 +20637,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNoindex_declRange___
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(381u);
x_1 = lean_unsigned_to_nat(385u);
x_2 = lean_unsigned_to_nat(31u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -20649,7 +20649,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNoindex_declRange___
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(381u);
x_1 = lean_unsigned_to_nat(385u);
x_2 = lean_unsigned_to_nat(42u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);

339
stage0/stdlib/Lean/Elab/Do.c generated
View file

@ -402,7 +402,7 @@ static lean_object* l_Lean_Elab_Term_Do_pullExitPointsAux___lambda__1___closed__
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_ToTerm_Kind_noConfusion___rarg(uint8_t, uint8_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_eraseOptVar(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_Do_pullExitPointsAux___lambda__1___closed__8;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__15;
static lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
static lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__3;
@ -882,7 +882,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__L
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_pullExitPointsAux___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_Do_ToTerm_toTerm_go___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__15;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_35099_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_35100_(lean_object*);
static lean_object* l_Lean_Elab_Term_Do_pullExitPointsAux___lambda__1___closed__9;
static lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode___closed__3;
static lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doReassignArrowToCode___closed__3;
@ -1120,7 +1120,7 @@ lean_object* lean_panic_fn(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__39;
static lean_object* l_Lean_Elab_Term_Do_ToTerm_reassignToTerm___closed__5;
static lean_object* l___regBuiltin_Lean_Elab_Term_expandTermTry_declRange___closed__7;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_Do_getLetDeclVars___closed__2;
LEAN_EXPORT uint8_t l_Lean_Elab_Term_Do_hasExitPoint___lambda__1(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___spec__6___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*);
@ -1348,7 +1348,6 @@ LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_expandTermUnless_declRang
static lean_object* l_Lean_Elab_Term_Do_hasExitPoint___closed__1;
static lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__11___closed__1;
static lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_extractBind___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__5;
static lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doForToCode___lambda__3___closed__31;
static lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
@ -1390,8 +1389,8 @@ lean_object* l_Lean_Elab_getBetterRef(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_Do_mkAuxDeclFor___rarg___lambda__1___closed__3;
static lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__6;
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_expandTermFor_declRange(lean_object*);
static lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__41;
@ -17466,49 +17465,48 @@ x_1 = lean_mk_string_from_bytes("with_annotate_term", 18);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_5 = lean_ctor_get(x_1, 0);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_ctor_get(x_5, 1);
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; lean_object* x_16; lean_object* x_17;
x_6 = lean_ctor_get(x_1, 0);
lean_inc(x_6);
lean_dec(x_5);
lean_inc(x_2);
x_7 = l_Lean_SourceInfo_fromRef(x_2);
lean_dec(x_1);
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
lean_dec(x_6);
x_8 = l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___closed__3;
x_9 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_9, 0, x_7);
lean_ctor_set(x_9, 0, x_2);
lean_ctor_set(x_9, 1, x_8);
x_10 = l_Lean_Elab_Term_Do_mkAuxDeclFor___rarg___lambda__4___closed__10;
x_11 = lean_array_push(x_10, x_9);
x_12 = lean_array_push(x_11, x_3);
x_13 = lean_array_push(x_12, x_2);
x_13 = lean_array_push(x_12, x_4);
x_14 = lean_box(2);
x_15 = l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___closed__2;
x_16 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_16, 0, x_14);
lean_ctor_set(x_16, 1, x_15);
lean_ctor_set(x_16, 2, x_13);
x_17 = lean_apply_2(x_6, lean_box(0), x_16);
x_17 = lean_apply_2(x_7, lean_box(0), x_16);
return x_17;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_1, 2);
lean_inc(x_7);
lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_8 = lean_ctor_get(x_1, 2);
lean_inc(x_8);
lean_dec(x_1);
x_8 = lean_alloc_closure((void*)(l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___boxed), 4, 3);
lean_closure_set(x_8, 0, x_2);
lean_closure_set(x_8, 1, x_3);
lean_closure_set(x_8, 2, x_4);
x_9 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_7, x_8);
return x_9;
x_9 = lean_alloc_closure((void*)(l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___boxed), 5, 4);
lean_closure_set(x_9, 0, x_2);
lean_closure_set(x_9, 1, x_3);
lean_closure_set(x_9, 2, x_4);
lean_closure_set(x_9, 3, x_5);
x_10 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_8, x_9);
return x_10;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
@ -17518,12 +17516,13 @@ lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_1, 1);
lean_inc(x_7);
lean_inc(x_5);
x_8 = lean_alloc_closure((void*)(l_Lean_Elab_Term_Do_annotate___rarg___lambda__2___boxed), 6, 5);
x_8 = lean_alloc_closure((void*)(l_Lean_Elab_Term_Do_annotate___rarg___lambda__2___boxed), 7, 6);
lean_closure_set(x_8, 0, x_1);
lean_closure_set(x_8, 1, x_2);
lean_closure_set(x_8, 2, x_3);
lean_closure_set(x_8, 3, x_4);
lean_closure_set(x_8, 4, x_5);
lean_closure_set(x_8, 2, x_6);
lean_closure_set(x_8, 3, x_3);
lean_closure_set(x_8, 4, x_4);
lean_closure_set(x_8, 5, x_5);
x_9 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_7, x_8);
return x_9;
}
@ -17531,20 +17530,30 @@ return x_9;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg(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_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;
x_6 = lean_ctor_get(x_1, 1);
lean_inc(x_6);
lean_inc(x_2);
lean_inc(x_1);
x_7 = l_Lean_MonadRef_mkInfoFromRefPos___rarg(x_1, x_2);
lean_inc(x_6);
x_8 = lean_alloc_closure((void*)(l_Lean_Elab_Term_Do_annotate___rarg___lambda__3___boxed), 6, 5);
lean_inc(x_5);
x_8 = lean_alloc_closure((void*)(l_Lean_Elab_Term_Do_annotate___rarg___lambda__3), 6, 5);
lean_closure_set(x_8, 0, x_3);
lean_closure_set(x_8, 1, x_1);
lean_closure_set(x_8, 2, x_5);
lean_closure_set(x_8, 3, x_4);
lean_closure_set(x_8, 2, x_4);
lean_closure_set(x_8, 3, x_5);
lean_closure_set(x_8, 4, x_6);
lean_inc(x_6);
x_9 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_7, x_8);
return x_9;
x_10 = lean_ctor_get(x_2, 0);
lean_inc(x_10);
x_11 = lean_alloc_closure((void*)(l_Lean_Elab_Term_Do_mkAuxDeclFor___rarg___lambda__14___boxed), 4, 3);
lean_closure_set(x_11, 0, x_5);
lean_closure_set(x_11, 1, x_2);
lean_closure_set(x_11, 2, x_9);
x_12 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_10, x_11);
return x_12;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate(lean_object* x_1) {
@ -17555,31 +17564,22 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_Do_annotate___rarg), 5, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_Elab_Term_Do_annotate___rarg___lambda__1(x_1, x_2, x_3, x_4);
lean_dec(x_4);
return x_5;
lean_object* x_6;
x_6 = l_Lean_Elab_Term_Do_annotate___rarg___lambda__1(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_5);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_7;
x_7 = l_Lean_Elab_Term_Do_annotate___rarg___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_6);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___rarg___lambda__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_Lean_Elab_Term_Do_annotate___rarg___lambda__3(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_6);
return x_7;
lean_object* x_8;
x_8 = l_Lean_Elab_Term_Do_annotate___rarg___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_7);
return x_8;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_ToTerm_Kind_toCtorIdx(uint8_t x_1) {
@ -18007,7 +18007,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___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_2 = l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__21;
x_3 = lean_unsigned_to_nat(911u);
x_3 = lean_unsigned_to_nat(923u);
x_4 = lean_unsigned_to_nat(24u);
x_5 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -19059,7 +19059,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___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_2 = l_Lean_Elab_Term_Do_ToTerm_continueToTerm___closed__1;
x_3 = lean_unsigned_to_nat(920u);
x_3 = lean_unsigned_to_nat(932u);
x_4 = lean_unsigned_to_nat(24u);
x_5 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -19311,7 +19311,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___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_2 = l_Lean_Elab_Term_Do_ToTerm_continueToTerm___closed__1;
x_3 = lean_unsigned_to_nat(924u);
x_3 = lean_unsigned_to_nat(936u);
x_4 = lean_unsigned_to_nat(24u);
x_5 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -20044,7 +20044,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___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_2 = l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__1;
x_3 = lean_unsigned_to_nat(932u);
x_3 = lean_unsigned_to_nat(944u);
x_4 = lean_unsigned_to_nat(24u);
x_5 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -20130,7 +20130,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___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_2 = l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__1;
x_3 = lean_unsigned_to_nat(936u);
x_3 = lean_unsigned_to_nat(948u);
x_4 = lean_unsigned_to_nat(24u);
x_5 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -20988,7 +20988,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___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_2 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__13;
x_3 = lean_unsigned_to_nat(947u);
x_3 = lean_unsigned_to_nat(959u);
x_4 = lean_unsigned_to_nat(24u);
x_5 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -25019,31 +25019,50 @@ return x_148;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___at_Lean_Elab_Term_Do_ToTerm_toTerm___spec__1(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; lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_6 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Term_Do_ToTerm_returnToTerm___spec__1___rarg(x_4, x_5);
x_7 = lean_ctor_get(x_6, 1);
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; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_6 = lean_ctor_get(x_4, 0);
x_7 = lean_ctor_get(x_4, 1);
x_8 = lean_ctor_get(x_4, 2);
x_9 = lean_ctor_get(x_4, 3);
x_10 = lean_ctor_get(x_4, 4);
x_11 = lean_ctor_get(x_4, 5);
x_12 = l_Lean_replaceRef(x_2, x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_dec(x_6);
lean_inc(x_2);
x_8 = l_Lean_SourceInfo_fromRef(x_2);
x_9 = l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___closed__3;
x_10 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_10, 0, x_8);
lean_ctor_set(x_10, 1, x_9);
x_11 = l_Lean_Elab_Term_Do_mkAuxDeclFor___rarg___lambda__4___closed__10;
x_12 = lean_array_push(x_11, x_10);
x_13 = lean_array_push(x_12, x_1);
x_14 = lean_array_push(x_13, x_2);
x_15 = lean_box(2);
x_16 = l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___closed__2;
x_17 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_17, 0, x_15);
lean_ctor_set(x_17, 1, x_16);
lean_ctor_set(x_17, 2, x_14);
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_7);
return x_18;
lean_inc(x_6);
x_13 = lean_alloc_ctor(0, 6, 0);
lean_ctor_set(x_13, 0, x_6);
lean_ctor_set(x_13, 1, x_7);
lean_ctor_set(x_13, 2, x_8);
lean_ctor_set(x_13, 3, x_9);
lean_ctor_set(x_13, 4, x_10);
lean_ctor_set(x_13, 5, x_12);
x_14 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Term_Do_ToTerm_returnToTerm___spec__1___rarg(x_13, x_5);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_ctor_get(x_14, 1);
lean_inc(x_16);
lean_dec(x_14);
x_17 = l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___closed__3;
x_18 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_18, 0, x_15);
lean_ctor_set(x_18, 1, x_17);
x_19 = l_Lean_Elab_Term_Do_mkAuxDeclFor___rarg___lambda__4___closed__10;
x_20 = lean_array_push(x_19, x_18);
x_21 = lean_array_push(x_20, x_1);
x_22 = lean_array_push(x_21, x_2);
x_23 = lean_box(2);
x_24 = l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___closed__2;
x_25 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
lean_ctor_set(x_25, 2, x_22);
x_26 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_16);
return x_26;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_ToTerm_toTerm(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
@ -25081,6 +25100,7 @@ x_10 = lean_ctor_get(x_8, 0);
lean_inc(x_10);
lean_dec(x_8);
x_11 = l_Lean_Elab_Term_Do_annotate___at_Lean_Elab_Term_Do_ToTerm_toTerm___spec__1(x_10, x_6, x_2, x_3, x_7);
lean_dec(x_3);
lean_dec(x_2);
return x_11;
}
@ -25121,6 +25141,7 @@ _start:
{
lean_object* x_6;
x_6 = l_Lean_Elab_Term_Do_annotate___at_Lean_Elab_Term_Do_ToTerm_toTerm___spec__1(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_4);
lean_dec(x_3);
return x_6;
}
@ -25172,7 +25193,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___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_2 = l_Lean_Elab_Term_Do_ToTerm_mkNestedKind___closed__1;
x_3 = lean_unsigned_to_nat(1087u);
x_3 = lean_unsigned_to_nat(1099u);
x_4 = lean_unsigned_to_nat(27u);
x_5 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -25341,7 +25362,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___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__1;
x_3 = lean_unsigned_to_nat(1143u);
x_3 = lean_unsigned_to_nat(1155u);
x_4 = lean_unsigned_to_nat(27u);
x_5 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -35130,35 +35151,69 @@ goto _start;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_annotate___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_11 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__2___rarg(x_8, x_9, x_10);
x_12 = lean_ctor_get(x_11, 1);
lean_inc(x_12);
lean_dec(x_11);
x_13 = lean_st_ref_get(x_9, x_12);
x_14 = lean_ctor_get(x_13, 1);
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38;
x_11 = lean_ctor_get(x_8, 0);
x_12 = lean_ctor_get(x_8, 1);
x_13 = lean_ctor_get(x_8, 2);
x_14 = lean_ctor_get(x_8, 3);
x_15 = lean_ctor_get(x_8, 4);
x_16 = lean_ctor_get(x_8, 5);
x_17 = lean_ctor_get(x_8, 6);
x_18 = lean_ctor_get(x_8, 7);
x_19 = lean_ctor_get(x_8, 8);
x_20 = lean_ctor_get(x_8, 9);
x_21 = lean_ctor_get(x_8, 10);
x_22 = l_Lean_replaceRef(x_2, x_16);
lean_inc(x_21);
lean_inc(x_20);
lean_inc(x_19);
lean_inc(x_18);
lean_inc(x_17);
lean_inc(x_15);
lean_inc(x_14);
lean_dec(x_13);
lean_inc(x_2);
x_15 = l_Lean_SourceInfo_fromRef(x_2);
x_16 = l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___closed__3;
x_17 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_17, 0, x_15);
lean_ctor_set(x_17, 1, x_16);
x_18 = l_Lean_Elab_Term_Do_mkAuxDeclFor___rarg___lambda__4___closed__10;
x_19 = lean_array_push(x_18, x_17);
x_20 = lean_array_push(x_19, x_1);
x_21 = lean_array_push(x_20, x_2);
x_22 = lean_box(2);
x_23 = l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___closed__2;
x_24 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_24, 0, x_22);
lean_ctor_set(x_24, 1, x_23);
lean_ctor_set(x_24, 2, x_21);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_14);
return x_25;
lean_inc(x_13);
lean_inc(x_12);
lean_inc(x_11);
x_23 = lean_alloc_ctor(0, 11, 0);
lean_ctor_set(x_23, 0, x_11);
lean_ctor_set(x_23, 1, x_12);
lean_ctor_set(x_23, 2, x_13);
lean_ctor_set(x_23, 3, x_14);
lean_ctor_set(x_23, 4, x_15);
lean_ctor_set(x_23, 5, x_22);
lean_ctor_set(x_23, 6, x_17);
lean_ctor_set(x_23, 7, x_18);
lean_ctor_set(x_23, 8, x_19);
lean_ctor_set(x_23, 9, x_20);
lean_ctor_set(x_23, 10, x_21);
x_24 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__2___rarg(x_23, x_9, x_10);
x_25 = lean_ctor_get(x_24, 0);
lean_inc(x_25);
x_26 = lean_ctor_get(x_24, 1);
lean_inc(x_26);
lean_dec(x_24);
x_27 = lean_st_ref_get(x_9, x_26);
x_28 = lean_ctor_get(x_27, 1);
lean_inc(x_28);
lean_dec(x_27);
x_29 = l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___closed__3;
x_30 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_30, 0, x_25);
lean_ctor_set(x_30, 1, x_29);
x_31 = l_Lean_Elab_Term_Do_mkAuxDeclFor___rarg___lambda__4___closed__10;
x_32 = lean_array_push(x_31, x_30);
x_33 = lean_array_push(x_32, x_1);
x_34 = lean_array_push(x_33, x_2);
x_35 = lean_box(2);
x_36 = l_Lean_Elab_Term_Do_annotate___rarg___lambda__1___closed__2;
x_37 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_37, 0, x_35);
lean_ctor_set(x_37, 1, x_36);
lean_ctor_set(x_37, 2, x_34);
x_38 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_38, 0, x_37);
lean_ctor_set(x_38, 1, x_28);
return x_38;
}
}
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__7(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) {
@ -35813,7 +35868,6 @@ x_102 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_102, 0, x_66);
lean_ctor_set(x_102, 1, x_101);
lean_ctor_set(x_102, 2, x_100);
lean_inc(x_18);
lean_inc(x_1);
x_103 = l_Lean_Elab_Term_Do_annotate___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__4(x_1, x_102, x_13, x_14, x_15, x_16, x_17, x_18, x_19, x_51);
x_104 = lean_ctor_get(x_103, 0);
@ -35935,7 +35989,6 @@ x_162 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_162, 0, x_127);
lean_ctor_set(x_162, 1, x_161);
lean_ctor_set(x_162, 2, x_160);
lean_inc(x_18);
lean_inc(x_1);
x_163 = l_Lean_Elab_Term_Do_annotate___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__4(x_1, x_162, x_13, x_14, x_15, x_16, x_17, x_18, x_19, x_112);
x_164 = lean_ctor_get(x_163, 0);
@ -36236,6 +36289,7 @@ lean_ctor_set(x_46, 1, x_45);
lean_ctor_set(x_46, 2, x_44);
x_47 = l_Lean_Elab_Term_Do_annotate___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__4(x_5, x_46, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_29);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
@ -40437,7 +40491,6 @@ x_124 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_124, 0, x_102);
lean_ctor_set(x_124, 1, x_123);
lean_ctor_set(x_124, 2, x_122);
lean_inc(x_30);
x_125 = l_Lean_Elab_Term_Do_annotate___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__4(x_1, x_124, x_3, x_4, x_5, x_6, x_7, x_30, x_9, x_90);
x_126 = lean_ctor_get(x_125, 0);
lean_inc(x_126);
@ -40535,7 +40588,6 @@ x_173 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_173, 0, x_150);
lean_ctor_set(x_173, 1, x_172);
lean_ctor_set(x_173, 2, x_171);
lean_inc(x_30);
x_174 = l_Lean_Elab_Term_Do_annotate___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__4(x_1, x_173, x_3, x_4, x_5, x_6, x_7, x_30, x_9, x_137);
x_175 = lean_ctor_get(x_174, 0);
lean_inc(x_175);
@ -40964,7 +41016,6 @@ x_362 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_362, 0, x_214);
lean_ctor_set(x_362, 1, x_361);
lean_ctor_set(x_362, 2, x_360);
lean_inc(x_30);
x_363 = l_Lean_Elab_Term_Do_annotate___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__4(x_1, x_362, x_3, x_4, x_5, x_6, x_7, x_30, x_9, x_227);
x_364 = lean_ctor_get(x_363, 0);
lean_inc(x_364);
@ -41274,7 +41325,6 @@ x_510 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_510, 0, x_214);
lean_ctor_set(x_510, 1, x_509);
lean_ctor_set(x_510, 2, x_508);
lean_inc(x_30);
x_511 = l_Lean_Elab_Term_Do_annotate___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__4(x_1, x_510, x_3, x_4, x_5, x_6, x_7, x_30, x_9, x_374);
x_512 = lean_ctor_get(x_511, 0);
lean_inc(x_512);
@ -43592,6 +43642,7 @@ _start:
lean_object* x_11;
x_11 = l_Lean_Elab_Term_Do_annotate___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__4(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
@ -44299,7 +44350,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Do_elabDo_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1641u);
x_1 = lean_unsigned_to_nat(1653u);
x_2 = lean_unsigned_to_nat(24u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -44311,7 +44362,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Do_elabDo_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1649u);
x_1 = lean_unsigned_to_nat(1661u);
x_2 = lean_unsigned_to_nat(84u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -44339,7 +44390,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Do_elabDo_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1641u);
x_1 = lean_unsigned_to_nat(1653u);
x_2 = lean_unsigned_to_nat(28u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -44351,7 +44402,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Do_elabDo_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1641u);
x_1 = lean_unsigned_to_nat(1653u);
x_2 = lean_unsigned_to_nat(34u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -44397,7 +44448,7 @@ x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_35099_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_35100_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -44553,7 +44604,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermFor_declRange_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1660u);
x_1 = lean_unsigned_to_nat(1672u);
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -44565,7 +44616,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermFor_declRange_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1660u);
x_1 = lean_unsigned_to_nat(1672u);
x_2 = lean_unsigned_to_nat(57u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -44593,7 +44644,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermFor_declRange_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1660u);
x_1 = lean_unsigned_to_nat(1672u);
x_2 = lean_unsigned_to_nat(4u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -44605,7 +44656,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermFor_declRange_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1660u);
x_1 = lean_unsigned_to_nat(1672u);
x_2 = lean_unsigned_to_nat(17u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -44711,7 +44762,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermTry_declRange_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1663u);
x_1 = lean_unsigned_to_nat(1675u);
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -44723,7 +44774,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermTry_declRange_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1663u);
x_1 = lean_unsigned_to_nat(1675u);
x_2 = lean_unsigned_to_nat(57u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -44751,7 +44802,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermTry_declRange_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1663u);
x_1 = lean_unsigned_to_nat(1675u);
x_2 = lean_unsigned_to_nat(4u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -44763,7 +44814,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermTry_declRange_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1663u);
x_1 = lean_unsigned_to_nat(1675u);
x_2 = lean_unsigned_to_nat(17u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -44869,7 +44920,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermUnless_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1666u);
x_1 = lean_unsigned_to_nat(1678u);
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -44881,7 +44932,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermUnless_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1666u);
x_1 = lean_unsigned_to_nat(1678u);
x_2 = lean_unsigned_to_nat(63u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -44909,7 +44960,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermUnless_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1666u);
x_1 = lean_unsigned_to_nat(1678u);
x_2 = lean_unsigned_to_nat(4u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -44921,7 +44972,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermUnless_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1666u);
x_1 = lean_unsigned_to_nat(1678u);
x_2 = lean_unsigned_to_nat(20u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -45027,7 +45078,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermReturn_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1669u);
x_1 = lean_unsigned_to_nat(1681u);
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -45039,7 +45090,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermReturn_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1669u);
x_1 = lean_unsigned_to_nat(1681u);
x_2 = lean_unsigned_to_nat(63u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -45067,7 +45118,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermReturn_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1669u);
x_1 = lean_unsigned_to_nat(1681u);
x_2 = lean_unsigned_to_nat(4u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -45079,7 +45130,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandTermReturn_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1669u);
x_1 = lean_unsigned_to_nat(1681u);
x_2 = lean_unsigned_to_nat(20u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -46488,7 +46539,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Do_elabDo_declRange___closed_
res = l___regBuiltin_Lean_Elab_Term_Do_elabDo_declRange(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_35099_(lean_io_mk_world());
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_35100_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Term_expandTermFor___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_expandTermFor___closed__1();

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

@ -387,7 +387,6 @@ LEAN_EXPORT uint8_t l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_sameHeadSymbol(
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqArgsFirstPass___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_CheckAssignment_assignToConstFun___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processAssignment_process___spec__2(lean_object*, lean_object*, size_t, size_t);
extern lean_object* l_Lean_instInhabitedProjectionFunctionInfo;
uint8_t l_Lean_Expr_hasExprMVar(lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_checkpointDefEq___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqQuickMVarMVar___spec__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -402,7 +401,6 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_CheckAssignmen
LEAN_EXPORT lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqEta(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_isExprDefEqAuxImpl___lambda__2___closed__2;
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_isProjectionFn___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_mkHashMapImp___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_CheckAssignment_checkMVar___spec__67___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_throwIsDefEqStuck___rarg(lean_object*);
@ -575,12 +573,10 @@ extern lean_object* l_Lean_Meta_instInhabitedParamInfo;
size_t lean_usize_land(size_t, size_t);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_CheckAssignment_checkMVar___spec__59___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_Lean_LocalDecl_fvarId(lean_object*);
extern lean_object* l_Lean_projectionFnInfoExt;
lean_object* l___private_Lean_Util_Trace_0__Lean_addTraceOptions(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqProj_isDefEqSingleton___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_CheckAssignment_checkMVar___closed__1;
lean_object* l_Lean_registerInternalExceptionId(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_isProjectionFn___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_checkpointDefEq___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqEtaStruct_go___spec__2___closed__5;
static lean_object* l_Lean_Meta_isExprDefEqAuxImpl___lambda__2___closed__19;
static lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqEtaStruct_go___closed__4;
@ -648,7 +644,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_assignCons
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
uint8_t lean_usize_dec_le(size_t, size_t);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_CheckAssignment_checkMVar___spec__63___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_isProjectionFn___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___spec__1___closed__1;
static lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processConstApprox_go_cont___closed__1;
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_CheckAssignmentQuick_check_visit___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_hasMVar(lean_object*);
@ -735,7 +730,7 @@ LEAN_EXPORT lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentA
LEAN_EXPORT lean_object* l_Std_PersistentArray_anyM___at_Lean_Meta_CheckAssignment_checkMVar___spec__46___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitMain___at_Lean_Meta_CheckAssignment_checkMVar___spec__4(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqArgsFirstPass___closed__3;
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_16734_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_16874_(lean_object*);
lean_object* l_Lean_Expr_app___override(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_CheckAssignment_throwCheckAssignmentFailure___rarg___closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -768,7 +763,6 @@ lean_object* l_Lean_mkFreshFVarId___at___private_Lean_Meta_Basic_0__Lean_Meta_fo
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_CheckAssignment_checkMVar___spec__33___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_CheckAssignment_checkMVar___spec__40(lean_object*, lean_object*, size_t, size_t);
lean_object* l_instHashableProd___rarg___boxed(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_MapDeclarationExtension_contains___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_cacheResult(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_replace___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_mkLambdaFVarsWithLetDeps_collectLetDeclsFrom_visit___spec__6___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getTransparency(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -796,6 +790,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqLef
LEAN_EXPORT lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processAssignmentFOApproxAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Std_HashSetImp_contains___at___private_Lean_MetavarContext_0__Lean_DependsOn_shouldVisit___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isAssignable___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getProjectionFnInfo_x3f___at_Lean_Meta_getStuckMVar_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_LocalContext_foldlM___at_Lean_Meta_CheckAssignment_checkMVar___spec__51___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_CheckAssignment_checkMVar___spec__48___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqEtaStruct_go___spec__1___lambda__1___closed__1;
@ -60713,63 +60708,13 @@ lean_dec(x_1);
return x_10;
}
}
static lean_object* _init_l_Lean_isProjectionFn___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___spec__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_projectionFnInfoExt;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_isProjectionFn___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; uint8_t x_8;
x_7 = lean_st_ref_get(x_5, x_6);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14;
x_9 = lean_ctor_get(x_7, 0);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
lean_dec(x_9);
x_11 = l_Lean_instInhabitedProjectionFunctionInfo;
x_12 = l_Lean_isProjectionFn___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___spec__1___closed__1;
x_13 = l_Lean_MapDeclarationExtension_contains___rarg(x_11, x_12, x_10, x_1);
x_14 = lean_box(x_13);
lean_ctor_set(x_7, 0, x_14);
return x_7;
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; lean_object* x_21; lean_object* x_22;
x_15 = lean_ctor_get(x_7, 0);
x_16 = lean_ctor_get(x_7, 1);
lean_inc(x_16);
lean_inc(x_15);
lean_dec(x_7);
x_17 = lean_ctor_get(x_15, 0);
lean_inc(x_17);
lean_dec(x_15);
x_18 = l_Lean_instInhabitedProjectionFunctionInfo;
x_19 = l_Lean_isProjectionFn___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___spec__1___closed__1;
x_20 = l_Lean_MapDeclarationExtension_contains___rarg(x_18, x_19, x_17, x_1);
x_21 = lean_box(x_20);
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_16);
return x_22;
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16;
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_10 = l_Lean_ConstantInfo_name(x_1);
lean_inc(x_10);
x_11 = l_Lean_isProjectionFn___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___spec__1(x_10, x_5, x_6, x_7, x_8, x_9);
x_11 = l_Lean_getProjectionFnInfo_x3f___at_Lean_Meta_getStuckMVar_x3f___spec__1(x_10, x_5, x_6, x_7, x_8, x_9);
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
@ -60777,30 +60722,35 @@ lean_inc(x_13);
lean_dec(x_11);
x_14 = l_Lean_ConstantInfo_name(x_2);
lean_inc(x_14);
x_15 = l_Lean_isProjectionFn___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___spec__1(x_14, x_5, x_6, x_7, x_8, x_13);
x_16 = lean_unbox(x_12);
lean_dec(x_12);
if (x_16 == 0)
x_15 = l_Lean_getProjectionFnInfo_x3f___at_Lean_Meta_getStuckMVar_x3f___spec__1(x_14, x_5, x_6, x_7, x_8, x_13);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_17; uint8_t x_18;
lean_object* x_16;
x_16 = lean_ctor_get(x_15, 0);
lean_inc(x_16);
if (lean_obj_tag(x_16) == 0)
{
lean_object* x_17; lean_object* x_18;
lean_dec(x_14);
x_17 = lean_ctor_get(x_15, 0);
lean_inc(x_17);
x_18 = lean_unbox(x_17);
lean_dec(x_17);
if (x_18 == 0)
{
lean_object* x_19; lean_object* x_20;
lean_dec(x_10);
x_19 = lean_ctor_get(x_15, 1);
lean_inc(x_19);
x_17 = lean_ctor_get(x_15, 1);
lean_inc(x_17);
lean_dec(x_15);
x_20 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldReducibeDefEq(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_19);
return x_20;
x_18 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldReducibeDefEq(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_17);
return x_18;
}
else
{
lean_object* x_19; uint8_t x_20;
x_19 = lean_ctor_get(x_16, 0);
lean_inc(x_19);
lean_dec(x_16);
x_20 = lean_ctor_get_uint8(x_19, sizeof(void*)*3);
lean_dec(x_19);
if (x_20 == 0)
{
lean_object* x_21; lean_object* x_22;
lean_dec(x_14);
x_21 = lean_ctor_get(x_15, 1);
lean_inc(x_21);
lean_dec(x_15);
@ -60869,59 +60819,51 @@ return x_32;
}
}
}
}
else
{
lean_object* x_33; uint8_t x_34;
lean_object* x_33; lean_object* x_34;
lean_dec(x_10);
x_33 = lean_ctor_get(x_15, 0);
x_33 = lean_ctor_get(x_15, 1);
lean_inc(x_33);
x_34 = lean_unbox(x_33);
lean_dec(x_33);
if (x_34 == 0)
{
lean_object* x_35; lean_object* x_36;
x_35 = lean_ctor_get(x_15, 1);
lean_inc(x_35);
lean_dec(x_15);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
x_36 = l_Lean_Meta_unfoldDefinition_x3f(x_4, x_5, x_6, x_7, x_8, x_35);
if (lean_obj_tag(x_36) == 0)
x_34 = l_Lean_Meta_unfoldDefinition_x3f(x_4, x_5, x_6, x_7, x_8, x_33);
if (lean_obj_tag(x_34) == 0)
{
lean_object* x_37;
x_37 = lean_ctor_get(x_36, 0);
lean_inc(x_37);
if (lean_obj_tag(x_37) == 0)
lean_object* x_35;
x_35 = lean_ctor_get(x_34, 0);
lean_inc(x_35);
if (lean_obj_tag(x_35) == 0)
{
lean_object* x_38; lean_object* x_39;
lean_object* x_36; lean_object* x_37;
lean_dec(x_14);
x_38 = lean_ctor_get(x_36, 1);
lean_inc(x_38);
lean_dec(x_36);
x_39 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldDefEq(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_38);
return x_39;
x_36 = lean_ctor_get(x_34, 1);
lean_inc(x_36);
lean_dec(x_34);
x_37 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldDefEq(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_36);
return x_37;
}
else
{
lean_object* x_40; lean_object* x_41; lean_object* x_42;
lean_object* x_38; lean_object* x_39; lean_object* x_40;
lean_dec(x_4);
x_40 = lean_ctor_get(x_36, 1);
lean_inc(x_40);
lean_dec(x_36);
x_41 = lean_ctor_get(x_37, 0);
lean_inc(x_41);
lean_dec(x_37);
x_42 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqRight(x_14, x_3, x_41, x_5, x_6, x_7, x_8, x_40);
return x_42;
x_38 = lean_ctor_get(x_34, 1);
lean_inc(x_38);
lean_dec(x_34);
x_39 = lean_ctor_get(x_35, 0);
lean_inc(x_39);
lean_dec(x_35);
x_40 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqRight(x_14, x_3, x_39, x_5, x_6, x_7, x_8, x_38);
return x_40;
}
}
else
{
uint8_t x_43;
uint8_t x_41;
lean_dec(x_14);
lean_dec(x_8);
lean_dec(x_7);
@ -60929,49 +60871,215 @@ lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_43 = !lean_is_exclusive(x_36);
if (x_43 == 0)
x_41 = !lean_is_exclusive(x_34);
if (x_41 == 0)
{
return x_36;
return x_34;
}
else
{
lean_object* x_44; lean_object* x_45; lean_object* x_46;
x_44 = lean_ctor_get(x_36, 0);
x_45 = lean_ctor_get(x_36, 1);
lean_object* x_42; lean_object* x_43; lean_object* x_44;
x_42 = lean_ctor_get(x_34, 0);
x_43 = lean_ctor_get(x_34, 1);
lean_inc(x_43);
lean_inc(x_42);
lean_dec(x_34);
x_44 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_44, 0, x_42);
lean_ctor_set(x_44, 1, x_43);
return x_44;
}
}
}
}
}
else
{
lean_object* x_45; uint8_t x_46;
x_45 = lean_ctor_get(x_12, 0);
lean_inc(x_45);
lean_inc(x_44);
lean_dec(x_36);
x_46 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_46, 0, x_44);
lean_ctor_set(x_46, 1, x_45);
return x_46;
lean_dec(x_12);
x_46 = lean_ctor_get_uint8(x_45, sizeof(void*)*3);
lean_dec(x_45);
if (x_46 == 0)
{
lean_object* x_47;
lean_dec(x_10);
x_47 = lean_ctor_get(x_15, 0);
lean_inc(x_47);
if (lean_obj_tag(x_47) == 0)
{
lean_object* x_48; lean_object* x_49;
x_48 = lean_ctor_get(x_15, 1);
lean_inc(x_48);
lean_dec(x_15);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
x_49 = l_Lean_Meta_unfoldDefinition_x3f(x_4, x_5, x_6, x_7, x_8, x_48);
if (lean_obj_tag(x_49) == 0)
{
lean_object* x_50;
x_50 = lean_ctor_get(x_49, 0);
lean_inc(x_50);
if (lean_obj_tag(x_50) == 0)
{
lean_object* x_51; lean_object* x_52;
lean_dec(x_14);
x_51 = lean_ctor_get(x_49, 1);
lean_inc(x_51);
lean_dec(x_49);
x_52 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldDefEq(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_51);
return x_52;
}
else
{
lean_object* x_53; lean_object* x_54; lean_object* x_55;
lean_dec(x_4);
x_53 = lean_ctor_get(x_49, 1);
lean_inc(x_53);
lean_dec(x_49);
x_54 = lean_ctor_get(x_50, 0);
lean_inc(x_54);
lean_dec(x_50);
x_55 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqRight(x_14, x_3, x_54, x_5, x_6, x_7, x_8, x_53);
return x_55;
}
}
else
{
lean_object* x_47; lean_object* x_48;
uint8_t x_56;
lean_dec(x_14);
x_47 = lean_ctor_get(x_15, 1);
lean_inc(x_47);
lean_dec(x_15);
x_48 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldReducibeDefEq(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_47);
return x_48;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_isProjectionFn___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_Lean_isProjectionFn___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___spec__1(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(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_7;
x_56 = !lean_is_exclusive(x_49);
if (x_56 == 0)
{
return x_49;
}
else
{
lean_object* x_57; lean_object* x_58; lean_object* x_59;
x_57 = lean_ctor_get(x_49, 0);
x_58 = lean_ctor_get(x_49, 1);
lean_inc(x_58);
lean_inc(x_57);
lean_dec(x_49);
x_59 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_59, 0, x_57);
lean_ctor_set(x_59, 1, x_58);
return x_59;
}
}
}
else
{
lean_object* x_60; lean_object* x_61;
lean_dec(x_47);
lean_dec(x_14);
x_60 = lean_ctor_get(x_15, 1);
lean_inc(x_60);
lean_dec(x_15);
x_61 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldReducibeDefEq(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_60);
return x_61;
}
}
else
{
lean_object* x_62;
lean_dec(x_14);
x_62 = lean_ctor_get(x_15, 0);
lean_inc(x_62);
if (lean_obj_tag(x_62) == 0)
{
lean_object* x_63; lean_object* x_64;
x_63 = lean_ctor_get(x_15, 1);
lean_inc(x_63);
lean_dec(x_15);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_3);
x_64 = l_Lean_Meta_unfoldDefinition_x3f(x_3, x_5, x_6, x_7, x_8, x_63);
if (lean_obj_tag(x_64) == 0)
{
lean_object* x_65;
x_65 = lean_ctor_get(x_64, 0);
lean_inc(x_65);
if (lean_obj_tag(x_65) == 0)
{
lean_object* x_66; lean_object* x_67;
lean_dec(x_10);
x_66 = lean_ctor_get(x_64, 1);
lean_inc(x_66);
lean_dec(x_64);
x_67 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldDefEq(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_66);
return x_67;
}
else
{
lean_object* x_68; lean_object* x_69; lean_object* x_70;
lean_dec(x_3);
x_68 = lean_ctor_get(x_64, 1);
lean_inc(x_68);
lean_dec(x_64);
x_69 = lean_ctor_get(x_65, 0);
lean_inc(x_69);
lean_dec(x_65);
x_70 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqLeft(x_10, x_69, x_4, x_5, x_6, x_7, x_8, x_68);
return x_70;
}
}
else
{
uint8_t x_71;
lean_dec(x_10);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_71 = !lean_is_exclusive(x_64);
if (x_71 == 0)
{
return x_64;
}
else
{
lean_object* x_72; lean_object* x_73; lean_object* x_74;
x_72 = lean_ctor_get(x_64, 0);
x_73 = lean_ctor_get(x_64, 1);
lean_inc(x_73);
lean_inc(x_72);
lean_dec(x_64);
x_74 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_74, 0, x_72);
lean_ctor_set(x_74, 1, x_73);
return x_74;
}
}
}
else
{
lean_object* x_75; lean_object* x_76;
lean_dec(x_62);
lean_dec(x_10);
x_75 = lean_ctor_get(x_15, 1);
lean_inc(x_75);
lean_dec(x_15);
x_76 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldReducibeDefEq(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_75);
return x_76;
}
}
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___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) {
@ -81057,7 +81165,7 @@ lean_dec(x_4);
return x_10;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_16734_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_16874_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -81607,8 +81715,6 @@ l_Lean_Meta_checkpointDefEq___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_tryH
lean_mark_persistent(l_Lean_Meta_checkpointDefEq___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_tryHeuristic___spec__1___closed__1);
l_Lean_Meta_checkpointDefEq___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_tryHeuristic___spec__1___closed__2 = _init_l_Lean_Meta_checkpointDefEq___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_tryHeuristic___spec__1___closed__2();
lean_mark_persistent(l_Lean_Meta_checkpointDefEq___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_tryHeuristic___spec__1___closed__2);
l_Lean_isProjectionFn___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___spec__1___closed__1 = _init_l_Lean_isProjectionFn___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___spec__1___closed__1();
lean_mark_persistent(l_Lean_isProjectionFn___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___spec__1___closed__1);
l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqQuickOther___lambda__2___closed__1 = _init_l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqQuickOther___lambda__2___closed__1();
lean_mark_persistent(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqQuickOther___lambda__2___closed__1);
l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqQuickOther___lambda__2___closed__2 = _init_l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqQuickOther___lambda__2___closed__2();
@ -81709,7 +81815,7 @@ l_Lean_Meta_isExprDefEqAuxImpl___closed__1 = _init_l_Lean_Meta_isExprDefEqAuxImp
lean_mark_persistent(l_Lean_Meta_isExprDefEqAuxImpl___closed__1);
l_Lean_Meta_isExprDefEqAuxImpl___closed__2 = _init_l_Lean_Meta_isExprDefEqAuxImpl___closed__2();
lean_mark_persistent(l_Lean_Meta_isExprDefEqAuxImpl___closed__2);
res = l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_16734_(lean_io_mk_world());
res = l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_16874_(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));

641
stage0/stdlib/Lean/Server/InfoUtils.c generated
View file

@ -41,6 +41,7 @@ LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_InfoTree_goalsAt_
lean_object* l_Lean_Syntax_getTrailingSize(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__21___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__7___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_LocalDecl_userName(lean_object*);
LEAN_EXPORT uint8_t l_Std_PersistentArray_anyMAux___at_Lean_Elab_InfoTree_goalsAt_x3f_hasNestedTactic___spec__7(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_hasSorry(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_visitM_x27___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -114,6 +115,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_getCompletionInfos(lean_object*);
static lean_object* l_Lean_Elab_InfoTree_hoverableInfoAt_x3f___lambda__3___closed__5;
lean_object* l_Lean_Elab_Info_updateContext_x3f(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_visitM_go___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_findFVar_x3f(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_Range_contains___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_instBEqRange;
LEAN_EXPORT lean_object* l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -171,6 +173,7 @@ LEAN_EXPORT lean_object* l_panic___at_Lean_Elab_InfoTree_collectNodesBottomUp___
LEAN_EXPORT uint8_t l_Std_PersistentArray_anyMAux___at_Lean_Elab_InfoTree_goalsAt_x3f_hasNestedTactic___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_panic___at_Lean_FileMap_toPosition_loop___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__20(lean_object*);
uint8_t l_Lean_Name_hasMacroScopes(lean_object*);
LEAN_EXPORT uint8_t l_Std_PersistentArray_anyM___at_Lean_Elab_InfoTree_goalsAt_x3f_hasNestedTactic___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__9;
LEAN_EXPORT lean_object* l_Lean_Elab_Info_size_x3f___boxed(lean_object*);
@ -6911,51 +6914,107 @@ x_17 = l_Lean_Expr_isConst(x_1);
if (x_17 == 0)
{
lean_object* x_18;
lean_inc(x_1);
x_18 = l_Lean_Meta_ppExpr(x_1, x_3, x_4, x_5, x_6, x_16);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
if (lean_obj_tag(x_18) == 0)
{
uint8_t x_19;
x_19 = !lean_is_exclusive(x_18);
if (x_19 == 0)
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_19 = lean_ctor_get(x_18, 0);
lean_inc(x_19);
x_20 = lean_ctor_get(x_18, 1);
lean_inc(x_20);
if (lean_is_exclusive(x_18)) {
lean_ctor_release(x_18, 0);
lean_ctor_release(x_18, 1);
x_21 = x_18;
} else {
lean_dec_ref(x_18);
x_21 = lean_box(0);
}
x_22 = lean_ctor_get(x_3, 1);
lean_inc(x_22);
lean_dec(x_3);
if (lean_obj_tag(x_1) == 1)
{
lean_object* x_20; uint8_t x_21;
x_20 = lean_ctor_get(x_18, 0);
x_21 = l_Lean_Elab_Info_fmtHover_x3f_isAtomicFormat(x_20);
if (x_21 == 0)
lean_object* x_43;
x_43 = l_Lean_LocalContext_findFVar_x3f(x_22, x_1);
if (lean_obj_tag(x_43) == 0)
{
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_dec(x_20);
x_22 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__6;
x_23 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_15);
x_24 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_22);
x_25 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__2;
x_26 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_24);
x_27 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__4;
x_28 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_28, 0, x_26);
lean_ctor_set(x_28, 1, x_27);
x_29 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_18, 0, x_29);
return x_18;
uint8_t x_44;
x_44 = 0;
x_23 = x_44;
goto block_42;
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40;
lean_object* x_45; lean_object* x_46; uint8_t x_47;
x_45 = lean_ctor_get(x_43, 0);
lean_inc(x_45);
lean_dec(x_43);
x_46 = l_Lean_LocalDecl_userName(x_45);
lean_dec(x_45);
x_47 = l_Lean_Name_hasMacroScopes(x_46);
lean_dec(x_46);
if (x_47 == 0)
{
uint8_t x_48;
x_48 = 1;
x_23 = x_48;
goto block_42;
}
else
{
uint8_t x_49;
x_49 = 0;
x_23 = x_49;
goto block_42;
}
}
}
else
{
uint8_t x_50;
lean_dec(x_22);
lean_dec(x_1);
x_50 = l_Lean_Elab_Info_fmtHover_x3f_isAtomicFormat(x_19);
x_23 = x_50;
goto block_42;
}
block_42:
{
if (x_23 == 0)
{
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_dec(x_19);
x_24 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__2;
x_25 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_15);
x_26 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__4;
x_27 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_27, 0, x_25);
lean_ctor_set(x_27, 1, x_26);
x_28 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_28, 0, x_27);
if (lean_is_scalar(x_21)) {
x_29 = lean_alloc_ctor(0, 2, 0);
} else {
x_29 = x_21;
}
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_20);
return x_29;
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_30 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__6;
x_31 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_20);
lean_ctor_set(x_31, 1, x_19);
x_32 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__8;
x_33 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_33, 0, x_31);
@ -6976,369 +7035,309 @@ lean_ctor_set(x_39, 0, x_37);
lean_ctor_set(x_39, 1, x_38);
x_40 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_18, 0, x_40);
return x_18;
if (lean_is_scalar(x_21)) {
x_41 = lean_alloc_ctor(0, 2, 0);
} else {
x_41 = x_21;
}
}
else
{
lean_object* x_41; lean_object* x_42; uint8_t x_43;
x_41 = lean_ctor_get(x_18, 0);
x_42 = lean_ctor_get(x_18, 1);
lean_inc(x_42);
lean_inc(x_41);
lean_dec(x_18);
x_43 = l_Lean_Elab_Info_fmtHover_x3f_isAtomicFormat(x_41);
if (x_43 == 0)
{
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_dec(x_41);
x_44 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__6;
x_45 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_45, 0, x_44);
lean_ctor_set(x_45, 1, x_15);
x_46 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_46, 0, x_45);
lean_ctor_set(x_46, 1, x_44);
x_47 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__2;
x_48 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_48, 0, x_47);
lean_ctor_set(x_48, 1, x_46);
x_49 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__4;
x_50 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_50, 0, x_48);
lean_ctor_set(x_50, 1, x_49);
x_51 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_51, 0, x_50);
x_52 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_52, 0, x_51);
lean_ctor_set(x_52, 1, x_42);
return x_52;
}
else
{
lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64;
x_53 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__6;
x_54 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_54, 0, x_53);
lean_ctor_set(x_54, 1, x_41);
x_55 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__8;
x_56 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_56, 0, x_54);
lean_ctor_set(x_56, 1, x_55);
x_57 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_57, 0, x_56);
lean_ctor_set(x_57, 1, x_15);
x_58 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_58, 0, x_57);
lean_ctor_set(x_58, 1, x_53);
x_59 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__2;
x_60 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_60, 0, x_59);
lean_ctor_set(x_60, 1, x_58);
x_61 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__4;
x_62 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_62, 0, x_60);
lean_ctor_set(x_62, 1, x_61);
x_63 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_63, 0, x_62);
x_64 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_64, 0, x_63);
lean_ctor_set(x_64, 1, x_42);
return x_64;
lean_ctor_set(x_41, 0, x_40);
lean_ctor_set(x_41, 1, x_20);
return x_41;
}
}
}
else
{
uint8_t x_65;
uint8_t x_51;
lean_dec(x_15);
x_65 = !lean_is_exclusive(x_18);
if (x_65 == 0)
lean_dec(x_3);
lean_dec(x_1);
x_51 = !lean_is_exclusive(x_18);
if (x_51 == 0)
{
return x_18;
}
else
{
lean_object* x_66; lean_object* x_67; lean_object* x_68;
x_66 = lean_ctor_get(x_18, 0);
x_67 = lean_ctor_get(x_18, 1);
lean_inc(x_67);
lean_inc(x_66);
lean_object* x_52; lean_object* x_53; lean_object* x_54;
x_52 = lean_ctor_get(x_18, 0);
x_53 = lean_ctor_get(x_18, 1);
lean_inc(x_53);
lean_inc(x_52);
lean_dec(x_18);
x_68 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_68, 0, x_66);
lean_ctor_set(x_68, 1, x_67);
return x_68;
x_54 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_54, 0, x_52);
lean_ctor_set(x_54, 1, x_53);
return x_54;
}
}
}
else
{
uint8_t x_69;
x_69 = !lean_is_exclusive(x_5);
if (x_69 == 0)
uint8_t x_55;
x_55 = !lean_is_exclusive(x_5);
if (x_55 == 0)
{
lean_object* x_70; lean_object* x_71; uint8_t x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77;
x_70 = lean_ctor_get(x_5, 2);
x_71 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__9;
x_72 = 1;
x_73 = l_Lean_Option_set___at_Lean_Meta_withPPInaccessibleNamesImp___spec__2(x_70, x_71, x_72);
x_74 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__10;
x_75 = l_Lean_Option_set___at_Lean_Meta_withPPInaccessibleNamesImp___spec__2(x_73, x_74, x_72);
lean_ctor_set(x_5, 2, x_75);
x_76 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__11;
x_77 = l_Lean_PrettyPrinter_ppUsing(x_1, x_76, x_3, x_4, x_5, x_6, x_16);
if (lean_obj_tag(x_77) == 0)
lean_object* x_56; lean_object* x_57; uint8_t x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63;
x_56 = lean_ctor_get(x_5, 2);
x_57 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__9;
x_58 = 1;
x_59 = l_Lean_Option_set___at_Lean_Meta_withPPInaccessibleNamesImp___spec__2(x_56, x_57, x_58);
x_60 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__10;
x_61 = l_Lean_Option_set___at_Lean_Meta_withPPInaccessibleNamesImp___spec__2(x_59, x_60, x_58);
lean_ctor_set(x_5, 2, x_61);
x_62 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__11;
x_63 = l_Lean_PrettyPrinter_ppUsing(x_1, x_62, x_3, x_4, x_5, x_6, x_16);
if (lean_obj_tag(x_63) == 0)
{
uint8_t x_78;
x_78 = !lean_is_exclusive(x_77);
if (x_78 == 0)
uint8_t x_64;
x_64 = !lean_is_exclusive(x_63);
if (x_64 == 0)
{
lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87;
x_79 = lean_ctor_get(x_77, 0);
x_80 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__2;
x_81 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_81, 0, x_80);
lean_ctor_set(x_81, 1, x_79);
x_82 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__8;
x_83 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_83, 0, x_81);
lean_ctor_set(x_83, 1, x_82);
x_84 = lean_alloc_ctor(4, 2, 0);
lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73;
x_65 = lean_ctor_get(x_63, 0);
x_66 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__2;
x_67 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_67, 0, x_66);
lean_ctor_set(x_67, 1, x_65);
x_68 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__8;
x_69 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_69, 0, x_67);
lean_ctor_set(x_69, 1, x_68);
x_70 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_70, 0, x_69);
lean_ctor_set(x_70, 1, x_15);
x_71 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__4;
x_72 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_72, 0, x_70);
lean_ctor_set(x_72, 1, x_71);
x_73 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_73, 0, x_72);
lean_ctor_set(x_63, 0, x_73);
return x_63;
}
else
{
lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84;
x_74 = lean_ctor_get(x_63, 0);
x_75 = lean_ctor_get(x_63, 1);
lean_inc(x_75);
lean_inc(x_74);
lean_dec(x_63);
x_76 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__2;
x_77 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_77, 0, x_76);
lean_ctor_set(x_77, 1, x_74);
x_78 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__8;
x_79 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_79, 0, x_77);
lean_ctor_set(x_79, 1, x_78);
x_80 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_80, 0, x_79);
lean_ctor_set(x_80, 1, x_15);
x_81 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__4;
x_82 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_82, 0, x_80);
lean_ctor_set(x_82, 1, x_81);
x_83 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_83, 0, x_82);
x_84 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_84, 0, x_83);
lean_ctor_set(x_84, 1, x_15);
x_85 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__4;
x_86 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_86, 0, x_84);
lean_ctor_set(x_86, 1, x_85);
x_87 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_87, 0, x_86);
lean_ctor_set(x_77, 0, x_87);
return x_77;
lean_ctor_set(x_84, 1, x_75);
return x_84;
}
}
else
{
lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98;
x_88 = lean_ctor_get(x_77, 0);
x_89 = lean_ctor_get(x_77, 1);
uint8_t x_85;
lean_dec(x_15);
x_85 = !lean_is_exclusive(x_63);
if (x_85 == 0)
{
return x_63;
}
else
{
lean_object* x_86; lean_object* x_87; lean_object* x_88;
x_86 = lean_ctor_get(x_63, 0);
x_87 = lean_ctor_get(x_63, 1);
lean_inc(x_87);
lean_inc(x_86);
lean_dec(x_63);
x_88 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_88, 0, x_86);
lean_ctor_set(x_88, 1, x_87);
return x_88;
}
}
}
else
{
lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; uint8_t x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107;
x_89 = lean_ctor_get(x_5, 0);
x_90 = lean_ctor_get(x_5, 1);
x_91 = lean_ctor_get(x_5, 2);
x_92 = lean_ctor_get(x_5, 3);
x_93 = lean_ctor_get(x_5, 4);
x_94 = lean_ctor_get(x_5, 5);
x_95 = lean_ctor_get(x_5, 6);
x_96 = lean_ctor_get(x_5, 7);
x_97 = lean_ctor_get(x_5, 8);
x_98 = lean_ctor_get(x_5, 9);
x_99 = lean_ctor_get(x_5, 10);
lean_inc(x_99);
lean_inc(x_98);
lean_inc(x_97);
lean_inc(x_96);
lean_inc(x_95);
lean_inc(x_94);
lean_inc(x_93);
lean_inc(x_92);
lean_inc(x_91);
lean_inc(x_90);
lean_inc(x_89);
lean_inc(x_88);
lean_dec(x_77);
x_90 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__2;
x_91 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_91, 0, x_90);
lean_ctor_set(x_91, 1, x_88);
x_92 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__8;
x_93 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_93, 0, x_91);
lean_ctor_set(x_93, 1, x_92);
x_94 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_94, 0, x_93);
lean_ctor_set(x_94, 1, x_15);
x_95 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__4;
x_96 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_96, 0, x_94);
lean_ctor_set(x_96, 1, x_95);
x_97 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_97, 0, x_96);
x_98 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_98, 0, x_97);
lean_ctor_set(x_98, 1, x_89);
return x_98;
}
}
else
{
uint8_t x_99;
lean_dec(x_15);
x_99 = !lean_is_exclusive(x_77);
if (x_99 == 0)
{
return x_77;
}
else
{
lean_object* x_100; lean_object* x_101; lean_object* x_102;
x_100 = lean_ctor_get(x_77, 0);
x_101 = lean_ctor_get(x_77, 1);
lean_inc(x_101);
lean_inc(x_100);
lean_dec(x_77);
x_102 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_102, 0, x_100);
lean_ctor_set(x_102, 1, x_101);
return x_102;
}
}
}
else
{
lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; uint8_t x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121;
x_103 = lean_ctor_get(x_5, 0);
x_104 = lean_ctor_get(x_5, 1);
x_105 = lean_ctor_get(x_5, 2);
x_106 = lean_ctor_get(x_5, 3);
x_107 = lean_ctor_get(x_5, 4);
x_108 = lean_ctor_get(x_5, 5);
x_109 = lean_ctor_get(x_5, 6);
x_110 = lean_ctor_get(x_5, 7);
x_111 = lean_ctor_get(x_5, 8);
x_112 = lean_ctor_get(x_5, 9);
x_113 = lean_ctor_get(x_5, 10);
lean_inc(x_113);
lean_inc(x_112);
lean_inc(x_111);
lean_inc(x_110);
lean_inc(x_109);
lean_inc(x_108);
lean_inc(x_107);
lean_inc(x_106);
lean_inc(x_105);
lean_inc(x_104);
lean_inc(x_103);
lean_dec(x_5);
x_114 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__9;
x_115 = 1;
x_116 = l_Lean_Option_set___at_Lean_Meta_withPPInaccessibleNamesImp___spec__2(x_105, x_114, x_115);
x_117 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__10;
x_118 = l_Lean_Option_set___at_Lean_Meta_withPPInaccessibleNamesImp___spec__2(x_116, x_117, x_115);
x_119 = lean_alloc_ctor(0, 11, 0);
lean_ctor_set(x_119, 0, x_103);
lean_ctor_set(x_119, 1, x_104);
lean_ctor_set(x_119, 2, x_118);
lean_ctor_set(x_119, 3, x_106);
lean_ctor_set(x_119, 4, x_107);
lean_ctor_set(x_119, 5, x_108);
lean_ctor_set(x_119, 6, x_109);
lean_ctor_set(x_119, 7, x_110);
lean_ctor_set(x_119, 8, x_111);
lean_ctor_set(x_119, 9, x_112);
lean_ctor_set(x_119, 10, x_113);
x_120 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__11;
x_121 = l_Lean_PrettyPrinter_ppUsing(x_1, x_120, x_3, x_4, x_119, x_6, x_16);
if (lean_obj_tag(x_121) == 0)
x_100 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__9;
x_101 = 1;
x_102 = l_Lean_Option_set___at_Lean_Meta_withPPInaccessibleNamesImp___spec__2(x_91, x_100, x_101);
x_103 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__10;
x_104 = l_Lean_Option_set___at_Lean_Meta_withPPInaccessibleNamesImp___spec__2(x_102, x_103, x_101);
x_105 = lean_alloc_ctor(0, 11, 0);
lean_ctor_set(x_105, 0, x_89);
lean_ctor_set(x_105, 1, x_90);
lean_ctor_set(x_105, 2, x_104);
lean_ctor_set(x_105, 3, x_92);
lean_ctor_set(x_105, 4, x_93);
lean_ctor_set(x_105, 5, x_94);
lean_ctor_set(x_105, 6, x_95);
lean_ctor_set(x_105, 7, x_96);
lean_ctor_set(x_105, 8, x_97);
lean_ctor_set(x_105, 9, x_98);
lean_ctor_set(x_105, 10, x_99);
x_106 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__11;
x_107 = l_Lean_PrettyPrinter_ppUsing(x_1, x_106, x_3, x_4, x_105, x_6, x_16);
if (lean_obj_tag(x_107) == 0)
{
lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133;
x_122 = lean_ctor_get(x_121, 0);
lean_inc(x_122);
x_123 = lean_ctor_get(x_121, 1);
lean_inc(x_123);
if (lean_is_exclusive(x_121)) {
lean_ctor_release(x_121, 0);
lean_ctor_release(x_121, 1);
x_124 = x_121;
lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119;
x_108 = lean_ctor_get(x_107, 0);
lean_inc(x_108);
x_109 = lean_ctor_get(x_107, 1);
lean_inc(x_109);
if (lean_is_exclusive(x_107)) {
lean_ctor_release(x_107, 0);
lean_ctor_release(x_107, 1);
x_110 = x_107;
} else {
lean_dec_ref(x_121);
x_124 = lean_box(0);
lean_dec_ref(x_107);
x_110 = lean_box(0);
}
x_125 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__2;
x_126 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_126, 0, x_125);
lean_ctor_set(x_126, 1, x_122);
x_127 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__8;
x_128 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_128, 0, x_126);
lean_ctor_set(x_128, 1, x_127);
x_129 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_129, 0, x_128);
lean_ctor_set(x_129, 1, x_15);
x_130 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__4;
x_131 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_131, 0, x_129);
lean_ctor_set(x_131, 1, x_130);
x_132 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_132, 0, x_131);
if (lean_is_scalar(x_124)) {
x_133 = lean_alloc_ctor(0, 2, 0);
x_111 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__2;
x_112 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_112, 0, x_111);
lean_ctor_set(x_112, 1, x_108);
x_113 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__8;
x_114 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_114, 0, x_112);
lean_ctor_set(x_114, 1, x_113);
x_115 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_115, 0, x_114);
lean_ctor_set(x_115, 1, x_15);
x_116 = l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___closed__4;
x_117 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_117, 0, x_115);
lean_ctor_set(x_117, 1, x_116);
x_118 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_118, 0, x_117);
if (lean_is_scalar(x_110)) {
x_119 = lean_alloc_ctor(0, 2, 0);
} else {
x_133 = x_124;
x_119 = x_110;
}
lean_ctor_set(x_133, 0, x_132);
lean_ctor_set(x_133, 1, x_123);
return x_133;
lean_ctor_set(x_119, 0, x_118);
lean_ctor_set(x_119, 1, x_109);
return x_119;
}
else
{
lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137;
lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123;
lean_dec(x_15);
x_134 = lean_ctor_get(x_121, 0);
lean_inc(x_134);
x_135 = lean_ctor_get(x_121, 1);
lean_inc(x_135);
if (lean_is_exclusive(x_121)) {
lean_ctor_release(x_121, 0);
lean_ctor_release(x_121, 1);
x_136 = x_121;
x_120 = lean_ctor_get(x_107, 0);
lean_inc(x_120);
x_121 = lean_ctor_get(x_107, 1);
lean_inc(x_121);
if (lean_is_exclusive(x_107)) {
lean_ctor_release(x_107, 0);
lean_ctor_release(x_107, 1);
x_122 = x_107;
} else {
lean_dec_ref(x_121);
x_136 = lean_box(0);
lean_dec_ref(x_107);
x_122 = lean_box(0);
}
if (lean_is_scalar(x_136)) {
x_137 = lean_alloc_ctor(1, 2, 0);
if (lean_is_scalar(x_122)) {
x_123 = lean_alloc_ctor(1, 2, 0);
} else {
x_137 = x_136;
x_123 = x_122;
}
lean_ctor_set(x_137, 0, x_134);
lean_ctor_set(x_137, 1, x_135);
return x_137;
lean_ctor_set(x_123, 0, x_120);
lean_ctor_set(x_123, 1, x_121);
return x_123;
}
}
}
}
else
{
uint8_t x_138;
uint8_t x_124;
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_138 = !lean_is_exclusive(x_14);
if (x_138 == 0)
x_124 = !lean_is_exclusive(x_14);
if (x_124 == 0)
{
return x_14;
}
else
{
lean_object* x_139; lean_object* x_140; lean_object* x_141;
x_139 = lean_ctor_get(x_14, 0);
x_140 = lean_ctor_get(x_14, 1);
lean_inc(x_140);
lean_inc(x_139);
lean_object* x_125; lean_object* x_126; lean_object* x_127;
x_125 = lean_ctor_get(x_14, 0);
x_126 = lean_ctor_get(x_14, 1);
lean_inc(x_126);
lean_inc(x_125);
lean_dec(x_14);
x_141 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_141, 0, x_139);
lean_ctor_set(x_141, 1, x_140);
return x_141;
x_127 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_127, 0, x_125);
lean_ctor_set(x_127, 1, x_126);
return x_127;
}
}
}
else
{
uint8_t x_142;
uint8_t x_128;
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_142 = !lean_is_exclusive(x_8);
if (x_142 == 0)
x_128 = !lean_is_exclusive(x_8);
if (x_128 == 0)
{
return x_8;
}
else
{
lean_object* x_143; lean_object* x_144; lean_object* x_145;
x_143 = lean_ctor_get(x_8, 0);
x_144 = lean_ctor_get(x_8, 1);
lean_inc(x_144);
lean_inc(x_143);
lean_object* x_129; lean_object* x_130; lean_object* x_131;
x_129 = lean_ctor_get(x_8, 0);
x_130 = lean_ctor_get(x_8, 1);
lean_inc(x_130);
lean_inc(x_129);
lean_dec(x_8);
x_145 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_145, 0, x_143);
lean_ctor_set(x_145, 1, x_144);
return x_145;
x_131 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_131, 0, x_129);
lean_ctor_set(x_131, 1, x_130);
return x_131;
}
}
}