Skip to Content.
Sympa Menu

coq-club - Re: Re: [Coq-Club] applying a function definition

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: Re: [Coq-Club] applying a function definition


chronological Thread 
  • From: brandon_m_moore AT yahoo.com
  • To: coq-club AT inria.fr
  • Subject: Re: Re: [Coq-Club] applying a function definition
  • Date: Mon, 27 Jun 2011 20:27:17 +0200

The code seems to work correctly after replacing

Definition hdT (a:T) : T :=
match a with
| E => E
| C _ y =>y
end.

by

Definition hdT (a:T) : T :=
match a with
| E => E
| C x _ =>x
end.



Archive powered by MhonArc 2.6.16.

Top of Page