summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith/Int.lean (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Update Lean to v4.9.0-rc1Son Ho2024-06-131-4/+4
|
* Merge branch 'main' into prop-has-imp-sortSon HO2024-06-121-3/+3
|\
| * Add the Simp.Config to the simp wrappersSon Ho2024-06-121-3/+3
| |
* | feat: `PropHasImp` can have `Sort u` as premissesRyan Lahfa2024-06-111-1/+1
|/ | | | | | | This makes it possible to have `InBounds ... : Type 1` for example as `x`. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* Update scalar_tac to use omega instead of linarithSon Ho2024-05-241-97/+65
|
* Update the lean toolchain and fix the proofsSon Ho2024-04-051-1/+0
|
* Refold the scalar types when applying progressSon Ho2023-10-171-2/+2
|
* Implement tactics for termination proofs which involve arithmeticSon Ho2023-10-171-0/+11
|
* Improve scalar_tacSon Ho2023-09-181-3/+5
|
* Update to Lean 4.0.0 and fix some broken proofsSon Ho2023-09-141-1/+1
|
* Start adding support for Arrays/Slices in the Lean librarySon Ho2023-08-041-10/+21
|
* Update the syntax of the progress tacticSon Ho2023-07-261-1/+1
|
* Make progress on the proofs of the hashmapSon Ho2023-07-251-0/+1
|
* Make progress on the hashmap propertiesSon Ho2023-07-251-0/+2
|
* Improve int_tac and scalar_tacSon Ho2023-07-251-7/+56
|
* Make some proofs in Hashmap/Properties.lean and improve progressSon Ho2023-07-201-1/+1
|
* Improve progressSon Ho2023-07-191-8/+0
|
* Reorganize the Lean backendSon Ho2023-07-171-0/+236
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-21 08:37:42 +0000