KinoIsabelle (kino_isabelle v0.1.0-alpha.1)

Copy Markdown View Source

Livebook smart cell for Isabelle theories.

The "Isabelle theory" smart cell edits theory text and checks it with check/2 on the runtime's shared Isabelle server.

Summary

Functions

check(text, opts \\ [])

Checks text as an Isabelle theory.

Functions

check(text, opts \\ [])

@spec check(String.t(), keyword()) ::
  {:ok, KinoIsabelle.Result.t()} | {:error, term()}

Checks text as an Isabelle theory.

Options:

  • :session - logic session, default "HOL"
  • :theory - theory name, default "Scratch"
  • :imports - imported theories, default ["Main"]
  • :header_mode - :auto (default) wraps text in a theory header using :theory and :imports; :manual expects a complete theory

Returns {:ok, result} also when the theory has errors; {:error, reason} when Isabelle could not be run.