| Commit message (Expand) | Author | Age | Files | Lines |
... | |
| * | | | Regenerate the betree example for Lean | Son Ho | 2023-10-26 | 1 | -40/+39 |
| * | | | Regenerate several test files for Lean | Son Ho | 2023-10-26 | 4 | -122/+132 |
| * | | | Improve the handling of saved function effects in ExtractBuiltin.ml | Son Ho | 2023-10-26 | 2 | -24/+44 |
| * | | | Regenerate the array files for Lean | Son Ho | 2023-10-26 | 2 | -111/+103 |
| * | | | Make progress on fixing the extraction | Son Ho | 2023-10-26 | 2 | -72/+88 |
| * | | | Improve ExtractBuiltin.ml | Son Ho | 2023-10-26 | 2 | -46/+57 |
| * | | | Make progress on fixing the extraction for Lean | Son Ho | 2023-10-26 | 5 | -220/+180 |
| * | | | Fix more issues at extraction and factor out defs in ExtractBuiltin | Son Ho | 2023-10-26 | 2 | -266/+166 |
| * | | | Regenerate the hashmap files | Son Ho | 2023-10-25 | 2 | -86/+133 |
| * | | | Make the hashmap files typecheck again in Lean | Son Ho | 2023-10-25 | 12 | -2775/+2778 |
| * | | | Regenerate the Lean array test | Son Ho | 2023-10-25 | 1 | -169/+150 |
| * | | | Fix some issues at extraction and add builtins | Son Ho | 2023-10-25 | 11 | -61/+546 |
| * | | | Fix some issues to make the array test succeed again | Son Ho | 2023-10-25 | 2 | -16/+44 |
| * | | | Remove the warning for loops | Son Ho | 2023-10-25 | 1 | -8/+0 |
| * | | | Update following the addition of raw pointers | Son Ho | 2023-10-25 | 12 | -17/+77 |
| * | | | Handle properly the builtin, non fallible functions | Son Ho | 2023-10-24 | 5 | -26/+62 |
| * | | | Merge branch 'son_traits' into son_traits_types | Son Ho | 2023-10-24 | 3 | -8/+50 |
| |\ \ \ |
|
| | * \ \ | Merge branch 'son_traits_arrow' into protz_numeric | Son Ho | 2023-10-24 | 16 | -100/+163 |
| | |\ \ \ |
|
| | * | | | | Add more support for numeric operations, xor, rotate | Jonathan Protzenko | 2023-10-22 | 3 | -8/+50 |
| * | | | | | Start taking into account non-fallible functions like core::mem::replace | Son Ho | 2023-10-24 | 3 | -75/+79 |
| * | | | | | Fix minor issues | Son Ho | 2023-10-24 | 2 | -6/+6 |
| * | | | | | Fix an issue coming from the modification for the opaque signatures | Son Ho | 2023-10-24 | 1 | -12/+7 |
| * | | | | | Fix a printing issue with scalar values | Son Ho | 2023-10-24 | 1 | -3/+5 |
| * | | | | | Filter some type arguments for the builtin types/functions | Son Ho | 2023-10-24 | 4 | -10/+87 |
| * | | | | | Remove the possibility of generating opaque module signatures | Son Ho | 2023-10-24 | 4 | -330/+111 |
| * | | | | | Add support for builtin trait implementations | Son Ho | 2023-10-24 | 4 | -20/+80 |
| * | | | | | Fix various issues with the builtins | Son Ho | 2023-10-24 | 4 | -122/+234 |
| * | | | | | Add definitions in for the Lean Primitives library | Son Ho | 2023-10-24 | 3 | -0/+57 |
| * | | | | | Add some debugging information | Son Ho | 2023-10-24 | 1 | -0/+7 |
| * | | | | | Deactivate the concrete interpreter tests | Son Ho | 2023-10-24 | 1 | -2/+2 |
| * | | | | | Make progress on handling the builtins | Son Ho | 2023-10-23 | 4 | -154/+270 |
| * | | | | | Remove some assumed types and add more support for builtin definitions | Son Ho | 2023-10-23 | 24 | -808/+763 |
| | |/ / /
| |/| | | |
|
| * | | | | Start updating to handle function pointers | Son Ho | 2023-10-20 | 16 | -100/+163 |
| |/ / / |
|
| * | | | Refold the scalar types when applying progress | Son Ho | 2023-10-17 | 4 | -16/+91 |
| * | | | Implement tactics for termination proofs which involve arithmetic | Son Ho | 2023-10-17 | 4 | -21/+37 |
| * | | | Merge branch 'main' into son_traits and fix some issues | Son Ho | 2023-10-16 | 18 | -107/+780 |
| |\ \ \
| |/ / /
|/| | | |
|
* | | | | Merge pull request #41 from AeneasVerif/son-readme | Son HO | 2023-10-05 | 1 | -0/+2 |
|\ \ \ \ |
|
| * | | | | Add a mention to the Zulip in the README | Son Ho | 2023-10-05 | 1 | -0/+2 |
|/ / / / |
|
| * | | | Improve formatting of scalars in Lean | Son Ho | 2023-10-16 | 2 | -23/+25 |
| * | | | Fix a small issue | Son Ho | 2023-10-16 | 2 | -13/+53 |
| * | | | Update Primitives.fst | Son Ho | 2023-10-13 | 1 | -0/+3 |
| * | | | Add support for array repeat | Son Ho | 2023-10-13 | 1 | -26/+7 |
| * | | | Add sup | Son Ho | 2023-10-13 | 9 | -4/+91 |
| * | | | Slightly improve formatting of the generated code | Son Ho | 2023-10-06 | 2 | -11/+16 |
| * | | | Generate the Traits test files for Lean | Son Ho | 2023-10-06 | 4 | -0/+320 |
| * | | | Cleanup a bit | Son Ho | 2023-09-19 | 2 | -12/+12 |
| * | | | Normalize the function signatures before translation to pure | Son Ho | 2023-09-17 | 9 | -150/+294 |
| * | | | Make minor modifications | Son Ho | 2023-09-17 | 2 | -15/+9 |
| * | | | Merge trans_ctx and decls_ctx | Son Ho | 2023-09-17 | 7 | -120/+53 |
| * | | | Make progress on correctly extracting trait method calls | Son Ho | 2023-09-17 | 3 | -39/+121 |