Module fungi_lang::normal

Expand description

Static (typing-time) term reduction/normalization.

Structs

Canonical form (normal form) for a name set

Name set constructor; the subsets of a NmSet are (uniformly) combined as “apart” or “union”

Name set term. Representation for “apart/union-normal” name set terms.

Convert the highly-structured, vectorized name set representation into a less structured, AST representation.

True when the index term is normal

True when the name term is normal

Normalize a computation effect.

Normalize a computation effect.

Normalize a computation type.

Normalize an effect.

Normalize index terms, by expanding definitions and reducing function applications where possible.

Compute normal form for index term

Compute normal form for name term (expand definitions and reduce applications).

Compute normal form for name term (expand definitions and reduce applications).

Normalize types (expand definitions and reduce applications).

Unroll a rec type, exposing its recursive body’s type structure.