The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

The last definition worked for me if I revised it to:

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

As for why the definition wasn't accepted as you wrote it: I'm not
sure how exactly the new match type generation from Coq 8.4 actually
works, so I can't really answer that.
-- 
Daniel Schepler

On Thu, Feb 13, 2014 at 10:54 AM, Kirill Taran 
<kirill.t256 AT gmail.com>
 wrote:
> Hello,
>
> I tried such code:
>
> Inductive  Tag     : Type := Left | Right.
> Inductive  Element : Tag -> Type :=
>   | left  : Element Left
>   | right : Element Right.
> Inductive  Node    : Type :=
>   | L : Element Left  -> Node
>   | R : Element Right -> Node.
> Definition HList   : Type := list Node.
> Definition Matching (n : Node) :=
>   match n with
>   | L left  => True
>   | R right => True
>   end.
>
> 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?
>
> Sincerely,
> Kirill Taran