summaryrefslogtreecommitdiff
path: root/tests/fstar/hashmap/Hashmap.Funs.fst (unfollow)
Commit message (Expand)AuthorFilesLines
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
2022-02-13Start tracking the automatically generated/copied files for hashmapSon Ho1-0/+663
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 17:13:10 +0000