coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- Re: [Coq-Club] applying a function definition, Paul Tarau
- Re: [Coq-Club] applying a function definition, Andreas Abel
- Re: [Coq-Club] applying a function definition,
AUGER Cedric
- Re: [Coq-Club] applying a function definition,
Paul Tarau
- Re: [Coq-Club] applying a function definition, Paul Tarau
- Re: [Coq-Club] applying a function definition,
Paul Tarau
- <Possible follow-ups>
- Re: Re: [Coq-Club] applying a function definition, brandon_m_moore
- Re: [Coq-Club] applying a function definition, Paul Tarau
Archive powered by MhonArc 2.6.16.