Macro fungi_lang::fgi_ceffect
source · macro_rules! fgi_ceffect {
{ fromast $ast:expr } => { ... };
{ ($($e:tt)+) } => { ... };
{ forallt ($a:ident):$k:tt.$($e:tt)+ } => { ... };
{ forallt $a:ident:$k:tt.$($e:tt)+ } => { ... };
{ forallt ($a:ident,$($vars:ident),+):$k:tt.$($e:tt)+ } => { ... };
{ foralli ($a:ident):$g:tt|$p:tt.$($e:tt)+ } => { ... };
{ foralli $a:ident:$g:tt|$p:tt.$($e:tt)+ } => { ... };
{ foralli ($a:ident,$($vars:ident),+):$g:tt|$p:tt.$($e:tt)+ } => { ... };
{ foralli $a:ident:$g:tt.$($e:tt)+ } => { ... };
{ foralli ($a:ident):$g:tt.$($e:tt)+ } => { ... };
{ foralli ($a:ident,$($vars:ident),+):$g:tt.$($e:tt)+ } => { ... };
{ $($arr:tt)+ } => { ... };
{ $($any:tt)* } => { ... };
}
Expand description
Parser for Computations with effects
E ::=
fromast ast (inject ast nodes)
(E) (parens)
forallt (a,...):K.E (extended type polymorphism)
foralli (a,...):g|P.E (index polymorphism)
foralli (a,...):g.E (index polymorphism -- true prop)
ε C (computation with effect)