[Agda] `let' in record decl

Serge D. Mechveliani mechvel at botik.ru
Tue Oct 9 15:29:15 CEST 2012

Please, how to abbreviate  `Carrier ord'  in the declaration  of
record Merge1
  {c l1 l2 : Level} (ord : DecTotalOrder c l1 l2)
  (m : Carrier ord) (xs : List $ Carrier ord) (ys : List $ Carrier ord)
                                        : Set (suc $ max c $ max l1 l2)
  A = Carrier ord
  field list    : List A                     
        ordered : OrderedList? ord (m :: list)
(Agda-, MAlonzo).

After `where', it works  `A = Carrier ord'.
But how to abbreviate the previous three occurences?

Question 2.
(suc $ max c $ max l1 l2) : Level   
comes from my declaration of the type  OrderedList?
-- where this expression is copied from  DecTotalOrder 
(of Standard Library lib-0.6), without understanding of how the levels
must be set.
Now, what level needs to be set for  record Merge1  ?

Thank you in advance for explanation,


More information about the Agda mailing list