isSingleton : Bool -> TypeisSingleton True = NatisSingleton False = List Nat mkSingle : (x : Bool) -> isSingleton xmkSingle True = 0mkSingle False = [] sum : (single : Bool) -> isSingleton single -> Natsum True x = xsum False [] = 0sum False (x :: xs) = x + sum False xs
isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat
mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []
sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False [] = 0
sum False (x :: xs) = x + sum False xs