## Stream: lean4

#### Jason Gross (Mar 12 2021 at 14:23):

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

#### Sebastian Ullrich (Mar 12 2021 at 14:33):

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 (Mar 12 2021 at 14:34):

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

#### Jason Gross (Mar 12 2021 at 14:49):

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 (Mar 12 2021 at 15:07):

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 (Mar 12 2021 at 15:19):

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 (Mar 12 2021 at 15:22):

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)

Last updated: May 07 2021 at 13:21 UTC