[Isarmathlib-devel] Coq

[Victor Porton]

Do you consider a project similar to IsarMathLib but with Coq?

What are relative advantages of Isabelle and Coq? (For me it seems that Coq is 
more structured and elegant.)

I started reading about Coq but laid it aside as there are not even cardinal 
arithmetic (based on ZFC) for Coq.

I do not want to code cardinal arithmetic myself. But if somebody will do, I 
may consider to learn Coq and code my theory (and maybe even the theory of 
posets and lattices which my theory is based on) in it. (Or I may don't.)

-- 
Victor Porton - http://portonvictor.org