Module fungi_lang::normal
[−]
[src]
Static (typing-time) term reduction/normalization.
Structs
NmSet |
Canonical form (normal form) for a name set |
Enums
NmSetCons |
Name set constructor; the subsets of a |
NmSetTm |
Name set term. Representation for "apart/union-normal" name set terms. |
Functions
idxtm_of_nmsettms |
Convert the highly-structured, vectorized name set representation into a less structured, AST representation. |
is_normal_idxtm |
True when the index term is normal |
is_normal_nmtm |
True when the name term is normal |
normal_ceffect |
Normalize a computation effect. |
normal_ceffect_rec |
Normalize a computation effect. |
normal_ctype |
Normalize a computation type. |
normal_effect |
Normalize an effect. |
normal_idxtm |
Normalize index terms, by expanding definitions and reducing function applications where possible. |
normal_idxtm_rec |
Compute normal form for index term |
normal_nmtm |
Compute normal form for name term (expand definitions and reduce applications). |
normal_nmtm_rec |
Compute normal form for name term (expand definitions and reduce applications). |
normal_type |
Normalize types (expand definitions and reduce applications). |
unroll_type |
Unroll a |
Type Definitions
NmSetTms |