summaryrefslogtreecommitdiff
path: root/backends/hol4/primitivesTheory.sig (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Update the HOL4 proofs for the last *release* version of HOL4Son Ho1-113/+113
2023-06-04Finish the proofs of the hashmapSon Ho1-4/+20
2023-06-04Make good progress on the proofs of the hashmap in HOL4Son Ho1-6/+33
2023-06-04Make the theorems used by the progress tactic persistentSon Ho1-10/+5
2023-06-04Make progress on the HOL4 backendSon Ho1-16/+143
2023-06-04Make progress on extracting the HOL4 filesSon Ho1-2/+97
2023-06-04Update the definitions of mk_vec and vec_insert_backSon Ho1-6/+15
2023-06-04Cleanup a bit the HOL4 backend and implement eval_convSon Ho1-0/+104
2023-06-04Make good progress on generating code for HOL4Son Ho1-0/+331
2023-06-04Cleanup a bit and reorganizeSon Ho1-0/+6
2023-06-04Start working on divDefLib for diverging definitionsSon Ho1-11/+11
2023-06-04Make progress on the standard library for HOL4Son Ho1-2/+2
2023-06-04Cleanup a bitSon Ho1-5/+0
2023-06-04Make progress on primitivesScriptSon Ho1-166/+125
2023-06-04Make more progress on primitivesScript.smlSon Ho1-148/+136
2023-06-04Use lower case in the names for the HOL4 backendSon Ho1-403/+401
2023-06-04Make progress on primitivesScript.sml and experiment a bitSon Ho1-81/+312
2023-06-04Organize a bit the HOL filesSon Ho1-74/+19
2023-06-04Add a HolmakefileSon Ho1-0/+1667
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-02 00:18:55 +0000