summaryrefslogtreecommitdiff
path: root/backends/lean/Base (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'main' into option-takeSon Ho2024-04-251-0/+15
|\
| * feat(backends/lean): scalars form a linear orderRyan Lahfa2024-04-231-0/+15
| | | | | | | | | | | | | | More than c1c33de8, actually, scalars form a linear order with a decidable ≤ operation which is induced by the integer (Z) model. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* | 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>
* lean: scalars form a preorderRyan Lahfa2024-04-121-0/+10
| | | | | | | | | | Via the canonical injection, we can easily define an induced preorder on scalars and inherit all nice properties. It's useful to reason on specific scalar preorders w.r.t. Ordering, see the binary search tree verification example. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* Add more definitions to the Lean librarySon Ho2024-04-124-0/+127
|
* Reorganize the files in the Lean backend a bitSon Ho2024-04-125-241/+266
|
* Start adding integer functions to the Lean librarySon Ho2024-04-123-3/+266
|
* Fix a proofSon Ho2024-04-121-1/+0
|
* Update the core.num.checked_* definitionsSon Ho2024-04-121-31/+233
|
* Merge branch 'son/clean' into checked-opsSon Ho2024-04-1111-231/+232
|\
| * Merge remote-tracking branch 'origin/main' into son/cleanSon Ho2024-04-118-14/+17
| |\
| | * Update the lean toolchain and fix the proofsSon Ho2024-04-057-11/+3
| | |
| | * Fix the coerce notation for scalars and update some lemmasSon Ho2024-04-041-4/+15
| | |
| * | Rename Result.ret as Result.ok in the backendsSon Ho2024-04-048-217/+215
| |/
* / Add builtins for some checked ops such as checked_addZyad Hassan2024-04-031-0/+29
|/
* Fix a minor issueSon Ho2024-03-181-1/+3
|
* Regenerate the constants tests and update Primitives/Base.leanSon Ho2024-03-181-1/+1
|
* Fix an issue with the divergent encodingSon Ho2024-03-091-3/+27
|
* Fix tuple indexing for Lean backendZyad Hassan2024-03-081-1/+1
|
* Update the generation of constant bodies for LeanSon Ho2024-03-081-2/+2
|
* Update the tuples syntaxSon Ho2024-03-081-1/+3
|
* Update the tuples notationsSon Ho2024-03-083-51/+81
|
* Remove some commentsSon Ho2024-03-081-31/+0
|
* Update the handling of notations like #u32 or #isizeSon Ho2024-03-084-70/+104
|
* Update the notation for heterogeneous negationSon Ho2024-03-081-3/+12
|
* Introduce a notation for constant scalars in match patternsSon Ho2024-03-071-0/+29
|
* Add a notation for tuple field accesses in LeanSon Ho2024-03-071-0/+51
|
* Cleanup a bit Scalar.leanSon Ho2024-02-091-198/+198
|
* Fix more proofsSon Ho2024-02-023-13/+16
|
* Fix more proofsSon Ho2024-02-021-56/+55
|
* Update lean to v4.6.0-rc1 and start fixing the proofsSon Ho2024-02-026-42/+52
|
* Add some lemmas to the Lean backendSon Ho2024-01-271-4/+14
|
* Fix a minor issue with the progress tacticSon Ho2024-01-272-82/+112
|
* Improve the Lean backendSon Ho2024-01-265-10/+52
|
* Fix minor issuesSon Ho2023-12-221-0/+42
|
* Fix the models for core::mem::replaceSon Ho2023-12-221-1/+1
|
* Update the Lean standard librarySon Ho2023-12-225-81/+38
|
* Update the extraction to handle casts between integers/boolsSon Ho2023-12-131-0/+4
|
* Inline the let-bindings in the validity proofsSon Ho2023-12-121-7/+40
|
* Fix a minor issue with the divergent encodingSon Ho2023-12-121-53/+80
|
* Fix minor issues with the divergence encodingSon Ho2023-12-121-14/+5
|
* Make progress on supporting higher-order divergent functionsSon Ho2023-12-122-53/+95
|
* Implement a map-reduce visitor for expressions and fix issues with ↵Son Ho2023-12-121-31/+81
| | | | get{M,F}VarIds
* Update the validity proofs for higher-order functionsSon Ho2023-12-112-11/+96
|
* Start working on higher-order examples for DivergeSon Ho2023-12-114-218/+355
|
* Cleanup a bitSon Ho2023-12-111-16/+47
|
* Update Diverge/Elab.lean to use the more general FixII definitionsSon Ho2023-12-113-195/+387
|
* Reorganize a bitSon Ho2023-12-113-94/+49
|
* Reactivate the sanity checks for the progress tacticSon Ho2023-12-113-26/+24
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 17:07:06 +0000