[Agda] Type of Natural numbers representations

[Jason -Zhong Sheng- Hu]

Hi Herminie,

If I read you correctly, I think it is the case that `Nr n = List (Fin n)`.

Thanks,
Jason Hu
https://hustmphrrr.github.io/
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Herminie Pagel <herminie.pagel at gmail.com>
Sent: June 25, 2019 3:10 PM
To: agda at lists.chalmers.se
Subject: [Agda] Type of Natural numbers representations

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/205cf946/attachment.html>