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