summaryrefslogtreecommitdiff
path: root/tests/lean/hashmap_on_disk/Base (unfollow)
Commit message (Expand)AuthorFilesLines
2023-07-04Reorganize the Lean testsSon Ho1-583/+0
2023-06-04Add Result_Inhabited to Primitives.leanSon Ho1-0/+3
2023-06-04Regenerate the translated files for LeanSon Ho1-217/+405
2023-06-04Make minor modifications and regenerate the Lean filesSon Ho1-1/+1
2023-06-04WIPJonathan Protzenko1-35/+41
2023-06-04More commentsJonathan Protzenko1-0/+8
2023-06-04Some proseJonathan Protzenko1-40/+45
2023-06-04Idiomatic naming conventionsJonathan Protzenko1-50/+50
2023-06-04WIPJonathan Protzenko1-26/+50
2023-06-04Fill out more of the primitives file, attempt at type classes for scalar_castJonathan Protzenko1-2/+26
2023-06-04Remove last sorry in PrimitivesJonathan Protzenko1-4/+2
2023-06-04Fill out Primitives.leanJonathan Protzenko1-10/+107
2023-06-04Fix some printing bits, proper syntax for terminates and decreases clausesJonathan Protzenko1-3/+30
2023-06-04WIP lots of stuffJonathan Protzenko1-5/+30
2023-06-04Fixup one primitive that is not assumed to be monadicJonathan Protzenko1-4/+4
2023-06-04More cosmetic improvementsJonathan Protzenko1-0/+1
2023-06-04Fix a couple bugs here and there, improve Lean code-gen, still WIPJonathan Protzenko1-0/+1
2023-06-04New directory structure and corresponding extraction, + misc fixes, for LeanJonathan Protzenko1-0/+176