[Agda] "No instance"

[Sergei Meshveliani]

On Sat, 2018-11-17 at 19:38 -0300, Guillermo Calderón wrote:
> Hi,
> 
> You have to declare S and S'  as Setoid instances:
> 
> 
> ------------------------------------------------------------
> instance
>      foo1 : Setoid _ _
>      foo1 = S
>      foo2 : Setoid
>      foo2 = S'
> ------------------------------------------------------------
> 
> Names and types can be omitted:
> 
> ------------------------------------------------------------
> instance
>      _ = S
>      _ = S'
> ------------------------------------------------------------
> 


It helps. Thank you!

------
Sergei 




> On 17/11/18 08:35, Sergei Meshveliani wrote:
> > Please, what it wrong here?
> > 
> > ----------------------------------------------------------------------
> > open import Level using (suc; _⊔_)
> > open import Relation.Binary using (Rel; IsEquivalence; _Preserves_⟶_)
> > open import Data.Product using (Σ)
> > 
> > record Setoid {α} α= (Carrier : Set α) :  Set (suc (α ⊔ α=))  where
> >    infix 4 _≈_
> >    field
> >      _≈_           : Rel Carrier α=
> >      isEquivalence : IsEquivalence _≈_
> > 
> > 
> > module _ {α α= β β=} {C : Set α} {C' : Set β}
> >                       (S : Setoid α= C) (S' : Setoid β= C')
> >    where
> >    open Setoid {{...}}
> > 
> >    CongruentMap :  Set _
> >    CongruentMap =  Σ (C → C') (\f → f Preserves _≈_ ⟶ _≈_)
> > ---------------------------------------------------------------
> > 
> > Agda 2.6.0-c5cbc7e :
> > 
> > "No instance of type Setoid _ℓ₁_29 C was found in scope.
> > when checking that the expression _≈_ has type Rel C _ℓ₁_29
> > "
> > 
> > 
> > Thanks,
> > 
> > ------
> > Sergei
> > 
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> > 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda