aeneas - aeneas rust verifier with a hacky Isabelle backend

	Commit message (Collapse)	Author	Age	Files	Lines
*	Fix an issue with mkSigmasVal	Son Ho	2023-07-04	2	-106/+169
\|
*	Fix some issues with the extraction to Lean	Son Ho	2023-07-04	1	-16/+47
\|
*	Make Diverge use Primitives	Son Ho	2023-07-04	3	-69/+6
\|
*	Add an implemented_by attribute to fix	Son Ho	2023-07-04	1	-11/+18
\|
*	Cleanup a bit Diverge/Elab.lean	Son Ho	2023-07-03	1	-169/+197
\|
*	Automate the proofs of the unfolding theorems for Diverge	Son Ho	2023-07-03	2	-19/+89
\|
*	Add a missing case in the validity proofs	Son Ho	2023-07-03	1	-6/+19
\|
*	Generate the proofs of validity in Elab.lean	Son Ho	2023-07-03	3	-34/+446
\|
*	Generate the fixed-point bodies in Elab.lean	Son Ho	2023-06-30	3	-115/+391
\|
*	Write function to compute the input/output types	Son Ho	2023-06-29	3	-32/+126
\|
*	Generalize a bit FixI and add an example	Son Ho	2023-06-29	1	-109/+151
\|
*	Start working on Elab.lean	Son Ho	2023-06-29	3	-13/+203
\|
*	Reorganize backends/lean/Base	Son Ho	2023-06-28	3	-0/+1296