From 06de6db654717314b84deb5692203e11ef504334 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 10 Feb 2018 17:05:22 -0500 Subject: Add notation for option_bind --- src/Util/Option.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'src/Util/Option.v') 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) := -- cgit v1.2.3