diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-07 23:44:48 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-07 23:44:48 -0500 |
| commit | 5cd8f9cd475bc26ff610fbbe1e3f4b3338f4a607 (patch) | |
| tree | 8c4bed585cb132cb71c16aee8f79847d51e8ccc3 /src/Util/Option.v | |
| parent | 0deb004886acf74a23d375683731f96897d7da25 (diff) | |
Add option_map_map
Diffstat (limited to 'src/Util/Option.v')
| -rw-r--r-- | src/Util/Option.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Util/Option.v b/src/Util/Option.v index 5544fa428..a7b9df4e1 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -68,6 +68,12 @@ Proof. destruct v; reflexivity. Qed. +Lemma option_map_map : forall {A B C} (f:A->B) (g:B->C) v, + option_map g (option_map f v) = option_map (fun v => g (f v)) v. +Proof. + destruct v; reflexivity. +Qed. + Lemma option_rect_function {A B C S' N' v} f : f (option_rect (fun _ : option A => option B) S' N' v) = option_rect (fun _ : option A => C) (fun x => f (S' x)) (f N') v. |