overloading pairing notation

Stream: lean4

[Jason Gross]

Is there a way to overload , for Prod.mk? (I don't see it defined as a notation in user-land...)

[Sebastian Ullrich]

You can overload any syntax regardless of whether it is built-in or not

notation "(" x ", " y ")" => MyProd.mk x y

#check ((1, 2) : Prod _ _)
#check ((1, 2) : MyProd _ _)

[Sebastian Ullrich]

Note that the "anonymous constructor" ⟨x, y⟩ can usually be used instead of resorting to overloading

[Jason Gross]

Thanks! I'm trying to overload it for category theoretic pairing, so I don't think the anonymous constructor will help here. Is there a way to make the , notation variadic like the built-in one?

[Sebastian Ullrich]

The direct translation of the built-in syntax would be

syntax (name := myTuple) "(" term,* ")" : term
macro_rules [myTuple]
  | `(())          => `(Unit.unit)
  | `(($x))        => `($x)
  | `(($x, $ys,*)) => `(Prod.mk $x ($ys,*))

but that might not be a good idea since it overloads (e)... probably better to demand at least two elements and define a separate notation "(" ")" if desired

syntax (name := myTuple) "(" term "," term,+ ")" : term
macro_rules [myTuple]
  | `(($x, $y))        => `(Prod.mk $x $y)
  | `(($x, $y, $zs,*)) => `(Prod.mk $x ($y, $zs,*))

[Jason Gross]

Awesome, thanks! For my project, I'm probably going to put these in typeclasses a la HMul. (I guess this wouldn't work for the standard library because pattern matching wouldn't be able to see through the typeclass?)

[Mario Carneiro]

In lean 3 you can put the @[pattern] attribute to make pattern matching see through the typeclass, which is used for things like matching on 0 and n+1 on nat (both of which are actually typeclasses)