coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] impossible branches in pattern matching, Kirill Taran, 02/13/2014
- Re: [Coq-Club] impossible branches in pattern matching, Daniel Schepler, 02/13/2014
- Re: [Coq-Club] impossible branches in pattern matching, Pierre-Marie Pédrot, 02/13/2014
- Re: [Coq-Club] impossible branches in pattern matching, Kirill Taran, 02/13/2014
- Re: [Coq-Club] impossible branches in pattern matching, Kirill Taran, 02/14/2014
- Re: [Coq-Club] impossible branches in pattern matching, Kirill Taran, 02/14/2014
- Re: [Coq-Club] impossible branches in pattern matching, Daniel Schepler, 02/14/2014
- Re: [Coq-Club] impossible branches in pattern matching, Kirill Taran, 02/14/2014
- Re: [Coq-Club] impossible branches in pattern matching, Daniel Schepler, 02/14/2014
- Re: [Coq-Club] impossible branches in pattern matching, Jason Gross, 02/14/2014
- Re: [Coq-Club] impossible branches in pattern matching, Daniel Schepler, 02/14/2014
- Re: [Coq-Club] impossible branches in pattern matching, Daniel Schepler, 02/14/2014
- Re: [Coq-Club] impossible branches in pattern matching, Kirill Taran, 02/14/2014
- Re: [Coq-Club] impossible branches in pattern matching, Daniel Schepler, 02/14/2014
- Re: [Coq-Club] impossible branches in pattern matching, Kirill Taran, 02/14/2014
- Re: [Coq-Club] impossible branches in pattern matching, Kirill Taran, 02/14/2014
- Re: [Coq-Club] impossible branches in pattern matching, Kirill Taran, 02/13/2014
Archive powered by MHonArc 2.6.18.