Meta-data

• Description: A datatype with two elements. The only way to consume it is by either choosing the first or the second element. You must choose exactly one.
• Authors: Vilem-Benjamin Liepelt
• License: BSD3
• Copyright: (c) Authors 2018
• Issue-tracking: https://github.com/dorchard/granule/issues
• Repository: https://github.com/dorchard/granule

Contents

data Choice (a : Type) (b : Type) where
    OneOf (a [0..1]) (b [0..1])

choice : forall {a : Type, b : Type} 
       . a [0..1] -> b [0..1] -> Choice a b

choose1 : forall {a : Type, b : Type} 
        . Choice a b -> a

choose2 : forall {a : Type, b : Type} 
        . Choice a b -> b