Module Choice

Meta-data

Module does not export: OneOf

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