@@ -222,3 +222,19 @@ unproduct tm =
222222 both tm n1 n2
223223 try (unproduct (Var n1))
224224 try (unproduct (Var n2))
225+
226+
227+||| A special-purpose tactic that attempts to solve a goal using
228+||| `Refl`. This is useful for ensuring that goals in fact are trivial
229+||| when developing or testing other tactics; otherwise, consider
230+||| using `search`.
231+reflexivity : Elab ()
232+reflexivity =
233+ case !goalType of
234+ `((=) {A=~A} {B=~_} ~x ~_) =>
235+ do fill `(Refl {A=~A} {x=~x})
236+ solve
237+ _ => fail [ TextPart "The goal is not an equality, so"
238+ , NamePart `{reflexivity}
239+ , TextPart "is not applicable."
240+ ]