Lean4
@[term_elab letImplDetailStx, inherit_doc letImplDetailStx]
def elabLetImplDetail : TermElab := fun stx expectedType? =>
match stx with
| `(let_impl_detail $id := $valStx; $body) => do
let val ← elabTerm valStx none
let type ← inferType val
trace[Elab.let.decl]"{id.getId } : {type } := {val}"
let result ←
withLetDecl id.getId (kind := .default) type val fun x => do
addLocalVarInfo id x
let lctx ← getLCtx
let lctx := lctx.modifyLocalDecl x.fvarId! fun decl => decl.setKind .implDetail
withLCtx lctx (← getLocalInstances) do
let body ← elabTermEnsuringType body expectedType?
let body ← instantiateMVars body
mkLetFVars #[x] body (usedLetOnly := false)
pure result
| _ => throwUnsupportedSyntax
