summaryrefslogtreecommitdiff
path: root/tests/lean (unfollow)
Commit message (Expand)AuthorFilesLines
2023-10-27Regenerate some of the F* test filesSon Ho1-4/+4
2023-10-26Fix some issues and regenerate the HashmapMain example for LeanSon Ho2-99/+129
2023-10-26Regenerate the betree example for LeanSon Ho1-40/+39
2023-10-26Regenerate several test files for LeanSon Ho4-122/+132
2023-10-26Regenerate the array files for LeanSon Ho2-111/+103
2023-10-25Regenerate the hashmap filesSon Ho2-86/+133
2023-10-25Regenerate the Lean array testSon Ho1-169/+150
2023-10-24Handle properly the builtin, non fallible functionsSon Ho1-6/+6
2023-10-24Start taking into account non-fallible functions like core::mem::replaceSon Ho1-70/+64
2023-10-13Add support for array repeatSon Ho1-26/+7
2023-10-06Slightly improve formatting of the generated codeSon Ho1-10/+10
2023-10-06Generate the Traits test files for LeanSon Ho4-0/+320
2023-09-18Cleanup the tutorial a bitSon Ho1-80/+110
2023-09-18Make minor modifications to the tutorialSon Ho1-3/+2
2023-09-18Make progress on the tutorialSon Ho1-3/+66
2023-09-18Start writing a tutorialSon Ho2-0/+298
2023-09-14Fix the hashmap proofs in LeanSon Ho3-22/+33
2023-09-13Make minor modificationsSon Ho1-5/+3
2023-09-07Regenerate the test files and fix a proofSon Ho4-22/+5
2023-08-18Regenerate the array testsSon Ho1-0/+8
2023-08-18Add tests which use const generics as valuesSon Ho1-0/+4
2023-08-09Update the nix flake and regenerate the codeSon Ho4-4/+4
2023-08-08Regenerate the test filesSon Ho3-215/+215
2023-08-07Regenerate the test filesSon Ho2-42/+230
2023-08-04Fix a heart beat issue in a Lean proofSon Ho1-0/+4
2023-08-04Update the Makefile and regenerate the test filesSon Ho1-23/+18
2023-08-04Add a forgotten fileSon Ho1-0/+1
2023-08-04Generate the Array example in LeanSon Ho2-0/+295
2023-08-04Make minor modificationsSon Ho3-5/+5
2023-08-03Make a minor formatting modification for LeanSon Ho14-0/+14
2023-08-03Fix issuesSon Ho1-0/+1
2023-07-31Make minor modificationsSon Ho1-0/+9
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