aeneas - aeneas rust verifier with a hacky Isabelle backend

	Commit message (Collapse)	Author	Age	Files	Lines
*	Update Primitives.lean	Son Ho	2023-06-04	1	-90/+58
\|
*	Update Primitives.lean	Son Ho	2023-06-04	1	-194/+390
\|
*	Add backends/lean/lakefile.lean	Son Ho	2023-06-04	3	-0/+39
\|
*	Make minor modifications and regenerate the Lean files	Son Ho	2023-06-04	1	-1/+1
\|
*	WIP	Jonathan Protzenko	2023-06-04	1	-35/+41
\|
*	More comments	Jonathan Protzenko	2023-06-04	1	-40/+53
\|
*	Idiomatic naming conventions	Jonathan Protzenko	2023-06-04	1	-46/+46
\|
*	Rename primitives.lean to Primitives.lean	Son Ho	2023-06-04	1	-0/+0
\|
*	WIP	Jonathan Protzenko	2023-06-04	1	-26/+50
\|
*	Fill out more of the primitives file, attempt at type classes for scalar_cast	Jonathan Protzenko	2023-06-04	1	-2/+26
\|
*	Remove last sorry in Primitives	Jonathan Protzenko	2023-06-04	1	-10/+105
\|
*	Fix some printing bits, proper syntax for terminates and decreases clauses	Jonathan Protzenko	2023-06-04	1	-3/+30
\|
*	WIP lots of stuff	Jonathan Protzenko	2023-06-04	1	-5/+30
\|
*	Fixup one primitive that is not assumed to be monadic	Jonathan Protzenko	2023-06-04	1	-4/+4
\|
*	More cosmetic improvements	Jonathan Protzenko	2023-06-04	1	-0/+1
\|
*	Fix a couple bugs here and there, improve Lean code-gen, still WIP	Jonathan Protzenko	2023-06-04	1	-0/+1
\|
*	New directory structure and corresponding extraction, + misc fixes, for Lean	Jonathan Protzenko	2023-06-04	1	-7/+9
\|
*	Write a tactic to discharge integer literal proof obligations	Jonathan Protzenko	2023-06-04	1	-4/+23
\|
*	Initial Lean backend, WIP	Jonathan Protzenko	2023-06-04	1	-0/+155