# `ShotDs.Util.LatexFormatter`
[🔗](https://github.com/jcschuster/ShotDs/blob/v1.3.1/lib/shot_ds/util/latex_formatter.ex#L1)

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(type_o(), &(true_term() ||| &1))
    ...> # etc.

# `formattable`

```elixir
@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`

```elixir
@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`
    (`$$…$$`).

# `format`

```elixir
@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!`

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

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

# `with_latex_aliases`

```elixir
@spec with_latex_aliases(%{required(reference()) => String.t()}, (-> a)) :: a
when a: var
```

Runs `fun` with a **LaTeX** alias map active. Unlike
`ShotDs.Util.Formatter.with_aliases/2` — whose values go through
`escape_name/1` before being spliced into the output — values here
are used *verbatim* as LaTeX for the corresponding `reference()`
variable name or type goal. That lets callers hand out proper LaTeX
identifiers (e.g. `"H^{1}"`, `"\hat{F}_{2}"`) for fresh metas.

Falls back through `:hol_aliases` (plain-text nicknames) and finally
to the `V^{short_ref}`/`\mathrm{c}^{short_ref}`/`\tau_{short_ref}`
defaults for any ref not listed in this map (free variable, constant,
and type-goal, respectively). Restores the previous binding on exit.

Only `LatexFormatter` consults `:hol_latex_aliases` — the plain-text
`Formatter` and `Declaration.format/2` ignore it entirely, so the two
alias mechanisms don't interfere.

---

*Consult [api-reference.md](api-reference.md) for complete listing*