search

CakeML / cakeml

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

Upstream misc #549

Open xrchz opened 6 years ago

xrchz commented 6 years ago

CakeML's miscTheory and preamble contain many general-purpose theorems and tools that are supposed to be upstreamed to HOL wherever possible. This issue is to do an upstreaming pass. To resolve this issue, move things from miscTheory and preamble to HOL, or add a comment explaining why this is not possible, until no undocumented bindings remain.

xrchz commented 5 years ago

Note: this can only be finished after #414 is closed.

xrchz commented 5 years ago

I would add misc/basicComputeLib.sml as a place to look for things to upstream too (and probably most things under misc/)