| Commit message (Expand) | Author | Age | Files | Lines |
... | |
* | Remove some assumed types and add more support for builtin definitions | Son Ho | 2023-10-23 | 1 | -42/+65 |
* | Start updating to handle function pointers | Son Ho | 2023-10-20 | 1 | -5/+5 |
* | Make minor modifications | Son Ho | 2023-09-17 | 1 | -4/+1 |
* | Merge trans_ctx and decls_ctx | Son Ho | 2023-09-17 | 1 | -62/+17 |
* | Fix more issues with the extraction | Son Ho | 2023-09-17 | 1 | -7/+33 |
* | Add a strict_names_map in the extraction_ctx | Son Ho | 2023-09-16 | 1 | -0/+14 |
* | Map some globals like u32::MAX to standard definitions | Son Ho | 2023-09-07 | 1 | -18/+18 |
* | Do more cleanup | Son Ho | 2023-09-03 | 1 | -3/+1 |
* | Add the keep_fwd field in TranslateCore.pure_fun_translation | Son Ho | 2023-09-03 | 1 | -18/+16 |
* | Update TranslateCore.pure_fun_translation | Son Ho | 2023-09-03 | 1 | -21/+19 |
* | Update the type TranslateCore.fun_and_loops | Son Ho | 2023-09-03 | 1 | -23/+23 |
* | Make progress on extracting trait decls and merge gen_ctx and extraction_ctx | Son Ho | 2023-09-03 | 1 | -93/+70 |
* | Make more progress | Son Ho | 2023-09-03 | 1 | -18/+52 |
* | Make progress on the extraction | Son Ho | 2023-09-03 | 1 | -0/+1 |
* | Make progress on the extraction | Son Ho | 2023-09-03 | 1 | -16/+93 |
* | Start adding support for traits | Son Ho | 2023-08-31 | 1 | -3/+1 |
* | Update the code following a refactor on Charon's side | Son Ho | 2023-08-08 | 1 | -4/+7 |
* | Add an option to not override Hashmap.lean | Son Ho | 2023-08-04 | 1 | -2/+1 |
* | Fix issues with the extraction and extend the primitive libraries for Coq and F* | Son Ho | 2023-08-04 | 1 | -0/+2 |
* | Make a minor formatting modification for Lean | Son Ho | 2023-08-03 | 1 | -1/+1 |
* | Use short names for the structure fields in Lean | Son Ho | 2023-07-06 | 1 | -0/+1 |
* | Improve the generated comments | Son Ho | 2023-07-06 | 1 | -0/+4 |
* | Start using namespaces in the Lean backend | Son Ho | 2023-07-05 | 1 | -28/+52 |
* | Fix minor issues | Son Ho | 2023-07-04 | 1 | -51/+115 |
* | Reorganize the Lean tests | Son Ho | 2023-07-04 | 1 | -35/+35 |
* | Make progress on the HOL4 backend | Son Ho | 2023-06-04 | 1 | -29/+46 |
* | Make progress on extracting the HOL4 files | Son Ho | 2023-06-04 | 1 | -1/+1 |
* | Make good progress on generating code for HOL4 | Son Ho | 2023-06-04 | 1 | -190/+276 |
* | Make more updates for the Lean backend | Son Ho | 2023-06-04 | 1 | -12/+16 |
* | Make minor modifications | Son Ho | 2023-06-04 | 1 | -2/+14 |
* | Improve the generation of variant names for Lean | Son Ho | 2023-06-04 | 1 | -1/+5 |
* | Add a special expression for structure creation/update | Son Ho | 2023-06-04 | 1 | -1/+9 |
* | Don't create useless directories in Lean | Son Ho | 2023-06-04 | 1 | -2/+4 |
* | Update the extraction of Lean files | Son Ho | 2023-06-04 | 1 | -11/+23 |
* | Automate the generation of the lakefile.lean files | Son Ho | 2023-06-04 | 1 | -119/+166 |
* | Handle the "opaque_defs." prefix in a cleaner manner | Son Ho | 2023-06-04 | 1 | -2/+23 |
* | Consistently use the names TerminationMeasure and DecreasesProof | Son Ho | 2023-06-04 | 1 | -4/+6 |
* | Update the generation of termination and decreases_by templates for Lean | Son Ho | 2023-06-04 | 1 | -5/+9 |
* | More comments | Jonathan Protzenko | 2023-06-04 | 1 | -0/+8 |
* | Make minor fixes, improve formatting for Lean and generate code for all the t... | Son Ho | 2023-06-04 | 1 | -43/+60 |
* | WIP | Jonathan Protzenko | 2023-06-04 | 1 | -2/+19 |
* | Fix some printing bits, proper syntax for terminates and decreases clauses | Jonathan Protzenko | 2023-06-04 | 1 | -1/+4 |
* | WIP lots of stuff | Jonathan Protzenko | 2023-06-04 | 1 | -3/+11 |
* | New directory structure and corresponding extraction, + misc fixes, for Lean | Jonathan Protzenko | 2023-06-04 | 1 | -25/+37 |
* | Initial Lean backend, WIP | Jonathan Protzenko | 2023-06-04 | 1 | -22/+34 |
* | Implement a pass to filter the unused input arguments in the loop functions | Son Ho | 2023-02-03 | 1 | -13/+13 |
* | Fix an issue with the names of the loop decreases clauses | Son Ho | 2023-02-03 | 1 | -0/+10 |
* | Fix some issues with the values given back by loop backward translations | Son Ho | 2023-02-03 | 1 | -0/+1 |
* | Fix an issue in translate_forward_end | Son Ho | 2023-02-03 | 1 | -0/+1 |
* | Fix various issues with the generation of code for the loops | Son Ho | 2023-02-03 | 1 | -27/+58 |