[Agda] `using (DecTotalOrder)'

Dominique Devriese dominique.devriese at cs.kuleuven.be
Tue Oct 9 11:46:12 CEST 2012

2012/10/9 Serge D. Mechveliani <mechvel at botik.ru>:
> module OrdList where
> open import Relation.Nullary using ( Dec; yes; no )
> open import Relation.Binary  using ( DecTotalOrder )

> The checker reports
> "No such module  DecTotalOrder  when scope checking the declaration
>    open DecTotalOrder"

Regarding your first question: you should say
  open import Relation.Binary  using ( DecTotalOrder; module DecTotalOrder )
Name spaces for modules and terms are separate and can overlap, you
were importing the type DecTotalOrder, not the module.

> 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
> classes.

Please refer to the following part of the manual on the wiki:



More information about the Agda mailing list