| Commit message (Expand) | Author | Age | Files | Lines |
* | Map some globals like u32::MAX to standard definitions | Son Ho | 2023-09-07 | 7 | -38/+112 |
* | Fix a minor issue in HOL4 | Son Ho | 2023-09-04 | 1 | -1/+1 |
* | Fix minor issues | Son Ho | 2023-09-04 | 2 | -3/+15 |
* | Implement extract_trait_impl | Son Ho | 2023-09-03 | 1 | -6/+160 |
* | Extract the trait decl methods | Son Ho | 2023-09-03 | 2 | -34/+54 |
* | Make progress registering the trait decl method names | Son Ho | 2023-09-03 | 2 | -31/+93 |
* | Do more cleanup | Son Ho | 2023-09-03 | 3 | -9/+9 |
* | Add the keep_fwd field in TranslateCore.pure_fun_translation | Son Ho | 2023-09-03 | 4 | -35/+42 |
* | Update TranslateCore.pure_fun_translation | Son Ho | 2023-09-03 | 5 | -34/+33 |
* | Update the type TranslateCore.fun_and_loops | Son Ho | 2023-09-03 | 4 | -34/+35 |
* | Make progress on extracting trait decls and merge gen_ctx and extraction_ctx | Son Ho | 2023-09-03 | 3 | -98/+219 |
* | Register the names for the trait decls | Son Ho | 2023-09-03 | 2 | -14/+154 |
* | Make more progress | Son Ho | 2023-09-03 | 3 | -24/+67 |
* | Make progress on the extraction | Son Ho | 2023-09-03 | 3 | -61/+221 |
* | Make progress on the extraction | Son Ho | 2023-09-03 | 6 | -21/+264 |
* | Make progress on the extraction | Son Ho | 2023-09-03 | 6 | -52/+138 |
* | Improve the collision detection | Son Ho | 2023-09-03 | 1 | -16/+54 |
* | Make good progress on Extract.ml | Son Ho | 2023-09-01 | 2 | -224/+237 |
* | Update PureMicroPasses | Son Ho | 2023-09-01 | 2 | -44/+19 |
* | Compute the normalized trait types maps and update Interpreter | Son Ho | 2023-09-01 | 6 | -70/+206 |
* | Implement the normalization functions in AssociatedTypes | Son Ho | 2023-09-01 | 5 | -14/+335 |
* | Make progress on Extract and ExtractBase | Son Ho | 2023-08-31 | 3 | -52/+132 |
* | Update TranslateCore and factor out some definitions in PrintPure | Son Ho | 2023-08-31 | 2 | -42/+42 |
* | Finish updating SymbolicToPure.ml | Son Ho | 2023-08-31 | 4 | -115/+212 |
* | Start adding support for traits | Son Ho | 2023-08-31 | 31 | -776/+1258 |
* | Add tests which use const generics as values | Son Ho | 2023-08-18 | 2 | -2/+5 |
* | Update following the introduction of ConstantExpr | Son Ho | 2023-08-18 | 16 | -143/+220 |
* | Make a minor modification | Son Ho | 2023-08-17 | 1 | -11/+0 |
* | Update the code following a refactor on Charon's side | Son Ho | 2023-08-08 | 4 | -12/+27 |
* | Change some fun id names to use "Mut"/"Shared" as a suffix | Son Ho | 2023-08-07 | 5 | -66/+66 |
* | Add an option to not override Hashmap.lean | Son Ho | 2023-08-04 | 3 | -2/+15 |
* | Fix issues with the extraction and extend the primitive libraries for Coq and F* | Son Ho | 2023-08-04 | 2 | -12/+12 |
* | Add SliceLen as a primitive function and make minor adjustments | Son Ho | 2023-08-04 | 5 | -35/+62 |
* | Start adding support for Arrays/Slices in the Lean library | Son Ho | 2023-08-04 | 1 | -10/+12 |
* | Fix an issue with the extraction of aggregated arrays | Son Ho | 2023-08-03 | 10 | -180/+320 |
* | Make a minor formatting modification for Lean | Son Ho | 2023-08-03 | 1 | -1/+1 |
* | Fix issues | Son Ho | 2023-08-03 | 10 | -57/+139 |
* | Make minor modifications | Son Ho | 2023-08-02 | 3 | -16/+29 |
* | Add the function signatures in Assumed.ml | Son Ho | 2023-08-02 | 1 | -0/+143 |
* | Make more progress | Son Ho | 2023-08-02 | 2 | -75/+186 |
* | Make progress | Son Ho | 2023-08-02 | 5 | -53/+80 |
* | Make progress | Son Ho | 2023-08-02 | 14 | -76/+178 |
* | Make progress | Son Ho | 2023-08-02 | 7 | -164/+232 |
* | Make progress proapagating the changes | Son Ho | 2023-08-02 | 25 | -273/+407 |
* | Start adding support for const generics | Son Ho | 2023-08-01 | 11 | -226/+246 |
* | Make the `by inlit` implicit | Son Ho | 2023-07-12 | 1 | -1/+1 |
* | Use short names for the structure fields in Lean | Son Ho | 2023-07-06 | 5 | -19/+78 |
* | Improve the generated comments | Son Ho | 2023-07-06 | 3 | -24/+102 |
* | Simplify the names used in Primitives.lean | Son Ho | 2023-07-05 | 1 | -16/+33 |
* | Simplify the generated names for the types in Lean | Son Ho | 2023-07-05 | 1 | -5/+12 |