ShotDs.Util.LatexFormatter (shot_ds v1.2.4)

Renders HOL objects as LaTeX.

Types are printed as subscripts. Logical constants of the signature (⊤, ⊥, ¬, ∧, ∨, ⊃, ≡, =, ∀, ∃) are rendered as their standard LaTeX symbols without any type annotation. Bound variables are reconstructed with fresh names drawn from a type-specific pool, avoiding capture with free variables and outer binders. Duplicates are disambiguated with running superscripts (subscripts are reserved for the type annotation).

Examples

iex> import ShotDs.Hol.Dsl
iex> import ShotDs.Hol.Definitions
iex> alias ShotDs.Util.LatexFormatter
iex> t = forall(x_i(), &(x_i() &&& &1))
...> # etc.

Summary

Types

formattable()

HOL objects understood by the formatter.

opts()

Options accepted by format/2 and format!/2.

Functions

format(obj, opts \\ [])

Renders the given HOL object as a LaTeX string. Returns {:ok, result} or {:error, reason}.

format!(obj, opts \\ [])

Renders the given HOL object as a LaTeX string. Raises on error.

Types

formattable()

@type formattable() ::
  ShotDs.Data.Type.t()
  | ShotDs.Data.Declaration.t()
  | ShotDs.Data.Term.t()
  | ShotDs.Data.Term.term_id()
  | ShotDs.Data.Substitution.t()
  | ShotDs.Data.Problem.t()

HOL objects understood by the formatter.

opts()

@type opts() :: [
  hide_types: boolean(),
  merge_binder: boolean(),
  reconstruct_names: boolean(),
  math_mode: :raw | :inline | :display
]

Options accepted by format/2 and format!/2.

:hide_types — omit type subscripts on non-logical symbols (default false).
:merge_binder — collapse ∀(λx. body) into ∀ x.\, body (default true; ignored when :reconstruct_names is false).
:reconstruct_names — pick fresh names for bound variables (default true). When false, binders are rendered as \lambda_{τ} and bound references as \mathtt{k}_{τ}, preserving the raw de Bruijn structure.
:math_mode — one of :raw (default), :inline ( $…$ ) or :display ($$…$$).

Functions

format(obj, opts \\ [])

@spec format(formattable(), opts()) ::
  {:ok, String.t()}
  | ShotDs.Stt.TermFactory.lookup_error_t()
  | {:error, :unknown_argument}

Renders the given HOL object as a LaTeX string. Returns {:ok, result} or {:error, reason}.

format!(obj, opts \\ [])

@spec format!(formattable(), opts()) :: String.t()

Renders the given HOL object as a LaTeX string. Raises on error.