[Agda] a strange function type report

[James Wood]

Hi Sergei,

Did you mean to be applying an inhabitant of `Prime∣split`, rather than
`Prime∣split` itself?

Regards,
James

On 24/04/2020 20:40, mechvel at scico.botik.ru wrote:
> Sorry, here is attached a much smaller program, which is also zipped.
> The effect is the same as reported below.
> 
> 
> On 2020-04-24 22:21, mechvel at scico.botik.ru wrote:
>> Please, what is wrong in the attached program?
>>
>> In one module it is declared
>>
>>   Prime∣split :  Set _
>>   Prime∣split =  {p a b : Carrier} → IsPrime p → p ∣ (a * b) → p ∣ a ⊎
>> p ∣ b
>>
>> and in the last module it is implemented
>>
>>   test : (p x y : Carrier) → IsPrime p → p ∣ (x * y) → (p ∣ x) ⊎ (p ∣ y)
>>   test p x y p-prime p∣xy =  Prime∣split p-prime p∣xy
>>
>> And Agda 2.6.1 reports
>> "
>> Set (α ⊔ α=) should be a function type, but it isn't
>> when checking that p-prime p∣xy are valid arguments to a function
>> of type Set (α ⊔ α=)
>> ".
>>
>> Am I missing something, or it is a bug in the type checker?
>>
>> Regards,
>>
>> ------
>> Sergei
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7Cbc903f36811643fd532e08d7e887666a%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637233540559994693&sdata=fzNryLByr7XfEZCiJHSrkwc0VwfXBhEge%2BC3LubM8hc%3D&reserved=0
>>
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7Cbc903f36811643fd532e08d7e887666a%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637233540560014680&sdata=0SM60Mz%2BNl2YfhbWyYWOvT7Va%2FRhES1yah6mGe2yOtU%3D&reserved=0
>