summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives (unfollow)
Commit message (Expand)AuthorFilesLines
2024-04-24compiler: map `core::mem::swap` to the pure swapRyan Lahfa1-0/+2
2024-04-23feat(backends/lean): scalars form a linear orderRyan Lahfa1-0/+15
2024-04-17compiler: map `core::option::Option::take` to identity functionRyan Lahfa1-0/+2
2024-04-12lean: scalars form a preorderRyan Lahfa1-0/+10
2024-04-12Add more definitions to the Lean librarySon Ho4-0/+127
2024-04-12Reorganize the files in the Lean backend a bitSon Ho4-241/+265
2024-04-12Start adding integer functions to the Lean librarySon Ho2-2/+265
2024-04-12Fix a proofSon Ho1-1/+0
2024-04-12Update the core.num.checked_* definitionsSon Ho1-31/+233
2024-04-05Update the lean toolchain and fix the proofsSon Ho3-5/+2
2024-04-04Rename Result.ret as Result.ok in the backendsSon Ho5-130/+128
2024-04-04Fix the coerce notation for scalars and update some lemmasSon Ho1-4/+15
2024-04-03Add builtins for some checked ops such as checked_addZyad Hassan1-0/+29
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-08Remove some commentsSon Ho1-31/+0
2024-03-08Update the handling of notations like #u32 or #isizeSon Ho3-69/+103
2024-03-08Update the notation for heterogeneous negationSon Ho1-3/+12
2024-03-07Introduce a notation for constant scalars in match patternsSon Ho1-0/+29
2024-03-07Add a notation for tuple field accesses in LeanSon Ho1-0/+51
2024-02-09Cleanup a bit Scalar.leanSon Ho1-198/+198
2024-02-02Fix more proofsSon Ho2-2/+2
2024-02-02Fix more proofsSon Ho1-56/+55
2024-01-27Add some lemmas to the Lean backendSon Ho1-4/+14
2024-01-26Improve the Lean backendSon Ho2-0/+18
2023-12-22Fix minor issuesSon Ho1-0/+42
2023-12-22Fix the models for core::mem::replaceSon Ho1-1/+1
2023-12-22Update the Lean standard librarySon Ho5-81/+38
2023-12-13Update the extraction to handle casts between integers/boolsSon Ho1-0/+4
2023-12-08Update the progress tactic to use discrimination treesSon Ho1-63/+63
2023-11-29Add support for more bitwise operations and update the extractionSon Ho1-2/+40
2023-11-21Update more namesSon Ho1-16/+16
2023-11-21Update the standard librariesSon Ho3-26/+25
2023-11-09Update the failing proofsSon Ho1-4/+22
2023-10-26Make progress on fixing the extractionSon Ho1-64/+64
2023-10-26Make progress on fixing the extraction for LeanSon Ho1-114/+50
2023-10-25Make the hashmap files typecheck again in LeanSon Ho3-32/+105
2023-10-25Fix some issues at extraction and add builtinsSon Ho6-21/+204
2023-10-24Handle properly the builtin, non fallible functionsSon Ho1-2/+2
2023-10-24Fix minor issuesSon Ho1-2/+2
2023-10-24Add definitions in for the Lean Primitives librarySon Ho2-0/+55
2023-10-16Improve formatting of scalars in LeanSon Ho1-0/+15
2023-10-13Add supSon Ho1-0/+9
2023-09-18Prove that Vec is inhabitedSon Ho1-0/+4
2023-09-18Simplify some lemmas and prove that the scalars and Vec are inhabitedSon Ho1-0/+3
2023-09-18Add notations for the Isize.ofInt, etc.Son Ho1-0/+16
2023-09-18Add arithmetic lemmas in Scalar.leanSon Ho1-12/+179
2023-09-18Improve scalar_tacSon Ho1-51/+16
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 22:29:29 +0000