summaryrefslogtreecommitdiff
path: root/tests/hashmap/Hashmap.Funs.fst (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Regenerate the filesSon Ho2022-10-201-1/+1
|
* Corrected translation without using functions, remaining bug in hashmap ↵Sidney Congard2022-08-101-10/+9
| | | | translation
* Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2Sidney Congard2022-06-301-9/+14
| | | | Complete the constants extraction by making all functions fail
* Regenerate the F* filesSon Ho2022-05-151-35/+32
|
* Update the extraction to set the fuel to 1 in the Z3 optionsSon Ho2022-05-061-1/+1
|
* Regenerate some of the test filesSon Ho2022-05-011-4/+2
|
* Regenerate the test filesSon Ho2022-04-211-27/+29
|
* Regenerate the test filesSon Ho2022-04-201-47/+48
|
* Make an update in the hash mapSon Ho2022-03-051-4/+2
|
* Change the extension of the serialized files to .llbcSon Ho2022-03-031-25/+25
|
* Update the way function names are handledSon Ho2022-02-241-25/+25
|
* Improve variable name generationSon Ho2022-02-231-39/+40
|
* Inline more let-bindings and improve formattingSon Ho2022-02-231-72/+68
|
* Improve the code generation by inlining more let-bindingsSon Ho2022-02-231-108/+90
|
* Add [contains_key], make progress on the proofs for [contains_key],Son Ho2022-02-131-0/+41
| | | | | [get] and [get_mut] and stabilize the proof of [hash_map_move_elements_fwd_back_lem_refin]
* Start tracking the automatically generated/copied files for hashmapSon Ho2022-02-131-0/+663