[Agda] `using (DecTotalOrder)'

[Nils Anders Danielsson]

On 2012-10-09 13:31, Serge D. Mechveliani wrote:
> 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))

I think this bug has been fixed in the development version:

   http://code.google.com/p/agda/issues/detail?id=674

-- 
/NAD