[Agda] StrictLex in library

[Sergei Meshveliani]

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?
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>