Module fungi_lang::subst

Static (typing-time) substitutions.

Functions

alpha_vary	Simplistic policy to create a "primed" version of x
fv_contains	Test if a variable term appears in a vector of variable terms
fv_contains_idxtm	Test if an index term variable appears in a vector of variable terms
fv_of_ceffect
fv_of_ctype
fv_of_effect
fv_of_idxtm	Compute the free variables of an index term
fv_of_nmtm	Compute the free variables of a name term
fv_of_term	Compute a list of variables (as terms) that appear free in the given term
fv_of_type
idxtm_writescope_var_str	magic variable name for the write scope function over name sets ("@!")
nmtm_writescope_var_str	magic variable name for the write scope function over names ("@@")
subst_idxtm_type	Substitute an index for an index variable in another type
subst_nmtm	Substitute name terms into name terms
subst_nmtm_rec	Substitute name terms into name terms
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_prop_rec	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