Module fungi_lang::subst

source ·
Expand description

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