# `ShotTo.TypeOrder`
[🔗](https://github.com/jcschuster/ShotTo/blob/v0.1.0/lib/shot_to/type_order.ex#L1)

Admissible type order `≻_T` and related predicates used by NCPO-LNF.

The order implemented here is the concrete admissible order of Lemma 4
in the NCPO-LNF paper (Niederhauser & Middeldorp, 2025), which is in
turn Lemma 2.3 of the CPO paper [Blanqui/Jouannaud/Rubio, 2015]. It is
the smallest order `≻_T` on `ShotDs.Data.Type.t` that contains:

  * the strict part of the user-supplied sort precedence `≻_S`, and
  * the *right-argument* relation `▷_r` (i.e. `T → U ▷_r U`),

and is closed under right-congruence (`V ≻_T V'` implies
`U → V ≻_T U → V'` for every `U`).

Note: `ShotDs.Data.Type` represents function types in uncurried form, so
`T_1 → T_2 → … → T_n → a` corresponds to
`%Type{goal: a, args: [T_1, …, T_n]}`. The implementation is written
directly on this representation rather than on a curried view.

# `base?`

```elixir
@spec base?(ShotDs.Data.Type.t()) :: boolean()
```

Returns `true` if the argument type is a base type (no function arrows).

# `occurs_in?`

```elixir
@spec occurs_in?(atom(), ShotDs.Data.Type.t()) :: boolean()
```

Returns `true` if the base sort `a` occurs anywhere within the given
type. This is the boolean version of the `Pos_a(T) ≠ ∅` predicate used
by the structurally-smaller rule: the paper's requirement
`Pos_a(T_i) = ∅` translates to `not occurs_in?/2`.

    iex> alias ShotDs.Data.Type
    iex> alias ShotTo.TypeOrder
    iex> TypeOrder.occurs_in?(:i, Type.new(:o, [:i, :o]))
    true
    iex> TypeOrder.occurs_in?(:i, Type.new(:o))
    false

# `type_geq?`

```elixir
@spec type_geq?(ShotDs.Data.Type.t(), ShotDs.Data.Type.t(), ShotTo.Parameters.t()) ::
  boolean()
```

Reflexive closure: `t ⪰_T u` iff `t = u` or `t ≻_T u`.

# `type_gt?`

```elixir
@spec type_gt?(ShotDs.Data.Type.t(), ShotDs.Data.Type.t(), ShotTo.Parameters.t()) ::
  boolean()
```

Returns `true` if `lhs ≻_T rhs` in the admissible type order derived
from the sort precedence in `params`.

Strict order: `type_gt?(t, t, _)` is always `false`.

---

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