summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/Base.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2024-05-13backends/lean: repair definition of `core.mem.replace`Ryan Lahfa1-1/+4
2024-04-24Add core::option::unwrap builtinZyad Hassan1-0/+5
2024-04-24compiler: map `core::mem::swap` to the pure swapRyan Lahfa1-0/+2
2024-04-17compiler: map `core::option::Option::take` to identity functionRyan Lahfa1-0/+2
2024-04-04Rename Result.ret as Result.ok in the backendsSon Ho1-15/+15
2024-03-18Fix a minor issueSon Ho1-1/+3
2024-03-18Regenerate the constants tests and update Primitives/Base.leanSon Ho1-1/+1
2024-03-08Update the generation of constant bodies for LeanSon Ho1-2/+2
2024-03-08Update the tuples notationsSon Ho1-51/+0
2024-03-07Add a notation for tuple field accesses in LeanSon Ho1-0/+51
2024-01-26Improve the Lean backendSon Ho1-0/+7
2023-12-22Fix the models for core::mem::replaceSon Ho1-1/+1
2023-12-22Update the Lean standard librarySon Ho1-2/+1
2023-10-25Fix some issues at extraction and add builtinsSon Ho1-0/+7
2023-10-24Handle properly the builtin, non fallible functionsSon Ho1-2/+2
2023-10-24Fix minor issuesSon Ho1-2/+2
2023-07-25Make progress on the proofs of the hashmapSon Ho1-1/+1
2023-07-17Reorganize the Lean backendSon Ho1-0/+130
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 17:59:51 +0000