module Coercion:sig
..end
type
t
a set of coercions
val empty : t
val add : t -> Term.lsymbol -> t
adds a new coercion from function ls: ty1 -> ty2
raises an error if
ty2
to ty1
is already defined;ls
cannot be used as a coercion, e.g. ty1 = ty2
;ty1
to ty2
is already definedval find : t -> Ty.ty -> Ty.ty -> Term.lsymbol list
returns the coercion, or raises Not_found
val union : t -> t -> t
union s1 s2
merges the coercions from s2
into s1
(as a new set of coercions)
this is asymetric: a coercion from s2
may hide a coercion from s1