summaryrefslogtreecommitdiff
path: root/backends/hol4/primitivesTheory.sig (follow)
Commit message (Expand)AuthorAgeFilesLines
* Update the HOL4 proofs for the last *release* version of HOL4Son Ho2023-06-041-113/+113
* Finish the proofs of the hashmapSon Ho2023-06-041-4/+20
* Make good progress on the proofs of the hashmap in HOL4Son Ho2023-06-041-6/+33
* Make the theorems used by the progress tactic persistentSon Ho2023-06-041-10/+5
* Make progress on the HOL4 backendSon Ho2023-06-041-16/+143
* Make progress on extracting the HOL4 filesSon Ho2023-06-041-2/+97
* Update the definitions of mk_vec and vec_insert_backSon Ho2023-06-041-6/+15
* Cleanup a bit the HOL4 backend and implement eval_convSon Ho2023-06-041-0/+104
* Make good progress on generating code for HOL4Son Ho2023-06-041-0/+331
* Cleanup a bit and reorganizeSon Ho2023-06-041-0/+6
* Start working on divDefLib for diverging definitionsSon Ho2023-06-041-11/+11
* Make progress on the standard library for HOL4Son Ho2023-06-041-2/+2
* Cleanup a bitSon Ho2023-06-041-5/+0
* Make progress on primitivesScriptSon Ho2023-06-041-166/+125
* Make more progress on primitivesScript.smlSon Ho2023-06-041-148/+136
* Use lower case in the names for the HOL4 backendSon Ho2023-06-041-403/+401
* Make progress on primitivesScript.sml and experiment a bitSon Ho2023-06-041-81/+312
* Organize a bit the HOL filesSon Ho2023-06-041-0/+1612