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.

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

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

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.

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.instToJsonSubexprInfo.toJson : SubexprInfo → Json

Equations

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

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

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.

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

Equations

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

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.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

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.

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.instToJsonInteractiveGoalCore.toJson : InteractiveGoalCore → Json

Equations

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

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.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

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.

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

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.

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

Equations

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

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

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.instFromJsonInteractiveTermGoal.fromJson : Json → Except String InteractiveTermGoal

Equations

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

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.instToJsonInteractiveTermGoal.toJson : InteractiveTermGoal → Json

Equations

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

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

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

Equations

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

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.

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 α β

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.instFromJsonStrictOrLazy.fromJson {α✝ β✝ : Type} [FromJson α✝] [FromJson β✝] : Json → Except String (StrictOrLazy α✝ β✝)

Equations

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

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 }

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)]

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

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

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

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.instFromJsonInfoPopup.fromJson : Json → Except String InfoPopup

Equations

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

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.instToJsonInfoPopup.toJson : InfoPopup → Json

Equations

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

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

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.instFromJsonGetGoToLocationParams.fromJson : Json → Except String GetGoToLocationParams

Equations

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

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

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

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.instFromJsonHighlightMatchesParams.fromJson : Json → Except String HighlightMatchesParams

Equations

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

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

Equations

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

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

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

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

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.

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"

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.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

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

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

Equations

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

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.instToJsonHighlightedMsgEmbed.toJson : HighlightedMsgEmbed → Json

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

Test-only instances

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

Equations

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

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.

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

Equations

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

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.processWaitFor : RunnerM Unit

Equations

• Lean.Server.Test.Runner.processWaitFor = do let s ← get let __discr ← liftM (Lean.Lsp.Ipc.waitForMessage s.params) have x : Unit := __discr 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 : 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.