Idris stuff

stuff.idr

rev : List a -> List a                                                                              
rev xs = revAcc [] xs where    
  revAcc : List a -> List a -> List a    
  revAcc acc [] = acc    
  revAcc acc (x :: xs) = revAcc (x :: acc) xs    
    
even : Nat -> Bool    
even Z = True    
even (S k) = odd k where    
  odd Z = False    
  odd (S k) = even k    
    
odd : Nat -> Bool    
odd = not . even