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

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

• subexprPos : String
• diffStatus? : Option String

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

instance Lean.Server.Test.Runner.Client.instReprSubexprInfo : Repr SubexprInfo

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

• type : Widget.TaggedText SubexprInfo
• names : Array String
• isInserted? : Option Bool
• isRemoved? : Option Bool

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

instance Lean.Server.Test.Runner.Client.instReprHyp : Repr Hyp

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

• type : Widget.TaggedText SubexprInfo
• isInserted? : Option Bool
• isRemoved? : Option Bool
• hyps : Array Hyp

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

instance Lean.Server.Test.Runner.Client.instReprInteractiveGoal : Repr InteractiveGoal

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

• goals : Array InteractiveGoal

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

instance Lean.Server.Test.Runner.Client.instReprInteractiveGoals : Repr InteractiveGoals

Test-only instances

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

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

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

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

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

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

partial def Lean.Server.Test.Runner.main.readFirstResponse (requestNo : Nat) : Lsp.Ipc.IpcM Json