coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: David Pereira <dpereira AT liacc.up.pt>
- To: prateek agarwal <prat0318 AT gmail.com>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Needed assistance in Coq proof for kleene algebra axioms
- Date: Tue, 31 Mar 2009 17:10:07 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Dear Prateek,
The code described in the paper you are using, "KAT and PHL in Coq", puslished in ComSIS Volume 5, Number 2, December 2008, is part of a bigger project, and it will be publicly available when that project is completed.
Best regards,
David Pereira
On 2009/03/31, at 09:52, prateek agarwal wrote:
Hi,
If anyone has the coq proofs for the axioms of Kleene algebra
and Kleene algebra Tests, I shall be grateful if you could please
provide them to me. Or, I am having a short coq code written for their
proofs, but an error in compilation occurs in lines where ~ and #
symbols are used. I am a newbie in COQ, can anyone please sort out the
error.
<snippet from ka.v>...
Record boolean_theory : Prop := mk_bool {
ba_ax_1 : forall x, x * ~x = 0 ;
...
Error : The term "0" has the type "nat" while it is expected to have type "Set".
--
Prateek Agarwal
Senior Undergraduate Student
Dept. of Computer Science And Engg.
Indian Institute of Technology, Kharagpur
"Half the people you know are below average."
<ka.v>
- [Coq-Club] Needed assistance in Coq proof for kleene algebra axioms, prateek agarwal
- Re: [Coq-Club] Needed assistance in Coq proof for kleene algebra axioms, Adam Chlipala
- Re: [Coq-Club] Needed assistance in Coq proof for kleene algebra axioms, David Pereira
Archive powered by MhonArc 2.6.16.