diff options
Diffstat (limited to 'src/Util/Option.v')
-rw-r--r-- | src/Util/Option.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Util/Option.v b/src/Util/Option.v index db4b69dde..2c11771ff 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -60,3 +60,12 @@ Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect | [ |- context[option_rect ?P ?S ?N (Some ?x) ] ] => change (option_rect P S N (Some x)) with (S x); cbv beta end. + +Definition option_eq {A} eq (x y : option A) := + match x with + | None => y = None + | Some ax => match y with + | None => False + | Some ay => eq ax ay + end + end. |