[Agda] Decidable _\equiv_

[Sergei Meshveliani]

On Tue, 2015-03-17 at 16:44 +0400, Sergei Meshveliani wrote:
> People,
> 
> I have the two questions on the declaration of
> 
>   module Foo {α α= α≤} 
>              (dto  : DecTotalOrder α α= α≤)
>              (_≡?_ : Decidable (_≡_ {A = DecTotalOrder.Carrier dto})))
>              where
>   ...
> 
> 
> 1. Is it possible here something like 
>                   ...
>                   (_≡?_ : let C = DecTotalOrder.Carrier dto
>                           in  Decidable (_≡_ {A = C})
>                   )
>     ?
> [..]


Now I recall of anonymous modules.
I had

  module Foo {α α= α≤} 
     (dto : DecTotalOrder α α= α≤)
     (_≡?_           : Decidable (_≡_ {A = DecTotalOrder.Carrier dto}))
     (C-Show         : Show (DecTotalOrder.Carrier dto))
     (decInhabited-C : Dec (DecTotalOrder.Carrier dto))

And change it to

  module _ {α α= α≤} (dto : DecTotalOrder α α= α≤)
    where
    open DecTotalOrder dto using (_≤_) renaming (Carrier to C)

    module Foo (_≡?_           : Decidable (_≡_ {A = C}))
               (C-Show         : Show C)
               (decInhabited-C : Dec C)

Probably, it will be all right.

Regards,

------
Sergei