Module fungi_lang::subst

Static (typing-time) substitutions.

Functions

subst_idxtm_type	Substitute an index for an index variable in another type
subst_term_ceffect	Substitute terms into computation effects
subst_term_ceffect_rec	Substitute terms into computation effects
subst_term_ctype	Substitute terms into computation types
subst_term_effect	Substitute terms into effects
subst_term_effect_rec	Substitute terms into effects
subst_term_idxtm	Substitute terms into index terms
subst_term_idxtm_rec	Substitute terms into index terms
subst_term_nmtm	Substitute name terms into name terms
subst_term_nmtm_rec	Substitute terms into name terms
subst_term_prop	Substitute terms into propositions
subst_term_type	Substitute terms into types
subst_term_type_rec	Substitute terms into types
subst_type_type	Substitute a type for a type variable in another type
term_is_idxtm	Predicate for index terms
term_is_nmtm	Predicate for name terms
term_is_type	Predicate for type terms