Theoria.Term (theoria v0.3.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, levels \\ [])

constants(term)

Returns the environment constants referenced by term.

eq(type, left, right)

eq_rec(type, motive, base, proof)

forall(name, domain, body)

lam(name, domain, body)

let(name, type, value, body)

level_params(term)

Returns the universe parameters referenced by term.

refl(value)

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_levels(term, subst)

Substitutes universe level parameters in a term.

subst_top(body, replacement)

Substitutes the outermost bound variable in body with replacement.

well_scoped?(term, depth \\ 0)

Returns true when every bound variable index is in scope at the given depth.

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()
  | Theoria.Term.Let.t()
  | Theoria.Term.Eq.t()
  | Theoria.Term.Refl.t()
  | Theoria.Term.EqRec.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, levels \\ [])

@spec const(atom(), [non_neg_integer() | Theoria.Level.t()]) :: Theoria.Term.Const.t()

constants(term)

@spec constants(t()) :: MapSet.t(atom())

Returns the environment constants referenced by term.

eq(type, left, right)

@spec eq(t(), t(), t()) :: Theoria.Term.Eq.t()

eq_rec(type, motive, base, proof)

@spec eq_rec(t(), t(), t(), t()) :: Theoria.Term.EqRec.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()

let(name, type, value, body)

@spec let(atom(), t(), t(), t()) :: Theoria.Term.Let.t()

level_params(term)

@spec level_params(t()) :: MapSet.t(atom())

Returns the universe parameters referenced by term.

refl(value)

@spec refl(t()) :: Theoria.Term.Refl.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.Level.t()) :: 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_levels(term, subst)

@spec subst_levels(t(), Theoria.Level.subst()) :: t()

Substitutes universe level parameters in a term.

subst_top(body, replacement)

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

Substitutes the outermost bound variable in body with replacement.

well_scoped?(term, depth \\ 0)

@spec well_scoped?(t(), non_neg_integer()) :: boolean()

Returns true when every bound variable index is in scope at the given depth.