coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Casteran <pierre.casteran AT labri.fr>
- To: Jieung Kim <gbali AT kaist.ac.kr>
- Cc: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Problem with a simple proof
- Date: Thu, 07 Apr 2011 16:36:00 +0200
Dear Jieung Kim, Perhaps the first thing is to prove that "extends" is decidable (using lemmas on lists and the decidibility of equality on nat), then prove the decidibilty of "sub_ty" (may be not so trivial ? ) , then proceed as your first example. Pierre Le 07/04/2011 15:33, Jieung Kim a écrit :
|
- [Coq-Club] Problem with a simple proof, Jieung Kim
- Re: [Coq-Club] Problem with a simple proof,
Pierre Casteran
- Re: [Coq-Club] Problem with a simple proof,
Jieung Kim
- Re: [Coq-Club] Problem with a simple proof,
Adam Chlipala
- Re: [Coq-Club] Problem with a simple proof, Jieung Kim
- Re: [Coq-Club] Problem with a simple proof, Pierre Casteran
- Re: [Coq-Club] Problem with a simple proof, Jieung Kim
- Re: [Coq-Club] Problem with a simple proof,
Adam Chlipala
- Re: [Coq-Club] Problem with a simple proof,
Jieung Kim
- Re: [Coq-Club] Problem with a simple proof,
Pierre Casteran
Archive powered by MhonArc 2.6.16.