<div dir='auto'>Thanks! I have a piece of code that does not use infinity, nor equality in Size. While it can't be claimed to be safe, it can reasonably be evaluated as not (knowingly) being unsafe. That's better than nothing, I guess. I'm wondering whether this also applies to the size-based codata definitions in the standard library.</div><div class="gmail_extra"><br><div class="gmail_quote">Le 23 oct. 2020 09:44, Jesper Cockx <Jesper@sikanda.be> a écrit :<br type="attribution" /><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Hi Vlad,</div><div><br /></div><div>All known issues with sized types being able to prove false should be listed here: <a href="https://github.com/agda/agda/issues?q=is%3Aissue+is%3Aopen+label%3Afalse+label%3Asized-types">https://github.com/agda/agda/issues?q=is%3Aissue+is%3Aopen+label%3Afalse+label%3Asized-types</a>. From those, the only one that does not immediately seem to involve infinity is <a href="https://github.com/agda/agda/issues/4483">https://github.com/agda/agda/issues/4483</a>, but it seems to me the issue is no longer valid on the current development version of Agda.</div><div><br /></div><div>-- Jesper<br /></div></div><br /><div class="elided-text"><div dir="ltr">On Fri, Oct 23, 2020 at 12:23 AM vlad <<a href="mailto:Vlad.Rusu@inria.fr">Vlad.Rusu@inria.fr</a>> wrote:<br /></div><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb( 204 , 204 , 204 );padding-left:1ex">Dear Agda developers,<br />
<br />
You're getting a lot of those recently  - and thank you for the answers <br />
-  but I have yet another question about sized types.<br />
<br />
if I'm not mistaken, all the proofs of ⊥ based in sized types discussed <br />
in the bug reports do syntactically use ∞, so I was wondering:<br />
<br />
is there any known proof of ⊥ where the size constant ∞ does not <br />
(syntactically) occur? Implicit ocurrences ({∞} or _ ), and renamings, <br />
are also forbidden.<br />
<br />
all the best,<br />
<br />
- Vlad<br />
<br />
<br />
<br />
_______________________________________________<br />
Agda mailing list<br />
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br />
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br />
</blockquote></div>
</blockquote></div><br></div>