[Agda] boundings in data-where

[Serge D. Mechveliani]

Probably, this is called `binding' (under `where'), not `bounding'
(  where
   _~_ = Semigroup._\~~_ H
).


On Tue, Nov 06, 2012 at 12:07:22AM +0400, Serge D. Mechveliani wrote:
> People,
> there is a strange syntax difference between the `record' and `data'
> declarations with respect to bounding and `open' after `where'.
> [..]
> record LeftQuotient {c l : Level} (H : Semigroup c l)
>                     (a b : Semigroup.Carrier H) :  Set (max c l)
>   where
>   open Semigroup {{...}}     -- (1)
>   _~_ = Semigroup._\~~_ H    -- (2)
> [..]
> 
> data MbDivideLeft {c l : Level} (H : Semigroup c l)
>      (a : Semigroup.Carrier H) (b : Semigroup.Carrier H) : Set (max c l)
>   where
>   open Semigroup {{...}}     -- (1')
>   _~_ = Semigroup._\~~_ H    -- (2')
> [..]