mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 01:09:03 +03:00
14 lines
281 B
Idris
14 lines
281 B
Idris
|
|
||
|
|
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
|