Enum voile::syntax::abs::ast::Abs

pub enum Abs {
    Type(SyntaxInfo, Level),
    Bot(SyntaxInfo),
    Var(Ident, UID, DBI),
    Ref(Ident, DBI),
    Meta(Ident),
    Lift(SyntaxInfo, u32, Box<Self>),
    Cons(Ident),
    Variant(Ident),
    App(SyntaxInfo, Box<Self>, Box<Self>),
    Dt(SyntaxInfo, DtKind, UID, Box<Self>, Box<Self>),
    Lam(SyntaxInfo, Ident, UID, Box<Self>),
    Pair(SyntaxInfo, Box<Self>, Box<Self>),
    Fst(SyntaxInfo, Box<Self>),
    Snd(SyntaxInfo, Box<Self>),
    Sum(SyntaxInfo, Vec<Self>),
}

Variants

Type(SyntaxInfo, Level)Bot(SyntaxInfo)

Bottom type

Var(Ident, UID, DBI)

Local variable

Ref(Ident, DBI)

Global variable

Meta(Ident)

Meta variable

Lift(SyntaxInfo, u32, Box<Self>)

Lift an expression many times

Cons(Ident)

Constructor call

Variant(Ident)

One variant inside of a sum type

App(SyntaxInfo, Box<Self>, Box<Self>)

Apply or Pipeline in surface

Dt(SyntaxInfo, DtKind, UID, Box<Self>, Box<Self>)

Dependent Type, (a -> b -> c) as Dt(DtKind::Pi, a, Dt(DtKind::Pi, b, c))

Lam(SyntaxInfo, Ident, UID, Box<Self>)

The first SyntaxInfo is the syntax info of this whole lambda, while the second is about its parameter

Pair(SyntaxInfo, Box<Self>, Box<Self>)Fst(SyntaxInfo, Box<Self>)Snd(SyntaxInfo, Box<Self>)Sum(SyntaxInfo, Vec<Self>)

Methods

impl Abs

pub fn dependent_type(
    info: SyntaxInfo,
    kind: DtKind,
    name: UID,
    a: Self,
    b: Self
) -> Self

pub fn app(info: SyntaxInfo, function: Self, argument: Self) -> Self

pub fn fst(info: SyntaxInfo, of: Self) -> Self

pub fn snd(info: SyntaxInfo, of: Self) -> Self

pub fn lam(whole_info: SyntaxInfo, param: Ident, name: UID, body: Self) -> Self

pub fn pair(info: SyntaxInfo, first: Self, second: Self) -> Self

pub fn lift(info: SyntaxInfo, lift_count: u32, expr: Self) -> Self

pub fn pi(info: SyntaxInfo, name: UID, input: Self, output: Self) -> Self

pub fn sig(info: SyntaxInfo, name: UID, first: Self, second: Self) -> Self

Trait Implementations

impl ToSyntaxInfo for Abs

fn syntax_info(&self) -> SyntaxInfo

Borrow the syntax info.

impl Eq for Abs

fn assert_receiver_is_total_eq(&self)

impl PartialEq<Abs> for Abs

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

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

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

This method tests for !=.

impl Clone for Abs

fn clone(&self) -> Abs

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Abs

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

Formats the value using the given formatter.

impl Display for Abs

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

Formats the value using the given formatter.