@@ -195,3 +195,31 @@ refine tm =
195 where countPi : Raw -> Nat
195 where countPi : Raw -> Nat
196 countPi (RBind _ (Pi _ _) body) = S (countPi body)
196 countPi (RBind _ (Pi _ _) body) = S (countPi body)
197 countPi _ = Z
197 countPi _ = Z
200+||| Split a pair into its projections, binding them in the context
201+||| with the supplied names. A special case of Coq's `inversion`.
202+both : Raw -> TTName -> TTName -> Elab ()
204+ do -- We don't know that the term is canonical, so let-bind projections applied to it
205+ (A, B) <- isPairTy (snd !(check tm))
206+ remember n1 A; apply `(fst {a=~A} {b=~B} ~tm) []; solve
207+ remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve
209+ isPairTy : TT -> Elab (Raw, Raw)
210+ isPairTy `((~A, ~B) : Type) = [| MkPair (forgetTypes A) (forgetTypes B) |]
211+ isPairTy tm = fail [TermPart tm, TextPart "is not a pair"]
213+||| Let-bind all results of completely destructuring nested tuples.
215+||| This makes them available to the `hypothesis` tactic, among others.
217+||| @ tm the nested tuple to destructure
219+unproduct : (tm : Raw) -> Elab ()
221+ do n1 <- gensym "left"
222+ n2 <- gensym "right"
224+ try (unproduct (Var n1))
225+ try (unproduct (Var n2))