Zulip Chat Archive

Stream: new members

Topic: using exists


view this post on Zulip bulut (May 03 2019 at 15:34):

say i have a prop of the form \exists k, 2*k = x, and I want to "bind" k to use it - how to do this?

view this post on Zulip Patrick Massot (May 03 2019 at 15:35):

We need more context. Are you using term mode or tactic mode? What do you mean by "I have a prop"?

view this post on Zulip Chris Hughes (May 03 2019 at 15:36):

does cases h where h : Exists k, 2 * k = x do what you want? In term mode you can do let \<k, hk\> := h in

view this post on Zulip bulut (May 03 2019 at 15:37):

I'm sorry- I should have been more clear. I'm using tactic mode, and have a proposition of type ∃ (k : ℕ), 2 * k = x, and I want to bind k to a variable.

view this post on Zulip bulut (May 03 2019 at 15:38):

I will try cases now

view this post on Zulip Patrick Massot (May 03 2019 at 15:38):

Then the first part of Chris' answer is what you want

view this post on Zulip Patrick Massot (May 03 2019 at 15:39):

Assuming your assumption is called h (since you didn't want to disclose this information) then you can write cases h with k hk,


Last updated: May 17 2021 at 21:12 UTC