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
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2023-06-26
Make minor modifications
Son Ho
1
-16
/
+0
2023-06-26
Add FixI in Diverge
Son Ho
1
-22
/
+105
2023-06-26
Generalize some definitions
Son Ho
1
-12
/
+22
2023-06-26
Make the definitions in Diverge.Fix dependently typed
Son Ho
1
-48
/
+47
2023-06-26
Start working on a better encoding of mut rec defs for Diverge
Son Ho
1
-2
/
+100
2023-06-26
Make minor modifications to Arith.lean
Son Ho
1
-27
/
+37
2023-06-22
Make intro_has_prop_instances work
Son Ho
1
-26
/
+145
2023-06-22
Finish the custom_let tactic
Son Ho
1
-23
/
+21
2023-06-21
Start working on Arith.lean
Son Ho
3
-2
/
+224
2023-06-20
Remove the use of fun. ext. in Diverge.lean
Son Ho
1
-15
/
+19
2023-06-19
Cleanup Diverge.lean
Son Ho
2
-337
/
+333
2023-06-19
Add an example with even/odd in Diverge.lean
Son Ho
1
-1
/
+119
2023-06-19
Remove the obsolete examples from Diverge
Son Ho
1
-208
/
+5
2023-06-19
Simplify the id example in Diverge.lean
Son Ho
1
-24
/
+95
2023-06-19
Further simplify the proofs in Diverge.lean
Son Ho
1
-122
/
+151
2023-06-19
Make progress on making the proofs in Diverge more systematic
Son Ho
1
-8
/
+252
2023-06-18
Make minor modifications
Son Ho
2
-3
/
+3
2023-06-14
Make minor modifications
Son Ho
2
-6
/
+26
2023-06-13
Find sufficient validity criteria for Diverge.lean
Son Ho
1
-41
/
+309
2023-06-09
Start working on extrinsic proofs of termination
Son Ho
4
-7
/
+232
2023-06-09
Reorganize a bit the Lean library
Son Ho
4
-22
/
+36
2023-06-06
Remove the sorries from Primitives.lean
Son Ho
2
-65
/
+120
2023-06-04
Add a comment
Son Ho
1
-3
/
+7
2023-06-04
Update the HOL4 proofs for the last *release* version of HOL4
Son Ho
3
-145
/
+137
2023-06-04
Start setting up the Nix derivation for HOL4
Son Ho
2
-1
/
+9
2023-06-04
Simplify a proof
Son Ho
1
-12
/
+6
2023-06-04
Remove some obsolete files from the HOL4 backend
Son Ho
4
-3302
/
+0
2023-06-04
Finish the proofs of the hashmap
Son Ho
5
-9
/
+98
2023-06-04
Make progress on the proofs of the hash map
Son Ho
5
-2
/
+180
2023-06-04
Make good progress on the proofs of the hashmap in HOL4
Son Ho
6
-18
/
+155
2023-06-04
Make the theorems used by the progress tactic persistent
Son Ho
8
-186
/
+285
2023-06-04
Commit saveThmsLib.sig
Son Ho
1
-0
/
+46
2023-06-04
Improve the parsing for divDefLib
Son Ho
1
-1
/
+91
2023-06-04
Fix some minor issues
Son Ho
2
-41
/
+49
2023-06-04
Make progress on the HOL4 backend
Son Ho
2
-42
/
+298
2023-06-04
Make progress on extracting the HOL4 files
Son Ho
2
-2
/
+216
2023-06-04
Make the unfolding theorems collection from evalLib persistent
Son Ho
9
-242
/
+222
2023-06-04
Make minor modifications
Son Ho
1
-5
/
+11
2023-06-04
Start working on saveThmsLib
Son Ho
1
-0
/
+190
2023-06-04
Commit evalLib
Son Ho
2
-0
/
+170
2023-06-04
Update the definitions of mk_vec and vec_insert_back
Son Ho
2
-21
/
+71
2023-06-04
Cleanup a bit the HOL4 backend and implement eval_conv
Son Ho
14
-56
/
+238
2023-06-04
Make good progress on generating code for HOL4
Son Ho
3
-123
/
+736
2023-06-04
Make a minor modification
Son Ho
1
-3
/
+5
2023-06-04
Introduce fix_exec, an executable version of fix
Son Ho
5
-13
/
+90
2023-06-04
Make minor modifications
Son Ho
2
-8
/
+35
2023-06-04
Make minor modifications to divDefLib
Son Ho
2
-60
/
+65
2023-06-04
Fix minor issues
Son Ho
3
-12
/
+508
2023-06-04
Fix minor issues
Son Ho
2
-6
/
+17
2023-06-04
Do more cleanup
Son Ho
2
-1222
/
+0
[next]