Sophie

Sophie

distrib > Fedora > 19 > i386 > by-pkgid > 776d147ce804872da1339c5e2ebac30f > files > 115

idris-0.9.9-1.fc19.i686.rpm

module wheres

even : Nat -> Bool 
even Z = True
even (S k) = odd k where 
  odd Z = False
  odd (S k) = even k 

test : List Nat
test = [c (S 1), c Z, d (S Z)]
  where c x = 42 + x
        d y = c (y + 1 + z y)
              where z w = y + w