summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives.lean (follow)
Commit message (Expand)AuthorAgeFilesLines
* Reorganize the files in the Lean backend a bitSon Ho2024-04-121-0/+1
* Start adding integer functions to the Lean librarySon Ho2024-04-121-1/+1
* Update the tuples notationsSon Ho2024-03-081-0/+1
* Fix some issues at extraction and add builtinsSon Ho2023-10-251-2/+2
* Add definitions in for the Lean Primitives librarySon Ho2023-10-241-0/+2
* Start adding support for Arrays/Slices in the Lean librarySon Ho2023-08-041-0/+1
* Reorganize the Lean backendSon Ho2023-07-171-715/+3
* Move a definitionSon Ho2023-07-171-0/+3
* Make the `by inlit` implicitSon Ho2023-07-121-8/+7
* Improve the handling of arithmetic boundsSon Ho2023-07-121-111/+117
* Finish a first version of the progress tacticSon Ho2023-07-121-24/+65
* Improve the generated commentsSon Ho2023-07-061-1/+1
* Simplify the names used in Primitives.leanSon Ho2023-07-051-16/+21
* Make Diverge use PrimitivesSon Ho2023-07-041-21/+4
* Cleanup Diverge.leanSon Ho2023-06-191-0/+13
* Make minor modificationsSon Ho2023-06-181-3/+2
* Make minor modificationsSon Ho2023-06-141-0/+1
* Start working on extrinsic proofs of terminationSon Ho2023-06-091-7/+22
* Reorganize a bit the Lean librarySon Ho2023-06-091-0/+650