[Agda] Type of Natural numbers representations

[Herminie Pagel]

Hi,

when constructing the different unary, binary, ternary... types that
represent the natural numbers it seems that both the constructors and the
increment operator follow a pattern.

https://gist.github.com/pnlph/3f6aca8dea4ba570abcb461b37ae14cb

Is it possible or makes sense defining this pattern in Agda as a type of
natural numbers representations, say Nr, indexed on the natural numbers
themselves so that Nr 1 = N, Nr 2 = Bin, Nr 3 = Ter, ..., Nr 10 = Dec,...?

best, herminie
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190625/f70e75ad/attachment.html>