summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives (unfollow)
Commit message (Expand)AuthorFilesLines
2023-12-08Update the progress tactic to use discrimination treesSon Ho1-63/+63
2023-11-29Add support for more bitwise operations and update the extractionSon Ho1-2/+40
2023-11-21Update more namesSon Ho1-16/+16
2023-11-21Update the standard librariesSon Ho3-26/+25
2023-11-09Update the failing proofsSon Ho1-4/+22
2023-10-26Make progress on fixing the extractionSon Ho1-64/+64
2023-10-26Make progress on fixing the extraction for LeanSon Ho1-114/+50
2023-10-25Make the hashmap files typecheck again in LeanSon Ho3-32/+105
2023-10-25Fix some issues at extraction and add builtinsSon Ho6-21/+204
2023-10-24Handle properly the builtin, non fallible functionsSon Ho1-2/+2
2023-10-24Fix minor issuesSon Ho1-2/+2
2023-10-24Add definitions in for the Lean Primitives librarySon Ho2-0/+55
2023-10-16Improve formatting of scalars in LeanSon Ho1-0/+15
2023-10-13Add supSon Ho1-0/+9
2023-09-18Prove that Vec is inhabitedSon Ho1-0/+4
2023-09-18Simplify some lemmas and prove that the scalars and Vec are inhabitedSon Ho1-0/+3
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-09-07Fix some issuesSon Ho1-24/+24
2023-09-07Map some globals like u32::MAX to standard definitionsSon Ho1-0/+42
2023-08-04Fix issues with the extraction and extend the primitive libraries for Coq and F*Son Ho1-14/+14
2023-08-04Make minor modificationsSon Ho1-4/+4
2023-08-04Add SliceLen as a primitive function and make minor adjustmentsSon Ho1-42/+38
2023-08-04Start adding support for Arrays/Slices in the Lean librarySon Ho4-20/+425
2023-07-26Update some of the Vec function specsSon Ho1-4/+9
2023-07-25Make progress on the proofs of the hashmapSon Ho1-4/+43
2023-07-25Make progress on the proofs of the hashmapSon Ho2-13/+9
2023-07-25Make progress on the hashmap propertiesSon Ho2-24/+37
2023-07-25Improve int_tac and scalar_tacSon Ho1-13/+12
2023-07-20Add fine-grained lemmas for the arithmetic operationsSon Ho1-7/+130
2023-07-19Add arithmetic spec lemmasSon Ho1-6/+161
2023-07-18Make modifications to Vec.leanSon Ho1-3/+5
2023-07-17Start proving theorems for primitive definitionsSon Ho2-33/+57
2023-07-17Reorganize the Lean backendSon Ho3-0/+750
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 17:15:28 +0000