search

coq-contribs / zfc

An encoding of Zermelo-Fraenkel Set Theory in Coq
GNU Lesser General Public License v2.1
21 stars 3 forks source link

"exists" instead "EXType" #2

Open georgydunaev opened 5 years ago

georgydunaev commented 5 years ago

I think that it is common now to use "exists" instead "EXType". Shall I rename it in the whole repository? It is also possible to use "Defined." instead of "Qed." https://gmalecha.github.io/reflections/2017/qed-considered-harmful Will it be approved?

herbelin commented 5 years ago

I think that it is common now to use "exists" instead "EXType". Shall I rename it in the whole repository?

Yes, it will be approved.

It is also possible to use "Defined." instead of "Qed."

This question is more controversial. In a work like zfc where things do not compute a lot, I suspect that it does not matter so much, but in the general case, there is dilemma between ability to compute and ability to abstract. In practice, we may want one or the other depending on situation.

If you have a practical motivation for moving some statements to Defined, that will be approved. If it is just as an informal experiment w/o real need, I would lean towards staying with Qed.