summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/Scalar.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2023-09-18Add notations for the Isize.ofInt, etc.Son Ho1-0/+16
2023-09-18Add arithmetic lemmas in Scalar.leanSon Ho1-12/+179
2023-09-18Improve scalar_tacSon Ho1-51/+16
2023-08-04Start adding support for Arrays/Slices in the Lean librarySon Ho1-9/+2
2023-07-25Make progress on the proofs of the hashmapSon Ho1-4/+43
2023-07-25Make progress on the hashmap propertiesSon Ho1-21/+27
2023-07-20Add fine-grained lemmas for the arithmetic operationsSon Ho1-7/+130
2023-07-19Add arithmetic spec lemmasSon Ho1-6/+161
2023-07-17Start proving theorems for primitive definitionsSon Ho1-0/+1
2023-07-17Reorganize the Lean backendSon Ho1-218/+10
2023-07-17Move a definitionSon Ho1-0/+3
2023-07-12Make the `by inlit` implicitSon Ho1-8/+7
2023-07-12Improve the handling of arithmetic boundsSon Ho1-111/+117
2023-07-12Finish a first version of the progress tacticSon Ho1-24/+65
2023-07-06Improve the generated commentsSon Ho1-1/+1
2023-07-05Simplify the names used in Primitives.leanSon Ho1-16/+21
2023-07-04Make Diverge use PrimitivesSon Ho1-21/+4
2023-06-19Cleanup Diverge.leanSon Ho1-0/+13
2023-06-18Make minor modificationsSon Ho1-3/+2
2023-06-14Make minor modificationsSon Ho1-0/+1
2023-06-09Start working on extrinsic proofs of terminationSon Ho1-7/+22
2023-06-09Reorganize a bit the Lean librarySon Ho1-17/+30
2023-06-06Remove the sorries from Primitives.leanSon Ho1-65/+119
2023-06-04Add Result_Inhabited to Primitives.leanSon Ho1-0/+3
2023-06-04Make more updates for the Lean backendSon Ho1-33/+57
2023-06-04Update Primitives.leanSon Ho1-90/+58
2023-06-04Update Primitives.leanSon Ho1-194/+390
2023-06-04Make minor modifications and regenerate the Lean filesSon Ho1-1/+1
2023-06-04WIPJonathan Protzenko1-35/+41
2023-06-04More commentsJonathan Protzenko1-40/+53
2023-06-04Idiomatic naming conventionsJonathan Protzenko1-46/+46
2023-06-04Rename primitives.lean to Primitives.leanSon Ho1-0/+0
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-10/+105
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-7/+9
2023-06-04Write a tactic to discharge integer literal proof obligationsJonathan Protzenko1-4/+23
2023-06-04Initial Lean backend, WIPJonathan Protzenko1-0/+155
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 06:40:14 +0000