From f3fdfecccafccf3828604072f52d541cf9324e67 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 25 Jul 2018 11:07:14 -0400 Subject: Add option sequencing/return --- src/Util/Option.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'src/Util/Option.v') diff --git a/src/Util/Option.v b/src/Util/Option.v index b9e64910c..bccf3b6fc 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -10,11 +10,26 @@ Definition bind {A B} (v : option A) (f : A -> option B) : option B | None => None end. +Definition sequence {A} (v1 v2 : option A) : option A + := match v1 with + | Some v => Some v + | None => v2 + end. +Definition sequence_return {A} (v1 : option A) (v2 : A) : A + := match v1 with + | Some v => v + | None => v2 + end. +Global Arguments sequence {A} !v1 v2. +Global Arguments sequence_return {A} !v1 v2. + 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. + Infix ";;" := sequence : option_scope. + Infix ";;;" := sequence_return : option_scope. End Notations. Local Open Scope option_scope. -- cgit v1.2.3