summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Utils.lean (follow)
Commit message (Expand)AuthorAgeFilesLines
* Update scalar_tac to use omega instead of linarithSon Ho2024-05-241-6/+16
* 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 get{M,F}Va...Son Ho2023-12-121-31/+81
* 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-12-27 07:05:35 +0000