Meta-data

• Description: A result data type for computations that can fail (Result + documentation)
• 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 Result (a : Type) where
    Ok a
  ; Failed (String [0..1])

fromResult : forall {a : Type} 
           . (a [0..1]) -> (Result a) -> a

return_res : forall {a : Type} 
           . a -> Result a

bind_res : forall {a : Type, b : Type} 
         . (Result a) -> ((a -> Result b) [0..1]) -> Result b