summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* compiler: map `core::option::Option::take` to identity functionRyan Lahfa2024-04-172-0/+6
| | | | | | | | `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>
* Merge pull request #126 from RaitoBezarius/scalar-preordersSon HO2024-04-151-0/+10
|\ | | | | lean: scalars form a preorder
| * 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>
* | Merge pull request #127 from AeneasVerif/fix-ciSon HO2024-04-152-2/+5
|\ \ | |/ |/| Fix CI
| * Fix CINadrieril2024-04-152-2/+5
|/
* Merge pull request #124 from AeneasVerif/son/lean1Son HO2024-04-1211-60/+674
|\ | | | | Add more definitions to the Lean library
| * Add more definitions to the Lean librarySon Ho2024-04-125-0/+200
| |
| * Reorganize the files in the Lean backend a bitSon Ho2024-04-125-241/+266
| |
| * Start adding integer functions to the Lean librarySon Ho2024-04-127-58/+447
|/
* Merge pull request #110 from zhassan-aws/checked-opsSon HO2024-04-122-21/+279
|\ | | | | Add builtins for some checked ops for the Lean backend
| * Update the bindings for the extractionSon Ho2024-04-121-14/+11
| |
| * Merge branch 'main' into checked-opsSon Ho2024-04-120-0/+0
| |\ | |/ |/|
* | Merge pull request #123 from AeneasVerif/son/cleanSon HO2024-04-1180-1997/+1989
|\ \ | | | | | | Cleanup the code in preparation of the nested loops
| | * 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-11117-2327/+2546
| | |\ | | |/ | |/|
| * | Update a Lean fileSon Ho2024-04-111-1/+1
| | |
| * | Update some Lean proofsSon Ho2024-04-113-24/+24
| | |
| * | Update a commentSon Ho2024-04-111-2/+2
| | |
| * | Fix a Coq fileSon Ho2024-04-111-1/+1
| | |
| * | Fix some F* proofsSon Ho2024-04-111-4/+4
| | |
| * | Merge remote-tracking branch 'origin/main' into son/cleanSon Ho2024-04-1140-130/+310
| |\ \ | |/ / |/| |
* | | Merge pull request #121 from AeneasVerif/son/formatSon HO2024-04-111-9/+6
|\ \ \ | | | | | | | | Reformat the code
| * | | Reformat the codeSon Ho2024-04-111-9/+6
|/ / /
* | | Merge pull request #119 from AeneasVerif/generic-copyGuillaume Boisseau2024-04-114-11/+11
|\ \ \
| * | | Use charon mainNadrieril2024-04-112-5/+4
| | | |
| * | | Update a commentSon HO2024-04-111-1/+1
| | | |
| * | | Trust rustc regarding `Copy` boundsNadrieril2024-04-105-11/+12
|/ / /
* | | Merge pull request #115 from AeneasVerif/nixSon HO2024-04-101-0/+7
|\ \ \ | | | | | | | | Update flake.nix
| * | | Update flake.nixNadrieril2024-04-081-0/+7
|/ / / | | | | | | | | | | | | It was missing some dependencies, and while we're at it we can disable sanity checks in tests.
* | | Merge pull request #113 from AeneasVerif/escherichia/error_catching_translateSon HO2024-04-0715-66/+186
|\ \ \ | | | | | | | | Error catching should tell when code couldn't be generated
| * | | Improve the error messages furtherSon Ho2024-04-073-1/+44
| | | |
| * | | Cleanup a bit and improve the error messagesSon Ho2024-04-0712-82/+91
| | | |
| * | | Resolved comments and added the name of the not translated elementEscherichia2024-04-052-7/+18
| | | |
| * | | resolved commentsEscherichia2024-04-053-99/+113
| | | |
| * | | error catching should now be able to tell when code couldn't be generatedEscherichia2024-04-053-101/+144
| | | |
* | | | Merge pull request #114 from AeneasVerif/son/lean-versionSon HO2024-04-0512-36/+36
|\ \ \ \ | |/ / / |/| | | Bump the version of Lean to 4.7.0
| * | | Update the lean toolchain and fix the proofsSon Ho2024-04-0512-36/+36
| | | |
* | | | Merge pull request #106 from AeneasVerif/escherichia/error_catchingSon HO2024-04-0413-9/+54
|\ \ \ \ | | | | | | | | | | Added Error and EError to expressions and propagated related changes
| * | | | Fix a minor issueSon Ho2024-04-041-1/+1
| | | | |
| * | | | Merge remote-tracking branch 'origin/main' into escherichia/error_catchingSon Ho2024-04-0445-396/+446
| |\ \ \ \
| * | | | | Update the way errors are reportedSon Ho2024-04-042-10/+7
| | | | | |
| * | | | | Update the nix flakeSon Ho2024-04-041-3/+3
| | | | | |
| * | | | | Now prints all errors in the error_listEscherichia2024-04-042-3/+11
| | | | | |
| * | | | | Merge remote-tracking branch 'origin/main' into escherichia/error_catchingEscherichia2024-04-043-5/+2
| |\ \ \ \ \
| * | | | | | resolved requested changesEscherichia2024-04-031-1/+0
| | | | | | |
| * | | | | | resolved requested changesEscherichia2024-04-033-6/+4
| | | | | | |
| * | | | | | added extract_ty_errors and extract_texpression_errors to deal with the ↵Escherichia2024-04-032-3/+10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | error case in their respective types
| * | | | | | added Error and EError to expressions and propagated related changesEscherichia2024-04-0312-5/+41
| | | | | | |
* | | | | | | Merge pull request #112 from AeneasVerif/son/coerceSon HO2024-04-041-4/+15
|\ \ \ \ \ \ \ | |_|_|/ / / / |/| | | / / / | | |_|/ / / | |/| | | | Fix the coerce notation for scalars and update some lemmas
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 13:04:48 +0000