| Commit message (Expand) | Author | Age | Files | Lines |
... | |
| * | Update the interpreter so that it is not written in CPS style (#120) | Escherichia | 2024-05-23 | 19 | -2294/+2116 |
* | | Add simp, reducible attributes to generated Lean projectors | Aymeric Fromherz | 2024-05-23 | 1 | -0/+10 |
* | | Do not expand field projector for recursive structs to a let binding in Lean | Aymeric Fromherz | 2024-05-23 | 1 | -5/+0 |
* | | Improve formatting of Lean struct projectors | Aymeric Fromherz | 2024-05-23 | 1 | -2/+6 |
* | | Add printing of projectors for recursive structs in Lean backend | Aymeric Fromherz | 2024-05-23 | 1 | -3/+130 |
|/ |
|
* | Catch new literal variants | Nadrieril | 2024-05-14 | 2 | -0/+6 |
* | Ensure `./charon` points to a valid charon clone | Nadrieril | 2024-05-14 | 2 | -1/+1 |
* | Update charon | Nadrieril | 2024-05-06 | 2 | -3/+12 |
* | Add error when handling mutually recursive traits | Aymeric Fromherz | 2024-05-01 | 1 | -1/+4 |
* | Update compiler/ExtractBuiltin.ml | Son HO | 2024-04-26 | 1 | -1/+1 |
* | Update the backend and ExtractBuiltin.ml | Son Ho | 2024-04-25 | 1 | -1/+4 |
* | Merge branch 'main' into core-option-unwrap | Son Ho | 2024-04-25 | 1 | -0/+25 |
|\ |
|
| * | Merge branch 'main' into option-take | Son Ho | 2024-04-25 | 10 | -100/+212 |
| |\ |
|
| * | | compiler: introduce Lean-only translations | Ryan Lahfa | 2024-04-24 | 1 | -10/+25 |
| * | | compiler: map `core::option::Option::is_none` to `Option.isNone` | Ryan Lahfa | 2024-04-24 | 1 | -0/+4 |
| * | | compiler: map `core::mem::swap` to the pure swap | Ryan Lahfa | 2024-04-24 | 1 | -0/+2 |
| * | | compiler: map `core::option::Option::take` to identity function | Ryan Lahfa | 2024-04-17 | 1 | -0/+4 |
* | | | Add core::option::unwrap builtin | Zyad Hassan | 2024-04-24 | 1 | -0/+2 |
| |/
|/| |
|
* | | Fix an issue when joining a symbolic value with bottom | Son Ho | 2024-04-22 | 2 | -11/+33 |
* | | Reformat some files | Son Ho | 2024-04-22 | 5 | -24/+47 |
* | | Merge pull request #146 from RaitoBezarius/main | Son HO | 2024-04-19 | 1 | -3/+69 |
|\ \ |
|
| * | | fix(backends/lean): extract more keywords from `lstlean.tex` | Ryan Lahfa | 2024-04-18 | 1 | -0/+2 |
| * | | fix(backends/lean): extract more keywords from `lstlean.latex` | Ryan Lahfa | 2024-04-18 | 1 | -0/+62 |
| * | | chore(backends/lean): sort the keyword list | Ryan Lahfa | 2024-04-17 | 1 | -4/+4 |
| * | | fix(backends/lean): `from` is a keyword | Ryan Lahfa | 2024-04-17 | 1 | -0/+1 |
| * | | fix(backends/lean): `as` is a keyword | Ryan Lahfa | 2024-04-17 | 1 | -0/+1 |
| |/ |
|
* / | item_meta | Nadrieril | 2024-04-18 | 9 | -80/+81 |
|/ |
|
* | Add more definitions to the Lean library | Son Ho | 2024-04-12 | 1 | -0/+73 |
* | Start adding integer functions to the Lean library | Son Ho | 2024-04-12 | 4 | -55/+181 |
* | Update the bindings for the extraction | Son Ho | 2024-04-12 | 1 | -14/+11 |
* | Merge branch 'son/clean' into checked-ops | Son Ho | 2024-04-11 | 26 | -259/+517 |
|\ |
|
| * | Update a comment | Son Ho | 2024-04-11 | 1 | -2/+2 |
| * | Merge remote-tracking branch 'origin/main' into son/clean | Son Ho | 2024-04-11 | 25 | -88/+250 |
| |\ |
|
| | * | Reformat the code | Son Ho | 2024-04-11 | 1 | -9/+6 |
| | * | Update a comment | Son HO | 2024-04-11 | 1 | -1/+1 |
| | * | Trust rustc regarding `Copy` bounds | Nadrieril | 2024-04-10 | 3 | -7/+7 |
| | * | Improve the error messages further | Son Ho | 2024-04-07 | 3 | -1/+44 |
| | * | Cleanup a bit and improve the error messages | Son Ho | 2024-04-07 | 12 | -82/+91 |
| | * | Resolved comments and added the name of the not translated element | Escherichia | 2024-04-05 | 2 | -7/+18 |
| | * | resolved comments | Escherichia | 2024-04-05 | 3 | -99/+113 |
| | * | error catching should now be able to tell when code couldn't be generated | Escherichia | 2024-04-05 | 3 | -101/+144 |
| | * | Fix a minor issue | Son Ho | 2024-04-04 | 1 | -1/+1 |
| | * | Merge remote-tracking branch 'origin/main' into escherichia/error_catching | Son Ho | 2024-04-04 | 3 | -45/+86 |
| | |\ |
|
| | * | | Update the way errors are reported | Son Ho | 2024-04-04 | 2 | -10/+7 |
| | * | | Now prints all errors in the error_list | Escherichia | 2024-04-04 | 2 | -3/+11 |
| | * | | Merge remote-tracking branch 'origin/main' into escherichia/error_catching | Escherichia | 2024-04-04 | 2 | -4/+1 |
| | |\ \ |
|
| | * | | | resolved requested changes | Escherichia | 2024-04-03 | 1 | -1/+0 |
| | * | | | resolved requested changes | Escherichia | 2024-04-03 | 3 | -6/+4 |
| | * | | | added extract_ty_errors and extract_texpression_errors to deal with the error... | Escherichia | 2024-04-03 | 2 | -3/+10 |
| | * | | | added Error and EError to expressions and propagated related changes | Escherichia | 2024-04-03 | 12 | -5/+41 |