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

Equations

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

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

Equations

• Lean.Server.Test.Runner.Client.instReprSubexprInfo = { reprPrec := Lean.Server.Test.Runner.Client.reprSubexprInfo✝ }

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

Equations

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

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

Equations

• Lean.Server.Test.Runner.Client.instReprHyp = { reprPrec := Lean.Server.Test.Runner.Client.reprHyp✝ }

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

Equations

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

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

Equations

• Lean.Server.Test.Runner.Client.instReprInteractiveGoal = { reprPrec := Lean.Server.Test.Runner.Client.reprInteractiveGoal✝ }

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

• goals : Array InteractiveGoal

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

Equations

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

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

Equations

• Lean.Server.Test.Runner.Client.instReprInteractiveGoals = { reprPrec := Lean.Server.Test.Runner.Client.reprInteractiveGoals✝ }

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.

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

Equations

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

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.main (args : List String) : IO Unit

Equations

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

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