Zulip Chat Archive

Stream: general

Topic: (p ^ q) -> k


Cameron (Dec 13 2018 at 20:14):

Sorry last question. I have a show _ from _ and i get the error that i am expecting something of type k but i have something of type p ^ q -> k, how can i isolate just the right side of the implication? when i assume p is true and q is true before the show command i still run into issues

Mario Carneiro (Dec 13 2018 at 20:15):

you can use assume hpq : p /\ q,

Mario Carneiro (Dec 13 2018 at 20:15):

that contains a proof of the conjunction, which you can destruct with hpq.left and hpq.right

Chris Hughes (Dec 13 2018 at 20:16):

I think you might actually need hk ⟨hp, hq⟩ where hk is your proof of p ^ q -> k and hp is your proof of p and hq is your proof of q


Last updated: Dec 20 2023 at 11:08 UTC