summaryrefslogtreecommitdiff
path: root/tests/lean/hashmap_on_disk/Base (follow)
Commit message (Expand)AuthorAgeFilesLines
* WIPJonathan Protzenko2023-06-041-26/+50
* Fill out more of the primitives file, attempt at type classes for scalar_castJonathan Protzenko2023-06-041-2/+26
* Remove last sorry in PrimitivesJonathan Protzenko2023-06-041-4/+2
* Fill out Primitives.leanJonathan Protzenko2023-06-041-10/+107
* Fix some printing bits, proper syntax for terminates and decreases clausesJonathan Protzenko2023-06-041-3/+30
* WIP lots of stuffJonathan Protzenko2023-06-041-5/+30
* Fixup one primitive that is not assumed to be monadicJonathan Protzenko2023-06-041-4/+4
* More cosmetic improvementsJonathan Protzenko2023-06-041-0/+1
* Fix a couple bugs here and there, improve Lean code-gen, still WIPJonathan Protzenko2023-06-041-0/+1
* New directory structure and corresponding extraction, + misc fixes, for LeanJonathan Protzenko2023-06-041-0/+176