summaryrefslogtreecommitdiff
path: root/backends/hol4/primitivesArithScript.sml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Simplify a proofSon Ho1-12/+6
2023-06-04Make progress on the proofs of the hash mapSon Ho1-0/+118
2023-06-04Make good progress on the proofs of the hashmap in HOL4Son Ho1-0/+14
2023-06-04Cleanup a bit the HOL4 backend and implement eval_convSon Ho1-2/+1
2023-06-04Start working on more general fixed-point combinatorsSon Ho1-0/+1
2023-06-04Make more proofs about the hashmap protoSon Ho1-0/+6
2023-06-04Make progress on the standard library for HOL4Son Ho1-0/+7
2023-06-04Make progress on primitivesScriptSon Ho1-15/+40
2023-06-04Use lower case in the names for the HOL4 backendSon Ho1-63/+90
2023-06-04Make progress on the primitives library for HOL4Son Ho1-1/+1
2023-06-04Organize a bit the HOL filesSon Ho1-0/+147