parse error ? with open in telescope [Re: [Agda] problem with `abstract']

[mechvel at scico.botik.ru]

Andreas Abel писал 18.07.2016 07:52:
> You can use
> 
>   f : let open M in
>       A -> A
> 
> if you prefer.
> 


Sometimes it needs, say, three `open' members intermingled with
"(foo : Foo) -> ..", and it looks nicer without nested let-in.

Anyway, it looks like the subject does not present any problem.

(A real problem is the type-check performance: currently I fail to make
DoCon-A-0.04 type-checked, it takes too much memory*time, more than
26 Gb * 2 hours).

Regards,

------
Sergei


> On 17.07.2016 21:33, Sergei Meshveliani wrote:
>> On Sun, 2016-07-17 at 21:13 +0200, Andreas Abel wrote:
>>> On 17.07.2016 15:23, Sergei Meshveliani wrote:
>>>> 
>>>> The program
>>>> 
>>>>     f :  ∀ {α α=} → (A : Setoid α α=) →
>>>>                     (open Setoid A using (Carrier))      -- (1)
>>>>                     Carrier → ℕ                          -- (2)
>>>>     f _ _ = 0
>>>> 
>>>> 
>>>> yields a parse error report in Agda 2.5.1.1.
>>> 
>>> Yes, but so would
>>> 
>>>     f : (A : Set)
>>>         A -> A
>>> 
>>> so it is not different from
>>> 
>>>     g : (open M)
>>>         A -> A
>>> 
>>> Both yield parse errors, and that is intended.
>>> 
>> 
>> And
>>    f : (A : Set)
>>        (a : A) → ℕ
>> 
>>    f _ _ = 0
>> 
>> is type-checked.
>> Anyway, as it is intended, this is not important for me.
>> If the thing is not parsed, I would add arrow.
>> 
>> Regards,
>> 
>> ------
>> Sergei
>>