Struct Expr

pub struct Expr {
    pub data: ExprKind,
    pub range: Range,
}

Describes a single expression inside Kind2.

Fields

data: ExprKind

range: Range

Implementations

impl Expr

pub fn var(name: Ident) -> Box<Expr>

pub fn cons(name: QualifiedIdent, args: Spine, range: Range) -> Box<Expr>

pub fn all( param: Ident, typ: Box<Expr>, body: Box<Expr>, erased: bool, range: Range, ) -> Box<Expr>

pub fn lambda( param: Ident, typ: Option<Box<Expr>>, body: Box<Expr>, erased: bool, range: Range, ) -> Box<Expr>

pub fn typ(range: Range) -> Box<Expr>

pub fn app(fun: Box<Expr>, args: Vec<AppBinding>, range: Range) -> Box<Expr>

pub fn hole(range: Range) -> Box<Expr>

impl Expr

pub fn traverse_pi_types(&self) -> String

Trait Implementations

impl Clone for Expr

fn clone(&self) -> Expr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Expr

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

Formats the value using the given formatter.

impl Display for Expr

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

Formats the value using the given formatter.

impl Locatable for Expr

fn locate(&self) -> Range