[Agda] 1-infix-2

[Andreas Abel]

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/