Implicit argument by tactic

Stream: lean4

[Cody Roux]

How might one define a notation where an argument is filled at use-time by a tactic execution?

[Chris Bailey]

Is this what you're describing? https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Implicit.20evidences.20with.20simp.20proofs/near/462600813

[Cody Roux]

Yep, coolio. Don't understand the evaluation semantics of default args though. Are they all lazy like this?

[Floris van Doorn]

I believe that (h : T := t) and (h : T := by tac) are treated quite/completely differently by Lean.

[Yury G. Kudryashov]

If you write (h : T := t), then t has to make sense and have a correct type at the moment of declaration of your lemma/def. If you write (h : T := by tac), then it is stored as a Syntax, then executed whenever you apply your lemma.