Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] impossible branches in pattern matching

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] impossible branches in pattern matching


Chronological Thread 
  • From: Daniel Schepler <dschepler AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] impossible branches in pattern matching
  • Date: Thu, 13 Feb 2014 11:04:39 -0800

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



Archive powered by MHonArc 2.6.18.

Top of Page