[−][src]Enum voile::syntax::abs::Abs
Variants
Type(SyntaxInfo, Level)
Var(Ident, UID, DBI)
Local variable
Ref(Ident, GI)
Global variable
Meta(Ident, MI)
Meta variable
Lift(SyntaxInfo, u32, Box<Self>)
Lift an expression many times
Cons(Ident)
Constructor call
App(SyntaxInfo, Box<Self>, Box<Self>)
Apply or Pipeline in surface
Dt(SyntaxInfo, PiSig, 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>)
RowPoly(SyntaxInfo, VarRec, Vec<LabAbs>, Option<Box<Self>>)
Row-polymorphic types, corresponds to RowPoly
RowKind(SyntaxInfo, VarRec, Vec<Ident>)
Row-polymorphic kinds, corresponds to RowKind
Methods
impl Abs
[src]
pub fn dependent_type(
info: SyntaxInfo,
kind: PiSig,
name: UID,
a: Self,
b: Self
) -> Self
[src]
info: SyntaxInfo,
kind: PiSig,
name: UID,
a: Self,
b: Self
) -> Self
pub fn row_polymorphic_type(
info: SyntaxInfo,
kind: VarRec,
labels: Vec<LabAbs>,
rest: Option<Self>
) -> Self
[src]
info: SyntaxInfo,
kind: VarRec,
labels: Vec<LabAbs>,
rest: Option<Self>
) -> Self
pub fn app(info: SyntaxInfo, function: Self, argument: Self) -> Self
[src]
pub fn fst(info: SyntaxInfo, of: Self) -> Self
[src]
pub fn snd(info: SyntaxInfo, of: Self) -> Self
[src]
pub fn lam(whole_info: SyntaxInfo, param: Ident, name: UID, body: Self) -> Self
[src]
pub fn pair(info: SyntaxInfo, first: Self, second: Self) -> Self
[src]
pub fn lift(info: SyntaxInfo, lift_count: u32, expr: Self) -> Self
[src]
pub fn pi(info: SyntaxInfo, name: UID, input: Self, output: Self) -> Self
[src]
pub fn sig(info: SyntaxInfo, name: UID, first: Self, second: Self) -> Self
[src]
Trait Implementations
impl ToSyntaxInfo for Abs
[src]
fn syntax_info(&self) -> SyntaxInfo
[src]
impl Clone for Abs
[src]
fn clone(&self) -> Abs
[src]
fn clone_from(&mut self, source: &Self)
1.0.0[src]
Performs copy-assignment from source
. Read more
impl PartialEq<Abs> for Abs
[src]
impl Eq for Abs
[src]
fn assert_receiver_is_total_eq(&self)
[src]
impl Display for Abs
[src]
impl Debug for Abs
[src]
Auto Trait Implementations
impl Sync for Abs
impl Send for Abs
impl Unpin for Abs
impl UnwindSafe for Abs
impl RefUnwindSafe for Abs
Blanket Implementations
impl<T> From<T> for T
[src]
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T> ToString for T where
T: Display + ?Sized,
[src]
T: Display + ?Sized,
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,