Module Rename


module Rename: sig .. end

Variable renaming



type renaming 
val rename : renaming -> Term.term -> Term.term
Apply a renaming to a term
val renaming_away : Term.term -> renaming
Renaming away from a term
val renaming_aways : Term.term list -> renaming
val extend_away : renaming -> Term.term -> renaming
Extend a renaming
val eq_opt : Term.term -> Term.term -> Subs.subs option
Equality up to variable renaming. if eq_opt t1 t2 = Some s then apply s t1 = t2
val eq : Term.term -> Term.term -> bool
val compare : Term.term -> Term.term -> int