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