[Agda] any known proof of ⊥ that does not syntactically use ∞ ?

[Jesper Cockx]

Hi Vlad,

All known issues with sized types being able to prove false should be
listed here:
https://github.com/agda/agda/issues?q=is%3Aissue+is%3Aopen+label%3Afalse+label%3Asized-types.
>From those, the only one that does not immediately seem to involve infinity
is https://github.com/agda/agda/issues/4483, but it seems to me the issue
is no longer valid on the current development version of Agda.

-- Jesper

On Fri, Oct 23, 2020 at 12:23 AM vlad <Vlad.Rusu at inria.fr> wrote:

> Dear Agda developers,
>
> You're getting a lot of those recently  - and thank you for the answers
> -  but I have yet another question about sized types.
>
> if I'm not mistaken, all the proofs of ⊥ based in sized types discussed
> in the bug reports do syntactically use ∞, so I was wondering:
>
> is there any known proof of ⊥ where the size constant ∞ does not
> (syntactically) occur? Implicit ocurrences ({∞} or _ ), and renamings,
> are also forbidden.
>
> all the best,
>
> - Vlad
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201023/4a41e869/attachment.html>