(x : A . t) implicit argument synthesized by tactic

Stream: lean4

[Kevin Buzzard]

In Lean 3 we could use x . t notation to get a tactic to fill in a hole. Is this available in Lean 4? I would like Lean to try closing a goal with rfl if I don't supply a proof for a propositional structure field.

[Daniel Selsam]

There is autoParam, but no uses so far, and I couldn't get a working example in 5m of reading/tracing/twiddling.

[Daniel Selsam]

I'll try again later today if no one posts one first.

[Sebastian Ullrich]

inductive Foo where
  | mk (x y : Nat) (h : x = y := by rfl)

#check Foo.mk 1 1

It looks like support in structure is still missing; please file an issue