| Commit message (Expand) | Author | Files | Lines |
2024-03-20 | Regenerate the code | Son Ho | 9 | -126/+119 |
2024-03-19 | Regenerate the tests | Son Ho | 9 | -64/+26 |
2024-03-19 | Update the demo | Son Ho | 1 | -10/+38 |
2024-03-18 | Regenerate the test files | Son Ho | 2 | -22/+114 |
2024-03-18 | Regenerate the constants tests and update Primitives/Base.lean | Son Ho | 1 | -18/+35 |
2024-03-11 | Regenerate the test files | Son Ho | 3 | -83/+78 |
2024-03-11 | Update the generated files | Son Ho | 5 | -128/+134 |
2024-03-09 | Regenerate the test files | Son Ho | 2 | -0/+133 |
2024-02-09 | Add some missing files | Son Ho | 2 | -0/+30 |
2024-02-09 | Add some demo files | Son Ho | 2 | -0/+1066 |
2024-02-02 | Rename and regenerate some files | Son Ho | 5 | -119/+119 |
2024-01-25 | Regenerate the files | Son Ho | 2 | -66/+80 |
2023-12-23 | Fix an issue in External_FunsExternal.v | Son Ho | 1 | -15/+3 |
2023-12-23 | Fix an issue when deconstructing tuples in Coq | Son Ho | 1 | -2/+2 |
2023-12-23 | Regenerate the files | Son Ho | 9 | -91/+47 |
2023-12-23 | Improve the micro passes to eliminate pattern `let f := fun x => g x` | Son Ho | 1 | -18/+8 |
2023-12-22 | Regenerate the test files and add the fstar-split tests | Son Ho | 22 | -2666/+1731 |
2023-12-22 | Annotate the bound vars in the lambdas for Coq | Son Ho | 2 | -273/+231 |
2023-12-13 | Regenerate the test files | Son Ho | 7 | -61/+95 |
2023-12-07 | Regenerate the tests | Son Ho | 2 | -16/+39 |
2023-12-05 | Update following changes in Charon | Son Ho | 3 | -97/+155 |
2023-11-29 | Regenerate the other files | Son Ho | 7 | -0/+457 |
2023-11-29 | Generate the Bitwise test files | Son Ho | 1 | -0/+38 |
2023-11-29 | Regenerate the tests | Son Ho | 1 | -29/+42 |
2023-11-29 | Regenerate the test files | Son Ho | 1 | -5/+0 |
2023-11-27 | Generate a dedicated file for the external types | Son Ho | 28 | -54/+151 |
2023-11-27 | Update the generation of files for external definitions and regenerate the tests | Son Ho | 12 | -16/+136 |
2023-11-24 | Regenerate the files | Son Ho | 1 | -8/+2 |
2023-11-22 | Regenerate the test files | Son Ho | 1 | -45/+62 |
2023-11-21 | Regenerate the files | Son Ho | 1 | -27/+31 |
2023-11-21 | Regenerate the files | Son Ho | 18 | -478/+956 |
2023-11-21 | Regenerate the betree files | Son Ho | 2 | -58/+58 |
2023-11-21 | Regenerate the Traits files | Son Ho | 1 | -60/+66 |
2023-11-21 | Regenerate most of the test files | Son Ho | 13 | -383/+425 |
2023-11-09 | Regenerate the Coq test files | Son Ho | 14 | -80/+1403 |
2023-11-08 | Update the Makefile and regenerate some tests | Son Ho | 1 | -0/+12 |
2023-10-27 | Add some files for the Coq trait tests | Son Ho | 2 | -0/+28 |
2023-10-27 | Regenerate the Coq test files | Son Ho | 23 | -2117/+3588 |
2023-09-07 | Regenerate the test files and fix a proof | Son Ho | 9 | -23/+75 |
2023-08-18 | Regenerate the array tests | Son Ho | 1 | -0/+9 |
2023-08-18 | Add tests which use const generics as values | Son Ho | 1 | -0/+4 |
2023-08-09 | Update the nix flake and regenerate the code | Son Ho | 4 | -4/+4 |
2023-08-08 | Regenerate the test files | Son Ho | 3 | -273/+273 |
2023-08-07 | Regenerate the test files | Son Ho | 2 | -10/+180 |
2023-08-04 | Generate the array test files for Coq and F* | Son Ho | 5 | -0/+865 |
2023-08-04 | Update the Makefile and regenerate the test files | Son Ho | 20 | -24/+231 |
2023-07-06 | Improve the generated comments | Son Ho | 15 | -296/+325 |
2023-07-05 | Start using namespaces in the Lean backend | Son Ho | 3 | -3/+3 |
2023-06-04 | Make good progress on generating code for HOL4 | Son Ho | 8 | -108/+102 |
2023-06-04 | Start updating simplify_aggregates | Son Ho | 5 | -58/+178 |