aeneas/backends/lean/Base/Diverge, branch isabelleaeneas rust verifier with a hacky Isabelle backend
Update Lean to v4.9.0-rc12024-06-13T20:04:13+00:00Son Ho2024-06-13T20:04:13+00:00b3dd78ff4c8785b6ff9bce9927df90f8c78a9109
Merge remote-tracking branch 'origin/main' into son/clean2024-04-11T17:40:08+00:00Son Ho2024-04-11T17:40:08+00:0086c3680b1f3f50b4c4e6198eebc145cadfff3876
Update the lean toolchain and fix the proofs2024-04-05T12:04:25+00:00Son Ho2024-04-05T12:04:25+00:0065a77968d0abc2d01da92aa8982256855e7519a6
Rename Result.ret as Result.ok in the backends2024-04-04T14:08:32+00:00Son Ho2024-04-04T14:08:32+00:004828b77847ee981f5c6a1bbad7f8e6ed0e58eb0f
Fix an issue with the divergent encoding2024-03-08T23:40:21+00:00Son Ho2024-03-08T23:40:21+00:00814f94b9e60818aac8060715e82edeffa6d5233f
Update lean to v4.6.0-rc1 and start fixing the proofs2024-02-02T19:48:26+00:00Son Ho2024-02-02T19:48:26+00:00a68c231db4edf97c4f007724969aec7dd60941a1
Inline the let-bindings in the validity proofs2023-12-12T18:48:50+00:00Son Ho2023-12-12T18:48:50+00:00c14e3e5ffa261e4ed6e5539b06c182b371939ccf
Fix a minor issue with the divergent encoding2023-12-12T16:59:12+00:00Son Ho2023-12-12T16:59:12+00:0091f5cd49660b5f012a2faeaf00c49455c548734a
Fix minor issues with the divergence encoding2023-12-12T16:47:58+00:00Son Ho2023-12-12T16:47:58+00:00698f631e7addb92eb270a75607f1f6ffd8b2414f
Make progress on supporting higher-order divergent functions2023-12-12T16:28:34+00:00Son Ho2023-12-12T16:28:34+00:00dba35a41e66019e586502f563ce7c629356fb2d7