# [Agda] `using (DecTotalOrder)'

Serge D. Mechveliani mechvel at botik.ru
Tue Oct 9 13:31:30 CEST 2012

```On Tue, Oct 09, 2012 at 11:46:12AM +0200, Dominique Devriese wrote:
> 2012/10/9 Serge D. Mechveliani <mechvel at botik.ru>:
[..]
> > 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

First, I write

----------------------------------------------------------
open import Level ...
open import Relation.Nullary using ( Dec; yes; no )
open import Relation.Binary  using ( DecTotalOrder; module 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
where
...
cons : let A = Carrier ord
in
(x y : A) -> (xs : List A) ->
_<=_ ord x y ->               -- **
OrderedList? ord (y :: xs) -> OrderedList? ord (x :: y :: xs)
------------------------------------------------------------------------

(I rename for this letter  \<=  to  <= ).
And it works.
Then I need to replace   _<=_ ord x y   with   x <= y.
I write

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

And the type checker report is

Panic:  Unbound name:  OrdList.OrderedList? [0,57]@197591509
when checking that  ord  are valid arguments to a function of type
({{ : DecTotalOrder (_55 ord) (_56 ord) (_57 ord)}} Б├▓
Set (_55 ord))

Probably I am missing something.
On the other hand, `panic' is discovered.

Thanks,
Sergei
```