index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
...
*
Start working on Elab.lean
Son Ho
2023-06-29
3
-13
/
+203
*
Reorganize backends/lean/Base
Son Ho
2023-06-28
4
-1102
/
+1298
*
Reduce the time spent on some proofs
Son Ho
2023-06-27
1
-28
/
+20
*
Finish some proofs in Diverge
Son Ho
2023-06-27
1
-17
/
+102
*
Finish the proofs which use FixI
Son Ho
2023-06-27
1
-42
/
+157
*
Make minor modifications
Son Ho
2023-06-26
1
-16
/
+0
*
Add FixI in Diverge
Son Ho
2023-06-26
1
-22
/
+105
*
Generalize some definitions
Son Ho
2023-06-26
1
-12
/
+22
*
Make the definitions in Diverge.Fix dependently typed
Son Ho
2023-06-26
1
-48
/
+47
*
Start working on a better encoding of mut rec defs for Diverge
Son Ho
2023-06-26
1
-2
/
+100
*
Make minor modifications to Arith.lean
Son Ho
2023-06-26
1
-27
/
+37
*
Make intro_has_prop_instances work
Son Ho
2023-06-22
1
-26
/
+145
*
Finish the custom_let tactic
Son Ho
2023-06-22
1
-23
/
+21
*
Start working on Arith.lean
Son Ho
2023-06-21
3
-2
/
+224
*
Remove the use of fun. ext. in Diverge.lean
Son Ho
2023-06-20
1
-15
/
+19
*
Cleanup Diverge.lean
Son Ho
2023-06-19
2
-337
/
+333
*
Add an example with even/odd in Diverge.lean
Son Ho
2023-06-19
1
-1
/
+119
*
Remove the obsolete examples from Diverge
Son Ho
2023-06-19
1
-208
/
+5
*
Simplify the id example in Diverge.lean
Son Ho
2023-06-19
1
-24
/
+95
*
Further simplify the proofs in Diverge.lean
Son Ho
2023-06-19
1
-122
/
+151
*
Make progress on making the proofs in Diverge more systematic
Son Ho
2023-06-19
1
-8
/
+252
*
Make minor modifications
Son Ho
2023-06-18
2
-3
/
+3
*
Make minor modifications
Son Ho
2023-06-14
2
-6
/
+26
*
Find sufficient validity criteria for Diverge.lean
Son Ho
2023-06-13
1
-41
/
+309
*
Start working on extrinsic proofs of termination
Son Ho
2023-06-09
4
-7
/
+232
*
Reorganize a bit the Lean library
Son Ho
2023-06-09
4
-22
/
+36
*
Remove the sorries from Primitives.lean
Son Ho
2023-06-06
2
-65
/
+120
*
Add a comment
Son Ho
2023-06-04
1
-3
/
+7
*
Update the HOL4 proofs for the last *release* version of HOL4
Son Ho
2023-06-04
10
-470
/
+468
*
Start setting up the Nix derivation for HOL4
Son Ho
2023-06-04
6
-12
/
+58
*
Simplify a proof
Son Ho
2023-06-04
1
-12
/
+6
*
Remove some obsolete files from the HOL4 backend
Son Ho
2023-06-04
4
-3302
/
+0
*
Make minor modifications to the Makefile
Son Ho
2023-06-04
1
-2
/
+2
*
Add a comment
Son Ho
2023-06-04
1
-1
/
+5
*
Finish the proofs of the hashmap
Son Ho
2023-06-04
7
-472
/
+1559
*
Prove hash_map_insert_fwd_back_spec
Son Ho
2023-06-04
1
-1
/
+59
*
Make progress on the proofs of the hash map
Son Ho
2023-06-04
6
-6
/
+799
*
Make good progress on the proofs of the hashmap in HOL4
Son Ho
2023-06-04
7
-64
/
+841
*
Start working on the proofs of the hash map
Son Ho
2023-06-04
1
-0
/
+543
*
Make the theorems used by the progress tactic persistent
Son Ho
2023-06-04
8
-186
/
+285
*
Update tests/Makefile
Son Ho
2023-06-04
1
-1
/
+1
*
Add the generated HOL4 files
Son Ho
2023-06-04
44
-4
/
+13223
*
Commit saveThmsLib.sig
Son Ho
2023-06-04
1
-0
/
+46
*
Improve the parsing for divDefLib
Son Ho
2023-06-04
1
-1
/
+91
*
Fix some minor issues
Son Ho
2023-06-04
2
-41
/
+49
*
Make progress on the HOL4 backend
Son Ho
2023-06-04
4
-81
/
+378
*
Make progress on extracting the HOL4 files
Son Ho
2023-06-04
5
-18
/
+319
*
Make the unfolding theorems collection from evalLib persistent
Son Ho
2023-06-04
10
-251
/
+235
*
Make minor modifications
Son Ho
2023-06-04
1
-5
/
+11
*
Start working on saveThmsLib
Son Ho
2023-06-04
1
-0
/
+190
[prev]
[next]