aeneas/backends/lean/Base/Diverge, branch isabelle aeneas rust verifier with a hacky Isabelle backend https://stuebinm.eu/git/aeneas/atom/backends/lean/Base/Diverge?h=isabelle 2024-06-13T20:04:13Z Update Lean to v4.9.0-rc1 2024-06-13T20:04:13Z Son Ho 2024-06-13T20:04:13Z urn:sha1:b3dd78ff4c8785b6ff9bce9927df90f8c78a9109 Merge remote-tracking branch 'origin/main' into son/clean 2024-04-11T17:40:08Z Son Ho 2024-04-11T17:40:08Z urn:sha1:86c3680b1f3f50b4c4e6198eebc145cadfff3876 Update the lean toolchain and fix the proofs 2024-04-05T12:04:25Z Son Ho 2024-04-05T12:04:25Z urn:sha1:65a77968d0abc2d01da92aa8982256855e7519a6 Rename Result.ret as Result.ok in the backends 2024-04-04T14:08:32Z Son Ho 2024-04-04T14:08:32Z urn:sha1:4828b77847ee981f5c6a1bbad7f8e6ed0e58eb0f Fix an issue with the divergent encoding 2024-03-08T23:40:21Z Son Ho 2024-03-08T23:40:21Z urn:sha1:814f94b9e60818aac8060715e82edeffa6d5233f Update lean to v4.6.0-rc1 and start fixing the proofs 2024-02-02T19:48:26Z Son Ho 2024-02-02T19:48:26Z urn:sha1:a68c231db4edf97c4f007724969aec7dd60941a1 Inline the let-bindings in the validity proofs 2023-12-12T18:48:50Z Son Ho 2023-12-12T18:48:50Z urn:sha1:c14e3e5ffa261e4ed6e5539b06c182b371939ccf Fix a minor issue with the divergent encoding 2023-12-12T16:59:12Z Son Ho 2023-12-12T16:59:12Z urn:sha1:91f5cd49660b5f012a2faeaf00c49455c548734a Fix minor issues with the divergence encoding 2023-12-12T16:47:58Z Son Ho 2023-12-12T16:47:58Z urn:sha1:698f631e7addb92eb270a75607f1f6ffd8b2414f Make progress on supporting higher-order divergent functions 2023-12-12T16:28:34Z Son Ho 2023-12-12T16:28:34Z urn:sha1:dba35a41e66019e586502f563ce7c629356fb2d7