The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 13/02/2014 19:54, Kirill Taran wrote:
> But Coq complains about definition of Matching: it says that pattern
> matching is non-exhaustive and there are can be branches L right and R
> left. But we never can construct such objects. Why Coq can't infer that?

Because this is undecidable in general. You have to write out return
clauses by hand when you start messing with dependent pattern-matching.

Or you can use Program to do the dirty job for you.

Program Definition Matching (n : Node) :=
  match n with
  | L left  => True
  | R right => True
  | _ => !
  end.

(Here '!' stands for the absurd case. Have a look at the generated term
to understand how it works.)

The more your inductives will be dependent, the more you will need to do
things by hand. I recommend the reading of CPDT to get a handful of neat
design patterns when programming with dependent types.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature