Enum nar::syntax::core::Term

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

Type for terms.

Variants

Whnf(Val)

Redex(GI, Ident, Vec<Elim>)

Methods

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 Eq for Term

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<Term> for Term

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

This method tests for self and other values to be equal, and is used by ==.

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

This method tests for !=.

impl<A, B, X: RedEx<A>, Y: RedEx<B>> RedEx<(A, B), Term> for (X, Y)

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

Apply a substitution to a redex.

impl<R, T: RedEx<R>> RedEx<Bind<R>, Term> for Bind<T>

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

Apply a substitution to a redex.

impl RedEx<Closure, Term> for Closure

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

Apply a substitution to a redex.

impl<Ix, R, T: RedEx<R>> RedEx<Copat<Ix, R>, Term> for Copat<Ix, T>

fn reduce_dbi(self, subst: Rc<Subst>) -> Copat<Ix, R>

Apply a substitution to a redex.

impl RedEx<Elim, Term> for Elim

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

Apply a substitution to a redex.

impl RedEx<Equation, Term> for Equation

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

Apply a substitution to a redex.

impl<R, T: RedEx<R>> RedEx<Let<R>, Term> for Let<T>

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

Apply a substitution to a redex.

impl<R, T: RedEx<R>> RedEx<MetaSol<R>, Term> for MetaSol<T>

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

Apply a substitution to a redex.

impl<R, T: RedEx<R>> RedEx<MetaSolution<R>, Term> for MetaSolution<T>

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

Apply a substitution to a redex.

impl<Ix, R, T: RedEx<R>> RedEx<Pat<Ix, R>, Term> for Pat<Ix, T>

fn reduce_dbi(self, subst: Rc<Subst>) -> Pat<Ix, R>

Apply a substitution to a redex.

impl RedEx<Term, Term> for Term

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

Apply a substitution to a redex.

impl RedEx<Term, Term> for Val

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

Apply a substitution to a redex.

impl RedEx<ValData, Term> for ValData

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

Apply a substitution to a redex.

impl<R, T: RedEx<R>> RedEx<Vec<R>, Term> for Vec<T>

For Tele.

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

Apply a substitution to a redex.

impl StructuralEq for Term

impl StructuralPartialEq for Term

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.