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

[Andreas Abel]

You can use

   f : let open M in
       A -> A

if you prefer.

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
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/