The Coq mailing list

[David Pereira <dpereira AT liacc.up.pt>]

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>