🍃 Either.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Inductive t (a b : Set) : Set :=
| Left : a → t a b
| Right : b → t a b.
Arguments Left {_ _}.
Arguments Right {_ _}.
Definition equal {a b : Set} (cmpA : a → a → bool) (cmpB : b → b → bool)
(e : t a b) (f : t a b) : bool :=
match e, f with
| Left a, Left a' ⇒ cmpA a a'
| Right b, Right b' ⇒ cmpB b b'
| _, _ ⇒ false
end.
Definition compare {a b : Set} (cmpA : a → a → int) (cmpB : b → b → int)
(e : t a b) (f : t a b) : int :=
match e, f with
| Left a, Left a' ⇒ cmpA a a'
| Right b, Right b' ⇒ cmpB b b'
| Left _, Right _ ⇒ -1 (* Left < Right *)
| Right _, Left _ ⇒ 1 (* Right > Left *)
end.
Require Import CoqOfOCaml.Settings.
Inductive t (a b : Set) : Set :=
| Left : a → t a b
| Right : b → t a b.
Arguments Left {_ _}.
Arguments Right {_ _}.
Definition equal {a b : Set} (cmpA : a → a → bool) (cmpB : b → b → bool)
(e : t a b) (f : t a b) : bool :=
match e, f with
| Left a, Left a' ⇒ cmpA a a'
| Right b, Right b' ⇒ cmpB b b'
| _, _ ⇒ false
end.
Definition compare {a b : Set} (cmpA : a → a → int) (cmpB : b → b → int)
(e : t a b) (f : t a b) : int :=
match e, f with
| Left a, Left a' ⇒ cmpA a a'
| Right b, Right b' ⇒ cmpB b b'
| Left _, Right _ ⇒ -1 (* Left < Right *)
| Right _, Left _ ⇒ 1 (* Right > Left *)
end.