From cba593ad55f11631055ae1337efde89acae67eca Mon Sep 17 00:00:00 2001 From: jadep Date: Sun, 10 Jul 2016 15:11:44 -0400 Subject: added proofs about addition chain exponentiation for later use in ModularBaseSystem [pow], which we need for sqrt and inversion. --- src/Util/Option.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'src/Util/Option.v') 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. -- cgit v1.2.3