@@ -271,6 +271,24 @@ splitPair =
271271 solve ; pure (x, y)
272272 _ => fail [TextPart "Goal is not a pair"]
273273
274+||| Try to apply the constructors of the goal data type one by one,
275+||| and apply the first one that works.
276+||| Similar to `constructor` in Coq.
277+construct : Elab (List TTName)
278+construct =
279+ do g <- goalType
280+ case headName g of
281+ Nothing =>
282+ fail [RawPart g, TextPart "is not a type declared with the data keyword"]
283+ Just h =>
284+ choiceMap (\(n, xs, _) => apply (Var n) (map shouldUnify xs) <* solve)
285+ !(constructors <$> lookupDatatypeExact h)
286+ where
287+ shouldUnify : CtorArg -> Bool
288+ shouldUnify (CtorParameter _) = True
289+ shouldUnify (CtorField (MkFunArg _ _ Explicit _)) = False
290+ shouldUnify (CtorField (MkFunArg _ _ _ _)) = True
291+
274292||| A special-purpose tactic that attempts to solve a goal using
275293||| `Refl`. This is useful for ensuring that goals in fact are trivial
276294||| when developing or testing other tactics; otherwise, consider