Zulip Chat Archive

Stream: lean4

Topic: overloading pairing notation


view this post on Zulip 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...)

view this post on Zulip 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 _ _)

view this post on Zulip Sebastian Ullrich (Mar 12 2021 at 14:34):

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

view this post on Zulip 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?

view this post on Zulip 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,*))

view this post on Zulip 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?)

view this post on Zulip 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