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