search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
965 stars 84 forks source link

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

Open myreen opened 5 years ago

myreen commented 5 years ago

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.

dnezam commented 2 months ago

Fully updating to the new Quote syntax depends on https://github.com/HOL-Theorem-Prover/HOL/issues/1313 - in particular, there is at least once instance in characteristic/examples/cf_examplesScript.sml that is affected by this.