Zulip Chat Archive

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: