# `Theoria.Term`
[🔗](https://github.com/elixir-vibe/theoria/blob/main/lib/theoria/term.ex#L1)

Core terms for Theoria's trusted kernel.

Terms use de Bruijn indices internally. User-facing names are retained only for
diagnostics and pretty-printing; binding correctness is determined by indices.

# `t`

```elixir
@type t() ::
  Theoria.Term.Sort.t()
  | Theoria.Term.BVar.t()
  | Theoria.Term.Const.t()
  | Theoria.Term.App.t()
  | Theoria.Term.Lam.t()
  | Theoria.Term.Forall.t()
```

# `app`

```elixir
@spec app(t(), t()) :: Theoria.Term.App.t()
```

# `arrow`

```elixir
@spec arrow(t(), t()) :: Theoria.Term.Forall.t()
```

# `bvar`

```elixir
@spec bvar(non_neg_integer()) :: Theoria.Term.BVar.t()
```

# `const`

```elixir
@spec const(atom()) :: Theoria.Term.Const.t()
```

# `forall`

```elixir
@spec forall(atom(), t(), t()) :: Theoria.Term.Forall.t()
```

# `lam`

```elixir
@spec lam(atom(), t(), t()) :: Theoria.Term.Lam.t()
```

# `shift`

```elixir
@spec shift(t(), integer(), non_neg_integer()) :: t()
```

Shifts de Bruijn indices by `amount` at and above `cutoff`.

# `sort`

```elixir
@spec sort(non_neg_integer()) :: Theoria.Term.Sort.t()
```

# `subst`

```elixir
@spec subst(t(), non_neg_integer(), t(), non_neg_integer()) :: t()
```

Substitutes de Bruijn variable `index` with `replacement`.

# `subst_top`

```elixir
@spec subst_top(t(), t()) :: t()
```

Substitutes the outermost bound variable in `body` with `replacement`.

---

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