Module fungi_lang::subst [−][src]
Static (typing-time) substitutions.
Functions
alpha_vary |
Simplistic policy to create a "primed" version of |
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 |