[Agda] Trouble with sizes

[Andreas Abel]

Could be the following issue:

   https://github.com/agda/agda/issues/2420

On 29.03.2017 19:28, Manuel Bärenz 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
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/