Enum fungi_lang::ast::NameTm
source · pub enum NameTm {
Var(Var),
Ident(Ident),
ValVar(Var),
Name(Name),
Bin(NameTmRec, NameTmRec),
Lam(Var, Sort, NameTmRec),
App(NameTmRec, NameTmRec),
WriteScope,
NoParse(String),
}
Expand description
Name Terms
Variants
Var(Var)
Name-term level variable x
, of some sort g
:
Γ(x) = g
----------- :: Var
Γ ⊢ x : g
Ident(Ident)
Γ(x) = (Γ', i)
Γ' ⊢ i : g
----------------- :: Ident (contextual definition)
Γ ⊢ i : g
ValVar(Var)
Injected value-level variable x
, of type Nm[i]
, for some name set i
:
Γ(x) = Nm[i]
-------------- :: ValVar
Γ ⊢ ~x : Nm
Name(Name)
------------ :: Name
Γ ⊢ n : Nm
Bin(NameTmRec, NameTmRec)
Γ ⊢ N : Nm
Γ ⊢ M : Nm
--------------- :: Bin
Γ ⊢ N * M : Nm
Lam(Var, Sort, NameTmRec)
Γ, x:g1 ⊢ M : g2
------------------------- :: Lam
Γ ⊢ #x:g1. M : g1 -> g2
App(NameTmRec, NameTmRec)
Γ ⊢ M : g1 -> g2
Γ ⊢ N : g1
------------------ :: App
Γ ⊢ [M] N : g2
WriteScope
@@ : Nm -> Nm
This is the initial/default/neutral/ambient write scope. All other write scopes are functions that compose with this one (where this function is always the “last” function in the composition).
NoParse(String)
Trait Implementations
sourceimpl Ord for NameTm
impl Ord for NameTm
1.21.0 · sourcefn max(self, other: Self) -> Selfwhere
Self: Sized,
fn max(self, other: Self) -> Selfwhere
Self: Sized,
Compares and returns the maximum of two values. Read more
1.21.0 · sourcefn min(self, other: Self) -> Selfwhere
Self: Sized,
fn min(self, other: Self) -> Selfwhere
Self: Sized,
Compares and returns the minimum of two values. Read more
1.50.0 · sourcefn clamp(self, min: Self, max: Self) -> Selfwhere
Self: Sized + PartialOrd<Self>,
fn clamp(self, min: Self, max: Self) -> Selfwhere
Self: Sized + PartialOrd<Self>,
Restrict a value to a certain interval. Read more
sourceimpl PartialOrd<NameTm> for NameTm
impl PartialOrd<NameTm> for NameTm
sourcefn partial_cmp(&self, other: &NameTm) -> Option<Ordering>
fn partial_cmp(&self, other: &NameTm) -> Option<Ordering>
1.0.0 · sourcefn le(&self, other: &Rhs) -> bool
fn le(&self, other: &Rhs) -> bool
This method tests less than or equal to (for
self
and other
) and is used by the <=
operator. Read moreimpl Eq for NameTm
impl StructuralEq for NameTm
impl StructuralPartialEq for NameTm
Auto Trait Implementations
impl RefUnwindSafe for NameTm
impl !Send for NameTm
impl !Sync for NameTm
impl Unpin for NameTm
impl UnwindSafe for NameTm
Blanket Implementations
sourceimpl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more