Acts like have, but removes a hypothesis with the same name as
this one if possible. For example, if the state is:
f : α → β
h : α
⊢ goal
→ β
h : α
⊢ goal
⊢ goal
Then after replace h := f h the state will be:
f : α → β
h : β
⊢ goal
→ β
h : β
⊢ goal
⊢ goal
whereas have h := f h would result in:
f : α → β
h† : α
h : β
⊢ goal
→ β
h† : α
h : β
⊢ goal
⊢ goal
This can be used to simulate the specialize and apply at tactics of Coq.
Equations
- One or more equations did not get rendered due to their size.
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:
case h
f : α → β
h : α
⊢ β
f : α → β
h : β
⊢ goal
→ β
h : α
⊢ β
f : α → β
h : β
⊢ goal
⊢ β
f : α → β
h : β
⊢ goal
→ β
h : β
⊢ goal
⊢ goal
whereas have h : β would result in:
case h
f : α → β
h : α
⊢ β
f : α → β
h✝ : α
h : β
⊢ goal
→ β
h : α
⊢ β
f : α → β
h✝ : α
h : β
⊢ goal
⊢ β
f : α → β
h✝ : α
h : β
⊢ goal
→ β
h✝ : α
h : β
⊢ goal
✝ : α
h : β
⊢ goal
⊢ goal
Equations
- One or more equations did not get rendered due to their size.