Theoria.Term (theoria v0.1.0)

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.

Summary

Types

t()

Functions

app(fun, arg)

arrow(domain, codomain)

bvar(index)

const(name)

forall(name, domain, body)

lam(name, domain, body)

shift(term, amount, cutoff \\ 0)

Shifts de Bruijn indices by amount at and above cutoff.

sort(level)

subst(term, index, replacement, depth \\ 0)

Substitutes de Bruijn variable index with replacement.

subst_top(body, replacement)

Substitutes the outermost bound variable in body with replacement.

Types

t()

@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()

Functions

app(fun, arg)

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

arrow(domain, codomain)

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

bvar(index)

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

const(name)

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

forall(name, domain, body)

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

lam(name, domain, body)

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

shift(term, amount, cutoff \\ 0)

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

Shifts de Bruijn indices by amount at and above cutoff.

sort(level)

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

subst(term, index, replacement, depth \\ 0)

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

Substitutes de Bruijn variable index with replacement.

subst_top(body, replacement)

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

Substitutes the outermost bound variable in body with replacement.