[Agda] `using (DecTotalOrder)'

[Dominique Devriese]

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:

  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ModellingTypeClassesWithInstanceArguments

Dominique