Zulip Chat Archive

Stream: general

Topic: extract `imp` from `iff`


Scott Morrison (Oct 07 2018 at 00:10):

I'd like a function meta imp_of_iff : expr -> tactic expr, that takes a lemma that says, \Pi (...), P \iff Q, and gives me instead the lemma \Pi (...), P \to Q. Has anyone seen this lying around somewhere in mathlib? It's probably not too hard, I'm just hoping it's already done!

Scott Morrison (Oct 07 2018 at 00:28):

Ugh, okay, I revise that, I'm finding it hard. :-)

Scott Morrison (Oct 07 2018 at 00:31):

Ah, maybw tactic/alias.lean has mk_iff_mp_app, which seems promising.

Scott Morrison (Oct 07 2018 at 00:34):

Hmm, not clear that helps, it seems tied to actual declarations.

Scott Morrison (Oct 07 2018 at 00:51):

Sorted it out. tactic/alias.lean has everything I need.


Last updated: Dec 20 2023 at 11:08 UTC