| Commit message (Expand) | Author | Files | Lines |
2024-05-24 | Rename meta into span | Aymeric Fromherz | 1 | -16/+16 |
2024-05-24 | Rename span into raw_span | Aymeric Fromherz | 1 | -1/+1 |
2024-04-04 | Update the extraction | Son Ho | 1 | -1/+1 |
2024-04-03 | added Error and EError to expressions and propagated related changes | Escherichia | 1 | -0/+8 |
2024-03-20 | Improve the generation of pretty name and the micro passes | Son Ho | 1 | -1/+7 |
2024-03-18 | Make good progress on adding generics to global constants | Son Ho | 1 | -0/+20 |
2024-03-17 | Update following changes in Charon | Son Ho | 1 | -4/+2 |
2024-03-11 | Update the generation of names | Son Ho | 1 | -2/+2 |
2024-03-08 | Make progress on propagating the changes | Son Ho | 1 | -3/+1 |
2023-12-22 | Fix the output type of the loops backward functions | Son Ho | 1 | -3/+1 |
2023-12-21 | Fix several issues | Son Ho | 1 | -17/+0 |
2023-12-21 | Simplify the type of the merged fwd/back functions | Son Ho | 1 | -0/+6 |
2023-12-15 | Make progress on propagating the changes | Son Ho | 1 | -2/+1 |
2023-12-15 | Make good progress on updating SymbolicToPure | Son Ho | 1 | -3/+4 |
2023-12-15 | Make progress on generalizing the signature information | Son Ho | 1 | -40/+90 |
2023-12-15 | Make minor modifications | Son Ho | 1 | -4/+5 |
2023-12-14 | Start updating Pure.fun_sig_info to handle merged forward and backward functions | Son Ho | 1 | -4/+20 |
2023-12-13 | Update the extraction to handle casts between integers/bools | Son Ho | 1 | -1/+1 |
2023-12-13 | Update Pure.fun_sig_info | Son Ho | 1 | -14/+16 |
2023-12-13 | Add the num_fwd_inputs_no_fuel_no_state field in Pure.fun_sig | Son Ho | 1 | -3/+5 |
2023-11-27 | Fix the issues with the cross-references for OCaml doc | Son Ho | 1 | -2/+2 |
2023-11-22 | Improve further the generation of parent clause/trait clause names | Son Ho | 1 | -0/+27 |
2023-11-21 | Add span information to the generated code | Son Ho | 1 | -2/+11 |
2023-11-21 | Add an `is_local` field to declarations | Son Ho | 1 | -0/+4 |
2023-11-16 | Finish propagating the changes to the names and cleaning | Son Ho | 1 | -0/+1 |
2023-11-15 | Start updating the name type, cleanup the names and the module abbrevs | Son Ho | 1 | -10/+17 |
2023-11-12 | Prefix variants related to types with "T" | Son Ho | 1 | -12/+12 |
2023-11-12 | Remove the 'r type variable from the ty type definition | Son Ho | 1 | -7/+5 |
2023-11-07 | Update the normalization of associated types | Son Ho | 1 | -0/+1 |
2023-11-06 | Update following some changes in Charon | Son Ho | 1 | -0/+1 |
2023-10-30 | Make minor updates following changes in Charon | Son Ho | 1 | -1/+0 |
2023-10-25 | Make the hashmap files typecheck again in Lean | Son Ho | 1 | -2/+2 |
2023-10-25 | Update following the addition of raw pointers | Son Ho | 1 | -1/+17 |
2023-10-23 | Remove some assumed types and add more support for builtin definitions | Son Ho | 1 | -11/+1 |
2023-09-11 | Make progress on correctly handling trait method calls in the symbolic execution | Son Ho | 1 | -3/+11 |
2023-09-10 | Add support for the trait associated constants | Son Ho | 1 | -1/+3 |
2023-09-03 | Make progress on the extraction | Son Ho | 1 | -0/+44 |
2023-09-03 | Make progress on the extraction | Son Ho | 1 | -3/+13 |
2023-08-31 | Finish updating SymbolicToPure.ml | Son Ho | 1 | -3/+4 |
2023-08-31 | Start adding support for traits | Son Ho | 1 | -11/+89 |
2023-08-18 | Update following the introduction of ConstantExpr | Son Ho | 1 | -0/+2 |
2023-08-03 | Fix an issue with the extraction of aggregated arrays | Son Ho | 1 | -42/+97 |
2023-08-02 | Make progress | Son Ho | 1 | -5/+1 |
2023-08-02 | Make progress | Son Ho | 1 | -0/+1 |
2023-08-02 | Make progress | Son Ho | 1 | -3/+7 |
2023-08-02 | Make progress proapagating the changes | Son Ho | 1 | -13/+30 |
2023-08-01 | Start adding support for const generics | Son Ho | 1 | -17/+7 |
2023-07-05 | Start using namespaces in the Lean backend | Son Ho | 1 | -3/+7 |
2023-06-04 | Add a special expression for structure creation/update | Son Ho | 1 | -10/+91 |
2023-06-04 | Custom syntax support for structures in Lean | Jonathan Protzenko | 1 | -11/+11 |