set tactic

Stream: general

[Yury G. Kudryashov]

It seems that set x : α := y with h adds x : α := y and h : x = y to the local context. Do we have a version that adds x and h : x = y or a way to replace x : α := y with an opaque x : α?

[Adam Topaz]

What happens if you replace x := x after the set ...?

[Bhavik Mehta]

Yury G. Kudryashov said:

a way to replace x : α := y with an opaque x : α?

clear_value x

[Yury G. Kudryashov]

Thanks!