summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/Scalar.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-22Do some cleanup in the Lean backend (#257)Son HO1-1/+8
2024-06-21Add some proofs for the Lean backend (#255)Son HO1-5/+6
2024-06-13Update Lean to v4.9.0-rc1Son Ho1-12/+12
2024-06-12Update the scalar notations in LeanSon Ho1-102/+21
2024-06-12Revert "Update the scalar notation for the Lean backend"Son Ho1-25/+25
2024-06-12Update the scalar notation for the Lean backendSon Ho1-25/+25
2024-06-12Deactivate the coercion from Nat to ScalarSon Ho1-0/+7
2024-05-24feat: add small pieces of max theoryRyan Lahfa1-0/+39
2024-05-21feat(backends/lean): make `max`-related coercions nicerRyan Lahfa1-0/+12
2024-04-30feat(backend/lean): Raw Lean literals can be parsed into scalars automaticallyRyan Lahfa1-0/+5
2024-04-24Add core::option::unwrap builtinZyad Hassan1-5/+0
2024-04-23feat(backends/lean): scalars form a linear orderRyan Lahfa1-0/+15
2024-04-12lean: scalars form a preorderRyan Lahfa1-0/+10
2024-04-12Add more definitions to the Lean librarySon Ho1-0/+63
2024-04-12Reorganize the files in the Lean backend a bitSon Ho1-239/+0
2024-04-12Start adding integer functions to the Lean librarySon Ho1-0/+255
2024-04-12Fix a proofSon Ho1-1/+0
2024-04-12Update the core.num.checked_* definitionsSon Ho1-31/+233
2024-04-04Rename Result.ret as Result.ok in the backendsSon Ho1-73/+71
2024-04-04Fix the coerce notation for scalars and update some lemmasSon Ho1-4/+15
2024-04-03Add builtins for some checked ops such as checked_addZyad Hassan1-0/+29
2024-03-08Remove some commentsSon Ho1-31/+0
2024-03-08Update the handling of notations like #u32 or #isizeSon Ho1-67/+101
2024-03-08Update the notation for heterogeneous negationSon Ho1-3/+12
2024-03-07Introduce a notation for constant scalars in match patternsSon Ho1-0/+29
2024-02-09Cleanup a bit Scalar.leanSon Ho1-198/+198
2024-02-02Fix more proofsSon Ho1-56/+55
2024-01-27Add some lemmas to the Lean backendSon Ho1-4/+14
2024-01-26Improve the Lean backendSon Ho1-0/+11
2023-12-13Update the extraction to handle casts between integers/boolsSon Ho1-0/+4
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-10-16Improve formatting of scalars in LeanSon Ho1-0/+15
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 07:25:51 +0000