Notation for functions of several argument

Stream: lean4

[Yaël Dillies]

How is one supposed to write notation that feeds several arguments to a function? I want the kernel[m] notation, similar to how we have Measurable[m], but I am not managing:

class MeasurableSpace (X : Type) where

def kernel (α β : Type) [MeasurableSpace α] : Nat := sorry

example {α β : Type} [MeasurableSpace α] : kernel α β = 0 := sorry
-- First attempt:

notation "kernel[" m "]" α β => @kernel α β m _
-- I would like the following to work

example {α β : Type} {mα : MeasurableSpace α} : kernel[mα] α β = 0 := sorry
-- unexpected token ':='; expected term
-- Second attempt:

notation "kernel[" m "]" α " " β => @kernel α β m _
-- invalid parser '«termKernel[_]___1»', invalid empty symbol
-- Third attempt:

notation "kernel[" m "]" α => fun β ↦ @kernel α β m _

example {α β : Type} {mα : MeasurableSpace α} : kernel[mα] α β = 0 := sorry

/-

function expected at

  α

term has type

  Type
-/

[Kyle Miller]

Probably

notation "kernel[" m "]" α:arg β:arg => @kernel α β m _

[Yaël Dillies]

Oh, what's that :arg doing? I never saw it before

[Eric Wieser]

It's operator precedence

[Eric Wieser]

:arg is short for :1000 or similar, I think

[Yaël Dillies]

Oh, so similar to :max?

[Kyle Miller]

Yes, it's max - 1

[Kyle Miller]

#eval eval_prec max
-- 1024
#eval eval_prec arg
-- 1023