[Haskell-cafe] Agda's BUILTIN Naturals in Haskell

Hey, Is there any way to do something similar to what Agda does with natural numbers via BUILTIN pragmas? More precisely I want to have correct-by-construction natural numbers, that at runtime are treated as `Integer`s. My initial idea was to abuse rewrite rules to turn `data N = Z | S N` into `Integer` terms somehow, but I'm not sure if this is possible. ======= Georgi