Module fungi_lang::normal[−][src]

Static (typing-time) term reduction/normalization.

Structs

Canonical form (normal form) for a name set

NmSetCons	Name set constructor; the subsets of a `NmSet` are (uniformly) combined as "apart" or "union"
NmSetTm	Name set term. Representation for "apart/union-normal" name set terms.

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
match_ceffect
match_ctype
match_type
match_type_rec
nmset_cons_join
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 `rec` type, exposing its recursive body's type structure.