Theoria.Syntax (theoria v0.6.0)

Copy Markdown View Source

Named surface terms for building Theoria core terms.

Surface terms are not trusted. They must be elaborated to Theoria.Term values and checked by Theoria.Kernel before they can prove anything.

Summary

Types

t()

Functions

app(fun, arg)
arrow(domain, codomain)
const(name, levels \\ [])
eq(type, left, right)
eq_rec(type, motive, base, proof)
forall(name, domain, body)
from_core(term, context \\ [])

Converts a core de Bruijn term back to named syntax using context for bound variables.

lam(name, domain, body)
let(name, type, value, body)
refl(value)
sort(level)
var(name)

Types

t()

@type t() ::
  Theoria.Syntax.Sort.t()
  | Theoria.Syntax.Var.t()
  | Theoria.Syntax.Const.t()
  | Theoria.Syntax.App.t()
  | Theoria.Syntax.Lam.t()
  | Theoria.Syntax.Forall.t()
  | Theoria.Syntax.Let.t()
  | Theoria.Syntax.Eq.t()
  | Theoria.Syntax.Refl.t()
  | Theoria.Syntax.EqRec.t()

Functions

app(fun, arg)

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

arrow(domain, codomain)

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

const(name, levels \\ [])

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

eq(type, left, right)

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

eq_rec(type, motive, base, proof)

@spec eq_rec(t(), t(), t(), t()) :: Theoria.Syntax.EqRec.t()

forall(name, domain, body)

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

from_core(term, context \\ [])

@spec from_core(Theoria.Term.t(), [atom()]) :: t()

Converts a core de Bruijn term back to named syntax using context for bound variables.

lam(name, domain, body)

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

let(name, type, value, body)

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

refl(value)

@spec refl(t()) :: Theoria.Syntax.Refl.t()

sort(level)

@spec sort(non_neg_integer() | Theoria.Level.t()) :: Theoria.Syntax.Sort.t()

var(name)

@spec var(atom()) :: Theoria.Syntax.Var.t()