namespace inference with `@`

Stream: lean4

[Horațiu Cheval]

Is there way to use namespace inference when referring to a function with @? A syntax like

def x : List Nat := .@cons Nat 0 [1, 2, 3]

that would mean

def x : List Nat := @List.cons Nat 0 [1, 2, 3]

I imagine there isn't as I've tried all the combination of @ and . I could think of, but I figured I would also ask.

[Floris van Doorn]

Would

def x : List Nat := .cons (α := Nat) 0 [1, 2, 3]

work for your purposes?

[Horațiu Cheval]

Thanks, I hadn't thought of doing that. My purpose was referring to implicit arguments of constructors in pattern matching. This syntax is even nicer than what I imagined because it saves you from all the underscores for the arguments you don't care about.