index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
backends
/
hol4
/
primitivesBaseTacLib.sml
(
follow
)
Commit message (
Collapse
)
Author
Age
Files
Lines
*
Add a comment
Son Ho
2023-06-04
1
-3
/
+7
|
*
Start setting up the Nix derivation for HOL4
Son Ho
2023-06-04
1
-0
/
+8
|
*
Make good progress on the proofs of the hashmap in HOL4
Son Ho
2023-06-04
1
-4
/
+28
|
*
Fix some minor issues
Son Ho
2023-06-04
1
-22
/
+45
|
*
Make the unfolding theorems collection from evalLib persistent
Son Ho
2023-06-04
1
-2
/
+20
|
*
Cleanup a bit the HOL4 backend and implement eval_conv
Son Ho
2023-06-04
1
-2
/
+1
|
*
Introduce fix_exec, an executable version of fix
Son Ho
2023-06-04
1
-0
/
+1
|
*
Reimplement DefineDiv with the new fixed point operator
Son Ho
2023-06-04
1
-1
/
+4
|
*
Improve the performance of dependent rewrites by using nets
Son Ho
2023-06-04
1
-49
/
+106
|
*
Make more proofs about the hashmap proto
Son Ho
2023-06-04
1
-4
/
+21
|
*
Update the hashmap proofs and fix some tactics
Son Ho
2023-06-04
1
-21
/
+44
|
*
Start working on divDefLib for diverging definitions
Son Ho
2023-06-04
1
-18
/
+81
|
*
Reorganize the HOL4 files and fix some issues with the arithmetic proofs
Son Ho
2023-06-04
1
-11
/
+16
|
*
Make progress on the standard library for HOL4
Son Ho
2023-06-04
1
-4
/
+89
|
*
Cleanup a bit
Son Ho
2023-06-04
1
-8
/
+14
|
*
Use lower case in the names for the HOL4 backend
Son Ho
2023-06-04
1
-3
/
+9
|
*
Make progress on primitivesScript.sml and experiment a bit
Son Ho
2023-06-04
1
-2
/
+397
|
*
Make progress on the primitives library for HOL4
Son Ho
2023-06-04
1
-2
/
+20
|
*
Organize a bit the HOL files
Son Ho
2023-06-04
1
-0
/
+16
