From 7cb67bb123e98c47c8f03fdb2597922a78e2111a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Aug 2022 15:57:45 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/Lean/DocString.lean | 8 +- stage0/src/Lean/Elab/App.lean | 9 +- stage0/src/Lean/Elab/BuiltinNotation.lean | 18 +- stage0/src/Lean/Elab/Do.lean | 20 +- stage0/src/Lean/Meta/ExprDefEq.lean | 32 +- stage0/src/Lean/Server/InfoUtils.lean | 7 +- stage0/stdlib/Lean/DocString.c | 239 ++++---- stage0/stdlib/Lean/Elab/App.c | 78 +-- stage0/stdlib/Lean/Elab/BuiltinNotation.c | 40 +- stage0/stdlib/Lean/Elab/Do.c | 339 +++++++----- stage0/stdlib/Lean/Meta/ExprDefEq.c | 386 ++++++++----- stage0/stdlib/Lean/Server/InfoUtils.c | 641 +++++++++++----------- 12 files changed, 992 insertions(+), 825 deletions(-) diff --git a/stage0/src/Lean/DocString.lean b/stage0/src/Lean/DocString.lean index a9e16fefea..7e02121fa4 100644 --- a/stage0/src/Lean/DocString.lean +++ b/stage0/src/Lean/DocString.lean @@ -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 diff --git a/stage0/src/Lean/Elab/App.lean b/stage0/src/Lean/Elab/App.lean index 5e36d8ad6c..c4174d35b7 100644 --- a/stage0/src/Lean/Elab/App.lean +++ b/stage0/src/Lean/Elab/App.lean @@ -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 diff --git a/stage0/src/Lean/Elab/BuiltinNotation.lean b/stage0/src/Lean/Elab/BuiltinNotation.lean index 071f412d42..d61b686cc5 100644 --- a/stage0/src/Lean/Elab/BuiltinNotation.lean +++ b/stage0/src/Lean/Elab/BuiltinNotation.lean @@ -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 diff --git a/stage0/src/Lean/Elab/Do.lean b/stage0/src/Lean/Elab/Do.lean index eacf74b51c..1cd02b9a16 100644 --- a/stage0/src/Lean/Elab/Do.lean +++ b/stage0/src/Lean/Elab/Do.lean @@ -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 diff --git a/stage0/src/Lean/Meta/ExprDefEq.lean b/stage0/src/Lean/Meta/ExprDefEq.lean index 611f3d2fc3..9bc18d59fc 100644 --- a/stage0/src/Lean/Meta/ExprDefEq.lean +++ b/stage0/src/Lean/Meta/ExprDefEq.lean @@ -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. diff --git a/stage0/src/Lean/Server/InfoUtils.lean b/stage0/src/Lean/Server/InfoUtils.lean index b31b8389aa..2bd0feddfc 100644 --- a/stage0/src/Lean/Server/InfoUtils.lean +++ b/stage0/src/Lean/Server/InfoUtils.lean @@ -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} ```" diff --git a/stage0/stdlib/Lean/DocString.c b/stage0/stdlib/Lean/DocString.c index e05a192507..956b9f1b84 100644 --- a/stage0/stdlib/Lean/DocString.c +++ b/stage0/stdlib/Lean/DocString.c @@ -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); diff --git a/stage0/stdlib/Lean/Elab/App.c b/stage0/stdlib/Lean/Elab/App.c index 1cf79776ca..6b8ea1d740 100644 --- a/stage0/stdlib/Lean/Elab/App.c +++ b/stage0/stdlib/Lean/Elab/App.c @@ -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); diff --git a/stage0/stdlib/Lean/Elab/BuiltinNotation.c b/stage0/stdlib/Lean/Elab/BuiltinNotation.c index 080bc4beb3..f7cc245fd0 100644 --- a/stage0/stdlib/Lean/Elab/BuiltinNotation.c +++ b/stage0/stdlib/Lean/Elab/BuiltinNotation.c @@ -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); diff --git a/stage0/stdlib/Lean/Elab/Do.c b/stage0/stdlib/Lean/Elab/Do.c index 6c31db6eeb..d52ccd4143 100644 --- a/stage0/stdlib/Lean/Elab/Do.c +++ b/stage0/stdlib/Lean/Elab/Do.c @@ -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(); diff --git a/stage0/stdlib/Lean/Meta/ExprDefEq.c b/stage0/stdlib/Lean/Meta/ExprDefEq.c index 4c7b37bb8b..b88260c384 100644 --- a/stage0/stdlib/Lean/Meta/ExprDefEq.c +++ b/stage0/stdlib/Lean/Meta/ExprDefEq.c @@ -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)); diff --git a/stage0/stdlib/Lean/Server/InfoUtils.c b/stage0/stdlib/Lean/Server/InfoUtils.c index 99d448eb2a..b0d771e9fb 100644 --- a/stage0/stdlib/Lean/Server/InfoUtils.c +++ b/stage0/stdlib/Lean/Server/InfoUtils.c @@ -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; } } }