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

Georgi Lyubenov godzbanebane at gmail.com
Sun Apr 28 09:38:17 UTC 2019


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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20190428/332529c9/attachment.html>

More information about the Haskell-Cafe mailing list