Skip to content

Add destruct_or tactics to (possibly repeatedly) split disjunctions in an assumption

Armaël Guéneau requested to merge Armael/stdpp:split_or into master

Following split_and, the new tactics are split_or H, split_or? H and split_or! H. The name H is reused for the assumptions that are produced by destructing the disjunction (no fresh name is introduced).

I was pondering whether the tactic should be split_or H or split_or in H. The second one follows the usual pattern of in+assumption, but at the same time there is not going to be a split_or tactic that works on the goal, so...

Edited by Armaël Guéneau

Merge request reports