Enum fungi_lang::bitype::NmTmRule
source · pub enum NmTmRule {
Var(Var),
ValVar(Var),
Name(Name),
Bin(NmTmDer, NmTmDer),
Lam(Var, Sort, NmTmDer),
App(NmTmDer, NmTmDer),
WriteScope,
NoParse(String),
}
Expand description
Name term sorting rule
Variants
Var(Var)
Name-term level variable x
, of some sort g
:
Γ(x) = g
----------- :: Var
Γ ⊢ x : 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(NmTmDer, NmTmDer)
Γ ⊢ N : Nm
Γ ⊢ M : Nm
--------------- :: Bin
Γ ⊢ N * M : Nm
Lam(Var, Sort, NmTmDer)
Γ, x:g1 ⊢ M : g2
------------------------- :: Lam
Γ ⊢ #x:g1. M : g1 -> g2
App(NmTmDer, NmTmDer)
Γ ⊢ 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
impl Eq for NmTmRule
impl StructuralEq for NmTmRule
impl StructuralPartialEq for NmTmRule
Auto Trait Implementations
impl !RefUnwindSafe for NmTmRule
impl !Send for NmTmRule
impl !Sync for NmTmRule
impl Unpin for NmTmRule
impl !UnwindSafe for NmTmRule
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