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

Update code base to use Theorem, Definition, Inductive, Type etc #681

Open
myreen opened this issue Aug 22, 2019 · 0 comments

Comments

@myreen
Copy link
Contributor

commented Aug 22, 2019

The latest HOL has support for nice user facing syntax. This issue is about updating the entire code base to use the new syntax.

Two steps:

  1. update all definitions, lemmas and theorems to use the new syntax
  2. enforce the use of new syntax by making readme_gen reject old syntax.

Note that the updates need to be staged so that we don't create too much extra work on long running branches, such as words-bitwidth-semantics and ffi-ctypes. For example, I suspect we don't want to ban prove before those branches are merged into master or at least are closer to master.

@myreen myreen added the enhancement label Aug 22, 2019

@myreen myreen self-assigned this Aug 22, 2019

myreen added a commit that referenced this issue Aug 22, 2019
myreen added a commit that referenced this issue Aug 22, 2019
myreen added a commit that referenced this issue Aug 22, 2019
myreen added a commit that referenced this issue Aug 25, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
1 participant
You can’t perform that action at this time.