
Meta-data
- Description: Library for working with values that may be absent
- Authors: Vilem-Benjamin Liepelt, Dominic Orchard
- License: BSD3
- Copyright: (c) Authors 2018
- Issue-tracking: https://github.com/dorchard/granule/issues
- Repository: https://github.com/dorchard/granule
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