summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Utils.lean (follow)
Commit message (Collapse)AuthorAgeFilesLines
* 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-12-27 11:20:29 +0000