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