Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Regenerate the tests | Son Ho | 2024-06-17 | 26 | -2/+77 |
| | |||||
* | Deactivate some linter options for the generated Lean files | Son Ho | 2024-06-17 | 1 | -0/+9 |
| | |||||
* | Update the tests | Son Ho | 2024-06-17 | 6 | -4/+31 |
| | |||||
* | Automatically add a @[reducible] attribute to some generated functions | Son Ho | 2024-06-17 | 4 | -3/+66 |
| | |||||
* | Update Hashmap/Properties.lean | Son Ho | 2024-06-17 | 1 | -36/+34 |
| | |||||
* | Update the code of the hashmap | Son Ho | 2024-06-17 | 12 | -459/+465 |
| | |||||
* | Make a minor cleanup | Son Ho | 2024-06-17 | 1 | -9/+11 |
| | |||||
* | Merge branch 'son/update-lean' into has-int-pred | Son Ho | 2024-06-17 | 24 | -321/+458 |
|\ | |||||
| * | Update the Lean dependencies | Son Ho | 2024-06-17 | 2 | -8/+8 |
| | | |||||
| * | Update the tests | Son Ho | 2024-06-14 | 2 | -4/+4 |
| | | |||||
| * | Start updating Lean to 4.9.0-rc2 | Son Ho | 2024-06-14 | 2 | -4/+4 |
| | | |||||
| * | Merge pull request #243 from AeneasVerif/son/update-lean | Son HO | 2024-06-13 | 18 | -168/+196 |
| |\ | | | | | | | Update Lean to v4.9.0-rc1 | ||||
| | * | Update the tests | Son Ho | 2024-06-13 | 4 | -34/+29 |
| | | | |||||
| | * | Update Lean to v4.9.0-rc1 | Son Ho | 2024-06-13 | 15 | -139/+172 |
| |/ | |||||
| * | Merge pull request #242 from AeneasVerif/son/scalars2 | Son HO | 2024-06-13 | 9 | -114/+150 |
| |\ | | | | | | | Update the scalar notations for the Lean backend | ||||
| | * | Fix more issues with the scalar notations | Son Ho | 2024-06-13 | 1 | -15/+29 |
| | | | |||||
| | * | Fix more issues | Son Ho | 2024-06-13 | 3 | -16/+22 |
| | | | |||||
| | * | Fix a proof | Son Ho | 2024-06-13 | 1 | -1/+1 |
| | | | |||||
| | * | Merge branch 'main' into son/scalars2 | Son HO | 2024-06-13 | 1 | -1/+1 |
| | |\ | | |/ | |/| | |||||
| * | | Merge pull request #238 from RaitoBezarius/prop-has-imp-sort | Son HO | 2024-06-13 | 1 | -1/+1 |
| |\ \ | | | | | | | | | feat: `PropHasImp` can have `Sort u` as premisses | ||||
| | * \ | Merge branch 'main' into prop-has-imp-sort | Son HO | 2024-06-12 | 5 | -45/+118 |
| | |\ \ | | |/ / | |/| | | |||||
| | * | | feat: `PropHasImp` can have `Sort u` as premisses | Ryan Lahfa | 2024-06-11 | 1 | -1/+1 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | This makes it possible to have `InBounds ... : Type 1` for example as `x`. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | ||||
| | | * | Merge branch 'main' into son/scalars2 | Son HO | 2024-06-12 | 0 | -0/+0 |
| | | |\ | | |_|/ | |/| | | |||||
| * | | | Merge pull request #241 from AeneasVerif/son/tactics | Son HO | 2024-06-12 | 5 | -45/+118 |
| |\ \ \ | | |/ / | |/| | | Do minor improvements to the Lean backend | ||||
| | | * | Add an example | Son Ho | 2024-06-12 | 1 | -0/+3 |
| | | | | |||||
| | | * | Update the code extraction and regenerate the tests | Son Ho | 2024-06-12 | 3 | -9/+15 |
| | | | | |||||
| | | * | Update the scalar notations in Lean | Son Ho | 2024-06-12 | 3 | -102/+109 |
| | |/ | |||||
| | * | Revert "Update the scalar notation for the Lean backend" | Son Ho | 2024-06-12 | 2 | -26/+26 |
| | | | | | | | | | | | | This reverts commit c8272aeea205ca9cb36e22757473ca2a931a4933. | ||||
| | * | Revert "Regenerate the tests" | Son Ho | 2024-06-12 | 12 | -333/+338 |
| | | | | | | | | | | | | This reverts commit cd5542fc82edee11181a43e3a342a2567c929e7e. | ||||
| | * | Revert "Update CoreConvertNum.lean" | Son Ho | 2024-06-12 | 1 | -22/+22 |
| | | | | | | | | | | | | This reverts commit fe59d3afe131e9f83cbdf73b1c8089ad090d92fb. | ||||
| | * | Revert "Fix some mistakes" | Son Ho | 2024-06-12 | 4 | -17/+15 |
| | | | | | | | | | | | | This reverts commit f05a0faf14fdd558039da52624d57028eb64f9fd. | ||||
| | * | Fix some mistakes | Son Ho | 2024-06-12 | 4 | -15/+17 |
| | | | |||||
| | * | Update CoreConvertNum.lean | Son Ho | 2024-06-12 | 1 | -22/+22 |
| | | | |||||
| | * | Regenerate the tests | Son Ho | 2024-06-12 | 12 | -338/+333 |
| | | | |||||
| | * | Update the scalar notation for the Lean backend | Son Ho | 2024-06-12 | 2 | -26/+26 |
| | | | |||||
| | * | Deactivate the coercion from Nat to Scalar | Son Ho | 2024-06-12 | 2 | -0/+17 |
| | | | |||||
| | * | Slightly simplify the progress tactic | Son Ho | 2024-06-12 | 1 | -8/+4 |
| | | | |||||
| | * | Add wrappers around the rewriter | Son Ho | 2024-06-12 | 1 | -0/+61 |
| | | | |||||
| | * | Add the Simp.Config to the simp wrappers | Son Ho | 2024-06-12 | 4 | -37/+36 |
| |/ | |||||
* / | backends/lean: introduce `HasIntPred` automation | Ryan Lahfa | 2024-06-12 | 2 | -8/+38 |
|/ | | | | | | | | | | | | | `HasIntPred` enable generation of facts based on specific terms in the context rather than their types, e.g. if the "length of a list" occurs in the context, generate the fact 0 ≤ length of that list, which can be further used for `scalar_tac` automation to discharge bounds goals. The aim is to use it to simplify various height related computations, e.g. whenever "height of a (left ; right) tree" is encountered, generate "height left < height of a (left ; right) tree", etc. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | ||||
* | Merge pull request #237 from AeneasVerif/son/tuples | Son HO | 2024-06-11 | 6 | -28/+96 |
|\ | | | | | Do not use tuple projectors in the Lean backend | ||||
| * | Deactivate the use of tuple projectors in the Lean backend | Son Ho | 2024-06-11 | 3 | -7/+12 |
| | | |||||
| * | Update the tests for tuples | Son Ho | 2024-06-11 | 4 | -22/+85 |
|/ | |||||
* | Merge pull request #232 from Nadrieril/type-alias | Guillaume Boisseau | 2024-06-06 | 7 | -12/+56 |
|\ | |||||
| * | Filter out type aliases | Nadrieril | 2024-06-06 | 7 | -12/+56 |
|/ | |||||
* | Merge pull request #233 from AeneasVerif/son/borrow-check | Son HO | 2024-06-06 | 45 | -759/+1500 |
|\ | | | | | Add a `-borrow-check` option | ||||
| * | Regenerate the Coq and Lean betrees | Son Ho | 2024-06-05 | 2 | -178/+423 |
| | | |||||
| * | Fix a minor issue | Son Ho | 2024-06-05 | 1 | -0/+1 |
| | | |||||
| * | Update the F* betree | Son Ho | 2024-06-05 | 3 | -144/+280 |
| | | |||||
| * | Fix a minor issue | Son Ho | 2024-06-05 | 1 | -0/+1 |
| | |