Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Pierce Software Foundations. Runs fine in Coq 8.4, but error in 8.5.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Pierce Software Foundations. Runs fine in Coq 8.4, but error in 8.5.


Chronological Thread 
  • From: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Pierce Software Foundations. Runs fine in Coq 8.4, but error in 8.5.
  • Date: Tue, 24 Feb 2015 07:31:28 +0100

On 24/02/2015 07:20, Sriram Srinivasan wrote:
Can someone explain why the following doesn't work in 8.5beta1?

Inductive list (X:Type) : Type :=
| nil : list X
| cons : X -> list X -> list X.

Fixpoint length (X:Type) (l:list X) : nat :=
match l with
|nil => 0
|cons h t => S (length X t)
end.

Error: The constructor nil (in type list) expects 1 argument.

Constructors and destructors are no longer separate in 8.5. Since the constructor nil takes an argument, the destructor nil also takes an argument. Since this argument is noninformative, it has to be "_".

Fixpoint length (X:Type) (l:list X) : nat :=
match l with
| nil _ => 0
| cons _ h t => S (length X t)
end.

You can recover the old behavior by using

Set Asymmetric Patterns.

Best regards,

Guillaume



Archive powered by MHonArc 2.6.18.

Top of Page