summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives.lean (follow)
Commit message (Collapse)AuthorAgeFilesLines
* 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 17:25:43 +0000