can "notation" abbreviate types?

Stream: lean4

[Malvin Gattinger]

Can I use "notation" to define types where some parts are repeated?

#check Sum Int Int → Sum Char Char → Sum Int Char

notation "Pairing" T a b => T a a → T b b → T a b

#check Pairing Sum Int Char
-- error: unexpected end of input

[Jannis Limperg]

Should be #check Pairing Sum Int Char, right?

[Malvin Gattinger]

Yes, corrected now. Thanks. Same error still.

[Malvin Gattinger]

My use case is actually this:

notation "Pairing" T a b => T a a → T b b → T a b

inductive Thing : Type 1 → Type 1 → Type 2
  | basic : σ → τ → Thing σ τ
  | pair : Thing τ τ → Thing σ σ → Thing τ σ
  -- imagine τ and σ are long and I want to mention them only once, using notation from above:
  | pair' : Pairing Thing τ σ

open Thing  -- error: unexpected token, expected term

#check pair' (basic 1 1) (basic 1 2)

[Jannis Limperg]

I imagine this is a precedence issue. Until one of our syntax wizards comes along, here's a version that works:

notation "Pairing" "(" T "," a "," b ")" => T a a → T b b → T a b

#check Pairing(Sum, Int, Char)

inductive Thing : Type 1 → Type 1 → Type 2
  | basic : σ → τ → Thing σ τ
  | pair : Thing τ τ → Thing σ σ → Thing τ σ
  | pair' : Pairing(Thing, τ, σ)

open Thing

#check pair' (basic 1 1) (basic 1 2)

[Kyle Miller]

The problem is that it's parsing Sum Int Char as the first argument. You either need separators, or you need to set the precedence. Here's by setting max precedence per argument:

notation "Pairing" T:max a:max b:max => T a a → T b b → T a b

#check Pairing Sum Int Char

(Edit: If you use arg instead of max then it is more like a function argument. It's a slight difference, and I think it only affects whether certain notations like do ... would work without parentheses.)

[Kyle Miller]

This notation doesn't pretty print, but if you use mathlib you can use the notation3 command to get it to.

notation3 "Pairing" T:max a:max b:max => (T : Type _ → Type _ → Type _) a a → T b b → T a b

#check Pairing Sum Int Char

[Malvin Gattinger]

Ah, wonderful, thank you both!