The Coq mailing list

[prateek agarwal <prat0318 AT gmail.com>]

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."

Attachment: ka.v
Description: Binary data