Stream: new members
Topic: using exists
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?
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"?
Chris Hughes (May 03 2019 at 15:36):
cases h where
h : Exists k, 2 * k = x do what you want? In term mode you can do
let \<k, hk\> := h in
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.
bulut (May 03 2019 at 15:38):
I will try cases now
Patrick Massot (May 03 2019 at 15:38):
Then the first part of Chris' answer is what you want
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