summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Utils.lean (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Update lean to v4.6.0-rc1 and start fixing the proofsSon Ho2024-02-021-4/+2
|
* 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-111-3/+3
|
* Reactivate the sanity checks for the progress tacticSon Ho2023-12-111-0/+6
|
* Refold the scalar types when applying progressSon Ho2023-10-171-12/+63
|
* Fix the hashmap proofs in LeanSon Ho2023-09-141-1/+1
|
* Update to Lean 4.0.0 and fix some broken proofsSon Ho2023-09-141-0/+4
|
* Update the syntax of the progress tacticSon Ho2023-07-261-4/+8
|
* Make progress on the proofs of the hashmapSon Ho2023-07-251-11/+25
|
* Add the possibility of using "_" as ident for progressSon Ho2023-07-251-2/+5
|
* Improve the syntax of progress: `as ⟨ x, y .. ⟩`Son Ho2023-07-251-13/+48
|
* Make progress on some of the hashmap proofsSon Ho2023-07-201-8/+22
|
* Make some proofs in Hashmap/Properties.lean and improve progressSon Ho2023-07-201-8/+24
|
* Cleanup moreSon Ho2023-07-191-3/+0
|
* Improve progressSon Ho2023-07-191-0/+19
|
* Improve progressSon Ho2023-07-181-0/+4
|
* Finish implementing the syntax for `progress`Son Ho2023-07-131-10/+37
|
* Improve progress to use assumptions and start working on a nice syntaxSon Ho2023-07-121-0/+62
|
* Finish a first version of the progress tacticSon Ho2023-07-121-22/+225
|
* Work on the progress tacticSon Ho2023-07-111-0/+28
|
* Start working on the progress tacticSon Ho2023-07-101-0/+95
|
* Reorganize a bit the lean backend filesSon Ho2023-07-061-0/+119
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 11:28:29 +0000