replace' — Mathlib

Lean4
/-- Acts like `have`, but removes a hypothesis with the same name as
this one if possible. For example, if the state is:

Then after `replace h : β` the state will be:

```lean
case h
f : α → β
h : α
⊢ β

f : α → β
h : β
⊢ goal
```

whereas `have h : β` would result in:

```lean
case h
f : α → β
h : α
⊢ β

f : α → β
h✝ : α
h : β
⊢ goal
```
-/
@[tactic_parser 1000]
public meta def replace' : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.replace' 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "replace" false✝)
      (ParserDescr.parser✝ `Mathlib.Tactic.haveIdLhs'))
Похожие утверждения