module Equal: Generic_core_equal
Type equality predicate.
type ('_, '_) equal =
x : ('a,'b) equal is a witness that 'a and 'b are intensionally equal.
Pattern matching x with Refl will force the type checker to unify 'a and 'b.
type ('a, 'b) t = ('a, 'b) equal
type
|
f : 'a 'b.
'a Ty.t ->
'b Ty.t -> ('a, 'b) equal option; |
}
val ext : 'a Ty.pat -> equal_fun -> unit
extends equal with a new case.
val equal : 'a Ty.t ->
'b Ty.t -> ('a, 'b) equal option
val coerce : 'a Ty.t -> 'b Ty.t -> 'a -> 'b option
Coerces a value between two intensionally equal types.
In other words, ('a, 'b) equal must be inhabited for a
value of type 'a to be coerced into the type 'b.