module Sum: Generic_util_sum
Empty and Sum datatypes.
Types
type
Type with zero element.
type ('a, 'b) sum =
| |
Left of 'a |
| |
Right of 'b |
Sum type.
type '_ Ty.t +=
| |
Empty : empty Ty.t |
| |
Sum : 'a Ty.t * 'b Ty.t -> ('a, 'b) sum Ty.t |
Type witnesses for empty and sum.
val left : 'a -> ('a, 'b) sum
val right : 'b -> ('a, 'b) sum
Operations
val empty_elim : empty -> 'a
Empty elimination: anything can be proved from a
falsehood. It shouldn't be possible to execute that function
since we cannot give it any actual argument, however, the
function is useful when pattern matching requires some
impossible cases to be given anyway.
val either : ('a -> 'c) -> ('b -> 'c) -> ('a, 'b) sum -> 'c
val sum : ('a -> 'c) ->
('b -> 'd) -> ('a, 'b) sum -> ('c, 'd) sum