Module Maybe

Meta-data

Contents

data Maybe (a : Type) where
    Nothing 
  ; Just a
Type-safe null; wrap a computation that could fail
maybe : forall {a : Type, b : Type} 
      . b [0..1] -> (a -> b) [0..1] -> Maybe a -> b
The maybe function takes a default value, a function, and a Maybe value. If the Maybe value is Nothing, the function returns the default value. Otherwise, it applies the function to the value inside the Just and returns the result.
returnMb : forall {a : Type} 
         . a -> Maybe a
Monad interface for Maybe
bindMb : forall {a : Type, b : Type} 
       . Maybe a -> (a -> Maybe b) [0..1] -> Maybe b
Monad interface for Maybe
fromMaybe : forall {a : Type} 
          . a [0..1] -> Maybe a -> a

isJust : forall {a : Type} 
       . Maybe (a [0]) -> Bool
Whether a Maybe a value is Just a
isNothing : forall {a : Type} 
          . Maybe (a [0]) -> Bool
Whether a Maybe a value is Nothing