| Commit message (Expand) | Author | Age | Files | Lines |
... | |
* | | Fix some issues | Son Ho | 2023-09-07 | 1 | -1/+0 |
* | | Map some globals like u32::MAX to standard definitions | Son Ho | 2023-09-07 | 1 | -1/+7 |
* | | Fix a minor issue in HOL4 | Son Ho | 2023-09-04 | 1 | -1/+1 |
* | | Implement extract_trait_impl | Son Ho | 2023-09-03 | 1 | -6/+160 |
* | | Extract the trait decl methods | Son Ho | 2023-09-03 | 1 | -19/+47 |
* | | Make progress registering the trait decl method names | Son Ho | 2023-09-03 | 1 | -17/+33 |
* | | Do more cleanup | Son Ho | 2023-09-03 | 1 | -3/+5 |
* | | Update TranslateCore.pure_fun_translation | Son Ho | 2023-09-03 | 1 | -1/+2 |
* | | Update the type TranslateCore.fun_and_loops | Son Ho | 2023-09-03 | 1 | -2/+2 |
* | | Make progress on extracting trait decls and merge gen_ctx and extraction_ctx | Son Ho | 2023-09-03 | 1 | -5/+145 |
* | | Register the names for the trait decls | Son Ho | 2023-09-03 | 1 | -6/+84 |
* | | Make more progress | Son Ho | 2023-09-03 | 1 | -6/+13 |
* | | Make progress on the extraction | Son Ho | 2023-09-03 | 1 | -53/+165 |
* | | Make progress on the extraction | Son Ho | 2023-09-03 | 1 | -1/+12 |
* | | Make progress on the extraction | Son Ho | 2023-09-03 | 1 | -26/+50 |
* | | Make good progress on Extract.ml | Son Ho | 2023-09-01 | 1 | -221/+193 |
* | | Make progress on Extract and ExtractBase | Son Ho | 2023-08-31 | 1 | -41/+102 |
* | | Update following the introduction of ConstantExpr | Son Ho | 2023-08-18 | 1 | -0/+3 |
|/ |
|
* | Change some fun id names to use "Mut"/"Shared" as a suffix | Son Ho | 2023-08-07 | 1 | -30/+30 |
* | Fix issues with the extraction and extend the primitive libraries for Coq and F* | Son Ho | 2023-08-04 | 1 | -12/+10 |
* | Add SliceLen as a primitive function and make minor adjustments | Son Ho | 2023-08-04 | 1 | -28/+30 |
* | 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 | 1 | -85/+133 |
* | Fix issues | Son Ho | 2023-08-03 | 1 | -38/+77 |
* | Make more progress | Son Ho | 2023-08-02 | 1 | -75/+172 |
* | Make progress | Son Ho | 2023-08-02 | 1 | -34/+56 |
* | 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 | 1 | -4/+9 |
* | Improve the generated comments | Son Ho | 2023-07-06 | 1 | -19/+65 |
* | 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 |
* | Start using namespaces in the Lean backend | Son Ho | 2023-07-05 | 1 | -13/+15 |
* | Fix minor issues | Son Ho | 2023-07-04 | 1 | -4/+10 |
* | Fix some issues with the extraction to Lean | Son Ho | 2023-07-04 | 1 | -48/+86 |
* | Reorganize the Lean tests | Son Ho | 2023-07-04 | 1 | -8/+6 |
* | Make progress on the HOL4 backend | Son Ho | 2023-06-04 | 1 | -10/+34 |
* | Make progress on extracting the HOL4 files | Son Ho | 2023-06-04 | 1 | -15/+78 |
* | Make the unfolding theorems collection from evalLib persistent | Son Ho | 2023-06-04 | 1 | -9/+13 |
* | Make good progress on generating code for HOL4 | Son Ho | 2023-06-04 | 1 | -291/+906 |
* | Make more updates for the Lean backend | Son Ho | 2023-06-04 | 1 | -14/+27 |
* | Make minor modifications | Son Ho | 2023-06-04 | 1 | -1/+9 |
* | Update Extract.ml | Son Ho | 2023-06-04 | 1 | -15/+35 |
* | Make extract_adt_cons call extract_adt_g_value | Son Ho | 2023-06-04 | 1 | -54/+15 |
* | Make a minor fix | Son Ho | 2023-06-04 | 1 | -7/+1 |
* | Improve the generation of variant names for Lean | Son Ho | 2023-06-04 | 1 | -14/+21 |
* | Improve simplify_aggregates to introduce structure updates | Son Ho | 2023-06-04 | 1 | -1/+7 |
* | Add a special expression for structure creation/update | Son Ho | 2023-06-04 | 1 | -51/+54 |
* | Update the extraction of Lean files | Son Ho | 2023-06-04 | 1 | -14/+28 |
* | Reorganize the Lean tests and extract the Polonius tests to Lean | Son Ho | 2023-06-04 | 1 | -1/+1 |
* | Handle the "opaque_defs." prefix in a cleaner manner | Son Ho | 2023-06-04 | 1 | -31/+70 |