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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-15 09:46:23 -07:00
parent a57403be6e
commit 33a7f75599
27 changed files with 5969 additions and 4415 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
stage0/src/Init/Control/Except.lean generated
View file

@ -145,6 +145,11 @@ instance (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (Excep
restoreM x := x
class MonadFinally (m : Type u → Type v) where
/-- `tryFinally' x f` runs `x` and then the "finally" computation `f`.
When `x` succeeds with `a : α`, `f (some a)` is returned. If `x` fails
for `m`'s definition of failure, `f none` is returned. Hence `tryFinally'`
can be thought of as performing the same role as a `finally` block in
an imperative programming language. -/
tryFinally' {α β} : m α → (Option α → m β) → m (α × β)
export MonadFinally (tryFinally')

11
stage0/src/Init/Notation.lean generated
View file

@ -348,8 +348,15 @@ macro "try " t:tacticSeq : tactic => `(first | $t | skip)
/-- `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal, concatenating all goals produced by `tac'`. -/
macro:1 x:tactic " <;> " y:tactic:0 : tactic => `(tactic| focus ($x:tactic; all_goals $y:tactic))
/-- `rfl` is equivalent to `exact rfl`, but has a few optimizatons. -/
syntax (name := refl) "rfl" : tactic
/-- `eq_refl` is equivalent to `exact rfl`, but has a few optimizatons. -/
syntax (name := refl) "eq_refl" : tactic
/--
This tactic tries to close the current goal using reflexivity.
This is supposed to be an extensible tactic and users can add their own support
to new reflexive relations.
-/
macro "rfl" : tactic => `(eq_refl)
/--
Similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,

21
stage0/src/Lean/Compiler/CSimpAttr.lean generated
View file

@ -13,15 +13,22 @@ namespace CSimp
structure Entry where
fromDeclName : Name
toDeclName : Name
thmName : Name
deriving Inhabited
abbrev State := SMap Name Name
structure State where
map : SMap Name Name := {}
thmNames : SSet Name := {}
deriving Inhabited
def State.switch : State → State
| { map, thmNames } => { map := map.switch, thmNames := thmNames.switch }
builtin_initialize ext : SimpleScopedEnvExtension Entry State ←
registerSimpleScopedEnvExtension {
name := `csimp
initial := {}
addEntry := fun s { fromDeclName, toDeclName } => s.insert fromDeclName toDeclName
addEntry := fun { map, thmNames } { fromDeclName, toDeclName, thmName } => { map := map.insert fromDeclName toDeclName, thmNames := thmNames.insert thmName }
finalizeImport := fun s => s.switch
}
@ -30,7 +37,7 @@ private def isConstantReplacement? (declName : Name) : CoreM (Option Entry) := d
match info.type.eq? with
| some (_, Expr.const fromDeclName us .., Expr.const toDeclName vs ..) =>
if us == vs then
return some { fromDeclName, toDeclName }
return some { fromDeclName, toDeclName, thmName := declName }
else
return none
| _ => return none
@ -52,14 +59,18 @@ builtin_initialize
@[export lean_csimp_replace_constants]
def replaceConstants (env : Environment) (e : Expr) : Expr :=
let map := ext.getState env
let s := ext.getState env
e.replace fun e =>
if e.isConst then
match map.find? e.constName! with
match s.map.find? e.constName! with
| some declNameNew => some (mkConst declNameNew e.constLevels!)
| none => none
else
none
end CSimp
def hasCSimpAttribute (env : Environment) (declName : Name) : Bool :=
CSimp.ext.getState env |>.thmNames.contains declName
end Lean.Compiler

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

@ -131,7 +131,7 @@ At runtime, `msg` and the file position are printed to stderr unless the C
function `lean_set_panic_messages(false)` has been executed before. If the C
function `lean_set_exit_on_panic(true)` has been executed before, the process is
then aborted. -/
@[builtinTermElab panic] def elabPanic : TermElab := fun stx expectedType? => do
@[builtinTermElab Lean.Parser.Term.panic] def elabPanic : TermElab := fun stx expectedType? => do
let arg := stx[1]
let pos ← getRefPosition
let env ← getEnv

101
stage0/src/Lean/Elab/InfoTree.lean generated
View file

@ -15,7 +15,7 @@ namespace Lean.Elab
open Std (PersistentArray PersistentArray.empty PersistentHashMap)
/- Context after executing `liftTermElabM`.
/-- Context after executing `liftTermElabM`.
Note that the term information collected during elaboration may contain metavariables, and their
assignments are stored at `mctx`. -/
structure ContextInfo where
@ -70,9 +70,11 @@ structure FieldInfo where
stx : Syntax
deriving Inhabited
/- We store the list of goals before and after the execution of a tactic.
We also store the metavariable context at each time since, we want to unassigned metavariables
at tactic execution time to be displayed as `?m...`. -/
/-- The information needed to render the tactic state in the infoview.
We store the list of goals before and after the execution of a tactic.
We also store the metavariable context at each time since we want metavariables
unassigned at tactic execution time to be displayed as `?m...`. -/
structure TacticInfo extends ElabInfo where
mctxBefore : MetavarContext
goalsBefore : List MVarId
@ -86,6 +88,17 @@ structure MacroExpansionInfo where
output : Syntax
deriving Inhabited
structure CustomInfo where
stx : Syntax
json : Json
deriving Inhabited
def CustomInfo.format : CustomInfo → Format
| i => Std.ToFormat.format i.json
instance : ToFormat CustomInfo := ⟨CustomInfo.format⟩
/-- Header information for a node in `InfoTree`. -/
inductive Info where
| ofTacticInfo (i : TacticInfo)
| ofTermInfo (i : TermInfo)
@ -93,13 +106,39 @@ inductive Info where
| ofMacroExpansionInfo (i : MacroExpansionInfo)
| ofFieldInfo (i : FieldInfo)
| ofCompletionInfo (i : CompletionInfo)
| ofCustomInfo (i : CustomInfo)
deriving Inhabited
/-- The InfoTree is a structure that is generated during elaboration and used
by the language server to look up information about objects at particular points
in the Lean document. For example, tactic information and expected type information in
the infoview and information about completions.
The infotree consists of nodes which may have child nodes. Each node
has an `Info` object that contains details about what kind of information
is present. Each `Info` object also contains a `Syntax` instance, this is used to
map positions in the Lean document to particular info objects.
An example of a function that extracts information from an infotree for a given
position is `InfoTree.goalsAt?` which finds `TacticInfo`.
Information concerning expressions requires that a context also be saved.
`context` nodes store a local context that is used to process expressions
in nodes below.
Because the info tree is generated during elaboration, some parts of the infotree
for a particular piece of syntax may not be ready yet. Hence InfoTree supports metavariable-like
`hole`s which are filled in later in the same way that unassigned metavariables are.
-/
inductive InfoTree where
| context (i : ContextInfo) (t : InfoTree) -- The context object is created by `liftTermElabM` at `Command.lean`
| node (i : Info) (children : PersistentArray InfoTree) -- The children contains information for nested term elaboration and tactic evaluation
| ofJson (j : Json) -- For user data
| hole (mvarId : MVarId) -- The elaborator creates holes (aka metavariables) for tactics and postponed terms
| /-- The context object is created by `liftTermElabM` at `Command.lean` -/
context (i : ContextInfo) (t : InfoTree)
| /-- The children contain information for nested term elaboration and tactic evaluation -/
node (i : Info) (children : PersistentArray InfoTree)
| /-- For user data. -/
ofJson (j : Json)
| /-- The elaborator creates holes (aka metavariables) for tactics and postponed terms -/
hole (mvarId : MVarId)
deriving Inhabited
partial def InfoTree.findInfo? (p : Info → Bool) (t : InfoTree) : Option Info :=
@ -112,9 +151,22 @@ partial def InfoTree.findInfo? (p : Info → Bool) (t : InfoTree) : Option Info
ts.findSome? (findInfo? p)
| _ => none
/-- This structure is the state that is being used to build an InfoTree object.
During elaboration, some parts of the info tree may be `holes` which need to be filled later.
The `assignments` field is used to assign these holes.
The `trees` field is a list of pending child trees for the infotree node currently being built.
You should not need to use `InfoState` directly, instead infotrees should be built with the help of the methods here
such as `pushInfoLeaf` to create leaf nodes and `withInfoContext` to create a nested child node.
To see how `trees` is used, look at the function body of `withInfoContext'`.
-/
structure InfoState where
enabled : Bool := false -- whether info trees should be recorded
assignment : PersistentHashMap MVarId InfoTree := {} -- map from holeId to InfoTree
/-- Whether info trees should be recorded. -/
enabled : Bool := false
/-- Map from holes in the infotree to child infotrees. -/
assignment : PersistentHashMap MVarId InfoTree := {}
/-- Pending child trees of a node. -/
trees : PersistentArray InfoTree := {}
deriving Inhabited
@ -128,6 +180,8 @@ instance [MonadLift m n] [MonadInfoTree m] : MonadInfoTree n where
getInfoState := liftM (getInfoState : m _)
modifyInfoState f := liftM (modifyInfoState f : m _)
/-- Instantiate the holes on the given `tree` with the assignment table.
(analoguous to instantiating the metavariables in an expression) -/
partial def InfoTree.substitute (tree : InfoTree) (assignment : PersistentHashMap MVarId InfoTree) : InfoTree :=
match tree with
| node i c => node i <| c.map (substitute · assignment)
@ -214,6 +268,7 @@ def Info.format (ctx : ContextInfo) : Info → IO Format
| ofMacroExpansionInfo i => i.format ctx
| ofFieldInfo i => i.format ctx
| ofCompletionInfo i => i.format ctx
| ofCustomInfo i => pure <| Std.ToFormat.format i
def Info.toElabInfo? : Info → Option ElabInfo
| ofTacticInfo i => some i.toElabInfo
@ -222,6 +277,7 @@ def Info.toElabInfo? : Info → Option ElabInfo
| ofMacroExpansionInfo i => none
| ofFieldInfo i => none
| ofCompletionInfo i => none
| ofCustomInfo i => none
/--
Helper function for propagating the tactic metavariable context to its children nodes.
@ -262,6 +318,7 @@ variable [Monad m] [MonadInfoTree m]
@[inline] private def modifyInfoTrees (f : PersistentArray InfoTree → PersistentArray InfoTree) : m Unit :=
modifyInfoState fun s => { s with trees := f s.trees }
/-- Returns the current array of InfoTrees and resets it to an empty array. -/
def getResetInfoTrees : m (PersistentArray InfoTree) := do
let trees := (← getInfoState).trees
modifyInfoTrees fun _ => {}
@ -278,6 +335,10 @@ def pushInfoLeaf (t : Info) : m Unit := do
def addCompletionInfo (info : CompletionInfo) : m Unit := do
pushInfoLeaf <| Info.ofCompletionInfo info
/-- This does the same job as resolveGlobalConstNoOverload; resolving an identifier
syntax to a unique fully resolved name or throwing if there are ambiguities.
But also adds this resolved name to the infotree. This means that when you hover
over a name in the sourcefile you will see the fully resolved name in the hover info.-/
def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) (expectedType? : Option Expr := none) : m Name := do
let n ← resolveGlobalConstNoOverload id
if (← getInfoState).enabled then
@ -285,6 +346,7 @@ def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [Mona
pushInfoLeaf <| Info.ofTermInfo { elaborator := Name.anonymous, lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx := id, expectedType? }
return n
/-- Similar to resolveGlobalConstNoOverloadWithInfo, except if there are multiple name resolutions then it returns them as a list. -/
def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) (expectedType? : Option Expr := none) : m (List Name) := do
let ns ← resolveGlobalConst id
if (← getInfoState).enabled then
@ -292,6 +354,12 @@ def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m]
pushInfoLeaf <| Info.ofTermInfo { elaborator := Name.anonymous, lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx := id, expectedType? }
return ns
/-- Use this to descend a node on the infotree that is being built.
It saves the current list of trees `t₀` and resets it and then runs `x >>= mkInfo`, producing either an `i : Info` or a hole id.
Running `x >>= mkInfo` will modify the trees state and produce a new list of trees `t₁`.
In the `i : Info` case, `t₁` become the children of a node `node i t₁` that is appended to `t₀`.
-/
def withInfoContext' [MonadFinally m] (x : m α) (mkInfo : α → m (Sum Info MVarId)) : m α := do
if (← getInfoState).enabled then
let treesSaved ← getResetInfoTrees
@ -307,6 +375,8 @@ def withInfoContext' [MonadFinally m] (x : m α) (mkInfo : α → m (Sum Info MV
else
x
/-- Saves the current list of trees `t₀`, runs `x` to produce a new tree list `t₁` and
runs `mkInfoTree t₁` to get `n : InfoTree` and then restores the trees to be `t₀ ++ [n]`.-/
def withInfoTreeContext [MonadFinally m] (x : m α) (mkInfoTree : PersistentArray InfoTree → m InfoTree) : m α := do
if (← getInfoState).enabled then
let treesSaved ← getResetInfoTrees
@ -317,9 +387,13 @@ def withInfoTreeContext [MonadFinally m] (x : m α) (mkInfoTree : PersistentArra
else
x
/-- Run `x` as a new child infotree node with header given by `mkInfo`. -/
@[inline] def withInfoContext [MonadFinally m] (x : m α) (mkInfo : m Info) : m α := do
withInfoTreeContext x (fun trees => do return InfoTree.node (← mkInfo) trees)
/-- Resets the trees state `t₀`, runs `x` to produce a new trees
state `t₁` and sets the state to be `t₀ ++ (InfoTree.context Γ <$> t₁)`
where `Γ` is the context derived from the monad state. -/
def withSaveInfoContext [MonadFinally m] [MonadEnv m] [MonadOptions m] [MonadMCtx m] [MonadResolveName m] [MonadFileMap m] (x : m α) : m α := do
if (← getInfoState).enabled then
let treesSaved ← getResetInfoTrees
@ -328,7 +402,12 @@ def withSaveInfoContext [MonadFinally m] [MonadEnv m] [MonadOptions m] [MonadMCt
let trees ← st.trees.mapM fun tree => do
let tree := tree.substitute st.assignment
pure <| InfoTree.context {
env := (← getEnv), fileMap := (← getFileMap), mctx := (← getMCtx), currNamespace := (← getCurrNamespace), openDecls := (← getOpenDecls), options := (← getOptions)
env := (← getEnv)
fileMap := (← getFileMap)
mctx := (← getMCtx)
currNamespace := (← getCurrNamespace)
openDecls := (← getOpenDecls)
options := (← getOptions)
} tree
modifyInfoTrees fun _ => treesSaved ++ trees
else

1
stage0/src/Lean/Elab/Quotation.lean generated
View file

@ -194,6 +194,7 @@ elab_stx_quot Parser.Term.attr.quot
elab_stx_quot Parser.Term.prio.quot
elab_stx_quot Parser.Term.doElem.quot
elab_stx_quot Parser.Term.dynamicQuot
elab_stx_quot Parser.Command.quot
/- match -/

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

@ -9,17 +9,19 @@ import Lean.Parser.Do
namespace Lean
namespace Parser
/--
Syntax quotation for terms and (lists of) commands. We prefer terms, so ambiguous quotations like
`` `($x $y) `` will be parsed as an application, not two commands. Use `` `($x:command $y:command) `` instead.
Multiple command will be put in a `` `null `` node, but a single command will not (so that you can directly
match against a quotation in a command kind's elaborator). -/
-- TODO: use two separate quotation parsers with parser priorities instead
@[builtinTermParser] def Term.quot := leading_parser "`(" >> incQuotDepth (termParser <|> many1Unbox commandParser) >> ")"
/-- Syntax quotation for terms. -/
@[builtinTermParser] def Term.quot := leading_parser "`(" >> incQuotDepth termParser >> ")"
@[builtinTermParser] def Term.precheckedQuot := leading_parser "`" >> Term.quot
namespace Command
/--
Syntax quotation for (sequences of) commands. The identical syntax for term quotations takes priority, so ambiguous quotations like
`` `($x $y) `` will be parsed as an application, not two commands. Use `` `($x:command $y:command) `` instead.
Multiple commands will be put in a `` `null `` node, but a single command will not (so that you can directly
match against a quotation in a command kind's elaborator). -/
@[builtinTermParser low] def quot := leading_parser "`(" >> incQuotDepth (many1Unbox commandParser) >> ")"
/--
A mutual block may be broken in different cliques, we identify them using an `ident` (an element of the clique)
We provide two kinds of hints to the termination checker:

2
stage0/src/Lean/Parser/Extension.lean generated
View file

@ -404,6 +404,8 @@ def addSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Environment :=
def isValidSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Bool :=
let kinds := (parserExtension.getState env).kinds
-- accept any constant in stage 1 (i.e. when compiled by stage 0) so that
-- we can add a built-in parser and its elaborator in the same stage
kinds.contains k || (Internal.isStage0 () && env.contains k)
def getSyntaxNodeKinds (env : Environment) : List SyntaxNodeKind :=

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

@ -74,6 +74,7 @@ def Info.stx : Info → Syntax
| ofMacroExpansionInfo i => i.stx
| ofFieldInfo i => i.stx
| ofCompletionInfo i => i.stx
| ofCustomInfo i => i.stx
def Info.lctx : Info → LocalContext
| Info.ofTermInfo i => i.lctx

2
stage0/stdlib/Init/Conv.c generated
View file

@ -5823,7 +5823,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macro
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("refl");
x_1 = lean_mk_string("tacticRfl");
return x_1;
}
}

193
stage0/stdlib/Init/Notation.c generated
View file

@ -127,6 +127,7 @@ static lean_object* l_stx___x3c_x7c_x3e_____closed__2;
static lean_object* l_Lean_Parser_Tactic_induction___closed__12;
static lean_object* l_term___xd7_____closed__5;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__Bind__bind__1___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticRfl;
static lean_object* l_Lean_Parser_Tactic_generalize___closed__2;
static lean_object* l_Lean_termThis___closed__3;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_rwSeq;
@ -840,11 +841,13 @@ static lean_object* l_term___x2f_____closed__3;
static lean_object* l_Lean_Parser_Tactic_discharger___closed__9;
static lean_object* l_Lean_Parser_Syntax_subPrio___closed__3;
LEAN_EXPORT lean_object* l_term___x3a_x3a__;
static lean_object* l_Lean_Parser_Tactic_tacticRfl___closed__5;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticAdmit;
static lean_object* l_Lean_Parser_Tactic_location___closed__1;
static lean_object* l_termDepIfThenElse___closed__34;
static lean_object* l___aux__Init__Notation______macroRules__term___x2b____1___closed__5;
static lean_object* l_prec_x28___x29___closed__1;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticRfl__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Syntax_addPrio___closed__3;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticTrivial__5(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_prioLow;
@ -946,6 +949,7 @@ LEAN_EXPORT lean_object* l_prio_x28___x29;
LEAN_EXPORT lean_object* l_term___x2d__;
static lean_object* l_term___x5c_x2f_____closed__2;
static lean_object* l___aux__Init__Notation______macroRules__term_x7e_x7e_x7e____1___closed__1;
static lean_object* l_Lean_Parser_Tactic_tacticRfl___closed__3;
static lean_object* l_Lean_Parser_Tactic_simpAll___closed__6;
static lean_object* l___aux__Init__Notation______macroRules__stx___x2b__1___closed__5;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__precArg__1(lean_object*, lean_object*, lean_object*);
@ -1177,6 +1181,7 @@ LEAN_EXPORT lean_object* l_termIfThenElse;
static lean_object* l_Lean_Parser_Tactic_injection___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__termWithout__expected__type____1___closed__10;
static lean_object* l___aux__Init__Notation______macroRules__term___x5c_x2f____1___closed__5;
static lean_object* l_Lean_Parser_Tactic_tacticRfl___closed__4;
static lean_object* l_term___x3e_____closed__2;
static lean_object* l___aux__Init__Notation______macroRules__stx___x2a__1___closed__2;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticHave_x27__;
@ -1359,6 +1364,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticLet__;
static lean_object* l_term_x25_x5b___x7c___x5d___closed__9;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__GT__gt__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a_x3e____1___closed__15;
static lean_object* l_Lean_Parser_Tactic_tacticRfl___closed__1;
static lean_object* l_Lean_Parser_Tactic_intros___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term_xac____1___closed__3;
static lean_object* l_termIfThenElse___closed__7;
@ -1609,6 +1615,7 @@ static lean_object* l_Lean_Parser_Tactic_case___closed__9;
static lean_object* l_Lean_Parser_Tactic_tacticTry_____closed__6;
static lean_object* l___aux__Init__Notation______macroRules__term_x7e_x7e_x7e____1___closed__9;
static lean_object* l_term___x26_x26_____closed__7;
static lean_object* l_Lean_Parser_Tactic_tacticRfl___closed__2;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__termWithout__expected__type____1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_letrec;
static lean_object* l___aux__Init__Notation______macroRules__term___x3e_x3e____1___closed__4;
@ -34314,7 +34321,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_refl___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("rfl");
x_1 = lean_mk_string("eq_refl");
return x_1;
}
}
@ -34352,6 +34359,158 @@ x_1 = l_Lean_Parser_Tactic_refl___closed__5;
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticRfl___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("tacticRfl");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticRfl___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_intro___closed__2;
x_2 = l_Lean_Parser_Tactic_tacticRfl___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticRfl___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("rfl");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticRfl___closed__4() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_tacticRfl___closed__3;
x_2 = 0;
x_3 = lean_alloc_ctor(6, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticRfl___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_tacticRfl___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_tacticRfl___closed__4;
x_4 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticRfl() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_tacticRfl___closed__5;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticRfl__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = l_Lean_Parser_Tactic_tacticRfl___closed__2;
x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7;
lean_dec(x_2);
x_6 = lean_box(1);
x_7 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_3);
return x_7;
}
else
{
lean_object* x_8; uint8_t x_9;
x_8 = l_Lean_MonadRef_mkInfoFromRefPos___at___aux__Init__Notation______macroRules__precMax__1___spec__1(x_2, x_3);
x_9 = !lean_is_exclusive(x_8);
if (x_9 == 0)
{
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;
x_10 = lean_ctor_get(x_8, 0);
x_11 = l_Lean_Parser_Tactic_refl___closed__3;
x_12 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
x_13 = l___aux__Init__Notation______macroRules__precMax__1___closed__4;
x_14 = lean_array_push(x_13, x_12);
x_15 = lean_box(2);
x_16 = l_Lean_Parser_Tactic_refl___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_array_push(x_13, x_17);
x_19 = l___aux__Init__Notation______macroRules__stx___x2b__1___closed__8;
x_20 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_20, 0, x_15);
lean_ctor_set(x_20, 1, x_19);
lean_ctor_set(x_20, 2, x_18);
x_21 = lean_array_push(x_13, x_20);
x_22 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticTry____1___closed__2;
x_23 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_23, 0, x_15);
lean_ctor_set(x_23, 1, x_22);
lean_ctor_set(x_23, 2, x_21);
lean_ctor_set(x_8, 0, x_23);
return x_8;
}
else
{
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; lean_object* x_39;
x_24 = lean_ctor_get(x_8, 0);
x_25 = lean_ctor_get(x_8, 1);
lean_inc(x_25);
lean_inc(x_24);
lean_dec(x_8);
x_26 = l_Lean_Parser_Tactic_refl___closed__3;
x_27 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_27, 0, x_24);
lean_ctor_set(x_27, 1, x_26);
x_28 = l___aux__Init__Notation______macroRules__precMax__1___closed__4;
x_29 = lean_array_push(x_28, x_27);
x_30 = lean_box(2);
x_31 = l_Lean_Parser_Tactic_refl___closed__2;
x_32 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_32, 0, x_30);
lean_ctor_set(x_32, 1, x_31);
lean_ctor_set(x_32, 2, x_29);
x_33 = lean_array_push(x_28, x_32);
x_34 = l___aux__Init__Notation______macroRules__stx___x2b__1___closed__8;
x_35 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_35, 0, x_30);
lean_ctor_set(x_35, 1, x_34);
lean_ctor_set(x_35, 2, x_33);
x_36 = lean_array_push(x_28, x_35);
x_37 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticTry____1___closed__2;
x_38 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_38, 0, x_30);
lean_ctor_set(x_38, 1, x_37);
lean_ctor_set(x_38, 2, x_36);
x_39 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_39, 0, x_38);
lean_ctor_set(x_39, 1, x_25);
return x_39;
}
}
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticRfl_x27___closed__1() {
_start:
{
@ -34556,14 +34715,14 @@ lean_inc(x_10);
x_25 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_25, 0, x_10);
lean_ctor_set(x_25, 1, x_24);
x_26 = l_Lean_Parser_Tactic_refl___closed__3;
x_26 = l_Lean_Parser_Tactic_tacticRfl___closed__3;
x_27 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_27, 0, x_10);
lean_ctor_set(x_27, 1, x_26);
x_28 = l___aux__Init__Notation______macroRules__precMax__1___closed__4;
x_29 = lean_array_push(x_28, x_27);
x_30 = lean_box(2);
x_31 = l_Lean_Parser_Tactic_refl___closed__2;
x_31 = l_Lean_Parser_Tactic_tacticRfl___closed__2;
x_32 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_32, 0, x_30);
lean_ctor_set(x_32, 1, x_31);
@ -34691,14 +34850,14 @@ lean_inc(x_74);
x_90 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_90, 0, x_74);
lean_ctor_set(x_90, 1, x_89);
x_91 = l_Lean_Parser_Tactic_refl___closed__3;
x_91 = l_Lean_Parser_Tactic_tacticRfl___closed__3;
x_92 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_92, 0, x_74);
lean_ctor_set(x_92, 1, x_91);
x_93 = l___aux__Init__Notation______macroRules__precMax__1___closed__4;
x_94 = lean_array_push(x_93, x_92);
x_95 = lean_box(2);
x_96 = l_Lean_Parser_Tactic_refl___closed__2;
x_96 = l_Lean_Parser_Tactic_tacticRfl___closed__2;
x_97 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_97, 0, x_95);
lean_ctor_set(x_97, 1, x_96);
@ -36574,14 +36733,14 @@ goto block_94;
block_94:
{
lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; 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; 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; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93;
x_39 = l_Lean_Parser_Tactic_refl___closed__3;
x_39 = l_Lean_Parser_Tactic_tacticRfl___closed__3;
x_40 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_40, 0, x_38);
lean_ctor_set(x_40, 1, x_39);
x_41 = l___aux__Init__Notation______macroRules__precMax__1___closed__4;
x_42 = lean_array_push(x_41, x_40);
x_43 = lean_box(2);
x_44 = l_Lean_Parser_Tactic_refl___closed__2;
x_44 = l_Lean_Parser_Tactic_tacticRfl___closed__2;
x_45 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_45, 0, x_43);
lean_ctor_set(x_45, 1, x_44);
@ -43970,14 +44129,14 @@ if (x_9 == 0)
{
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_10 = lean_ctor_get(x_8, 0);
x_11 = l_Lean_Parser_Tactic_refl___closed__3;
x_11 = l_Lean_Parser_Tactic_tacticRfl___closed__3;
x_12 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
x_13 = l___aux__Init__Notation______macroRules__precMax__1___closed__4;
x_14 = lean_array_push(x_13, x_12);
x_15 = lean_box(2);
x_16 = l_Lean_Parser_Tactic_refl___closed__2;
x_16 = l_Lean_Parser_Tactic_tacticRfl___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);
@ -43993,14 +44152,14 @@ x_19 = lean_ctor_get(x_8, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_8);
x_20 = l_Lean_Parser_Tactic_refl___closed__3;
x_20 = l_Lean_Parser_Tactic_tacticRfl___closed__3;
x_21 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_21, 0, x_18);
lean_ctor_set(x_21, 1, x_20);
x_22 = l___aux__Init__Notation______macroRules__precMax__1___closed__4;
x_23 = lean_array_push(x_22, x_21);
x_24 = lean_box(2);
x_25 = l_Lean_Parser_Tactic_refl___closed__2;
x_25 = l_Lean_Parser_Tactic_tacticRfl___closed__2;
x_26 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_26, 0, x_24);
lean_ctor_set(x_26, 1, x_25);
@ -48248,6 +48407,18 @@ l_Lean_Parser_Tactic_refl___closed__5 = _init_l_Lean_Parser_Tactic_refl___closed
lean_mark_persistent(l_Lean_Parser_Tactic_refl___closed__5);
l_Lean_Parser_Tactic_refl = _init_l_Lean_Parser_Tactic_refl();
lean_mark_persistent(l_Lean_Parser_Tactic_refl);
l_Lean_Parser_Tactic_tacticRfl___closed__1 = _init_l_Lean_Parser_Tactic_tacticRfl___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticRfl___closed__1);
l_Lean_Parser_Tactic_tacticRfl___closed__2 = _init_l_Lean_Parser_Tactic_tacticRfl___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticRfl___closed__2);
l_Lean_Parser_Tactic_tacticRfl___closed__3 = _init_l_Lean_Parser_Tactic_tacticRfl___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticRfl___closed__3);
l_Lean_Parser_Tactic_tacticRfl___closed__4 = _init_l_Lean_Parser_Tactic_tacticRfl___closed__4();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticRfl___closed__4);
l_Lean_Parser_Tactic_tacticRfl___closed__5 = _init_l_Lean_Parser_Tactic_tacticRfl___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticRfl___closed__5);
l_Lean_Parser_Tactic_tacticRfl = _init_l_Lean_Parser_Tactic_tacticRfl();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticRfl);
l_Lean_Parser_Tactic_tacticRfl_x27___closed__1 = _init_l_Lean_Parser_Tactic_tacticRfl_x27___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticRfl_x27___closed__1);
l_Lean_Parser_Tactic_tacticRfl_x27___closed__2 = _init_l_Lean_Parser_Tactic_tacticRfl_x27___closed__2();

806
stage0/stdlib/Lean/Compiler/CSimpAttr.c generated
View file

File diff suppressed because it is too large Load diff

8
stage0/stdlib/Lean/Data/Lsp/Capabilities.c generated
View file

@ -33,7 +33,7 @@ static lean_object* l_Lean_Lsp_instToJsonTextDocumentClientCapabilities___closed
LEAN_EXPORT lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonCompletionClientCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_109____boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Lsp_instFromJsonServerCapabilities;
static lean_object* l_Lean_Lsp_instToJsonCompletionClientCapabilities___closed__1;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3427_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3429_(lean_object*);
LEAN_EXPORT uint8_t l_Lean_Lsp_ServerCapabilities_workspaceSymbolProvider___default;
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonCompletionClientCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_87____spec__1___boxed(lean_object*, lean_object*);
static lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_396____closed__2;
@ -48,7 +48,7 @@ LEAN_EXPORT uint8_t l_Lean_Lsp_ServerCapabilities_documentHighlightProvider___de
LEAN_EXPORT lean_object* l_Lean_Lsp_instToJsonCompletionClientCapabilities;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonCompletionOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_112_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonCompletionItemCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_18____spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3358_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3360_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Lsp_instFromJsonTextDocumentClientCapabilities;
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_396____spec__1(lean_object*, lean_object*);
static lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_396____closed__7;
@ -1209,7 +1209,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_obj
x_4 = lean_ctor_get(x_2, 0);
lean_inc(x_4);
lean_dec(x_2);
x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3427_(x_4);
x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3429_(x_4);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_5);
@ -1624,7 +1624,7 @@ return x_4;
else
{
lean_object* x_5;
x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3358_(x_3);
x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3360_(x_3);
lean_dec(x_3);
if (lean_obj_tag(x_5) == 0)
{

2764
stage0/stdlib/Lean/Data/Lsp/LanguageFeatures.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -268,6 +268,7 @@ static lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_toMessageList___
LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___lambda__2___boxed(lean_object**);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppAux___spec__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Elab_App_0__Lean_Elab_Term_addLValArg___spec__4___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__4;
lean_object* l_Lean_Elab_Term_elabLevel(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabPipeProj___lambda__1___closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_addInstMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -28588,22 +28589,32 @@ return x_10;
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("elabNamedPattern");
return x_1;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__7;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("elabNamedPattern");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Term_elabApp___closed__3;
x_2 = l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__1;
x_2 = l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__2;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__3() {
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__4() {
_start:
{
lean_object* x_1;
@ -28616,9 +28627,9 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Lean_Elab_Term_elabApp___closed__6;
x_3 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__8;
x_4 = l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__2;
x_5 = l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__3;
x_3 = l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__1;
x_4 = l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__3;
x_5 = l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__4;
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
@ -28635,7 +28646,7 @@ LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_elabNamedPattern_docStrin
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__2;
x_2 = l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__3;
x_3 = l___regBuiltin_Lean_Elab_Term_elabNamedPattern_docString___closed__1;
x_4 = l_Lean_addBuiltinDocString(x_2, x_3, x_1);
return x_4;
@ -28737,7 +28748,7 @@ LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_elabNamedPattern_declRang
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__2;
x_2 = l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__3;
x_3 = l___regBuiltin_Lean_Elab_Term_elabNamedPattern_declRange___closed__7;
x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1);
return x_4;
@ -30711,6 +30722,8 @@ l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__2 = _init_l___regBuilti
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__2);
l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__3 = _init_l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__3);
l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__4 = _init_l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__4();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabNamedPattern___closed__4);
res = l___regBuiltin_Lean_Elab_Term_elabNamedPattern(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

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

@ -9719,7 +9719,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(134u);
x_2 = lean_unsigned_to_nat(25u);
x_2 = lean_unsigned_to_nat(42u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -9743,7 +9743,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___regBuiltin_Lean_Elab_Term_elabPanic_declRange___closed__1;
x_2 = lean_unsigned_to_nat(25u);
x_2 = lean_unsigned_to_nat(42u);
x_3 = l___regBuiltin_Lean_Elab_Term_elabPanic_declRange___closed__2;
x_4 = lean_unsigned_to_nat(63u);
x_5 = lean_alloc_ctor(0, 4, 0);
@ -9759,7 +9759,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(134u);
x_2 = lean_unsigned_to_nat(29u);
x_2 = lean_unsigned_to_nat(46u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -9771,7 +9771,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(134u);
x_2 = lean_unsigned_to_nat(38u);
x_2 = lean_unsigned_to_nat(55u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -9783,9 +9783,9 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___regBuiltin_Lean_Elab_Term_elabPanic_declRange___closed__4;
x_2 = lean_unsigned_to_nat(29u);
x_2 = lean_unsigned_to_nat(46u);
x_3 = l___regBuiltin_Lean_Elab_Term_elabPanic_declRange___closed__5;
x_4 = lean_unsigned_to_nat(38u);
x_4 = lean_unsigned_to_nat(55u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);

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

@ -201,6 +201,7 @@ static lean_object* l_Lean_Elab_Deriving_DecEq_mkAuxFunction___closed__8;
LEAN_EXPORT lean_object* l_Lean_Elab_Deriving_DecEq_mkEnumOfNat(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Deriving_DecEq_mkAuxFunction___closed__13;
lean_object* l_Lean_Elab_addMacroStack___at_Lean_Elab_Term_instAddErrorMessageContextTermElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__73;
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_DecEq_mkMatch_mkAlts___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Deriving_DecEq_mkMatch_mkSameCtorRhs___lambda__1___closed__27;
static lean_object* l_Lean_Elab_Deriving_DecEq_mkMatch_mkSameCtorRhs___lambda__1___closed__32;
@ -8267,14 +8268,22 @@ return x_3;
static lean_object* _init_l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__68() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("tacticRfl");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__69() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Deriving_DecEq_mkMatch_mkSameCtorRhs___lambda__1___closed__24;
x_2 = l_Lean_Elab_Deriving_DecEq_mkEnumOfNatThm___closed__6;
x_2 = l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__68;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__69() {
static lean_object* _init_l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__70() {
_start:
{
lean_object* x_1;
@ -8282,17 +8291,17 @@ x_1 = lean_mk_string("contradiction");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__70() {
static lean_object* _init_l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__71() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Deriving_DecEq_mkMatch_mkSameCtorRhs___lambda__1___closed__24;
x_2 = l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__69;
x_2 = l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__70;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__71() {
static lean_object* _init_l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__72() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -8302,7 +8311,7 @@ x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__72() {
static lean_object* _init_l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__73() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -8769,7 +8778,7 @@ x_210 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_210, 0, x_21);
lean_ctor_set(x_210, 1, x_209);
x_211 = lean_array_push(x_40, x_210);
x_212 = l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__68;
x_212 = l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__69;
x_213 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_213, 0, x_42);
lean_ctor_set(x_213, 1, x_212);
@ -8912,12 +8921,12 @@ x_277 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_277, 0, x_42);
lean_ctor_set(x_277, 1, x_142);
lean_ctor_set(x_277, 2, x_276);
x_278 = l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__69;
x_278 = l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__70;
x_279 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_279, 0, x_21);
lean_ctor_set(x_279, 1, x_278);
x_280 = lean_array_push(x_40, x_279);
x_281 = l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__70;
x_281 = l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__71;
x_282 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_282, 0, x_42);
lean_ctor_set(x_282, 1, x_281);
@ -9011,7 +9020,7 @@ x_330 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_330, 0, x_42);
lean_ctor_set(x_330, 1, x_329);
lean_ctor_set(x_330, 2, x_328);
x_331 = l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__71;
x_331 = l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__72;
x_332 = lean_array_push(x_331, x_30);
x_333 = lean_array_push(x_332, x_169);
x_334 = lean_array_push(x_333, x_169);
@ -9024,7 +9033,7 @@ x_340 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_340, 0, x_42);
lean_ctor_set(x_340, 1, x_339);
lean_ctor_set(x_340, 2, x_338);
x_341 = l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__72;
x_341 = l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__73;
x_342 = lean_array_push(x_341, x_340);
x_343 = l_Lean_Elab_Deriving_DecEq_mkAuxFunction___closed__8;
x_344 = lean_alloc_ctor(1, 3, 0);
@ -10481,6 +10490,8 @@ l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__71 = _init_l_Lean_Elab_Deriving
lean_mark_persistent(l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__71);
l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__72 = _init_l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__72();
lean_mark_persistent(l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__72);
l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__73 = _init_l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__73();
lean_mark_persistent(l_Lean_Elab_Deriving_DecEq_mkDecEqEnum___closed__73);
l_Lean_Elab_Deriving_DecEq_initFn____x40_Lean_Elab_Deriving_DecEq___hyg_4574____closed__1 = _init_l_Lean_Elab_Deriving_DecEq_initFn____x40_Lean_Elab_Deriving_DecEq___hyg_4574____closed__1();
lean_mark_persistent(l_Lean_Elab_Deriving_DecEq_initFn____x40_Lean_Elab_Deriving_DecEq___hyg_4574____closed__1);
res = l_Lean_Elab_Deriving_DecEq_initFn____x40_Lean_Elab_Deriving_DecEq___hyg_4574_(lean_io_mk_world());

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

@ -122,6 +122,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_withInfoHole(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_withSaveInfoContext___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_ppGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instInhabitedCustomInfo___closed__1;
static lean_object* l_Lean_Elab_FieldInfo_format___lambda__1___closed__1;
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_Elab_assignInfoHoleId___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_withInfoTreeContext___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -267,6 +268,7 @@ static lean_object* l_Lean_Elab_InfoState_trees___default___closed__2;
LEAN_EXPORT lean_object* l_Lean_Elab_addCompletionInfo___rarg(lean_object*, lean_object*, lean_object*);
size_t lean_usize_land(size_t, size_t);
static size_t l_Std_PersistentHashMap_findAux___at_Lean_Elab_InfoTree_substitute___spec__7___closed__2;
LEAN_EXPORT lean_object* l_Lean_Elab_instInhabitedCustomInfo;
LEAN_EXPORT lean_object* l_Lean_Elab_withInfoTreeContext___at_Lean_Elab_withInfoContext___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_ContextInfo_mctx___default___closed__3;
LEAN_EXPORT lean_object* l_Std_PersistentArray_mapM___at_Lean_Elab_withSaveInfoContext___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -351,6 +353,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_withSaveInfoConte
LEAN_EXPORT lean_object* l_Lean_Elab_withInfoTreeContext___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_enableInfoTree___rarg___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Json_render(lean_object*);
static lean_object* l_Lean_Elab_CompletionInfo_format___closed__2;
LEAN_EXPORT lean_object* l_Std_PersistentArray_findSomeMAux___at_Lean_Elab_InfoTree_findInfo_x3f___spec__2(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_instInhabitedInfoState;
@ -364,6 +367,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_CompletionInfo_format(lean_object*, lean_ob
static lean_object* l_Lean_Elab_CompletionInfo_format___closed__4;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_InfoTree_substitute___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_CommandInfo_format___closed__1;
static lean_object* l_Lean_Elab_instToFormatCustomInfo___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_Info_updateContext_x3f___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__3;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_withSaveInfoContext___spec__5___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
@ -376,6 +380,7 @@ static lean_object* l_Lean_Elab_ContextInfo_runMetaM___rarg___closed__15;
extern lean_object* l_Lean_Expr_instBEqExpr;
LEAN_EXPORT lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_withInfoTreeContext___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_instToFormatCustomInfo;
static lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__1;
static lean_object* l_Lean_Elab_ContextInfo_mctx___default___closed__2;
LEAN_EXPORT lean_object* l_List_mapM___at_Lean_Elab_ContextInfo_ppGoals___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -416,6 +421,7 @@ LEAN_EXPORT uint8_t l_Lean_Elab_InfoState_enabled___default;
LEAN_EXPORT lean_object* l_Lean_Elab_withInfoContext_x27___rarg___lambda__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_PersistentArray_mapMAux___at_Lean_Elab_withSaveInfoContext___spec__2___rarg___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_withInfoHole___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_CustomInfo_format(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_withInfoHole___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_withInfoTreeContext___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_ContextInfo_runMetaM___rarg___closed__3;
@ -923,6 +929,53 @@ x_1 = l_Lean_Elab_instInhabitedMacroExpansionInfo___closed__1;
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_instInhabitedCustomInfo___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = lean_box(0);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_instInhabitedCustomInfo() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Elab_instInhabitedCustomInfo___closed__1;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_CustomInfo_format(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
lean_dec(x_1);
x_3 = l_Lean_Json_render(x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_instToFormatCustomInfo___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_CustomInfo_format), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_instToFormatCustomInfo() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Elab_instToFormatCustomInfo___closed__1;
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_instInhabitedInfo___closed__1() {
_start:
{
@ -4934,7 +4987,7 @@ lean_dec(x_2);
x_13 = l_Lean_Elab_FieldInfo_format(x_1, x_12, x_3);
return x_13;
}
default:
case 5:
{
lean_object* x_14; lean_object* x_15;
x_14 = lean_ctor_get(x_2, 0);
@ -4943,6 +4996,19 @@ lean_dec(x_2);
x_15 = l_Lean_Elab_CompletionInfo_format(x_1, x_14, x_3);
return x_15;
}
default:
{
lean_object* x_16; lean_object* x_17; lean_object* x_18;
lean_dec(x_1);
x_16 = lean_ctor_get(x_2, 0);
lean_inc(x_16);
lean_dec(x_2);
x_17 = l_Lean_Elab_CustomInfo_format(x_16);
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_3);
return x_18;
}
}
}
}
@ -8510,7 +8576,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_assignInfoHoleId___rarg___lambda__2___closed__4;
x_2 = l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__5;
x_3 = lean_unsigned_to_nat(341u);
x_3 = lean_unsigned_to_nat(420u);
x_4 = lean_unsigned_to_nat(2u);
x_5 = l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -9106,6 +9172,14 @@ l_Lean_Elab_instInhabitedMacroExpansionInfo___closed__1 = _init_l_Lean_Elab_inst
lean_mark_persistent(l_Lean_Elab_instInhabitedMacroExpansionInfo___closed__1);
l_Lean_Elab_instInhabitedMacroExpansionInfo = _init_l_Lean_Elab_instInhabitedMacroExpansionInfo();
lean_mark_persistent(l_Lean_Elab_instInhabitedMacroExpansionInfo);
l_Lean_Elab_instInhabitedCustomInfo___closed__1 = _init_l_Lean_Elab_instInhabitedCustomInfo___closed__1();
lean_mark_persistent(l_Lean_Elab_instInhabitedCustomInfo___closed__1);
l_Lean_Elab_instInhabitedCustomInfo = _init_l_Lean_Elab_instInhabitedCustomInfo();
lean_mark_persistent(l_Lean_Elab_instInhabitedCustomInfo);
l_Lean_Elab_instToFormatCustomInfo___closed__1 = _init_l_Lean_Elab_instToFormatCustomInfo___closed__1();
lean_mark_persistent(l_Lean_Elab_instToFormatCustomInfo___closed__1);
l_Lean_Elab_instToFormatCustomInfo = _init_l_Lean_Elab_instToFormatCustomInfo();
lean_mark_persistent(l_Lean_Elab_instToFormatCustomInfo);
l_Lean_Elab_instInhabitedInfo___closed__1 = _init_l_Lean_Elab_instInhabitedInfo___closed__1();
lean_mark_persistent(l_Lean_Elab_instInhabitedInfo___closed__1);
l_Lean_Elab_instInhabitedInfo = _init_l_Lean_Elab_instInhabitedInfo();

156
stage0/stdlib/Lean/Elab/Quotation.c generated
View file

@ -62,6 +62,7 @@ static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__27;
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__24___closed__6;
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__6___closed__9;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__1;
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Meta_0__Lean_quoteList___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__8(lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__6___closed__44;
@ -179,6 +180,7 @@ static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___spec__5(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3849__declRange(lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__6___lambda__3___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__3;
static lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__27;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3825__declRange___closed__3;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3855__declRange___closed__1;
@ -257,6 +259,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean
lean_object* l_Lean_Elab_Term_Quotation_getPatternsVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__16___closed__7;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Quotation_mkTuple(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__14___closed__5;
static lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__13;
@ -287,6 +290,7 @@ static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__10___closed__27;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__6___lambda__3___closed__9;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891_(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3879_(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3885_(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3873_(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -472,6 +476,7 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quota
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__6___closed__43;
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__6___lambda__2___closed__8;
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__6___lambda__2___closed__13;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__4;
static lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__5___closed__8;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3843____closed__3;
static lean_object* l_List_mapM___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___spec__4___closed__3;
@ -498,6 +503,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3843__declRange___closed__4;
LEAN_EXPORT lean_object* l_panic___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___spec__14(lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___spec__7___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__2;
static lean_object* l_Lean_Elab_Term_Quotation_commandElab__stx__quot_______closed__12;
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l_Lean_Elab_addMacroStack___at_Lean_Elab_Term_instAddErrorMessageContextTermElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -583,7 +589,7 @@ lean_object* l_Std_RBNode_find___at___private_Lean_Hygiene_0__Lean_sanitizeSynta
LEAN_EXPORT lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__24(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_Quotation___aux__Lean__Elab__Quotation______macroRules__Lean__Elab__Term__Quotation__commandElab__stx__quot______1___closed__25;
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___spec__7___closed__5;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_11859_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_11865_(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3873____closed__3;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__23___closed__20;
@ -678,6 +684,7 @@ static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_
LEAN_EXPORT lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_noOpMatchAdaptPats___lambda__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__6___closed__37;
static lean_object* l_List_mapM___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___spec__4___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__3;
static lean_object* l_Lean_Elab_Term_Quotation___aux__Lean__Elab__Quotation______macroRules__Lean__Elab__Term__Quotation__commandElab__stx__quot______1___closed__5;
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___spec__7___closed__3;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3825____closed__3;
@ -693,6 +700,7 @@ static lean_object* l_Lean_Elab_Term_Quotation___aux__Lean__Elab__Quotation_____
uint8_t l_Lean_Syntax_isNodeOf(lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__6___closed__24;
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__6___lambda__3___closed__30;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange(lean_object*);
static lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__5___closed__7;
static lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__29;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3849____closed__3;
@ -754,6 +762,7 @@ LEAN_EXPORT lean_object* l___private_Init_Meta_0__Lean_quoteList___at___private_
static lean_object* l_Lean_Elab_Term_Quotation___aux__Lean__Elab__Quotation______macroRules__Lean__Elab__Term__Quotation__commandElab__stx__quot______1___closed__23;
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__6___lambda__3___closed__20;
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__6___closed__18;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891_(lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3843_(lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3831_(lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3825_(lean_object*);
@ -924,6 +933,7 @@ static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_
LEAN_EXPORT lean_object* l___private_Init_Meta_0__Lean_quoteList___at_Lean_Elab_Term_Quotation_ArrayStxBuilder_build___spec__1(lean_object*);
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__4___closed__6;
lean_object* lean_panic_fn(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__2;
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___closed__5;
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__12;
LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -14515,6 +14525,116 @@ x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891_(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;
x_10 = l_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3813____closed__1;
x_11 = l_Lean_Elab_Term_adaptExpander(x_10, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
return x_11;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_Quotation___aux__Lean__Elab__Quotation______macroRules__Lean__Elab__Term__Quotation__commandElab__stx__quot______1___closed__2;
x_2 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3813____closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3813____closed__12;
x_2 = lean_unsigned_to_nat(3891u);
x_3 = lean_name_mk_numeral(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891_), 9, 0);
return x_1;
}
}
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3813____closed__14;
x_3 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__1;
x_4 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__2;
x_5 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__3;
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(197u);
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(197u);
x_2 = lean_unsigned_to_nat(33u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__1;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__2;
x_4 = lean_unsigned_to_nat(33u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
lean_ctor_set(x_5, 2, x_3);
lean_ctor_set(x_5, 3, x_4);
return x_5;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__3;
x_2 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_2, 0, x_1);
lean_ctor_set(x_2, 1, x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__2;
x_3 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__4;
x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1);
return x_4;
}
}
static lean_object* _init_l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_noOpMatchAdaptPats___lambda__1___closed__1() {
_start:
{
@ -31866,7 +31986,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_Quotation_0__Lean_Elab_Term_Quotation_getSepFromSplice___closed__1;
x_2 = l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__4___closed__4;
x_3 = lean_unsigned_to_nat(503u);
x_3 = lean_unsigned_to_nat(504u);
x_4 = lean_unsigned_to_nat(12u);
x_5 = l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getSepFromSplice___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -34764,7 +34884,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchSynta
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(535u);
x_1 = lean_unsigned_to_nat(536u);
x_2 = lean_unsigned_to_nat(27u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -34776,7 +34896,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchSynta
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(536u);
x_1 = lean_unsigned_to_nat(537u);
x_2 = lean_unsigned_to_nat(35u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -34804,7 +34924,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchSynta
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(535u);
x_1 = lean_unsigned_to_nat(536u);
x_2 = lean_unsigned_to_nat(31u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -34816,7 +34936,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchSynta
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(535u);
x_1 = lean_unsigned_to_nat(536u);
x_2 = lean_unsigned_to_nat(46u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -34862,7 +34982,7 @@ x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_11859_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_11865_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -36039,6 +36159,26 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lea
res = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3885__declRange(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__1 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__1);
l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__2 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__2);
l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__3 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891____closed__3);
res = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__1);
l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__2);
l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__3 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__3);
l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__4 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__4();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange___closed__4);
res = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3891__declRange(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_noOpMatchAdaptPats___lambda__1___closed__1 = _init_l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_noOpMatchAdaptPats___lambda__1___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_noOpMatchAdaptPats___lambda__1___closed__1);
l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_noOpMatchAdaptPats___lambda__1___closed__2 = _init_l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_noOpMatchAdaptPats___lambda__1___closed__2();
@ -36554,7 +36694,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchSyntax_dec
res = l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchSyntax_declRange(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_11859_(lean_io_mk_world());
res = l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_11865_(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));

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

File diff suppressed because it is too large Load diff

2
stage0/stdlib/Lean/Elab/Tactic/Conv/Basic.c generated
View file

@ -3071,7 +3071,7 @@ static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalConvSeqBracketed___lambda_
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("refl");
x_1 = lean_mk_string("tacticRfl");
return x_1;
}
}

412
stage0/stdlib/Lean/Meta/Tactic/LinearArith/Solver.c generated
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

1746
stage0/stdlib/Lean/Server/FileWorker/RequestHandling.c generated
View file

File diff suppressed because it is too large Load diff

356
stage0/stdlib/Lean/Server/FileWorker/WidgetRequests.c generated
View file

@ -22,7 +22,8 @@ size_t lean_usize_add(size_t, size_t);
lean_object* l_Lean_instToJsonOption___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911_(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
static lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instFromJsonRpcEncodingPacket___closed__1;
static lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_Lean_Widget_InfoPopup_toJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_432____closed__6;
@ -35,41 +36,41 @@ lean_object* lean_name_mk_string(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__1___rarg___lambda__2(lean_object*, size_t, lean_object*);
uint8_t lean_usize_dec_eq(size_t, size_t);
lean_object* lean_array_uget(lean_object*, size_t);
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__1;
lean_object* lean_io_error_to_string(lean_object*);
lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_InfoWithCtx_decodeUnsafe____x40_Lean_Widget_InteractiveCode___hyg_5____rarg(lean_object*, lean_object*, size_t);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__16(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__2;
static lean_object* l_Lean_Widget_instInhabitedInfoPopup___closed__1;
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Widget_Lean_Widget_InteractiveGoals_instToJsonRpcEncodingPacket;
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket___lambda__5(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Widget_Lean_Widget_InfoWithCtx_instRpcEncodingWithRpcRefInfoWithCtxRpcRef;
lean_object* l_Lean_Elab_Info_type_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_Lean_Widget_InfoPopup_toJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_432____closed__5;
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__11___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__18___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___closed__3;
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instFromJsonRpcEncodingPacket;
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_612____spec__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__1;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__2___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_Lean_Widget_MsgToInteractive_fromJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_56_(lean_object*);
static lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_Lean_Widget_InfoPopup_fromJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_363____closed__2;
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_612____spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__3;
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__1;
extern lean_object* l_Lean_Widget_Lean_Widget_InteractiveTermGoal_instToJsonRpcEncodingPacket;
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__3;
lean_object* lean_st_ref_get(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__17___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__5;
extern lean_object* l_Lean_Server_builtinRpcProcedures;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__2(lean_object*);
LEAN_EXPORT uint8_t l_Lean_Widget_getInteractiveDiagnostics___lambda__3(lean_object*, lean_object*);
static lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____spec__1___closed__2;
static lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_Lean_Widget_InfoPopup_fromJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_363____closed__1;
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__5;
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket___lambda__4(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
@ -82,41 +83,39 @@ lean_object* l_Lean_FileMap_lspPosToUtf8Pos(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket___spec__2(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__9(lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__10(lean_object*);
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__3;
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__2;
LEAN_EXPORT lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____spec__1___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__8___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____boxed(lean_object*);
lean_object* l_List_join___rarg(lean_object*);
uint8_t lean_usize_dec_lt(size_t, size_t);
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____boxed(lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__14___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_946_(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_947_(lean_object*);
static lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____closed__1;
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____lambda__2(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instFromJsonRpcEncodingPacket;
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__11(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_instFromJsonGetInteractiveDiagnosticsParams;
static lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_Lean_Widget_InfoPopup_toJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_432____closed__4;
LEAN_EXPORT lean_object* l_Lean_Widget_instInhabitedGetInteractiveDiagnosticsParams;
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_612_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_947____spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Widget_getInteractiveDiagnostics___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__1___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__14(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Widget_getInteractiveDiagnostics___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__8(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonLineRange____x40_Lean_Data_Lsp_Extra___hyg_1812_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____spec__1___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Widget_TaggedText_0__Lean_Widget_toJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_579____rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket;
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__9(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_946____spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_612____spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_getLast_x3f___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__8(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instToJsonRpcEncodingPacket;
@ -127,25 +126,25 @@ static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetReq
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonPosition____x40_Lean_Data_Lsp_Basic___hyg_399____spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__2___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__3;
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__3;
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__10(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_getInteractiveDiagnostics___lambda__1(lean_object*, lean_object*);
static lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_Lean_Widget_InfoPopup_toJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_432____closed__3;
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__12___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonDocumentFilter____x40_Lean_Data_Lsp_Basic___hyg_2125____spec__1(lean_object*, lean_object*);
static lean_object* l_Lean_Widget_getInteractiveDiagnostics___closed__1;
LEAN_EXPORT lean_object* l_Lean_Widget_getInteractiveDiagnostics___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__3;
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____closed__8;
lean_object* l_Std_PersistentHashMap_insert___at_Lean_Server_registerBuiltinRpcProcedure___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_toString(lean_object*, uint8_t);
lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_Lean_MessageData_encodeUnsafe____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____spec__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__3;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__4___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__11(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Widget_Lean_Widget_InteractiveGoals_instRpcEncodingInteractiveGoalsRpcEncodingPacket;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_IO_AsyncList_waitAll___rarg(lean_object*, lean_object*, lean_object*);
@ -164,26 +163,26 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_Inf
lean_object* l_Lean_Server_instRpcEncoding___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_getInteractiveGoals(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2(lean_object*, lean_object*);
lean_object* l_Lean_Server_instRpcEncoding___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_Lean_Widget_MsgToInteractive_toJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_108_(lean_object*);
extern lean_object* l_Lean_Lsp_instFromJsonRpcRef;
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____closed__9;
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__4(lean_object*, size_t);
LEAN_EXPORT lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__4___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____spec__1___lambda__2___closed__2;
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__3___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Widget_exprToInteractiveExplicit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_instInhabitedInfoPopup;
static lean_object* l_Lean_Widget_getInteractiveDiagnostics___lambda__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Widget_Lean_Widget_InteractiveTermGoal_instRpcEncodingInteractiveTermGoalRpcEncodingPacket;
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_CodeToken_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveCode___hyg_178____spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__20(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_getInteractiveDiagnostics___lambda__1___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket___lambda__5___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_1030_(size_t);
LEAN_EXPORT lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__4(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_612____lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_getInteractiveDiagnostics___lambda__1___closed__2;
@ -208,7 +207,7 @@ LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfo
lean_object* l_Lean_Elab_Info_docString_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____closed__2;
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__2(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket___spec__1(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_Lean_Widget_MsgToInteractive_fromJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_56____boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__3___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, size_t);
@ -223,7 +222,7 @@ static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetReq
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__14(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_Lean_Widget_InfoPopup_toJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_432____closed__2;
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__3;
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__3;
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_612____lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____spec__1___lambda__1___closed__1;
static lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____spec__1___lambda__2___closed__1;
@ -241,11 +240,12 @@ LEAN_EXPORT lean_object* l_Lean_Widget_getInteractiveDiagnostics___lambda__3___b
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__5(lean_object*);
static lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__3___closed__1;
static lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket___closed__1;
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__2(lean_object*, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____closed__1;
LEAN_EXPORT lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__2(lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_Server_instRpcEncodingOption___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__12(lean_object*, lean_object*, lean_object*, size_t);
lean_object* l_Std_PersistentArray_toArray___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__3___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -261,39 +261,39 @@ LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPop
lean_object* l_Lean_Json_mkObj(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instToJsonRpcEncodingPacket;
uint8_t l_Std_PersistentHashMap_contains___at_Lean_Server_registerBuiltinRpcProcedure___spec__5(lean_object*, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__2;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__17(lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__1;
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__2;
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__3;
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__2;
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__4;
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Widget_TaggedText_0__Lean_Widget_toJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_579____at___private_Lean_Widget_InteractiveGoal_0__Lean_Widget_Lean_Widget_InteractiveHypothesis_toJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveGoal___hyg_216____spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__2;
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__1;
static lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___closed__2;
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__1;
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__1;
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__2;
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__1;
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__16(lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__15(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket___lambda__1(size_t, lean_object*, lean_object*);
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__2___closed__1;
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__15___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__1;
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____closed__6;
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__2___closed__2;
static lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instToJsonRpcEncodingPacket___closed__1;
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__2;
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__3(lean_object*);
lean_object* lean_io_initializing(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_612____lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_InfoWithCtx_encodeUnsafe____x40_Lean_Widget_InteractiveCode___hyg_5____rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__2___closed__2;
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____closed__3;
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__1___rarg___lambda__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__13___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_612____lambda__5(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____closed__5;
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__2___closed__1;
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__1___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__4;
lean_object* l_Lean_Server_RequestM_asTask___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__16___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__20___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -308,7 +308,6 @@ LEAN_EXPORT lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn_
static lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket___closed__3;
lean_object* l_Lean_Elab_ContextInfo_runMetaM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_Lean_Widget_InfoPopup_fromJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_363_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_instFromJsonGetInteractiveDiagnosticsParams___closed__1;
extern lean_object* l_Lean_Widget_MsgEmbed_instToJsonRpcEncodingPacket;
lean_object* l_Lean_Server_FileWorker_getInteractiveTermGoal(lean_object*, lean_object*, lean_object*);
@ -316,20 +315,21 @@ lean_object* l_Lean_Server_wrapRpcProcedure___elambda__1___boxed(lean_object*, l
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__18(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__9___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__2;
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_612____lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonLineRange____x40_Lean_Data_Lsp_Extra___hyg_1760_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___closed__1;
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__1;
lean_object* l_Lean_Server_RequestM_readDoc(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__7___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__4___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Widget_MsgEmbed_instRpcEncodingMsgEmbedRpcEncodingPacket;
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__19___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Lsp_instFromJsonPlainGoalParams;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__2;
LEAN_EXPORT lean_object* l_Lean_Widget_instInhabitedMsgToInteractive;
static lean_object* _init_l_Lean_Widget_instInhabitedMsgToInteractive___closed__1() {
_start:
@ -4761,7 +4761,7 @@ lean_dec(x_1);
return x_6;
}
}
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__1() {
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__1() {
_start:
{
lean_object* x_1;
@ -4769,7 +4769,7 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Server_instRpcEncoding___lambda__1___box
return x_1;
}
}
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__2() {
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__2() {
_start:
{
lean_object* x_1;
@ -4777,19 +4777,19 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Server_instRpcEncoding___lambda__2___box
return x_1;
}
}
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__3() {
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__1;
x_2 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__2;
x_1 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__1;
x_2 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__2;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__4() {
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -4798,7 +4798,7 @@ x_2 = l_Lean_Server_instRpcEncodingOption___rarg(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__5() {
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -4808,14 +4808,14 @@ lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2(lean_object* x_1, lean_object* x_2) {
LEAN_EXPORT lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__3;
x_3 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__3;
x_4 = l_Lean_Lsp_instFromJsonPlainGoalParams;
x_5 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__4;
x_6 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__5;
x_5 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__4;
x_6 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__5;
x_7 = lean_alloc_closure((void*)(l_Lean_Server_wrapRpcProcedure___elambda__1___boxed), 14, 10);
lean_closure_set(x_7, 0, x_1);
lean_closure_set(x_7, 1, lean_box(0));
@ -4830,12 +4830,12 @@ lean_closure_set(x_7, 9, x_2);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__1___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__1___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12;
lean_inc(x_1);
x_5 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2(x_1, x_2);
x_5 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2(x_1, x_2);
x_6 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____spec__1___lambda__1___closed__1;
x_7 = lean_st_ref_take(x_6, x_4);
x_8 = lean_ctor_get(x_7, 0);
@ -4865,7 +4865,7 @@ return x_15;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__1___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__1___lambda__2(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; uint8_t x_8;
@ -4886,7 +4886,7 @@ lean_object* x_12; lean_object* x_13;
lean_free_object(x_7);
lean_dec(x_3);
x_12 = lean_box(0);
x_13 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__1___lambda__1(x_1, x_2, x_12, x_10);
x_13 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__1___lambda__1(x_1, x_2, x_12, x_10);
return x_13;
}
else
@ -4921,7 +4921,7 @@ if (x_21 == 0)
lean_object* x_22; lean_object* x_23;
lean_dec(x_3);
x_22 = lean_box(0);
x_23 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__1___lambda__1(x_1, x_2, x_22, x_20);
x_23 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__1___lambda__1(x_1, x_2, x_22, x_20);
return x_23;
}
else
@ -4944,7 +4944,7 @@ return x_29;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12;
@ -5009,12 +5009,12 @@ x_27 = lean_ctor_get(x_10, 1);
lean_inc(x_27);
lean_dec(x_10);
x_28 = lean_box(0);
x_29 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__1___lambda__2(x_1, x_2, x_9, x_28, x_27);
x_29 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__1___lambda__2(x_1, x_2, x_9, x_28, x_27);
return x_29;
}
}
}
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__1() {
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__1() {
_start:
{
lean_object* x_1;
@ -5022,17 +5022,17 @@ x_1 = lean_mk_string("getInteractiveGoals");
return x_1;
}
}
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__2() {
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____closed__4;
x_2 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__1;
x_2 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__3() {
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__3() {
_start:
{
lean_object* x_1;
@ -5040,26 +5040,26 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Server_FileWorker_getInteractiveGoals),
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__2;
x_3 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__3;
x_4 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__1(x_2, x_3, x_1);
x_2 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__2;
x_3 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__3;
x_4 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__1(x_2, x_3, x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__1___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_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__1___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__1___lambda__1(x_1, x_2, x_3, x_4);
x_5 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__1___lambda__1(x_1, x_2, x_3, x_4);
lean_dec(x_3);
return x_5;
}
}
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__2___closed__1() {
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__2___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -5068,7 +5068,7 @@ x_2 = l_Lean_Server_instRpcEncodingOption___rarg(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__2___closed__2() {
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__2___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -5078,14 +5078,14 @@ lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__2(lean_object* x_1, lean_object* x_2) {
LEAN_EXPORT lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__2(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__3;
x_3 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__3;
x_4 = l_Lean_Lsp_instFromJsonPlainTermGoalParams;
x_5 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__2___closed__1;
x_6 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__2___closed__2;
x_5 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__2___closed__1;
x_6 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__2___closed__2;
x_7 = lean_alloc_closure((void*)(l_Lean_Server_wrapRpcProcedure___elambda__1___boxed), 14, 10);
lean_closure_set(x_7, 0, x_1);
lean_closure_set(x_7, 1, lean_box(0));
@ -5100,12 +5100,12 @@ lean_closure_set(x_7, 9, x_2);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__1___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__1___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12;
lean_inc(x_1);
x_5 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__2(x_1, x_2);
x_5 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__2(x_1, x_2);
x_6 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____spec__1___lambda__1___closed__1;
x_7 = lean_st_ref_take(x_6, x_4);
x_8 = lean_ctor_get(x_7, 0);
@ -5135,7 +5135,7 @@ return x_15;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__1___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__1___lambda__2(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; uint8_t x_8;
@ -5156,7 +5156,7 @@ lean_object* x_12; lean_object* x_13;
lean_free_object(x_7);
lean_dec(x_3);
x_12 = lean_box(0);
x_13 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__1___lambda__1(x_1, x_2, x_12, x_10);
x_13 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__1___lambda__1(x_1, x_2, x_12, x_10);
return x_13;
}
else
@ -5191,7 +5191,7 @@ if (x_21 == 0)
lean_object* x_22; lean_object* x_23;
lean_dec(x_3);
x_22 = lean_box(0);
x_23 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__1___lambda__1(x_1, x_2, x_22, x_20);
x_23 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__1___lambda__1(x_1, x_2, x_22, x_20);
return x_23;
}
else
@ -5214,7 +5214,7 @@ return x_29;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12;
@ -5279,12 +5279,12 @@ x_27 = lean_ctor_get(x_10, 1);
lean_inc(x_27);
lean_dec(x_10);
x_28 = lean_box(0);
x_29 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__1___lambda__2(x_1, x_2, x_9, x_28, x_27);
x_29 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__1___lambda__2(x_1, x_2, x_9, x_28, x_27);
return x_29;
}
}
}
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__1() {
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__1() {
_start:
{
lean_object* x_1;
@ -5292,17 +5292,17 @@ x_1 = lean_mk_string("getInteractiveTermGoal");
return x_1;
}
}
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__2() {
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____closed__4;
x_2 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__1;
x_2 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__3() {
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__3() {
_start:
{
lean_object* x_1;
@ -5310,21 +5310,21 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Server_FileWorker_getInteractiveTermGoal
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__2;
x_3 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__3;
x_4 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__1(x_2, x_3, x_1);
x_2 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__2;
x_3 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__3;
x_4 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__1(x_2, x_3, x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__1___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_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__1___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__1___lambda__1(x_1, x_2, x_3, x_4);
x_5 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__1___lambda__1(x_1, x_2, x_3, x_4);
lean_dec(x_3);
return x_5;
}
@ -5337,7 +5337,7 @@ x_1 = lean_box(0);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____spec__1(lean_object* x_1, lean_object* x_2) {
LEAN_EXPORT lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
@ -5401,7 +5401,7 @@ return x_14;
}
}
}
static lean_object* _init_l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____closed__1() {
static lean_object* _init_l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____closed__1() {
_start:
{
lean_object* x_1;
@ -5409,12 +5409,12 @@ x_1 = lean_mk_string("lineRange");
return x_1;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911_(lean_object* x_1) {
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____closed__1;
x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____spec__1(x_1, x_2);
x_2 = l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____closed__1;
x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____spec__1(x_1, x_2);
if (lean_obj_tag(x_3) == 0)
{
uint8_t x_4;
@ -5455,21 +5455,21 @@ return x_9;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____spec__1___boxed(lean_object* x_1, lean_object* x_2) {
LEAN_EXPORT lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____spec__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____spec__1(x_1, x_2);
x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____spec__1(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____boxed(lean_object* x_1) {
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911_(x_1);
x_2 = l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912_(x_1);
lean_dec(x_1);
return x_2;
}
@ -5478,7 +5478,7 @@ static lean_object* _init_l_Lean_Widget_instFromJsonGetInteractiveDiagnosticsPar
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____boxed), 1, 0);
return x_1;
}
}
@ -5490,7 +5490,7 @@ x_1 = l_Lean_Widget_instFromJsonGetInteractiveDiagnosticsParams___closed__1;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_946____spec__1(lean_object* x_1, lean_object* x_2) {
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_947____spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_2) == 0)
@ -5518,12 +5518,12 @@ return x_8;
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_946_(lean_object* x_1) {
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_947_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____closed__1;
x_3 = l_Lean_Json_opt___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_946____spec__1(x_2, x_1);
x_2 = l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____closed__1;
x_3 = l_Lean_Json_opt___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_947____spec__1(x_2, x_1);
x_4 = lean_box(0);
x_5 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_5, 0, x_3);
@ -5537,7 +5537,7 @@ static lean_object* _init_l_Lean_Widget_instToJsonGetInteractiveDiagnosticsParam
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_946_), 1, 0);
x_1 = lean_alloc_closure((void*)(l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_947_), 1, 0);
return x_1;
}
}
@ -5930,7 +5930,7 @@ lean_dec(x_2);
return x_4;
}
}
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__1() {
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -5939,7 +5939,7 @@ x_2 = l_Lean_Server_instRpcEncodingArray___rarg(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__2() {
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -5949,24 +5949,24 @@ lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__3() {
static lean_object* _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__2;
x_1 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_instToJsonArray___rarg), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2(lean_object* x_1, lean_object* x_2) {
LEAN_EXPORT lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__3;
x_3 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__3;
x_4 = l_Lean_Widget_instFromJsonGetInteractiveDiagnosticsParams;
x_5 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__1;
x_6 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__3;
x_5 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__1;
x_6 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__3;
x_7 = lean_alloc_closure((void*)(l_Lean_Server_wrapRpcProcedure___elambda__1___boxed), 14, 10);
lean_closure_set(x_7, 0, x_1);
lean_closure_set(x_7, 1, lean_box(0));
@ -5981,12 +5981,12 @@ lean_closure_set(x_7, 9, x_2);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__1___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__1___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12;
lean_inc(x_1);
x_5 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2(x_1, x_2);
x_5 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2(x_1, x_2);
x_6 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____spec__1___lambda__1___closed__1;
x_7 = lean_st_ref_take(x_6, x_4);
x_8 = lean_ctor_get(x_7, 0);
@ -6016,7 +6016,7 @@ return x_15;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__1___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__1___lambda__2(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; uint8_t x_8;
@ -6037,7 +6037,7 @@ lean_object* x_12; lean_object* x_13;
lean_free_object(x_7);
lean_dec(x_3);
x_12 = lean_box(0);
x_13 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__1___lambda__1(x_1, x_2, x_12, x_10);
x_13 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__1___lambda__1(x_1, x_2, x_12, x_10);
return x_13;
}
else
@ -6072,7 +6072,7 @@ if (x_21 == 0)
lean_object* x_22; lean_object* x_23;
lean_dec(x_3);
x_22 = lean_box(0);
x_23 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__1___lambda__1(x_1, x_2, x_22, x_20);
x_23 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__1___lambda__1(x_1, x_2, x_22, x_20);
return x_23;
}
else
@ -6095,7 +6095,7 @@ return x_29;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12;
@ -6160,12 +6160,12 @@ x_27 = lean_ctor_get(x_10, 1);
lean_inc(x_27);
lean_dec(x_10);
x_28 = lean_box(0);
x_29 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__1___lambda__2(x_1, x_2, x_9, x_28, x_27);
x_29 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__1___lambda__2(x_1, x_2, x_9, x_28, x_27);
return x_29;
}
}
}
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__1() {
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__1() {
_start:
{
lean_object* x_1;
@ -6173,17 +6173,17 @@ x_1 = lean_mk_string("getInteractiveDiagnostics");
return x_1;
}
}
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__2() {
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_245____closed__4;
x_2 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__1;
x_2 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__3() {
static lean_object* _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__3() {
_start:
{
lean_object* x_1;
@ -6191,21 +6191,21 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Widget_getInteractiveDiagnostics___boxed
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__2;
x_3 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__3;
x_4 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__1(x_2, x_3, x_1);
x_2 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__2;
x_3 = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__3;
x_4 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__1(x_2, x_3, x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__1___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_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__1___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__1___lambda__1(x_1, x_2, x_3, x_4);
x_5 = l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__1___lambda__1(x_1, x_2, x_3, x_4);
lean_dec(x_3);
return x_5;
}
@ -6353,42 +6353,42 @@ lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRe
res = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_612_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__1 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__1();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__1);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__2 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__2();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__2);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__3 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__3();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__3);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__4 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__4();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__4);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__5 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__5();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____spec__2___closed__5);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__1 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__1();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__1);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__2 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__2();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__2);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__3 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__3();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859____closed__3);
res = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_859_(lean_io_mk_world());
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__1 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__1();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__1);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__2 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__2();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__2);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__3 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__3();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__3);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__4 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__4();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__4);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__5 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__5();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____spec__2___closed__5);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__1 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__1();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__1);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__2 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__2();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__2);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__3 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__3();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860____closed__3);
res = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_860_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__2___closed__1 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__2___closed__1();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__2___closed__1);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__2___closed__2 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__2___closed__2();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____spec__2___closed__2);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__1 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__1();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__1);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__2 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__2();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__2);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__3 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__3();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875____closed__3);
res = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_875_(lean_io_mk_world());
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__2___closed__1 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__2___closed__1();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__2___closed__1);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__2___closed__2 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__2___closed__2();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____spec__2___closed__2);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__1 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__1();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__1);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__2 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__2();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__2);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__3 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__3();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876____closed__3);
res = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_876_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Widget_instInhabitedGetInteractiveDiagnosticsParams = _init_l_Lean_Widget_instInhabitedGetInteractiveDiagnosticsParams();
lean_mark_persistent(l_Lean_Widget_instInhabitedGetInteractiveDiagnosticsParams);
l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____closed__1 = _init_l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____closed__1();
lean_mark_persistent(l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_911____closed__1);
l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____closed__1 = _init_l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____closed__1();
lean_mark_persistent(l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_912____closed__1);
l_Lean_Widget_instFromJsonGetInteractiveDiagnosticsParams___closed__1 = _init_l_Lean_Widget_instFromJsonGetInteractiveDiagnosticsParams___closed__1();
lean_mark_persistent(l_Lean_Widget_instFromJsonGetInteractiveDiagnosticsParams___closed__1);
l_Lean_Widget_instFromJsonGetInteractiveDiagnosticsParams = _init_l_Lean_Widget_instFromJsonGetInteractiveDiagnosticsParams();
@ -6403,19 +6403,19 @@ l_Lean_Widget_getInteractiveDiagnostics___lambda__1___closed__2 = _init_l_Lean_W
lean_mark_persistent(l_Lean_Widget_getInteractiveDiagnostics___lambda__1___closed__2);
l_Lean_Widget_getInteractiveDiagnostics___closed__1 = _init_l_Lean_Widget_getInteractiveDiagnostics___closed__1();
lean_mark_persistent(l_Lean_Widget_getInteractiveDiagnostics___closed__1);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__1 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__1();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__1);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__2 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__2();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__2);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__3 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__3();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____spec__2___closed__3);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__1 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__1();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__1);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__2 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__2();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__2);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__3 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__3();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139____closed__3);
res = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1139_(lean_io_mk_world());
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__1 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__1();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__1);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__2 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__2();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__2);
l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__3 = _init_l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__3();
lean_mark_persistent(l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____spec__2___closed__3);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__1 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__1();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__1);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__2 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__2();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__2);
l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__3 = _init_l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__3();
lean_mark_persistent(l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140____closed__3);
res = l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1140_(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));

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

@ -2956,14 +2956,22 @@ x_8 = lean_ctor_get(x_1, 0);
x_9 = l_Lean_Elab_CompletionInfo_stx(x_8);
return x_9;
}
default:
case 6:
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
lean_object* x_10; lean_object* x_11;
x_10 = lean_ctor_get(x_1, 0);
x_11 = lean_ctor_get(x_10, 0);
x_12 = lean_ctor_get(x_11, 1);
lean_inc(x_12);
return x_12;
lean_inc(x_11);
return x_11;
}
default:
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = lean_ctor_get(x_1, 0);
x_13 = lean_ctor_get(x_12, 0);
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
return x_14;
}
}
}
@ -4092,30 +4100,39 @@ return x_3;
LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_hoverableInfoAt_x3f___lambda__2(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
if (lean_obj_tag(x_2) == 4)
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Lean_Elab_Info_contains(x_2, x_1);
x_4 = lean_box(x_3);
return x_4;
uint8_t x_9; lean_object* x_10;
x_9 = l_Lean_Elab_Info_contains(x_2, x_1);
x_10 = lean_box(x_9);
return x_10;
}
else
{
lean_object* x_11;
x_11 = lean_box(0);
x_3 = x_11;
goto block_8;
}
block_8:
{
lean_object* x_4;
lean_dec(x_3);
x_4 = l_Lean_Elab_Info_toElabInfo_x3f(x_2);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5;
x_5 = l_Lean_Elab_Info_toElabInfo_x3f(x_2);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_6;
x_6 = l_Lean_Elab_InfoTree_hoverableInfoAt_x3f___lambda__2___closed__2;
return x_6;
x_5 = l_Lean_Elab_InfoTree_hoverableInfoAt_x3f___lambda__2___closed__2;
return x_5;
}
else
{
uint8_t x_7; lean_object* x_8;
lean_dec(x_5);
x_7 = l_Lean_Elab_Info_contains(x_2, x_1);
x_8 = lean_box(x_7);
return x_8;
uint8_t x_6; lean_object* x_7;
lean_dec(x_4);
x_6 = l_Lean_Elab_Info_contains(x_2, x_1);
x_7 = lean_box(x_6);
return x_7;
}
}
}

12
stage0/stdlib/Lean/Server/Watchdog.c generated
View file

@ -317,7 +317,7 @@ static lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__1___c
lean_object* lean_get_prefix(lean_object*);
static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__11;
lean_object* l_Lean_FileMap_ofString(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSymbolInformation____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3107_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSymbolInformation____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3109_(lean_object*);
lean_object* l_Std_RBNode_balLeft___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_FileWorker_errorPendingRequests___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_mainLoop(lean_object*, lean_object*, lean_object*);
@ -539,7 +539,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol(lean_objec
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handleWorkspaceSymbol___spec__2___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_IO_FS_Stream_readLspRequestAs___at_Lean_Server_Watchdog_initAndRunWatchdog___spec__1___closed__1;
static lean_object* l_Lean_Server_Watchdog_findFileWorker_x21___closed__2;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonReferenceParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2277_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonReferenceParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2279_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handleNotification___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_References_definitionOf_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_to_int(lean_object*);
@ -550,7 +550,7 @@ lean_object* l_List_appendTR___rarg(lean_object*, lean_object*);
static lean_object* l_Lean_Server_Watchdog_handleWorkspaceSymbol___lambda__1___closed__6;
static lean_object* l_Lean_Server_Watchdog_forwardRequestToWorker___closed__1;
static uint8_t l_Lean_Server_Watchdog_tryWriteMessage___lambda__1___closed__1;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonWorkspaceSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2408_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonWorkspaceSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2410_(lean_object*);
LEAN_EXPORT lean_object* l_Std_RBNode_ins___at_Lean_Server_Watchdog_forwardRequestToWorker___spec__3(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_Watchdog_handleNotification___closed__3;
lean_object* l___private_Lean_Data_Lsp_InitShutdown_0__Lean_Lsp_toJsonInitializeResult____x40_Lean_Data_Lsp_InitShutdown___hyg_663_(lean_object*);
@ -13837,7 +13837,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Wat
_start:
{
lean_object* x_4;
x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonWorkspaceSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2408_(x_1);
x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonWorkspaceSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2410_(x_1);
if (lean_obj_tag(x_4) == 0)
{
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;
@ -13886,7 +13886,7 @@ lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; size_t x
x_5 = lean_array_uget(x_3, x_2);
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_array_uset(x_3, x_2, x_6);
x_8 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSymbolInformation____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3107_(x_5);
x_8 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSymbolInformation____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3109_(x_5);
x_9 = 1;
x_10 = lean_usize_add(x_2, x_9);
x_11 = lean_array_uset(x_7, x_2, x_8);
@ -13924,7 +13924,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Wat
_start:
{
lean_object* x_4;
x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonReferenceParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2277_(x_1);
x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonReferenceParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_2279_(x_1);
if (lean_obj_tag(x_4) == 0)
{
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;