summaryrefslogtreecommitdiff
path: root/backends (unfollow)
Commit message (Expand)AuthorFilesLines
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-08Update the Makefile and remove the split files for F*Son Ho4-931/+0
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
2024-03-08Update the tuples notationsSon Ho3-51/+81
2024-03-08Remove some commentsSon Ho1-31/+0
2024-03-08Update the handling of notations like #u32 or #isizeSon Ho4-70/+104
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-03-07Add a notation for tuple field accesses in LeanSon Ho1-0/+51
2024-02-09Cleanup a bit Scalar.leanSon Ho1-198/+198
2024-02-02Update the .gitignore filesSon Ho1-1/+2
2024-02-02Fix more proofsSon Ho3-13/+16
2024-02-02Fix more proofsSon Ho1-56/+55
2024-02-02Update lean to v4.6.0-rc1 and start fixing the proofsSon Ho8-93/+120
2024-01-27Add some lemmas to the Lean backendSon Ho1-4/+14
2024-01-27Fix a minor issue with the progress tacticSon Ho2-82/+112
2024-01-26Improve the Lean backendSon Ho5-10/+52
2023-12-22Fix minor issuesSon Ho3-1/+83
2023-12-22Fix the models for core::mem::replaceSon Ho3-3/+3
2023-12-22Update the library for CoqSon Ho1-74/+42
2023-12-22Update the library for F*Son Ho4-0/+876
2023-12-22Update the Lean standard librarySon Ho5-81/+38
2023-12-13Update the extraction to handle casts between integers/boolsSon Ho3-0/+12
2023-12-12Inline the let-bindings in the validity proofsSon Ho1-7/+40
2023-12-12Fix a minor issue with the divergent encodingSon Ho1-53/+80
2023-12-12Fix minor issues with the divergence encodingSon Ho1-14/+5
2023-12-12Make progress on supporting higher-order divergent functionsSon Ho2-53/+95
2023-12-12Implement a map-reduce visitor for expressions and fix issues with get{M,F}Va...Son Ho1-31/+81
2023-12-11Update the validity proofs for higher-order functionsSon Ho2-11/+96
2023-12-11Start working on higher-order examples for DivergeSon Ho4-218/+355
2023-12-11Cleanup a bitSon Ho1-16/+47
2023-12-11Update Diverge/Elab.lean to use the more general FixII definitionsSon Ho3-195/+387
2023-12-11Reorganize a bitSon Ho3-94/+49
2023-12-11Reactivate the sanity checks for the progress tacticSon Ho3-26/+24
2023-12-08Update the progress tactic to use discrimination treesSon Ho3-272/+175
2023-12-07Start working on a version of Diverge.FixI more suited to higher-order functionsSon Ho3-67/+510
2023-12-07Reorganize a bitSon Ho3-65/+94
2023-11-29Add support for more bitwise operations and update the extractionSon Ho3-10/+275
2023-11-21Update more namesSon Ho3-48/+48
2023-11-21Update the standard librariesSon Ho5-78/+85
2023-11-09Update the failing proofsSon Ho3-6/+40
2023-10-27Regenerate the Coq test filesSon Ho1-1/+1
2023-10-27Update Primitives.vSon Ho1-60/+342
2023-10-27Regenerate some of the F* test filesSon Ho1-2/+19
2023-10-26Update Primitives.fstSon Ho1-48/+318
2023-10-26Make progress on fixing the extractionSon Ho1-64/+64
2023-10-26Make progress on fixing the extraction for LeanSon Ho1-114/+50
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 19:57:08 +0000