[Agda] StrictLex in library

[Andreas Abel]

Since we now have maintainer (thumbs up to Matthew!), you are welcome to 
submit a pull request to the standard library.

On 12.07.2017 09:16, Sergei Meshveliani wrote:
> I recall that currently, I need only  A = Nat, A = Bit.
> So that  zero : Level  occurs sufficient.
> 
> Anyway, an arbitrary level is generally desirable.
> 
> 
> On Wed, 2017-07-12 at 10:42 +0300, Sergei Meshveliani wrote:
>> People,
>>
>> I look into  Relation.Binary.List.StrictLex
>>
>> of Standard library (of April 13, 2017)
>>
>> and see that it is for  (List A)  for  A : Set.
>>
>> What is the reason for restricting  A  to Set of the level  zero ?
>>
>> I need an implementation for StrictTotalOrder for List A,  where
>> A has StrictTotalOrder for _<_,  and  A : Set a,  a : Level.
>>
>> Need I to modify  Relation.Binary.List.StrictLex
>> by replacing  Set  with  (Set a) ?
>>
>> Can anyone advise, please?

-- 
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/