Add Data.Maybe

src/Data/Maybe.ard

@@ -0,0 +1,52 @@
+\import Logic
+\import Paths
+\import Set
+
+-- | Maybe A
+-- Maybe represents an optional value. It might also be used to represent failure.
+\data Maybe (A : \Type) | Nothing | Just A
+  \where {
+    \func bind {A B : \Type} (a : Maybe A)(f : A -> Maybe B) : Maybe B \elim a
+      | Nothing => Nothing
+      | Just a => f a
+
+    \lemma JustA/=Nothing  {A : \Type} (a : A) (p :  Just a = Nothing) : Empty =>
+      IsJust.absurd (transport IsJust p ItIsJust)
+  }
+
+
+-- | IsJust is a proof that the value is actually a Just
+\data IsJust {A : \Type} (m : Maybe A) : \Prop \with
+  | Just _ => ItIsJust
+  \where {
+    \func absurd {A B : \Type} (s : IsJust (Nothing{A})) : B
+
+    \lemma notNothing {A : \Type} (m : Maybe A) (ev : IsJust m) : Not (m = Nothing) \elim m, ev
+      | Just a, ItIsJust => \lam x => Maybe.JustA/=Nothing a x
+  }
+
+-- | IsNothing is a proof that maybe is Nothing
+\data IsNothing {A : \Type} (Maybe A) : \Prop \with
+  | Nothing => ItIsNothing
+  \where {
+    \func absurd {A B : \Type} (a : A) (s : IsNothing (Just a)) : B
+
+    \lemma notJustA {A : \Type} (a : A) (m : Maybe A) (ev : IsNothing m) : Not (Just a = m) \elim m, ev
+      | Nothing, ItIsNothing => \lam x => Maybe.JustA/=Nothing a x
+  }
+
+\func isJust {A : \Type} (m : Maybe A) : \Type
+  | Nothing => Empty
+  | Just a => IsJust (Just a)
+
+\func isNothing {A : \Type} (m : Maybe A) : \Type \elim m
+  | Nothing => IsNothing {A} (Nothing)
+  | Just a => Empty
+
+\func isItJust {A : \Type} (m : Maybe A) : Dec (IsJust m) \elim m
+  | Nothing => no (IsJust.absurd {A} {Empty} )
+  | Just a => yes ItIsJust
+
+\func isItNothing {A : \Type} (m : Maybe A) : Dec (IsNothing m) \elim m
+  | Nothing =>  yes ItIsNothing
+  | Just a => no (IsNothing.absurd {A} {Empty} a)