Enum Term

pub enum Term {
    Whnf(Val),
    Redex(GI, Ident, Vec<Elim>),
}

Type for terms.

Variants

Whnf(Val)

Redex(GI, Ident, Vec<Elim>)

Implementations

impl Term

Constructors and traversal functions.

pub fn is_type(&self) -> bool

pub fn is_universe(&self) -> bool

pub fn cons(name: ConHead, params: Vec<Self>) -> Self

pub fn data(info: ValData) -> Self

pub fn meta(index: MI, params: Vec<Elim>) -> Self

pub fn reflexivity() -> Self

pub fn universe(level: Level) -> Self

pub fn identity(ty: Self, a: Self, b: Self) -> Self

pub fn fresh_axiom() -> Self

pub(crate) fn postulate(uid: UID) -> Self

pub fn def(gi: GI, ident: Ident, elims: Vec<Elim>) -> Self

pub fn simple_def(gi: GI, ident: Ident) -> Self

pub fn pi_from_tele(tele: Tele, ret: Self) -> Self

pub fn tele_view(self) -> (Tele, Self)

Returns

The telescope and the return type.

pub fn pi(licit: Plicit, name: UID, param_type: Term, body: Closure) -> Self

pub fn pi2(param: Bind<Box<Term>>, body: Closure) -> Self

impl Term

pub fn apply(self, args: Vec<Term>) -> Self

Use Term instead of Self to emphasize that it’s not Elim.

pub fn apply_elim(self, args: Vec<Elim>) -> Self

impl Term

pub fn at(self, loc: Loc) -> TermInfo

Trait Implementations

impl Clone for Term

fn clone(&self) -> Term

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl DeBruijn for Term

fn dbi_view(&self) -> Option<DBI>

Agda.

fn from_dbi(dbi: DBI) -> Self

Agda.

impl Debug for Term

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for Term

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl FoldVal for Term

fn try_fold_val<E, R>( &self, init: R, f: impl Fn(R, &Val) -> Result<R, E> + Copy, ) -> Result<R, E>

impl HasMeta for Term

fn inline_meta(self, tcs: TCS) -> TCMS<Self>

Inline solved metas inside self.

impl PartialEq for Term

fn eq(&self, other: &Term) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl RedEx<Term> for Val

fn reduce_dbi(self, subst: Rc<Subst>) -> Term

Apply a substitution to a redex.

impl RedEx for Term

fn reduce_dbi(self, subst: Rc<Subst>) -> Term

Apply a substitution to a redex.

impl TryFrom<Copat<DBI, Term>> for Term

type Error = String

The type returned in the event of a conversion error.

fn try_from(p: CoreCopat) -> Result<Term, String>

Performs the conversion.

impl TryFrom<Pat<DBI, Term>> for Term

type Error = String

The type returned in the event of a conversion error.

fn try_from(p: CorePat) -> Result<Term, String>

Performs the conversion.

impl Unify for Term

fn unify(tcs: TCS, left: &Self, right: &Self) -> TCM

Conversion check, maybe can solve metas.

impl Eq for Term

impl StructuralPartialEq for Term