git.iko.soy/Idris-dev
on v0.99 help sign in
Idris-dev/samples/tutorial/wheres.idr
14 lines 242 B history raw
1module wheres
3even : Nat -> Bool
4even Z = True
5even (S k) = odd k where
6 odd Z = False
7 odd (S k) = even k
9test : List Nat
10test = [c (S 1), c Z, d (S Z)]
11 where c x = 42 + x
12 d y = c (y + 1 + z y)
13 where z w = y + w