Skip to main content

🍃 Either.v

Environment

Gitlab , OCaml

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 {_ _}.

Parameter equal : {a b : Set},
  (a a bool) (b b bool) t a b t a b bool.

Parameter compare : {a b : Set},
  (a a int) (b b int) t a b t a b int.