summaryrefslogtreecommitdiff
path: root/tests/fstar/hashmap/Hashmap.Funs.fst (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-17Update the code of the hashmapSon Ho1-124/+124
2024-06-05Update charonNadrieril1-16/+16
2024-05-31Regenerate testsAymeric Fromherz1-1/+1
2024-05-31Regenerate test outputAymeric Fromherz1-8/+146
2024-05-30Implement two phases of loops join + collapseAymeric Fromherz1-146/+8
2024-05-28tests: Rename hashmap_utils -> utilsNadrieril1-2/+2
2024-05-27tests: Merge the hashmap test filesNadrieril1-30/+39
2024-05-24Update test outputsNadrieril1-30/+30
2024-05-24Tweak a pathNadrieril1-30/+30
2024-04-04Regenerate the test filesSon Ho1-35/+30
2024-04-04Regenerate the test filesSon Ho1-6/+6
2024-04-04Regenerate the test filesSon Ho1-9/+8
2024-03-20Regenerate the codeSon Ho1-14/+10
2024-03-19Regenerate the testsSon Ho1-2/+1
2023-12-23Regenerate the filesSon Ho1-5/+4
2023-12-22Regenerate the test files and add the fstar-split testsSon Ho1-257/+154
2023-11-21Regenerate the filesSon Ho1-38/+76
2023-11-21Regenerate most of the test filesSon Ho1-66/+64
2023-10-27Fix a minor issue and regenerate some F* test filesSon Ho1-231/+261
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-38/+47
2023-06-04Make a minor fixSon Ho1-8/+8
2023-06-04Improve simplify_aggregates to introduce structure updatesSon Ho1-54/+11
2023-06-04Start updating simplify_aggregatesSon Ho1-17/+63
2023-06-04Make sure let-bindings in Lean end with line breaks and improve formattingSon Ho1-26/+27
2023-02-03Do not unfold the monadic lets for the generated F* codeSon Ho1-386/+154
2023-02-03Update the hashmap and regenerateSon Ho1-10/+5
2023-02-03Improve the pretty names generation for loopsSon Ho1-3/+3
2023-02-03Fix an issue with the names of the loop decreases clausesSon Ho1-12/+12
2023-02-03Improve the order of the loop input parametersSon Ho1-8/+8
2023-02-03Improve the heuristic to find pretty names for the variables in the loopsSon Ho1-53/+55
2023-02-03Regenerate the hashmap code and update the proofsSon Ho1-86/+150
2023-02-03Regenerate the filesSon Ho1-72/+14
2022-11-14Regenerate the files and fix the proofsSon Ho1-100/+100
2022-11-14Reorganize the project to prepare for new backendsSon Ho1-0/+0
2022-10-20Regenerate the filesSon Ho1-1/+1
2022-08-10Corrected translation without using functions, remaining bug in hashmap trans...Sidney Congard1-10/+9
2022-05-15Regenerate the F* filesSon Ho1-35/+32
2022-05-06Update the extraction to set the fuel to 1 in the Z3 optionsSon Ho1-1/+1
2022-05-01Regenerate some of the test filesSon Ho1-4/+2
2022-04-21Regenerate the test filesSon Ho1-27/+29
2022-04-20Regenerate the test filesSon Ho1-47/+48
2022-03-05Make an update in the hash mapSon Ho1-4/+2
2022-03-03Change the extension of the serialized files to .llbcSon Ho1-25/+25
2022-02-24Update the way function names are handledSon Ho1-25/+25
2022-02-23Improve variable name generationSon Ho1-39/+40
2022-02-23Inline more let-bindings and improve formattingSon Ho1-72/+68
2022-02-23Improve the code generation by inlining more let-bindingsSon Ho1-108/+90
2022-02-13Add [contains_key], make progress on the proofs for [contains_key],Son Ho1-0/+41
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 21:33:09 +0000