[Agda] data syntax ext.

[Serge D. Mechveliani]

To my

>> Suggestion 3 for the language. Current domain denotation
>> ---------------------------------------------------------
>>
>> To locally denote  `this' (`this defined type') the domain (constructor)
>> being defined by  `data',
>> and to put it as a synonym
>> (choose and reserve an appropriate word:  this, it, $$, @@, ...).
>>  [..]
>>    data MbDivideLeft {c l : Level} (H : Semigroup c l)
>>               (a : Semigroup.Carrier H) (b : Semigroup.Carrier H) :  Set _
>>      where
>>      quot       : Nat -> MbDivideLeft H a b                         -- (1)
>>      ...
>>       : (x : Carrier H) -> \neg ((x * b) ~~ a) -> MbDivideLeft H a b 
>>                                                                   -- (3)
>> [..]
>> let `this' be a local synonym:
>>      ...
>>      quot       : Nat -> this
>>      quot2      : Nat -> this H a (a * b)      --
>>      unsolvable : let open Semigroup {{...}}
>>                   in  (x : Carrier H) -> \neg ((x * b) ~~ a) -> this

A. Abel writes

> I am not so sure about this.  Id does not seem to make it so much  
> shorter.  If declarations are allowed in 'data', then you can do it 
> yourself
>
>   data D params : indices -> Set where
>     this = D params
>     constructor
>       c : telescope -> this inds

I agree. This your latter solution is all right 
-- if this extended syntax is accepted for `data'.

Regards,
Sergei.