[Agda] a strange function type report

[mechvel at scico.botik.ru]

I am sorry, I have got confused.

Prime∣split  is only a property.
In in the last module I apply it as a lemma proof.

Please, withdraw my question.

------
Sergei



On 2020-04-24 22:45, James Wood wrote:
> 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
>> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda