Syntax for defining functions with implicit variables

Stream: lean4

[Frédéric Dupuis]

What is the correct syntax to do the following?

example : ∀ {x : Nat}, True := fun x => trivial

(Obviously, this is for an example where I actually need to use x in the proof.)

[Mario Carneiro]

fun {x} => trivial or @fun x => trivial