summaryrefslogtreecommitdiff
path: root/lib/Coqlib.v
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Coqlib.v')
-rw-r--r--lib/Coqlib.v7
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index ce5d94e..58c9572 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -633,6 +633,13 @@ Qed.
Set Implicit Arguments.
+(** Comparing option types. *)
+
+Definition option_eq (A: Type) (eqA: forall (x y: A), {x=y} + {x<>y}):
+ forall (x y: option A), {x=y} + {x<>y}.
+Proof. decide equality. Defined.
+Global Opaque option_eq.
+
(** Mapping a function over an option type. *)
Definition option_map (A B: Type) (f: A -> B) (x: option A) : option B :=