diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-04-15 17:30:01 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-04-15 17:30:01 +0100 |
commit | 007b01bcae6abcc88dbcd540d024cdf3df6a603b (patch) | |
tree | b56a99e02f1d6fa6458161eacfa80481254ffc55 /src | |
parent | 16967f7623ed9292f14cd7c512f40d3cca89f475 (diff) | |
download | vericert-kvx-007b01bcae6abcc88dbcd540d024cdf3df6a603b.tar.gz vericert-kvx-007b01bcae6abcc88dbcd540d024cdf3df6a603b.zip |
Add do notation for option
Diffstat (limited to 'src')
-rw-r--r-- | src/common/Coquplib.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index 666d740..47360d6 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -65,6 +65,17 @@ Definition liftA2 {T : Type} (f : T -> T -> T) (a : option T) (b : option T) : o | _ => None end. +Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B := + match f with + | Some a => g a + | _ => None + end. + +Module Notation. +Notation "'do' X <- A ; B" := (bind A (fun X => B)) + (at level 200, X ident, A at level 100, B at level 200). +End Notation. + End Option. Parameter debug_print : string -> unit. |