## Stream: Is there code for X?

### Topic: Redefining Operators

#### Mac (Jun 25 2020 at 19:56):

Is there a way to overwrite/redefine an operator? For example, I want to redefine logical disjunction to use a class like so

class has_land (A : Sort u) (X : Sort v) (Y : Sort w) :=
(land : X -> Y -> A)

infix /\ := has_logical_conjunction.land


But this of course conflicts with the definition in core. I figured out I can force this by marking the file as prelude but I was hoping there was more elegant and less destructive way around this.

#### Patrick Massot (Jun 25 2020 at 20:00):

I think you can't do that in Lean3.

#### Patrick Massot (Jun 25 2020 at 20:01):

There are a lot of available unicode symbols.

#### Anatole Dedecker (Jun 25 2020 at 20:07):

E.g \And and \Or

#### Alex J. Best (Jun 25 2020 at 20:07):

notation 🧀 := 1
#check 🧀


#### Mac (Jun 25 2020 at 20:09):

I tend to keep my code ASCII only -- I prefer coding that way.

#### Patrick Massot (Jun 25 2020 at 20:10):

You should try Coq :stuck_out_tongue_wink:

#### Kyle Miller (Jun 25 2020 at 20:11):

Both //\\ and /^\ are free, for your "ultra-and". Or /'\, the "pen nib" operator.

#### Anatole Dedecker (Jun 25 2020 at 20:12):

10-characters notations incoming

#### Yakov Pechersky (Jun 25 2020 at 20:14):

Is there a way to do infix notation haskell style like f land g?

#### Patrick Massot (Jun 25 2020 at 20:16):

infix  //\\ := land


#### Kyle Miller (Jun 25 2020 at 20:42):

Yakov Pechersky said:

Is there a way to do infix notation haskell style like f land g?

I've been wondering this, too, but I haven't seen evidence that Lean has anything like this syntax.

This is probably a terrible idea, but you can mimic it with postfix operators:

def apply_arg {α β} : α → (α → β) → β := flip id

postfix  '< :100 := apply_arg
postfix  >' :100 := id

#eval 1 '< nat.add >' 2


or with a new notation

notation x  '< :100 f  >' :100 y := f x y
#eval 1 '< nat.add >' 2
#eval 1 '< function.on_fun nat.add nat.succ >' 2


(I'm just guessing with precedence levels and how the notation syntax is supposed to work, based on this documentation.)

#### Kevin Buzzard (Jun 25 2020 at 23:36):

Are you asking for more than Lean's infix operator?

#### Kyle Miller (Jun 25 2020 at 23:44):

Haskell has a feature where you can have an operator that is a variable: the notation x f y stands for f x y. It's described in the second paragraph after the grammar in this part of the Haskell 98 report.

It lets you do things like write 5 div 2 for integer division, since slash is reserved for the Fractional typeclass, which defines reciprocals.

#### Kyle Miller (Jun 25 2020 at 23:45):

If I understand it correctly, the infix operator will permanently make something infix, where this Haskell syntax is a one-off thing if you want it to be.

#### Alex J. Best (Jun 25 2020 at 23:51):

like this?:

def f : ℕ → ℕ → ℕ := nat.add

notation a 🧀 g 🧀 b := g a b

#eval 1 🧀f🧀 2


your choice of character may differ ;)

#### Alex J. Best (Jun 25 2020 at 23:55):

Lol I just saw you already did it this way too, my bad!

#### Kyle Miller (Jun 25 2020 at 23:57):

I used '< and >'; yours is clearly superior.

Do you know how precedence works for this? In the Haskell version, these "operator symbols" are left-associative and high precedence. Also, it restricts you to using a single (possibly qualified) variable or constructor id. Can you restrict the middle thing like that?

#### Kevin Buzzard (Jun 25 2020 at 23:59):

You can put a colon and a binding power after each emoji

#### Johan Commelin (Jun 26 2020 at 03:24):

Alex J. Best said:

like this?:

def f : ℕ → ℕ → ℕ := nat.add

notation a 🧀 g 🧀 b := g a b

#eval 1 🧀f🧀 2


your choice of character may differ ;)

You need more pizza!

Last updated: May 07 2021 at 22:14 UTC