[Agda] slightly wrong sized datatype definition leads to proof of False

[Nils Anders Danielsson]

On 2020-10-20 12:15, Frédéric Blanqui wrote:
> Where can I find the definitions of Size and Size<?
> https://github.com/agda/agda-stdlib/blob/master/src/Size.agda imports
> Agda.Builtin.Size but I don't know where to find this module. (Sorry,
> I am not familiar with Agda.)

This module may not be very useful to you:

   https://github.com/agda/agda/blob/02fe8918eb5c22bf75de040a4952c148858badb0/src/data/lib/prim/Agda/Builtin/Size.agda

-- 
/NAD