how to create a named hole

Stream: lean4

[Locria Cyber]

Is there something like def a := ?hole

I know sorry works as a hole

[Arthur Paulino]

What's the difference from sorry in terms of behavior that you're expecting?

[Chris Bailey]

The refine tactic is generally used for this.

example : True ∧ True := by
  refine And.intro ?l ?r
  case l => trivial
  case r => trivial

[Locria Cyber]

Arthur Paulino said:

What's the difference from sorry in terms of behavior that you're expecting?

Nothing. I only want to have named holes