summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/ArraySlice.lean (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Do some cleanup in the Lean backend (#257)Son HO2024-06-221-0/+8
|
* Add some proofs for the Lean backend (#255)Son HO2024-06-211-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * 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 <sonho@Sons-MacBook-Pro.local> Co-authored-by: Son Ho <sonho@Sons-MBP.lan>
* Update Lean to v4.9.0-rc1Son Ho2024-06-131-2/+1
|
* Fix a proofSon Ho2024-06-131-1/+1
|
* Reorganize the files in the Lean backend a bitSon Ho2024-04-121-1/+1
|
* Merge remote-tracking branch 'origin/main' into son/cleanSon Ho2024-04-111-3/+2
|\
| * Update the lean toolchain and fix the proofsSon Ho2024-04-051-3/+2
| |
* | Rename Result.ret as Result.ok in the backendsSon Ho2024-04-041-27/+27
|/
* Update the handling of notations like #u32 or #isizeSon Ho2024-03-081-1/+1
|
* Fix more proofsSon Ho2024-02-021-1/+1
|
* Fix minor issuesSon Ho2023-12-221-0/+42
|
* Update the Lean standard librarySon Ho2023-12-221-57/+11
|
* Update more namesSon Ho2023-11-211-16/+16
|
* Update the standard librariesSon Ho2023-11-211-20/+19
|
* Make progress on fixing the extractionSon Ho2023-10-261-64/+64
|
* Make progress on fixing the extraction for LeanSon Ho2023-10-261-114/+50
|
* Make the hashmap files typecheck again in LeanSon Ho2023-10-251-2/+59
|
* Fix some issues at extraction and add builtinsSon Ho2023-10-251-0/+560