[Agda] Nat Fuel vs Sized Types (and other Sized Type questions)

[Andrew M. Pitts]

> On 24 Apr 2020, at 18:10, Joey Eremondi <joey.eremondi at gmail.com> wrote:
>
> 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 <https://github.com/agda/agda/issues/3026>.
>
> Oh... well that definitely ruins what I was trying to do. Does --sized make Agda inconsistent even with --safe enabled?

Yes (see attached, for example).

Andy


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200424/b73de4bb/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: size-bug.agda
Type: application/octet-stream
Size: 1556 bytes
Desc: size-bug.agda
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200424/b73de4bb/attachment.obj>