InjectMinimalImperativeMaps.2-I
type t
The source type of the injection.
val encode : t -> M.key
An injection of t into u is an injective function of type t -> u. Because encode is injective, the value encode x can be thought of as the identity of the object x.
t
u
t -> u
encode
encode x
x