<div dir="ltr"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
But our enthusiasm for sized types in Agda was severely dampened when we
 learned later that in current versions they allow one to prove that 
true equals false :-( — see <<a href="https://github.com/agda/agda/issues/3026" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/3026</a>>. </blockquote><div><br></div><div>Oh... well that definitely ruins what I was trying to do. Does --sized make Agda inconsistent even with --safe enabled? <br></div><div><br></div><div>Looks like I'll have to either use Nat fuel or guardedness-based coinduction.</div><div><br></div><div>Thanks!<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Apr 24, 2020 at 3:21 AM Andrew M. Pitts <<a href="mailto:amp12@cam.ac.uk">amp12@cam.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>
<br>
> On 24 Apr 2020, at 10:41, Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>> wrote:<br>
> <br>
> On 2020-04-22 05:56, Joey Eremondi wrote:<br>
>> I'm wondering if there are general guidelines as to when to use sized<br>
>> types vs. just using natural numbers as fuel/index.<br>
> <br>
> Two data points:<br>
> <br>
> * I have found it practical to use sized coinductive types, together<br>
>  with explicit definitions of (strong or weak) bisimilarity.<br>
> <br>
> * I have found it less practical to use sized inductive types with<br>
>  /relevant/ size arguments together with propositional equality.<br>
<br>
I and my co-authors can’t seem to do without sized inductive types in the recent paper <<a href="https://www.cl.cam.ac.uk/~amp12/papers/coniqi/coniqi.pdf" rel="noreferrer" target="_blank">https://www.cl.cam.ac.uk/~amp12/papers/coniqi/coniqi.pdf</a>><br>
<br>
But our enthusiasm for sized types in Agda was severely dampened when we learned later that in current versions they allow one to prove that true equals false :-( — see <<a href="https://github.com/agda/agda/issues/3026" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/3026</a>>. <br>
<br>
Andy Pitts<br>
<br>
</blockquote></div>