summaryrefslogtreecommitdiff
path: root/backends/hol4/primitivesScript.sml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-09-07Fix some issuesSon Ho1-0/+26
2023-06-04Finish the proofs of the hashmapSon Ho1-5/+24
2023-06-04Make good progress on the proofs of the hashmap in HOL4Son Ho1-4/+35
2023-06-04Make the theorems used by the progress tactic persistentSon Ho1-2/+2
2023-06-04Make progress on the HOL4 backendSon Ho1-26/+155
2023-06-04Make progress on extracting the HOL4 filesSon Ho1-0/+119
2023-06-04Make the unfolding theorems collection from evalLib persistentSon Ho1-31/+16
2023-06-04Update the definitions of mk_vec and vec_insert_backSon Ho1-15/+56
2023-06-04Cleanup a bit the HOL4 backend and implement eval_convSon Ho1-12/+120
2023-06-04Make good progress on generating code for HOL4Son Ho1-117/+404
2023-06-04Cleanup a bit and reorganizeSon Ho1-0/+3
2023-06-04Start working on divDefLib for diverging definitionsSon Ho1-2/+2
2023-06-04Make progress on the standard library for HOL4Son Ho1-78/+3
2023-06-04Cleanup a bitSon Ho1-178/+3
2023-06-04Make progress on primitivesScriptSon Ho1-28/+16
2023-06-04Make more progress on primitivesScript.smlSon Ho1-61/+55
2023-06-04Use lower case in the names for the HOL4 backendSon Ho1-329/+222
2023-06-04Make progress on primitivesScript.sml and experiment a bitSon Ho1-0/+177
2023-06-04Make progress on the primitives library for HOL4Son Ho1-9/+175
2023-06-04Organize a bit the HOL filesSon Ho1-115/+29
2023-06-04Add a HolmakefileSon Ho1-6/+4
2023-06-04Make good progress on Primitives.smlSon Ho1-24/+997
2023-06-04Start working on Primitives.smlSon Ho1-0/+385
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 19:26:37 +0000