[Agda] Trouble with sizes

[Andrea Vezzosi]

The error message could be better, but "dLub Set (λ j → Set _2) =<
Set" is trying to say that the sort computed for your pi type
"{j : Size< i} → ?" is supposed to be smaller or equal to Set.

It can't know the sort of the codomain yet because you still have to
fill it in, so that's what the Set _2 represents.
"dLub" stands for dependent least upper bound.

On Wed, Mar 29, 2017 at 7:28 PM, Manuel Bärenz <manuel at enigmage.de> wrote:
> Dear list,
>
> I'm trying to write some simple code using sizes. Here is something that I
> don't understand:
>
>
> open import Size public
>
> record Test {i : Size} : Set where
>   field
>     test : {j : Size< i} → ?
>
>
> Take this code and try to load it. It will show the following error:
>
> Sort _2 [ at /....agda:5,28-35 ] ———— Errors
> ———————————————————————————————————————————————— Failed to solve the
> following constraints: dLub Set (λ j → Set _2) =< Set
>
>
>
> What's going on?
>
> Manuel
>
> --
> I'm using Enigmail on Thunderbird to sign and encrypt my emails with GPG!
> Why not try it yourself? https://enigmail.net/
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>