_aux_Mathlib_Tactic_Replace___elabRules_Mathlib_Tactic_replace'_1

Lean4

@[tactic Mathlib.Tactic.replace']
public meta def _aux_Mathlib_Tactic_Replace___elabRules_Mathlib_Tactic_replace'_1 : Lean.Elab.Tactic.Tactic✝ := fun
  | `(tactic| replace$n:optBinderIdent $bs*$[ : $t:term]?) =>
    withMainContext
      (do
        let (goal1, goal2) ← haveLetCore (← getMainGoal) n bs t false
        let name := optBinderIdent.name n
        let hId? := (← getLCtx).findFromUserName? name |>.map fun d ↦ d.fvarId
        match hId? with
        | some hId =>
          replaceMainGoal [goal1, (← observing? <| goal2.clear hId).getD goal2]
        | none =>
          replaceMainGoal [goal1, goal2])
  | _ => no_error_if_unused% throwUnsupportedSyntax✝

Похожие утверждения