summaryrefslogtreecommitdiff
path: root/tests/fstar/misc/Constants.fst (unfollow)
Commit message (Expand)AuthorFilesLines
2024-05-24Update test outputsNadrieril1-31/+31
2024-05-24Tweak a pathNadrieril1-31/+31
2024-04-04Regenerate the test filesSon Ho1-17/+17
2024-03-18Regenerate the test filesSon Ho1-18/+18
2024-03-18Regenerate the constants tests and update Primitives/Base.leanSon Ho1-18/+32
2024-03-11Update the generated filesSon Ho1-29/+29
2023-12-22Regenerate the test files and add the fstar-split testsSon Ho1-9/+9
2023-11-21Regenerate the filesSon Ho1-28/+56
2023-11-21Regenerate most of the test filesSon Ho1-1/+1
2023-10-27Regenerate some of the F* test filesSon Ho1-23/+23
2023-09-07Regenerate the test files and fix a proofSon Ho1-5/+1
2023-08-09Update the nix flake and regenerate the codeSon Ho1-1/+1
2023-07-06Improve the generated commentsSon Ho1-8/+8
2023-06-04Start updating simplify_aggregatesSon Ho1-3/+3
2023-06-04Make sure let-bindings in Lean end with line breaks and improve formattingSon Ho1-5/+10
2023-02-03Do not unfold the monadic lets for the generated F* codeSon Ho1-8/+1
2023-02-03Regenerate the filesSon Ho1-37/+11
2022-11-14Regenerate the files and fix the proofsSon Ho1-13/+25
2022-11-14Reorganize the project to prepare for new backendsSon Ho1-0/+0
2022-10-20Regenerate the filesSon Ho1-1/+1
2022-08-11Correct last PR remarksSidney Congard1-3/+3
2022-08-10Corrected translation without using functions, remaining bug in hashmap trans...Sidney Congard1-1/+122
2022-08-08Register global names, one error remainingSidney Congard1-0/+10
2022-07-29Create global declaration group, address PR changes but introduce bugsSidney Congard1-135/+0
2022-06-30Traduct globals body separately (WIP)Sidney Congard1-128/+1
2022-06-23adapt to new LLBC (without OperandConstantValue)Sidney Congard1-0/+19
2022-06-21concrete & symbolic evaluation work with new LLBC formatSidney Congard1-0/+119