The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Jan 10, 2015, at 9:01 , Cedric Auger <sedrikov AT gmail.com> wrote:

I do not like much to split your operator into three classes (Vop_i, Vop_o, others).

This distinction sounds awkward to me, and each lemma/definition will likely be split in three…

This is not much convenient, and reading will be harder.

Cedric,

Thanks for these commends. I have successfully reworked my language based on your suggestions and all 

worked out very nicely. I will make sure I will understand how it works exactly before proceeding. 

Sincerely,
Vadim Zaliva

--

CMU ECE PhD student

Mobile: +1(510)220-1060

Skype: vzaliva