@@ -257,22 +257,23 @@ unproduct tm =
257 try (unproduct (Var n2))
257 try (unproduct (Var n2))
259||| Try to apply the constructors of the goal data type one by one,
259||| 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.
261||| Similar to `constructor` in Coq.
264||| Similar to `constructor` in Coq.
262construct : Elab (List TTName)
265construct : Elab (List TTName)
265− case headName g of
266+construct = case headName !goalType of
266− Nothing =>
267+ Nothing =>
267− fail [RawPart g, TextPart "is not a type declared with the data keyword"]
268+ fail [TextPart "Goal is not of a type declared with the data keyword"]
268− Just h =>
269+ Just h =>
269− choiceMap (\(n, xs, _) => apply (Var n) (map shouldUnify xs) <* solve)
270+ choiceMap (\(n, xs, _) => apply (Var n) (map shouldUnify xs) <* solve)
270− !(constructors <$> lookupDatatypeExact h)
271+ !(constructors <$> lookupDatatypeExact h)
272+ <|> fail [TextPart "No constructors apply"]
272 shouldUnify : CtorArg -> Bool
274 shouldUnify : CtorArg -> Bool
273− shouldUnify (CtorParameter _) = True
274 shouldUnify (CtorField (MkFunArg _ _ Explicit _)) = False
275 shouldUnify (CtorField (MkFunArg _ _ Explicit _)) = False
275− shouldUnify (CtorField (MkFunArg _ _ _ _)) = True
276+ shouldUnify _ = True
277||| A special-purpose tactic that attempts to solve a goal using
278||| A special-purpose tactic that attempts to solve a goal using
278||| `Refl`. This is useful for ensuring that goals in fact are trivial
279||| `Refl`. This is useful for ensuring that goals in fact are trivial