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
/
lean
/
Base
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
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
2
-2
/
+223
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
1
-3
/
+2
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
2
-7
/
+230
2023-06-09
Reorganize a bit the Lean library
Son Ho
1
-0
/
+650