[Agda] Bin._<_

[James Deikun]

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.)