[Agda] Semigroup declaration

[Serge D. Mechveliani]

On Wed, Aug 29, 2012 at 09:58:54PM +0200, Dan Ros?n wrote:
> [..]
> (2.2)
>     The other fields can be inferred because of type dependencies.

I see now.

> (3) If you try this, you will get the error message:
>     `The record type Semigroup does not have the fields setoid'
>     If you look carefully at the definition of Semigroup, you'll see
>     that setoid is not defined under the keyword field. 
> [..]

Yes, my mistake. Thank you.

------
Sergei


> > [..]
> > I have a couple of a beginner questions on Semigroup in
> > Standard library  (Agda-2.3.0.1 + lib-0.6).
> > [..]
> > --------------------------------------------------
> > record Semigroup c Б└⌠ : Set (suc (c Б┼■ Б└⌠)) where
> >   infixl 7 _Б┬≥_
> >   infix  4 _Б┴┬_
> >   field
> >     Carrier     : Set c
> >     _Б┴┬_         : Rel Carrier Б└⌠
> >     _Б┬≥_         : OpБ┌┌ Carrier
> >     isSemigroup : IsSemigroup _Б┴┬_ _Б┬≥_
> >
> >   open IsSemigroup isSemigroup public
> >   setoid : Setoid _ _
> >   setoid = record { isEquivalence = isEquivalence }
> > -------------------------------------------------------
> > [..]
> >
> > (2.1) What does it mean this `= isEquivalence' ?
> >       Is it  IsSemigroup.isEquivalence  produced by opening
> >       IsSemigroup ?
> >
> > (2.2) This implementation for  setoid  skips the fields of
> >       Carrier  and  _Б┴┬_  in Setoid.
> >

> > (3) The  setoid  part in Semigroup  must agree with the Semigroup
> >     signature values, in particular, to refer to the same
> >     Setoid.Carrier  value that  Semigroup.Setoid.
> > [..]