Zulip Chat Archive

Stream: general

Topic: And-elim phrasing


view this post on Zulip Patrick Stevens (May 28 2018 at 19:33):

Noob question here, trying to improve my mental model of Lean.
I have an inhabitant h of "and p q" in scope, and I want to create named inhabitants hp, hq of p and q respectively. I'm in tactic mode. One way to do this is "have hp : p, from h.left"; is that the one true way? Are there any other ways (that aren't just interchanging "and.left h" or "and.elim_left")?

view this post on Zulip Reid Barton (May 28 2018 at 19:33):

cases h with hp hq

view this post on Zulip Patrick Massot (May 28 2018 at 19:33):

cases

view this post on Zulip Patrick Massot (May 28 2018 at 19:33):

almost fast enough!

view this post on Zulip Patrick Massot (May 28 2018 at 19:34):

It's unfair, I was staring at an infinite class resolution trace when the notification popped up

view this post on Zulip Patrick Stevens (May 28 2018 at 19:34):

Thanks - it's nontrivial to search for this kind of thing in the docs

view this post on Zulip Patrick Massot (May 28 2018 at 19:34):

https://leanprover.github.io/theorem_proving_in_lean/tactics.html#more-tactics

view this post on Zulip Patrick Massot (May 28 2018 at 19:35):

Not trivial to find, I agree

view this post on Zulip Patrick Massot (May 28 2018 at 19:35):

But very important reading

view this post on Zulip Reid Barton (May 28 2018 at 19:35):

Yeah, I recommend a few rounds of reading that chapter and then playing around with stuff

view this post on Zulip Kevin Buzzard (May 28 2018 at 21:42):

We're trying to write docs, they appear in random places, but theorem proving in lean is where most of us started


Last updated: May 10 2021 at 00:31 UTC