aeneas/backends/lean/Base, branch isabelle

Bump Lean to v4.9.0rc3 (#261)

2024-06-25T08:34:24Z

Do some cleanup in the Lean backend (#257)

2024-06-22T13:07:14Z

Improve `scalar_tac` and `scalar_decr_tac` (#256)

2024-06-22T11:22:32Z

* Fix an issue in a proof of the hashmap * Improve scalar_decr_tac * Improve the error message of scalar_tac and add the missing Termination.lean

Add some proofs for the Lean backend (#255)

2024-06-21T21:24:01Z

* Make progress on the proofs of the hashmap * Make a minor modification to the hashmap * Make progress on the hashmap * Make progress on the proofs * Make progress on the proofs * Make progress on the proof of the hashmap * Progress on the proofs of the hashmap * Update a proof * Update the Charon pin * Make minor modifications to the hashmap * Regenerate the tests * Regenerate the hashmap * Add lemmas to the Lean backend * Make progress on the proofs of the hashmap * Make a minor fix * Finish the proof about the hashmap * Update scalar_tac * Make a minor modification in the hashmap * Update the proofs of the hashmap --------- Co-authored-by: Son Ho Co-authored-by: Son Ho

Make a minor cleanup

2024-06-17T04:26:43Z

Merge branch 'son/update-lean' into has-int-pred

2024-06-17T04:16:43Z

Update the tests

2024-06-13T20:37:18Z

Update Lean to v4.9.0-rc1

2024-06-13T20:04:13Z

Fix more issues with the scalar notations

2024-06-13T13:07:21Z

Fix more issues

2024-06-13T09:33:13Z