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

Theorems can't be given certain names when saved/stored. #225

Closed
mn200 opened this Issue Jan 19, 2015 · 0 comments

Comments

Projects
None yet
1 participant
@mn200
Copy link
Member

mn200 commented Jan 19, 2015

Attempting to call a theorem Empty results in an error when the system attempts to use the generated theory file because Empty counts as a constructor name. We've also seen this with the name GREATER and others. I think it's buggy to fail so late in the process, and we should probably just allow the name to be used.

Most recent report of this thanks to Thibault Gauthier.

@mn200 mn200 added Bug Kernel labels Jan 19, 2015

@mn200 mn200 self-assigned this Jan 19, 2015

@mn200 mn200 closed this in 2673d9c Jan 19, 2015

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment