
<html>

<head>

<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">

<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>

</head>

<body dir="ltr">

<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">

Hi Herminie,</div>

<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">

<br>

</div>

<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">

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

</div>

<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">

<br>

</div>

<div id="Signature">

<div></div>

<div id="divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">

<font size="3"><b>Thanks,</b></font></div>

<div dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">

<font size="3"><b>Jason Hu</b></font></div>

<div dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">

<font size="3"><b><a href="https://hustmphrrr.github.io/">https://hustmphrrr.github.io/</a></b></font><br>

<font size="3"><b></b></font><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><a target="_blank"></a></b></span></span></font></div>

</div>

<div id="appendonsend"></div>

<hr style="display:inline-block;width:98%" tabindex="-1">

<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Herminie Pagel <herminie.pagel@gmail.com><br>

<b>Sent:</b> June 25, 2019 3:10 PM<br>

<b>To:</b> agda@lists.chalmers.se<br>

<b>Subject:</b> [Agda] Type of Natural numbers representations</font>

<div> </div>

</div>

<div>

<div dir="ltr">

<div>Hi,</div>

<div><br>

</div>

<div>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.</div>

<div><br>

</div>

<div><a href="https://gist.github.com/pnlph/3f6aca8dea4ba570abcb461b37ae14cb">https://gist.github.com/pnlph/3f6aca8dea4ba570abcb461b37ae14cb</a></div>

<div><br>

</div>

<div>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,...?<br>

</div>

<div><br>

</div>

<div>best, herminie</div>

</div>

</div>

</body>

</html>