summaryrefslogtreecommitdiff
path: root/backends/hol4/primitivesScript.sml (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Fix some issuesSon Ho2023-09-071-0/+26
|
* Finish the proofs of the hashmapSon Ho2023-06-041-5/+24
|
* Make good progress on the proofs of the hashmap in HOL4Son Ho2023-06-041-4/+35
|
* Make the theorems used by the progress tactic persistentSon Ho2023-06-041-2/+2
|
* Make progress on the HOL4 backendSon Ho2023-06-041-26/+155
|
* Make progress on extracting the HOL4 filesSon Ho2023-06-041-0/+119
|
* Make the unfolding theorems collection from evalLib persistentSon Ho2023-06-041-31/+16
|
* Update the definitions of mk_vec and vec_insert_backSon Ho2023-06-041-15/+56
|
* Cleanup a bit the HOL4 backend and implement eval_convSon Ho2023-06-041-12/+120
|
* Make good progress on generating code for HOL4Son Ho2023-06-041-117/+404
|
* Cleanup a bit and reorganizeSon Ho2023-06-041-0/+3
|
* Start working on divDefLib for diverging definitionsSon Ho2023-06-041-2/+2
|
* Make progress on the standard library for HOL4Son Ho2023-06-041-78/+3
|
* Cleanup a bitSon Ho2023-06-041-178/+3
|
* Make progress on primitivesScriptSon Ho2023-06-041-28/+16
|
* Make more progress on primitivesScript.smlSon Ho2023-06-041-61/+55
|
* Use lower case in the names for the HOL4 backendSon Ho2023-06-041-329/+222
|
* Make progress on primitivesScript.sml and experiment a bitSon Ho2023-06-041-0/+177
|
* Make progress on the primitives library for HOL4Son Ho2023-06-041-9/+175
|
* Organize a bit the HOL filesSon Ho2023-06-041-0/+1270