leanprover/lean — pull request #377 by avigad (2014-12-15 21:56:28+00:00)
Title: cleaning up the library

I started renaming theorems in logic, cleaning up comments, etc. I created a markdown file for the init folder. I still have to repair the rest of the markdown files.

I suggest the following changes to init.logic:

iff.flip_sign -> not_iff_not_of_iff
exists_intro -> exists.intro
exists_elim -> exists.elim
decidable_iff_equiv -> decidable_of_decidable_of_iff

I don't feel strongly about the first and last, but I think exists.into and exists.elim are important. Leo, I think you have to do this, right?

I had a hard time coming up with better names for eq. I propose to make the following changes:

eq.id_refl -> eq_refl_of_eq
delete equal_f (it is just congr_fun)
eqmp -> eq.mp
eqmpr -> eq.mp' (not that it is any better, but we have iff.mp')
imp_trans -> imp.trans
imp_eq_trans -> eq_of_imp_of_eq
eq_imp_trans -> eq_of_eq_of_imp
p_ne_false -> ne_false
p_ne_true -> ne_true_of_not

@javra @fpvandoorn feel free to offer suggestions here.

The names in cast seem to be an even bigger mess, but it is better to leave it to someone actively using cast to clean it up.

@javra I hope this renaming is not causing problems for the HoTT split.

This housecleaning is boring, so I will spread it out and do a little at a time. The files in the top level of logic are o.k., but I still have to clean up the axioms folder.