[Agda] Bin._<_

James Deikun james at place.org
Fri Aug 3 23:16:22 CEST 2012

On Fri, 2012-08-03 at 13:37 -0400, James Deikun wrote:
> (BTW Andreas or anybody who knows -- why can't the level of Ord be
> inferred?)

I think I figured this out myself -- it would also be valid to place Ord
at any level that's always at least as high (at every value of the level
parameters) as the one given.

Maybe there should be special syntax for inferring the least possible
level for types like this?  It seems like it's a very mechanical process
in most cases.  (On the other hand, it's often useful to know what the
level *is*.  But when it isn't useful, the level can often be big enough
to obscure the formatting of the code and make it hard to read.)

More information about the Agda mailing list