diff options
| -rw-r--r-- | src/Util/Option.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/Util/Option.v b/src/Util/Option.v index a7b9df4e1..a5b19ae4a 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -2,6 +2,20 @@ Require Import Coq.Classes.Morphisms. Require Import Coq.Relations.Relation_Definitions. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Notations. + +Definition bind {A B} (v : option A) (f : A -> option B) : option B + := match v with + | Some v => f v + | None => None + end. + +Module Export Notations. + Delimit Scope option_scope with option. + Bind Scope option_scope with option. + + Notation "A <- X ; B" := (bind X (fun A => B%option)) : option_scope. +End Notations. Section Relations. Definition option_eq {A} eq (x y : option A) := |