[Agda] Bin._<_

[Andreas Abel]

Hi James,

the Agda Prelude has an overloading for strictTotalOrder.

On 03.08.12 11:16 PM, James Deikun wrote:
> 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.)

To get least possible levels, we could switch to cumulative universes. 
That would also greatly reduce the amount of levels since you can 
silently cast A : Set a to A : Set (lsuc a).  It is on my todo list, but 
so are many other things, and the changes to the Agda core would be 
substantial.

Cheers,
Andreas


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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/