aeneas - aeneas rust verifier with a hacky Isabelle backend

	Commit message (Collapse)	Author	Age	Files	Lines
*	Update lean to v4.6.0-rc1 and start fixing the proofs	Son Ho	2024-02-02	1	-6/+10
\|
*	Start working on higher-order examples for Diverge	Son Ho	2023-12-11	1	-1/+62
\|
*	Update Diverge/Elab.lean to use the more general FixII definitions	Son Ho	2023-12-11	1	-0/+2
\|
*	Start working on a version of Diverge.FixI more suited to higher-order functions	Son Ho	2023-12-07	1	-0/+6
\|
*	Make progress on the int tactic	Son Ho	2023-07-09	1	-112/+0
\|
*	Fix an issue with mkSigmasVal	Son Ho	2023-07-04	1	-21/+26
\|
*	Make Diverge use Primitives	Son Ho	2023-07-04	1	-4/+4
\|
*	Automate the proofs of the unfolding theorems for Diverge	Son Ho	2023-07-03	1	-0/+1
\|
*	Generate the proofs of validity in Elab.lean	Son Ho	2023-07-03	1	-0/+1
\|
*	Generate the fixed-point bodies in Elab.lean	Son Ho	2023-06-30	1	-4/+43
\|
*	Write function to compute the input/output types	Son Ho	2023-06-29	1	-0/+1
\|
*	Start working on Elab.lean	Son Ho	2023-06-29	1	-2/+73
\|
*	Reorganize backends/lean/Base	Son Ho	2023-06-28	1	-0/+9