parametrized notations

Stream: lean4

[Anthony Bordg]

Is it possible to define directly parametrized notations in Lean, i.e. notations that embark a term of some type (a parameter), or do we need to declare this parameter as a variable beforehand to introduce the notation, possibly by grouping the variable declaration and the notation in some "Notations" section?

[Aaron Liu]

What do you mean by this? Can you give an example of what you want to do?

[Anthony Bordg]

structure Struc where
 field1 : type1
 field2 : type2

Assume I want to introduce a notation for Struct.field1 that depends on the name t of a parameter t : Struct. I first need to have a term t of type Struct for introducing such a notation. Can I do this on the fly as part of the notation declaration or do I need to declare a variable t of type Struc beforehand?

[Aaron Liu]

Depending on your exact use case, I think it is doable to have the notation before having the t : Struct.

[Marcus Rossel]

So you mean something like this?

structure Struc where
  field1 : Nat
  field2 : Nat

notation t "$$$" => Struc.field1 t

def zero : Struc where
  field1 := 0
  field2 := 0

#eval zero$$$ -- 0

[Anthony Bordg]

Aaron Liu said:

Depending on your exact use case, I think it is doable to have the notation before having the t : Struct.

How? :)

[Eric Wieser]

I think it would help if you gave a clearer example of what you want to be able to write vs what you want it to elaborate to

[Anthony Bordg]

Marcus Rossel said:

notation t "$$$" => Struc.field1 t

Here, Lean has no way to understand that t is expected to have type Struc, right? And it should be more something like t.field1 on the right side of =>, no?

[Aaron Liu]

Anthony Bordg said:

Aaron Liu said:

Depending on your exact use case, I think it is doable to have the notation before having the t : Struct.

How? :)

I will point to @Marcus Rossel's solution until you demonstrate that it doesn't work for your use case.

[Anthony Bordg]

Will try to give more details later, but basically t is not an argument of Struct.field1, so I don't even see what Struc.field1 t would mean. Also, I realize that if one writes t.Struc.field1 on the right side, then it may not be possible to write t on the left side, something I want, because then Lean would consider t as an unused variable.

[Kyle Miller]

I'm confused... The first parameter of Struct.field1 is a value of Struct, which is why Marcus's solution works. Try doing #check Struct.field1 to see its type.

[Kyle Miller]

Every structure field gets a projection function like this whose first explicit parameter is the structure itself.

[Johan Commelin]

I think Anthony is looking for a type-aware version of notation. And I think the answer is: if you want that, you have to write your own elaborator for that specific bit of notation. But also, you don't need to do it, because the type-unaware notation is good enough 99% of the time.

[Anthony Bordg]

Kyle Miller said:

I'm confused... The first parameter of Struct.field1 is a value of Struct, which is why Marcus's solution works. Try doing #check Struct.field1 to see its type.

Marcus and you are right, and Marcus' solution solves my problem, thanks.