Destructors for csum.

bf59ec9e · Robbert Krebbers · 481992cf · bf59ec9e
Commit bf59ec9e authored Sep 20, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 5 additions and 0 deletions

algebra/csum.v algebra/csum.v +5 -0

No files found.
--- a/algebra/csum.v
+++ b/algebra/csum.v
@@ -15,6 +15,11 @@ Arguments Cinl {_ _} _.
 Arguments Cinr {_ _} _.
 Arguments CsumBot {_ _}.

+Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x,
+  match x with Cinl a => Some a | _ => None end.
+Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
+  match x with Cinr b => Some b | _ => None end.
+
 Section cofe.
 Context {A B : cofeT}.
 Implicit Types a : A.