@@ -256,6 +256,21 @@ unproduct tm =
256 try (unproduct (Var n1))
256 try (unproduct (Var n1))
257 try (unproduct (Var n2))
257 try (unproduct (Var n2))
259+||| If the goal is a tuple or a dependent pair, then split it into
260+||| two goals and return the new goal names.
261+||| It fails if the goal is neither a `Pair` nor a `DPair`.
262+splitPair : Elab (TTName, TTName)
264+ let bug = [TextPart "Splitting created wrong number of holes"] in
266+ `(Pair ~A ~B) => do [x, y] <- apply `(MkPair {A=~A} {B=~B}) [False, False]
269+ `(DPair ~A ~Pr) => do [x, y] <- apply `(MkDPair {a=~A} {P=~Pr}) [False, False]
272+ _ => fail [TextPart "Goal is not a pair"]
259||| A special-purpose tactic that attempts to solve a goal using
274||| A special-purpose tactic that attempts to solve a goal using
260||| `Refl`. This is useful for ensuring that goals in fact are trivial
275||| `Refl`. This is useful for ensuring that goals in fact are trivial
261||| when developing or testing other tactics; otherwise, consider
276||| when developing or testing other tactics; otherwise, consider