Zulip Chat Archive

Stream: general

Topic: set tactic


view this post on Zulip Yury G. Kudryashov (Mar 25 2021 at 00:36):

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 : α?

view this post on Zulip Adam Topaz (Mar 25 2021 at 00:37):

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

view this post on Zulip Bhavik Mehta (Mar 25 2021 at 00:38):

Yury G. Kudryashov said:

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

clear_value x

view this post on Zulip Yury G. Kudryashov (Mar 25 2021 at 00:38):

Thanks!


Last updated: May 18 2021 at 16:25 UTC