KinoIsabelle.Result (kino_isabelle v0.1.0-alpha.1)

Copy Markdown View Source

Result of KinoIsabelle.check/2. Renders in Livebook as tabs.

  • :status - :ok when Isabelle accepted the theory, else :failed
  • :theory - the theory name
  • :text - the checked cell text
  • :messages - KinoIsabelle.Messages.message/0s ordered by position; from and to are UTF-16 offsets in :text
  • :node_status - Isabelle's node status counters, nil if the header failed
  • :raw - the raw use_theories result

Summary

Types

t()

Types

t()

@type t() :: %KinoIsabelle.Result{
  messages: [KinoIsabelle.Messages.message()],
  node_status: map() | nil,
  raw: map(),
  status: :ok | :failed,
  text: String.t(),
  theory: String.t()
}