summaryrefslogtreecommitdiff
path: root/backends/lean (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-22Improve `scalar_tac` and `scalar_decr_tac` (#256)Son HO7-50/+155
2024-06-21Add some proofs for the Lean backend (#255)Son HO9-40/+125
2024-06-17Make a minor cleanupSon Ho1-9/+11
2024-06-17Update the Lean dependenciesSon Ho1-4/+4
2024-06-14Start updating Lean to 4.9.0-rc2Son Ho2-4/+4
2024-06-13Update the testsSon Ho1-5/+0
2024-06-13Update Lean to v4.9.0-rc1Son Ho15-139/+172
2024-06-13Fix more issues with the scalar notationsSon Ho1-15/+29
2024-06-13Fix more issuesSon Ho3-16/+22
2024-06-13Fix a proofSon Ho1-1/+1
2024-06-12Add an exampleSon Ho1-0/+3
2024-06-12Update the scalar notations in LeanSon Ho3-102/+109
2024-06-12Revert "Update the scalar notation for the Lean backend"Son Ho1-25/+25
2024-06-12Revert "Update CoreConvertNum.lean"Son Ho1-22/+22
2024-06-12Update CoreConvertNum.leanSon Ho1-22/+22
2024-06-12Update the scalar notation for the Lean backendSon Ho1-25/+25
2024-06-12Deactivate the coercion from Nat to ScalarSon Ho2-0/+17
2024-06-12Slightly simplify the progress tacticSon Ho1-8/+4
2024-06-12Add wrappers around the rewriterSon Ho1-0/+61
2024-06-12Add the Simp.Config to the simp wrappersSon Ho4-37/+36
2024-06-12backends/lean: introduce `HasIntPred` automationRyan Lahfa2-8/+38
2024-06-11feat: `PropHasImp` can have `Sort u` as premissesRyan Lahfa1-1/+1
2024-05-24feat: add small pieces of max theoryRyan Lahfa1-0/+39
2024-05-24Update scalar_tac to use omega instead of linarithSon Ho4-104/+82
2024-05-21Fix an issue in the progress tacticSon Ho1-0/+13
2024-05-21feat(backends/lean): make `max`-related coercions nicerRyan Lahfa1-0/+12
2024-05-13backends/lean: repair definition of `core.mem.replace`Ryan Lahfa1-1/+4
2024-04-30feat(backend/lean): Raw Lean literals can be parsed into scalars automaticallyRyan Lahfa1-0/+5
2024-04-25Update the backend and ExtractBuiltin.mlSon Ho1-1/+1
2024-04-24Add core::option::unwrap builtinZyad Hassan3-5/+13
2024-04-24compiler: map `core::mem::swap` to the pure swapRyan Lahfa1-0/+2
2024-04-23feat(backends/lean): scalars form a linear orderRyan Lahfa1-0/+15
2024-04-17compiler: map `core::option::Option::take` to identity functionRyan Lahfa1-0/+2
2024-04-12lean: scalars form a preorderRyan Lahfa1-0/+10
2024-04-12Add more definitions to the Lean librarySon Ho4-0/+127
2024-04-12Reorganize the files in the Lean backend a bitSon Ho5-241/+266
2024-04-12Start adding integer functions to the Lean librarySon Ho3-3/+266
2024-04-12Fix a proofSon Ho1-1/+0
2024-04-12Update the core.num.checked_* definitionsSon Ho1-31/+233
2024-04-05Update the lean toolchain and fix the proofsSon Ho9-20/+12
2024-04-04Rename Result.ret as Result.ok in the backendsSon Ho8-217/+215
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-25backend(/tests)/lean: 4.6.0-rc1 → 4.6.1Ryan Lahfa1-1/+1
2024-03-18Fix a minor issueSon Ho1-1/+3
2024-03-18Regenerate the constants tests and update Primitives/Base.leanSon Ho1-1/+1
2024-03-09Fix an issue with the divergent encodingSon Ho1-3/+27
2024-03-08Fix tuple indexing for Lean backendZyad Hassan1-1/+1
2024-03-08Update the generation of constant bodies for LeanSon Ho1-2/+2
2024-03-08Update the tuples syntaxSon Ho1-1/+3
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 13:35:14 +0000