[Agda] `using (DecTotalOrder)'

Serge D. Mechveliani mechvel at botik.ru
Tue Oct 9 11:28:02 CEST 2012

Can you, please, tell how to import  DecTotalOrder  with `using' ?

(Agda-, MAlonzo, 
 record DecTotalOrder ...   defined in  Relation.Binary  of Standard
 Library  lib-0.6

module OrdList where
open import Relation.Nullary using ( Dec; yes; no )
open import Relation.Binary  using ( DecTotalOrder )

open DecTotalOrder
data OrderedList? {c l1 l2 : Level} (ord : DecTotalOrder c l1 l2) :
                  List $ Carrier ord -> Set $ L-suc $ max c $ max l1 l2
  cons : let A = Carrier ord
         (x y : A) -> (xs : List A) -> _<=_ ord x y ->
         OrderedList? ord (y :: xs) -> OrderedList? ord (x :: y :: xs)

(for this letter I replace the math symbols  \<= to <=,  \:: to :: ). 

The checker reports 
"No such module  DecTotalOrder  when scope checking the declaration
   open DecTotalOrder
If I remove  ``using ( DecTotalOrder )'',  then it does type-check.
But for most modules M, I would like to restrict explicitly, what is 
used from M. 

Question 2:
how to omit here the argument  ord  in  ``_<=_ ord x y''  ?
For it is said that  dep.records + hidden agruments  stands for type 
Currently I do not think that it is crucial, but for curiosity.

Thank you in advance for explanation,


More information about the Agda mailing list