summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/Base.lean (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Do some cleanup in the Lean backend (#257)Son HO2024-06-221-12/+10
|
* backends/lean: repair definition of `core.mem.replace`Ryan Lahfa2024-05-131-1/+4
| | | | | | Oops, it is supposed to do something with the second argument! Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* Merge branch 'main' into core-option-unwrapSon Ho2024-04-251-0/+4
|\
| * compiler: map `core::mem::swap` to the pure swapRyan Lahfa2024-04-241-0/+2
| | | | | | | | | | | | | | | | | | In the pure functional model, `swap` is mostly about borrow checking and should simplify to the pure swap in our backends. Other backends than Lean are not done in this commit. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
| * compiler: map `core::option::Option::take` to identity functionRyan Lahfa2024-04-171-0/+2
| | | | | | | | | | | | | | | | `take` in a pure functional model is the identity function and everything related to borrow checking is handled by the forward/backward mechanism. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* | Add core::option::unwrap builtinZyad Hassan2024-04-241-0/+5
|/
* Rename Result.ret as Result.ok in the backendsSon Ho2024-04-041-15/+15
|
* Fix a minor issueSon Ho2024-03-181-1/+3
|
* Regenerate the constants tests and update Primitives/Base.leanSon Ho2024-03-181-1/+1
|
* Update the generation of constant bodies for LeanSon Ho2024-03-081-2/+2
|
* Update the tuples notationsSon Ho2024-03-081-51/+0
|
* Add a notation for tuple field accesses in LeanSon Ho2024-03-071-0/+51
|
* Improve the Lean backendSon Ho2024-01-261-0/+7
|
* Fix the models for core::mem::replaceSon Ho2023-12-221-1/+1
|
* Update the Lean standard librarySon Ho2023-12-221-2/+1
|
* Fix some issues at extraction and add builtinsSon Ho2023-10-251-0/+7
|
* Handle properly the builtin, non fallible functionsSon Ho2023-10-241-2/+2
|
* Fix minor issuesSon Ho2023-10-241-2/+2
|
* Make progress on the proofs of the hashmapSon Ho2023-07-251-1/+1
|
* Reorganize the Lean backendSon Ho2023-07-171-0/+130