@@ -257,22 +257,23 @@ unproduct tm =
257257 try (unproduct (Var n2))
258258
259259||| Try to apply the constructors of the goal data type one by one,
260−||| and apply the first one that works.
260+||| and apply the first one that works. If one of the constructors work,
261+||| the explicit arguments to the constructor are created as new holes and
262+||| the hole names are returned in a list. The parameters of the type and
263+||| the implicit arguments of the constructor will be solved by unification.
261264||| Similar to `constructor` in Coq.
262265construct : Elab (List TTName)
263−construct =
264− do g <- goalType
265− case headName g of
266− Nothing =>
267− fail [RawPart g, TextPart "is not a type declared with the data keyword"]
268− Just h =>
269− choiceMap (\(n, xs, _) => apply (Var n) (map shouldUnify xs) <* solve)
270− !(constructors <$> lookupDatatypeExact h)
266+construct = case headName !goalType of
267+ Nothing =>
268+ fail [TextPart "Goal is not of a type declared with the data keyword"]
269+ Just h =>
270+ choiceMap (\(n, xs, _) => apply (Var n) (map shouldUnify xs) <* solve)
271+ !(constructors <$> lookupDatatypeExact h)
272+ <|> fail [TextPart "No constructors apply"]
271273 where
272274 shouldUnify : CtorArg -> Bool
273− shouldUnify (CtorParameter _) = True
274275 shouldUnify (CtorField (MkFunArg _ _ Explicit _)) = False
275− shouldUnify (CtorField (MkFunArg _ _ _ _)) = True
276+ shouldUnify _ = True
276277
277278||| A special-purpose tactic that attempts to solve a goal using
278279||| `Refl`. This is useful for ensuring that goals in fact are trivial