| Commit message (Expand) | Author | Age | Files | Lines |
* | Make minor modifications and update the array test for F* | Son Ho | 2023-10-26 | 1 | -1/+3 |
* | Remove the warning for loops | Son Ho | 2023-10-25 | 1 | -8/+0 |
* | Fix a small issue | Son Ho | 2023-10-16 | 1 | -2/+0 |
* | Add sup | Son Ho | 2023-10-13 | 1 | -0/+2 |
* | Map some globals like u32::MAX to standard definitions | Son Ho | 2023-09-07 | 1 | -14/+0 |
* | Fix minor issues | Son Ho | 2023-09-04 | 1 | -1/+3 |
* | Update the code following a refactor on Charon's side | Son Ho | 2023-08-08 | 1 | -2/+6 |
* | Add an option to not override Hashmap.lean | Son Ho | 2023-08-04 | 1 | -0/+6 |
* | Use short names for the structure fields in Lean | Son Ho | 2023-07-06 | 1 | -1/+3 |
* | Reorganize the Lean tests | Son Ho | 2023-07-04 | 1 | -0/+6 |
* | Make good progress on generating code for HOL4 | Son Ho | 2023-06-04 | 1 | -0/+5 |
* | Add a sanity check in Driver.ml | Son Ho | 2023-06-04 | 1 | -0/+13 |
* | Remove the symbolic interpreter tests | Son Ho | 2023-06-04 | 1 | -5/+0 |
* | Automate the generation of the lakefile.lean files | Son Ho | 2023-06-04 | 1 | -1/+1 |
* | Add a check in Driver.ml | Son Ho | 2023-06-04 | 1 | -0/+12 |
* | Consistently use the names TerminationMeasure and DecreasesProof | Son Ho | 2023-06-04 | 1 | -11/+13 |
* | Add more checks in Driver.ml | Son Ho | 2023-06-04 | 1 | -2/+6 |
* | Print warnings for the Lean backend and loops | Son Ho | 2023-06-04 | 1 | -8/+13 |
* | WIP lots of stuff | Jonathan Protzenko | 2023-06-04 | 1 | -15/+19 |
* | Initial Lean backend, WIP | Jonathan Protzenko | 2023-06-04 | 1 | -0/+2 |
* | Do not unfold the monadic lets for the generated F* code | Son Ho | 2023-02-03 | 1 | -2/+3 |
* | Split InterpreterLoops into several files | Son Ho | 2023-02-03 | 1 | -0/+3 |
* | Make minor modifications and generate code for loops | Son Ho | 2023-02-03 | 1 | -24/+28 |
* | Remove the meta-value field from AMutBorrow | Son Ho | 2023-02-03 | 1 | -16/+18 |
* | Generate record field projectors for Coq | Son Ho | 2022-11-16 | 1 | -7/+0 |
* | Add a `-use-fuel` option | Son Ho | 2022-11-14 | 1 | -0/+8 |
* | Implement a pass to decompose nested patterns in let-bindings | Son Ho | 2022-11-14 | 1 | -21/+13 |
* | Make good progress on the Coq backend | Son Ho | 2022-11-14 | 1 | -5/+31 |
* | Make the Nix build work | Son Ho | 2022-11-11 | 1 | -3/+4 |
* | Implement a Config.ml file which groups all the global options in references | Son Ho | 2022-11-10 | 1 | -63/+21 |
* | Implement the generation of stateful backward functions (controlled by an opt... | Son Ho | 2022-11-10 | 1 | -2/+10 |
* | Add some .mli files | Son Ho | 2022-11-07 | 1 | -0/+1 |
* | Make minor modifications | Son Ho | 2022-10-28 | 1 | -1/+1 |
* | Make minor updates to account for Charon's changes | Son Ho | 2022-10-28 | 1 | -1/+1 |
* | Rename driver.ml to Driver.ml | Son Ho | 2022-10-27 | 1 | -0/+208 |