[Agda] What does "Set !=< {some type}" mean?

[James Wood]

Incidentally, have the developers ever considered using a “nicer” symbol 
like ⊈ or ≰? Maybe even ASCII </= would be more readable. My impression 
is that !=< is illegible to newcomers unless they either ask or notice 
that it decomposes, with ! being “not”, = being the main bit, and < 
giving a direction for subtyping. On the other hand, I'm sure there are 
several advantages to sticking to ASCII, and also with picking something 
that doesn't appear in users' code. Probably most other languages use 
words (“is not a subtype of”) in their error messages.

James

On 16/01/2021 10:00, Jesper Cockx wrote:
> CAUTION: This email originated outside the University. Check before 
> clicking links or attachments.
> Hi David,
> 
> It means that you gave a type as an argument where Agda expected 
> something of {some type} (or possibly the other way around). The symbol 
> !=< means "is not a subtype of". Agda only uses subtypes in a few 
> specific circumstances, so in most cases you can read it as "is not 
> equal to".
> 
> -- Jesper
> 
> On Sat, Jan 16, 2021 at 1:06 AM David Banas <capn.freako at gmail.com 
> <mailto:capn.freako at gmail.com>> wrote:
> 
>     Hi all,
> 
>     Could someone help me understand what this Agda error means?
> 
>         *Set !=< {some type}*
> 
> 
>     Thanks,
>     -db
> 
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>