Enum fungi_lang::ast::IdxTm
source · pub enum IdxTm {
Show 22 variants
Var(Var),
Ident(Ident),
Sing(NameTm),
Empty,
Apart(IdxTmRec, IdxTmRec),
Union(IdxTmRec, IdxTmRec),
Unit,
Bin(IdxTmRec, IdxTmRec),
Pair(IdxTmRec, IdxTmRec),
Proj1(IdxTmRec),
Proj2(IdxTmRec),
WriteScope,
NmSet(NmSet),
Lam(Var, Sort, IdxTmRec),
App(IdxTmRec, IdxTmRec),
Map(NameTmRec, IdxTmRec),
MapStar(NameTmRec, IdxTmRec),
FlatMap(IdxTmRec, IdxTmRec),
FlatMapStar(IdxTmRec, IdxTmRec),
NmTm(NameTm),
NoParse(String),
Unknown,
}
Expand description
Index terms
Variants
Var(Var)
Γ(x) = g
----------- :: Var
Γ ⊢ x : g
Ident(Ident)
Γ(x) = (Γ', i)
Γ' ⊢ i : g
----------------- :: Ident (contextual definition)
Γ ⊢ i : g
Sing(NameTm)
Γ ⊢ M : Nm
------------------ :: Sing
Γ ⊢ { M } : NmSet
Empty
-------------- :: Empty
Γ ⊢ 0 : NmSet
Apart(IdxTmRec, IdxTmRec)
Γ ⊢ i : NmSet
Γ ⊢ j : NmSet
------------------- :: Apart
Γ ⊢ i % j : NmSet
Union(IdxTmRec, IdxTmRec)
Γ ⊢ i : NmSet
Γ ⊢ j : NmSet
------------------- :: Union
Γ ⊢ i U j : NmSet
Unit
-------------- :: Unit
Γ ⊢ () : ??
Bin(IdxTmRec, IdxTmRec)
Γ ⊢ i : NmSet
Γ ⊢ j : NmSet
----------------------- :: Bin
Γ ⊢ i * j : NmSet
Pair(IdxTmRec, IdxTmRec)
Γ ⊢ i : g1
Γ ⊢ j : g2
------------------------- :: Pair
Γ ⊢ (i , j) : g1 x g2
Proj1(IdxTmRec)
Γ ⊢ i : g1 x g2
------------------ :: Proj1
Γ ⊢ proj1 i : g1
Proj2(IdxTmRec)
Γ ⊢ i : g1 x g2
------------------ :: Proj2
Γ ⊢ proj2 i : g2
WriteScope
@! : NmSet -> NmSet
The ambient write scope (@@ : Nm -> Nm
), lifted to name sets.
NmSet(NmSet)
A normalized form for union/apart name sub-sets; never written
directly by the programmer. This form is used by the normal
module for distributing set-level functions over a sets’
constructors, for a uniform choice of type NmSetCons
.
Lam(Var, Sort, IdxTmRec)
Γ, x:g1 ⊢ i : g2
-------------------------- :: Lam
Γ ⊢ #x:g1. i : g1 -> g2
App(IdxTmRec, IdxTmRec)
Γ ⊢ i : g1 -> g2
Γ ⊢ j : g1
------------------ :: App
Γ ⊢ {i} j : g2
Map(NameTmRec, IdxTmRec)
Γ ⊢ M : Nm -> Nm
Γ ⊢ j : NmSet
------------------ :: Map
Γ ⊢ [M] j : NmSet
MapStar(NameTmRec, IdxTmRec)
Γ ⊢ M : Nm -> Nm
Γ ⊢ j : NmSet
------------------ :: MapStar
Γ ⊢ [M]^* j : NmSet
FlatMap(IdxTmRec, IdxTmRec)
Γ ⊢ i : Nm -> NmSet
Γ ⊢ j : NmSet
----------------------- :: FlatMap
Γ ⊢ (i) j : NmSet
FlatMapStar(IdxTmRec, IdxTmRec)
Γ ⊢ i : Nm -> NmSet
Γ ⊢ j : NmSet
----------------------- :: FlatMapStar
Γ ⊢ (i)^* j : NmSet
NmTm(NameTm)
Γ ⊢ M : g
--------------- :: nmtm
Γ ⊢ nmtm M : g
NoParse(String)
Unknown
Trait Implementations
sourceimpl Ord for IdxTm
impl Ord for IdxTm
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<IdxTm> for IdxTm
impl PartialOrd<IdxTm> for IdxTm
sourcefn partial_cmp(&self, other: &IdxTm) -> Option<Ordering>
fn partial_cmp(&self, other: &IdxTm) -> 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 IdxTm
impl StructuralEq for IdxTm
impl StructuralPartialEq for IdxTm
Auto Trait Implementations
impl RefUnwindSafe for IdxTm
impl !Send for IdxTm
impl !Sync for IdxTm
impl Unpin for IdxTm
impl UnwindSafe for IdxTm
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