Skip to main content

🍃 Either.v

Environment

Gitlab

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.