summaryrefslogtreecommitdiff
path: root/tests (unfollow)
Commit message (Expand)AuthorFilesLines
2023-07-26Make minor modificationsSon Ho1-3/+2
2023-07-26Make a minor modification to a hashmap proofSon Ho1-5/+9
2023-07-26Update some of the Vec function specsSon Ho1-16/+19
2023-07-26Update the syntax of the progress tacticSon Ho1-86/+85
2023-07-26Fix a proof for the hashmapSon Ho1-5/+12
2023-07-25Make progress on the proofs of the hashmapSon Ho1-18/+40
2023-07-25Make progress on the proofs of the hashmapSon Ho1-4/+112
2023-07-25Make progress on the hashmap propertiesSon Ho1-0/+92
2023-07-25Improve the syntax of progress: `as ⟨ x, y .. ⟩`Son Ho1-30/+4
2023-07-20Improve the interactivity of some hashmap proofsSon Ho1-75/+34
2023-07-20Make progress on some of the hashmap proofsSon Ho1-40/+127
2023-07-20Make some proofs in Hashmap/Properties.lean and improve progressSon Ho1-11/+65
2023-07-20Improve progress further and move some lemmasSon Ho1-84/+8
2023-07-19Improve progressSon Ho1-2/+32
2023-07-18Improve progressSon Ho1-13/+11
2023-07-17Make minor modificationsSon Ho1-25/+0
2023-07-17With @sonmarcho, some Lean proofs for hashmaps + comments about possible impr...Aymeric Fromherz2-0/+196
2023-07-17Update the lean dependencies and update IListSon Ho2-5/+5
2023-07-12Make the `by inlit` implicitSon Ho9-322/+269
2023-07-06Use short names for the structure fields in LeanSon Ho8-248/+154
2023-07-06Improve the generated commentsSon Ho56-1864/+1953
2023-07-05Simplify the names used in Primitives.leanSon Ho7-78/+76
2023-07-05Simplify the generated names for the types in LeanSon Ho19-889/+857
2023-07-05Start using namespaces in the Lean backendSon Ho38-614/+682
2023-07-04Fix an issue with mkSigmasValSon Ho1-1/+1
2023-07-04Regenerate the Lean test filesSon Ho22-192/+275
2023-07-04Reorganize the Lean testsSon Ho67-6245/+1481
2023-06-04Update the HOL4 proofs for the last *release* version of HOL4Son Ho6-325/+327
2023-06-04Start setting up the Nix derivation for HOL4Son Ho2-5/+16
2023-06-04Add a commentSon Ho1-1/+5
2023-06-04Finish the proofs of the hashmapSon Ho2-463/+1461
2023-06-04Prove hash_map_insert_fwd_back_specSon Ho1-1/+59
2023-06-04Make progress on the proofs of the hash mapSon Ho1-4/+619
2023-06-04Make good progress on the proofs of the hashmap in HOL4Son Ho1-46/+686
2023-06-04Start working on the proofs of the hash mapSon Ho1-0/+543
2023-06-04Update tests/MakefileSon Ho1-1/+1
2023-06-04Add the generated HOL4 filesSon Ho43-0/+13198
2023-06-04Make good progress on generating code for HOL4Son Ho11-109/+148
2023-06-04Add Result_Inhabited to Primitives.leanSon Ho8-0/+24
2023-06-04Regenerate the translated files for LeanSon Ho37-4931/+4452
2023-06-04Make a minor fixSon Ho4-39/+32
2023-06-04Improve the generation of variant names for LeanSon Ho11-451/+419
2023-06-04Improve simplify_aggregates to introduce structure updatesSon Ho7-314/+79
2023-06-04Start updating simplify_aggregatesSon Ho14-292/+589
2023-06-04Make minor modifications to the Lean filesSon Ho3-15/+14
2023-06-04Update the extraction of Lean filesSon Ho42-139/+364
2023-06-04Reorganize the Lean tests and extract the Polonius tests to LeanSon Ho29-0/+2357
2023-06-04Remove the tests/lean/hashmap_on_disk/Main.lean fileSon Ho1-10/+0
2023-06-04Generate all the lakefile.lean filesSon Ho6-0/+108
2023-06-04Automate the generation of the lakefile.lean filesSon Ho1-7/+3
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-28 20:09:46 +0000