The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

prateek agarwal wrote:
>         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".
>   

You seem to be trying to treat Coq's logic as untyped, which it isn't.  
Unless you explicitly introduce overrides of the standard notations, [0] 
always means natural-number zero, [*] always means natural-number 
multiplication, etc..  Each of your theory records should contain the 
[Set] being operated on, along with the constant and operator 
definitions, and the logical members of the record should refer to those 
operators, not some fixed set of operators, which can't be "polymorphic 
enough."  (There may be alternate ways of doing this with the newfangled 
type class support, but I don't know that stuff well enough to say.)