[Agda] 1-infix-2

[Sergei Meshveliani]

On Sun, 2017-06-04 at 20:00 +0300, Apostolis Xekoukoulotakis wrote:
> Try adding parentheses :
> 
> " (x ~ y) 


Sorry, I recall now of a certain known possibility. For example:

  _≢_nor_ :  ∀ {α} {A : Set α} → A → A → A → Set α

  x ≢ y nor z =  x ≢ y × x ≢ z

That is  ⟶  to be replaced with some name.

Regards,

------
Sergei


> 
> 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
>         
> 
>