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

Cleanup #612

Merged
merged 25 commits into from Jan 28, 2019

Conversation

Projects
None yet
2 participants
@xrchz
Copy link
Member

xrchz commented Jan 27, 2019

No description provided.

mn200 and others added some commits Jan 22, 2019

Move a theorem to HOL, renaming it to avoid name-clash
Rename forces tweak to use-sites (2 of them, both in stack_allocProof)
Fix some uses of Theorem syntax
Handling computed quotations is pushing this syntax pretty hard... I
don't know why it worked previously.
Move some theorems to HOL; mark other candidates as not movable
Moved theorems went to option and while theories (see HOL's b548a765b).
@mn200

This comment has been minimized.

Copy link
Contributor

mn200 commented on d867217 Jan 23, 2019

Theorem name (... is now taken for save_thm

@xrchz xrchz merged commit be8c718 into master Jan 28, 2019

1 check failed

cakeml-regression-test regression test failed
Details
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment