Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

"exists" instead "EXType" #2

Open
georgydunaev opened this issue Nov 2, 2018 · 1 comment
Open

"exists" instead "EXType" #2

georgydunaev opened this issue Nov 2, 2018 · 1 comment

Comments

@georgydunaev
Copy link

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
Copy link
Contributor

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants