[Agda] 1-infix-2

[Apostolis Xekoukoulotakis]

Try adding parentheses :

" (x ~ y) z"

On Sun, Jun 4, 2017 at 3:58 PM, Andreas Abel <andreas.abel at ifi.lmu.de>
wrote:

> On 04.06.2017 14:49, Sergei Meshveliani wrote:
>
>> is it possible to apply a relation  ~ : A → A → A → Set α
>> as
>>      x ~ y z
>> ?
>>
>
> No, that's not possible.
>
> I try
>>
>> _~_⟶_ :  ∀ {α} {A : Set α} → A → A → A → Set α
>> _~_⟶_ x y z =  x ≢ y × x ≢ z
>>
>> But I need the second line to be
>>                                x ~ y z =  x ≢ y × x ≢ z
>>
>
> I don't understand what you are up to here.
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www.cse.chalmers.se/~abela/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170604/237bf73b/attachment.html>