@@ -271,6 +271,24 @@ splitPair =
271 solve ; pure (x, y)
271 solve ; pure (x, y)
272 _ => fail [TextPart "Goal is not a pair"]
272 _ => fail [TextPart "Goal is not a pair"]
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)
282+ fail [RawPart g, TextPart "is not a type declared with the data keyword"]
284+ choiceMap (\(n, xs, _) => apply (Var n) (map shouldUnify xs) <* solve)
285+ !(constructors <$> lookupDatatypeExact h)
287+ shouldUnify : CtorArg -> Bool
288+ shouldUnify (CtorParameter _) = True
289+ shouldUnify (CtorField (MkFunArg _ _ Explicit _)) = False
290+ shouldUnify (CtorField (MkFunArg _ _ _ _)) = True
274||| A special-purpose tactic that attempts to solve a goal using
292||| A special-purpose tactic that attempts to solve a goal using
275||| `Refl`. This is useful for ensuring that goals in fact are trivial
293||| `Refl`. This is useful for ensuring that goals in fact are trivial
276||| when developing or testing other tactics; otherwise, consider
294||| when developing or testing other tactics; otherwise, consider