natToBin.idr

module natToBin

data Parity : Nat -> Type where
even : Parity (n + n)
odd : Parity (S (n + n))

parity : (n:Nat) -> Parity n

natToBin : Nat -> List Bool
natToBin Z = Nil
natToBin k with (parity k)
  natToBin (j + j) | even = False :: natToBin j
  natToBin (S (j + j)) | odd = True :: natToBin j         

--  - + Errors (1)
--   `-- foo.idr line 12 col 3:
--       j is not an accessible pattern variable