coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Cannot match on the parameter of an inductive

From: Evgeny Makarov <emakarov AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Cannot match on the parameter of an inductive
Date: Fri, 20 Aug 2010 14:34:47 +0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=KBJA8pCV3eM52K2vzCLxRq/vvbENy9El8ITuqiDn86BnsHKTXmjtkCHGOVULEIh8Lm V8aDz8i7X0w/TxX3Zq+CaVe0PrwHFdyYlxpcPpnSPgYshgjjmWLbvjsEq3apbYTyCEhi ePdX3HKHo/xBxY5GYjQmlzc6RmvUMZ1bTDTZQ=

Hello,

I don't have the solution, but this does look strange. If there are
two snippets of code of which only one works and which differ only in
"match e with" and "match id e with", then it looks like Coq does not
have the subject reduction property...

Evgeny

[Coq-Club] Cannot match on the parameter of an inductive, Alexandre Pilkiewicz
- Re: [Coq-Club] Cannot match on the parameter of an inductive, Evgeny Makarov
  - Re: [Coq-Club] Cannot match on the parameter of an inductive, Bruno Barras