Runner for tests/lean/interactive server tests. Put here to avoid repeated elaboration overhead per test.

structure Lean.Server.Test.Runner.Client.NormalizeState : Type

• freshPtr : USize
• knownPtrs : Std.TreeMap USize USize compare

@[reducible, inline]

abbrev Lean.Server.Test.Runner.Client.NormalizeM (α : Type) : Type

Equations

• Lean.Server.Test.Runner.Client.NormalizeM α = StateM Lean.Server.Test.Runner.Client.NormalizeState α

def Lean.Server.Test.Runner.Client.NormalizeM.run {α : Type} (x : NormalizeM α) (s : NormalizeState) : α

Equations

• x.run s = StateT.run' x s

def Lean.Server.Test.Runner.Client.normalizedRef (ref : Lsp.RpcRef) : NormalizeM Lsp.RpcRef

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonRpcRef : ToJson Lsp.RpcRef

Equations

• Lean.Server.Test.Runner.Client.instToJsonRpcRef = { toJson := fun (r : Lean.Lsp.RpcRef) => Lean.Json.mkObj [("__rpcref", Lean.toJson r.p)] }

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonRpcRef : FromJson Lsp.RpcRef

Equations

• Lean.Server.Test.Runner.Client.instFromJsonRpcRef = { fromJson? := fun (j : Lean.Json) => do let __do_lift ← j.getObjValAs? USize "__rpcref" pure { p := __do_lift } }

structure Lean.Server.Test.Runner.Client.SubexprInfo : Type

• info : Lsp.RpcRef
• subexprPos : String
• diffStatus? : Option String

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonSubexprInfo : FromJson SubexprInfo

Equations

• Lean.Server.Test.Runner.Client.instFromJsonSubexprInfo = { fromJson? := Lean.Server.Test.Runner.Client.instFromJsonSubexprInfo.fromJson }

def Lean.Server.Test.Runner.Client.instFromJsonSubexprInfo.fromJson : Json → Except String SubexprInfo

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.Client.instToJsonSubexprInfo.toJson : SubexprInfo → Json

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonSubexprInfo : ToJson SubexprInfo

Equations

• Lean.Server.Test.Runner.Client.instToJsonSubexprInfo = { toJson := Lean.Server.Test.Runner.Client.instToJsonSubexprInfo.toJson }

def Lean.Server.Test.Runner.Client.SubexprInfo.normalize (i : SubexprInfo) : NormalizeM SubexprInfo

Equations

• i.normalize = do let __do_lift ← Lean.Server.Test.Runner.Client.normalizedRef i.info pure { info := __do_lift, subexprPos := i.subexprPos, diffStatus? := i.diffStatus? }

structure Lean.Server.Test.Runner.Client.Hyp : Type

• type : Widget.TaggedText SubexprInfo
• names : Array String
• fvarIds : Array FVarId
• val? : Option (Widget.TaggedText SubexprInfo)
• isInstance? : Option Bool
• isType? : Option Bool
• isInserted? : Option Bool
• isRemoved? : Option Bool

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonHyp : FromJson Hyp

Equations

• Lean.Server.Test.Runner.Client.instFromJsonHyp = { fromJson? := Lean.Server.Test.Runner.Client.instFromJsonHyp.fromJson }

def Lean.Server.Test.Runner.Client.instFromJsonHyp.fromJson : Json → Except String Hyp

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonHyp : ToJson Hyp

Equations

• Lean.Server.Test.Runner.Client.instToJsonHyp = { toJson := Lean.Server.Test.Runner.Client.instToJsonHyp.toJson }

def Lean.Server.Test.Runner.Client.instToJsonHyp.toJson : Hyp → Json

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.Client.Hyp.normalize (h : Hyp) : NormalizeM Hyp

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Server.Test.Runner.Client.InteractiveGoalCore : Type

• hyps : Array Hyp
• type : Widget.TaggedText SubexprInfo
• ctx : Lsp.RpcRef

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoalCore : FromJson InteractiveGoalCore

Equations

• Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoalCore = { fromJson? := Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoalCore.fromJson }

def Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoalCore.fromJson : Json → Except String InteractiveGoalCore

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonInteractiveGoalCore : ToJson InteractiveGoalCore

Equations

• Lean.Server.Test.Runner.Client.instToJsonInteractiveGoalCore = { toJson := Lean.Server.Test.Runner.Client.instToJsonInteractiveGoalCore.toJson }

def Lean.Server.Test.Runner.Client.instToJsonInteractiveGoalCore.toJson : InteractiveGoalCore → Json

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.Client.InteractiveGoalCore.normalize (g : InteractiveGoalCore) : NormalizeM InteractiveGoalCore

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Server.Test.Runner.Client.InteractiveGoalextends Lean.Server.Test.Runner.Client.InteractiveGoalCore : Type

• hyps : Array Hyp
• type : Widget.TaggedText SubexprInfo
• ctx : Lsp.RpcRef
• userName? : Option String
• goalPrefix : String
• mvarId : MVarId
• isInserted? : Option Bool
• isRemoved? : Option Bool

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoal : FromJson InteractiveGoal

Equations

• Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoal = { fromJson? := Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoal.fromJson }

def Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoal.fromJson : Json → Except String InteractiveGoal

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.Client.instToJsonInteractiveGoal.toJson : InteractiveGoal → Json

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonInteractiveGoal : ToJson InteractiveGoal

Equations

• Lean.Server.Test.Runner.Client.instToJsonInteractiveGoal = { toJson := Lean.Server.Test.Runner.Client.instToJsonInteractiveGoal.toJson }

def Lean.Server.Test.Runner.Client.InteractiveGoal.normalize (goal : InteractiveGoal) : NormalizeM InteractiveGoal

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Server.Test.Runner.Client.InteractiveGoals : Type

• goals : Array InteractiveGoal

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoals : FromJson InteractiveGoals

Equations

• Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoals = { fromJson? := Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoals.fromJson }

def Lean.Server.Test.Runner.Client.instFromJsonInteractiveGoals.fromJson : Json → Except String InteractiveGoals

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonInteractiveGoals : ToJson InteractiveGoals

Equations

• Lean.Server.Test.Runner.Client.instToJsonInteractiveGoals = { toJson := Lean.Server.Test.Runner.Client.instToJsonInteractiveGoals.toJson }

def Lean.Server.Test.Runner.Client.instToJsonInteractiveGoals.toJson : InteractiveGoals → Json

Equations

• Lean.Server.Test.Runner.Client.instToJsonInteractiveGoals.toJson x✝ = Lean.Json.mkObj [[("goals", Lean.toJson x✝.goals)]].flatten

def Lean.Server.Test.Runner.Client.InteractiveGoals.normalize (gs : InteractiveGoals) : NormalizeM InteractiveGoals

Equations

• gs.normalize = do let __do_lift ← Array.mapM (fun (x : Lean.Server.Test.Runner.Client.InteractiveGoal) => x.normalize) gs.goals pure { goals := __do_lift }

structure Lean.Server.Test.Runner.Client.InteractiveTermGoalextends Lean.Server.Test.Runner.Client.InteractiveGoalCore : Type

• hyps : Array Hyp
• type : Widget.TaggedText SubexprInfo
• ctx : Lsp.RpcRef
• range : Lsp.Range
• term : Lsp.RpcRef

def Lean.Server.Test.Runner.Client.instFromJsonInteractiveTermGoal.fromJson : Json → Except String InteractiveTermGoal

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonInteractiveTermGoal : FromJson InteractiveTermGoal

Equations

• Lean.Server.Test.Runner.Client.instFromJsonInteractiveTermGoal = { fromJson? := Lean.Server.Test.Runner.Client.instFromJsonInteractiveTermGoal.fromJson }

def Lean.Server.Test.Runner.Client.instToJsonInteractiveTermGoal.toJson : InteractiveTermGoal → Json

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonInteractiveTermGoal : ToJson InteractiveTermGoal

Equations

• Lean.Server.Test.Runner.Client.instToJsonInteractiveTermGoal = { toJson := Lean.Server.Test.Runner.Client.instToJsonInteractiveTermGoal.toJson }

def Lean.Server.Test.Runner.Client.InteractiveTermGoal.normalize (g : InteractiveTermGoal) : NormalizeM InteractiveTermGoal

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Server.Test.Runner.Client.WidgetInstance : Type

• id : Name
• javascriptHash : UInt64
• props : Json

def Lean.Server.Test.Runner.Client.instFromJsonWidgetInstance.fromJson : Json → Except String WidgetInstance

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonWidgetInstance : FromJson WidgetInstance

Equations

• Lean.Server.Test.Runner.Client.instFromJsonWidgetInstance = { fromJson? := Lean.Server.Test.Runner.Client.instFromJsonWidgetInstance.fromJson }

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonWidgetInstance : ToJson WidgetInstance

Equations

• Lean.Server.Test.Runner.Client.instToJsonWidgetInstance = { toJson := Lean.Server.Test.Runner.Client.instToJsonWidgetInstance.toJson }

def Lean.Server.Test.Runner.Client.instToJsonWidgetInstance.toJson : WidgetInstance → Json

Equations

• One or more equations did not get rendered due to their size.

inductive Lean.Server.Test.Runner.Client.StrictOrLazy (α β : Type) : Type

• strict {α β : Type} : α → StrictOrLazy α β
• lazy {α β : Type} : β → StrictOrLazy α β

def Lean.Server.Test.Runner.Client.instFromJsonStrictOrLazy.fromJson {α✝ β✝ : Type} [FromJson α✝] [FromJson β✝] : Json → Except String (StrictOrLazy α✝ β✝)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonStrictOrLazy {α✝ β✝ : Type} [FromJson α✝] [FromJson β✝] : FromJson (StrictOrLazy α✝ β✝)

Equations

• Lean.Server.Test.Runner.Client.instFromJsonStrictOrLazy = { fromJson? := Lean.Server.Test.Runner.Client.instFromJsonStrictOrLazy.fromJson }

def Lean.Server.Test.Runner.Client.instToJsonStrictOrLazy.toJson {α✝ β✝ : Type} [ToJson α✝] [ToJson β✝] : StrictOrLazy α✝ β✝ → Json

Equations

• Lean.Server.Test.Runner.Client.instToJsonStrictOrLazy.toJson (Lean.Server.Test.Runner.Client.StrictOrLazy.strict a) = Lean.Json.mkObj [("strict", Lean.toJson a)]
• Lean.Server.Test.Runner.Client.instToJsonStrictOrLazy.toJson (Lean.Server.Test.Runner.Client.StrictOrLazy.lazy a) = Lean.Json.mkObj [("lazy", Lean.toJson a)]

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonStrictOrLazy {α✝ β✝ : Type} [ToJson α✝] [ToJson β✝] : ToJson (StrictOrLazy α✝ β✝)

Equations

• Lean.Server.Test.Runner.Client.instToJsonStrictOrLazy = { toJson := Lean.Server.Test.Runner.Client.instToJsonStrictOrLazy.toJson }

inductive Lean.Server.Test.Runner.Client.MsgEmbed : Type

• expr : Widget.TaggedText SubexprInfo → MsgEmbed
• goal : InteractiveGoal → MsgEmbed
• widget (wi : WidgetInstance) (alt : Widget.TaggedText MsgEmbed) : MsgEmbed
• trace (indent : Nat) (cls : Name) (msg : Widget.TaggedText MsgEmbed) (collapsed : Bool) (children : StrictOrLazy (Array (Widget.TaggedText MsgEmbed)) Lsp.RpcRef) : MsgEmbed

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonMsgEmbed : FromJson MsgEmbed

Equations

• Lean.Server.Test.Runner.Client.instFromJsonMsgEmbed = { fromJson? := Lean.Server.Test.Runner.Client.instFromJsonMsgEmbed.fromJson }

partial def Lean.Server.Test.Runner.Client.instFromJsonMsgEmbed.fromJson : Json → Except String MsgEmbed

partial def Lean.Server.Test.Runner.Client.instToJsonMsgEmbed.toJson : MsgEmbed → Json

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonMsgEmbed : ToJson MsgEmbed

Equations

• Lean.Server.Test.Runner.Client.instToJsonMsgEmbed = { toJson := Lean.Server.Test.Runner.Client.instToJsonMsgEmbed.toJson }

partial def Lean.Server.Test.Runner.Client.MsgEmbed.normalize (m : MsgEmbed) : NormalizeM MsgEmbed

@[reducible, inline]

abbrev Lean.Server.Test.Runner.Client.InteractiveDiagnostic : Type

Equations

• Lean.Server.Test.Runner.Client.InteractiveDiagnostic = Lean.Lsp.DiagnosticWith (Lean.Widget.TaggedText Lean.Server.Test.Runner.Client.MsgEmbed)

def Lean.Server.Test.Runner.Client.InteractiveDiagnostic.normalize (d : InteractiveDiagnostic) : InteractiveDiagnostic

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.Client.normalizeInteractiveDiagnostics (diags : Array InteractiveDiagnostic) : Array InteractiveDiagnostic

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Server.Test.Runner.Client.InfoPopup : Type

• type : Option (Widget.TaggedText SubexprInfo)
• exprExplicit : Option (Widget.TaggedText SubexprInfo)
• doc : Option String

def Lean.Server.Test.Runner.Client.instFromJsonInfoPopup.fromJson : Json → Except String InfoPopup

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonInfoPopup : FromJson InfoPopup

Equations

• Lean.Server.Test.Runner.Client.instFromJsonInfoPopup = { fromJson? := Lean.Server.Test.Runner.Client.instFromJsonInfoPopup.fromJson }

def Lean.Server.Test.Runner.Client.instToJsonInfoPopup.toJson : InfoPopup → Json

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonInfoPopup : ToJson InfoPopup

Equations

• Lean.Server.Test.Runner.Client.instToJsonInfoPopup = { toJson := Lean.Server.Test.Runner.Client.instToJsonInfoPopup.toJson }

def Lean.Server.Test.Runner.Client.InfoPopup.normalize (p : InfoPopup) : InfoPopup

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Server.Test.Runner.Client.GetGoToLocationParams : Type

• kind : GoToKind
• info : Lsp.RpcRef

def Lean.Server.Test.Runner.Client.instFromJsonGetGoToLocationParams.fromJson : Json → Except String GetGoToLocationParams

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonGetGoToLocationParams : FromJson GetGoToLocationParams

Equations

• Lean.Server.Test.Runner.Client.instFromJsonGetGoToLocationParams = { fromJson? := Lean.Server.Test.Runner.Client.instFromJsonGetGoToLocationParams.fromJson }

def Lean.Server.Test.Runner.Client.instToJsonGetGoToLocationParams.toJson : GetGoToLocationParams → Json

Equations

• Lean.Server.Test.Runner.Client.instToJsonGetGoToLocationParams.toJson x✝ = Lean.Json.mkObj [[("kind", Lean.toJson x✝.kind)], [("info", Lean.toJson x✝.info)]].flatten

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonGetGoToLocationParams : ToJson GetGoToLocationParams

Equations

• Lean.Server.Test.Runner.Client.instToJsonGetGoToLocationParams = { toJson := Lean.Server.Test.Runner.Client.instToJsonGetGoToLocationParams.toJson }

structure Lean.Server.Test.Runner.Client.HighlightMatchesParams : Type

• query : String
• msg : Widget.TaggedText MsgEmbed

def Lean.Server.Test.Runner.Client.instFromJsonHighlightMatchesParams.fromJson : Json → Except String HighlightMatchesParams

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonHighlightMatchesParams : FromJson HighlightMatchesParams

Equations

• Lean.Server.Test.Runner.Client.instFromJsonHighlightMatchesParams = { fromJson? := Lean.Server.Test.Runner.Client.instFromJsonHighlightMatchesParams.fromJson }

def Lean.Server.Test.Runner.Client.instToJsonHighlightMatchesParams.toJson : HighlightMatchesParams → Json

Equations

• Lean.Server.Test.Runner.Client.instToJsonHighlightMatchesParams.toJson x✝ = Lean.Json.mkObj [[("query", Lean.toJson x✝.query)], [("msg", Lean.toJson x✝.msg)]].flatten

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonHighlightMatchesParams : ToJson HighlightMatchesParams

Equations

• Lean.Server.Test.Runner.Client.instToJsonHighlightMatchesParams = { toJson := Lean.Server.Test.Runner.Client.instToJsonHighlightMatchesParams.toJson }

inductive Lean.Server.Test.Runner.Client.HighlightedSubexprInfo : Type

• subexpr (info : SubexprInfo) : HighlightedSubexprInfo
• highlighted : HighlightedSubexprInfo

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonHighlightedSubexprInfo : FromJson HighlightedSubexprInfo

Equations

• Lean.Server.Test.Runner.Client.instFromJsonHighlightedSubexprInfo = { fromJson? := Lean.Server.Test.Runner.Client.instFromJsonHighlightedSubexprInfo.fromJson }

def Lean.Server.Test.Runner.Client.instFromJsonHighlightedSubexprInfo.fromJson : Json → Except String HighlightedSubexprInfo

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonHighlightedSubexprInfo : ToJson HighlightedSubexprInfo

Equations

• Lean.Server.Test.Runner.Client.instToJsonHighlightedSubexprInfo = { toJson := Lean.Server.Test.Runner.Client.instToJsonHighlightedSubexprInfo.toJson }

def Lean.Server.Test.Runner.Client.instToJsonHighlightedSubexprInfo.toJson : HighlightedSubexprInfo → Json

Equations

• One or more equations did not get rendered due to their size.
• Lean.Server.Test.Runner.Client.instToJsonHighlightedSubexprInfo.toJson Lean.Server.Test.Runner.Client.HighlightedSubexprInfo.highlighted = Lean.toJson "highlighted"

def Lean.Server.Test.Runner.Client.HighlightedSubexprInfo.normalize : HighlightedSubexprInfo → NormalizeM HighlightedSubexprInfo

Equations

• Lean.Server.Test.Runner.Client.HighlightedSubexprInfo.highlighted.normalize = pure Lean.Server.Test.Runner.Client.HighlightedSubexprInfo.highlighted
• (Lean.Server.Test.Runner.Client.HighlightedSubexprInfo.subexpr i).normalize = do let __do_lift ← i.normalize pure (Lean.Server.Test.Runner.Client.HighlightedSubexprInfo.subexpr __do_lift)

inductive Lean.Server.Test.Runner.Client.HighlightedMsgEmbed : Type

• expr : Widget.TaggedText HighlightedSubexprInfo → HighlightedMsgEmbed
• goal : InteractiveGoal → HighlightedMsgEmbed
• widget (wi : WidgetInstance) (alt : Widget.TaggedText HighlightedMsgEmbed) : HighlightedMsgEmbed
• trace (indent : Nat) (cls : Name) (msg : Widget.TaggedText HighlightedMsgEmbed) (collapsed : Bool) (children : StrictOrLazy (Array (Widget.TaggedText HighlightedMsgEmbed)) Lsp.RpcRef) : HighlightedMsgEmbed
• highlighted : HighlightedMsgEmbed

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instFromJsonHighlightedMsgEmbed : FromJson HighlightedMsgEmbed

Equations

• Lean.Server.Test.Runner.Client.instFromJsonHighlightedMsgEmbed = { fromJson? := Lean.Server.Test.Runner.Client.instFromJsonHighlightedMsgEmbed.fromJson }

partial def Lean.Server.Test.Runner.Client.instFromJsonHighlightedMsgEmbed.fromJson : Json → Except String HighlightedMsgEmbed

partial def Lean.Server.Test.Runner.Client.instToJsonHighlightedMsgEmbed.toJson : HighlightedMsgEmbed → Json

@[implicit_reducible]

instance Lean.Server.Test.Runner.Client.instToJsonHighlightedMsgEmbed : ToJson HighlightedMsgEmbed

Equations

• Lean.Server.Test.Runner.Client.instToJsonHighlightedMsgEmbed = { toJson := Lean.Server.Test.Runner.Client.instToJsonHighlightedMsgEmbed.toJson }

partial def Lean.Server.Test.Runner.Client.HighlightedMsgEmbed.normalize (m : HighlightedMsgEmbed) : NormalizeM HighlightedMsgEmbed

Test-only instances

@[implicit_reducible]

instance Lean.Server.Test.Runner.instFromJsonPanelWidgetInstance : FromJson Widget.PanelWidgetInstance

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Server.Test.Runner.instFromJsonGetWidgetsResponse : FromJson Widget.GetWidgetsResponse

Equations

• Lean.Server.Test.Runner.instFromJsonGetWidgetsResponse = { fromJson? := Lean.Server.Test.Runner.instFromJsonGetWidgetsResponse.fromJson }

def Lean.Server.Test.Runner.instFromJsonGetWidgetsResponse.fromJson : Json → Except String Widget.GetWidgetsResponse

Equations

• One or more equations did not get rendered due to their size.

def Lean.Widget.GetWidgetsResponse.debugJson (r : GetWidgetsResponse) : Json

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.word : Std.Internal.Parsec.String.Parser String

Equations

• Lean.Server.Test.Runner.word = Std.Internal.Parsec.many1Chars (Std.Internal.Parsec.String.digit <|> Std.Internal.Parsec.String.asciiLetter <|> Std.Internal.Parsec.String.pchar '_')

def Lean.Server.Test.Runner.ident : Std.Internal.Parsec.String.Parser Name

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.patchUri (s : String) : IO String

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Server.Test.Runner.patchUris : Json → IO Json

def Lean.Server.Test.Runner.printOutputLn (j : Json) : IO Unit

Equations

• Lean.Server.Test.Runner.printOutputLn j = do let __do_lift ← Lean.Server.Test.Runner.patchUris j IO.eprintln __do_lift

structure Lean.Server.Test.Runner.RunnerState : Type

• uri : Lsp.DocumentUri
• synced : Bool
• rpcSessionId : Option UInt64
• lineNo : Nat
• lastActualLineNo : Nat
• pos : Lsp.Position
• method : String
• params : String
• versionNo : Nat
• requestNo : Nat

@[reducible, inline]

abbrev Lean.Server.Test.Runner.RunnerM (α : Type) : Type

Equations

• Lean.Server.Test.Runner.RunnerM = StateT Lean.Server.Test.Runner.RunnerState Lean.Lsp.Ipc.IpcM

def Lean.Server.Test.Runner.RunnerM.run {α : Type} (act : RunnerM α) (init : RunnerState) : Lsp.Ipc.IpcM Unit

Equations

• act.run init = discard (StateT.run act init)

def Lean.Server.Test.Runner.advanceRequestNo : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.advanceVersionNo : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.setSynced : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.setDesynced : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.request {α : Type u_1} (method : String) [ToJson α] (p : α) (β : Type) [FromJson β] : RunnerM β

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.requestWithLoggedResponse {α : Type u_1} (method : String) [ToJson α] (p : α) (β : Type) [FromJson β] [ToJson β] (logParam : Bool := true) : RunnerM β

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.logResponse {α : Type u_1} (method : String) [ToJson α] (p : α) (β : Type := Json) [FromJson β] [ToJson β] (logParam : Bool := true) : RunnerM Unit

Equations

• Lean.Server.Test.Runner.logResponse method p β logParam = discard (Lean.Server.Test.Runner.requestWithLoggedResponse method p β logParam)

def Lean.Server.Test.Runner.rpcRequest {α : Type u_1} (method : Name) [ToJson α] (p : α) (β : Type) [FromJson β] : RunnerM β

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.rpcRequestWithLoggedResponse {α : Type u_1} (method : Name) [ToJson α] (p : α) (β : Type) [FromJson β] [ToJson β] (logParam : Bool := true) (normalize : β → Client.NormalizeM β := pure) : RunnerM β

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.logRpcResponse {α : Type u_1} (method : Name) [ToJson α] (p : α) (β : Type := Json) [FromJson β] [ToJson β] (logParam : Bool := true) (normalize : β → Client.NormalizeM β := pure) : RunnerM Unit

Equations

• Lean.Server.Test.Runner.logRpcResponse method p β logParam normalize = discard (Lean.Server.Test.Runner.rpcRequestWithLoggedResponse method p β logParam normalize)

def Lean.Server.Test.Runner.reset : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.skipLineWithDirective : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.skipLineWithoutDirective : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Server.Test.Runner.expandTraces (msg : Client.MsgEmbed) : RunnerM Client.MsgEmbed

def Lean.Server.Test.Runner.processEdit : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processCollectDiagnostics : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processWaitForILeans : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processSync : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.waitForMessage (msg : String) : Lsp.Ipc.IpcM Unit

Waits for a textDocument/publishDiagnostics notification with a specific message to be emitted. Discards all received messages, so should not be combined with Ipc.collectDiagnostics. Used to implement the waitFor test directive.

If the server reports a $/lean/fileProgress notification with fatalError kind, this aborts with an error rather than blocking forever: the message we are waiting for will never be produced (the worker either crashed or its header processing failed fatally, so no body elaboration will run).

Kept here rather than in Lean.Lsp.Ipc because it is specifically a test-driver helper rather than a general-purpose IPC primitive.

Equations

• Lean.Server.Test.Runner.waitForMessage msg = Lean.Server.Test.Runner.waitForMessage.loop✝ msg

def Lean.Server.Test.Runner.processWaitFor : RunnerM Unit

Equations

• Lean.Server.Test.Runner.processWaitFor = do let s ← get liftM (Lean.Server.Test.Runner.waitForMessage s.params) Lean.Server.Test.Runner.setSynced

def Lean.Server.Test.Runner.processCodeAction : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processInteractiveDiagnostics : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processGoals : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processTermGoal : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processWidgets : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processCompletion : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processIncomingCallHierarchy : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processOutgoingCallHierarchy : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processReferences : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processSymbols : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processModuleHierarchyImports : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processModuleHierarchyImportedBy : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processInlayHints : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processGenericRequest : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processDirective (_ws directive : String) (directiveTargetLineNo directiveTargetColumn : Nat) : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.processLine (line : String) : RunnerM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Test.Runner.main (args : List String) : IO Unit

Equations

• One or more equations did not get rendered due to their size.