summaryrefslogtreecommitdiff
path: root/compiler/Extract.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-28Remove redundant `llbc_name` fieldNadrieril1-28/+33
2024-06-24Update charonNadrieril1-5/+5
2024-06-18Support for renaming using the rename attribute in charon (#239)Escherichia1-120/+173
2024-06-17Automatically add a @[reducible] attribute to some generated functionsSon Ho1-0/+4
2024-06-12Update the code extraction and regenerate the testsSon Ho1-2/+4
2024-06-05Add an option to run Aeneas as a borrow checkerSon Ho1-90/+95
2024-05-24Rename meta into spanAymeric Fromherz1-214/+214
2024-05-24Rename span into raw_spanAymeric Fromherz1-7/+7
2024-04-12Start adding integer functions to the Lean librarySon Ho1-4/+9
2024-04-07Cleanup a bit and improve the error messagesSon Ho1-1/+2
2024-04-05resolved commentsEscherichia1-91/+93
2024-04-05error catching should now be able to tell when code couldn't be generatedEscherichia1-89/+92
2024-04-04Update the extractionSon Ho1-3/+3
2024-04-03added extract_ty_errors and extract_texpression_errors to deal with the error...Escherichia1-2/+2
2024-04-03added Error and EError to expressions and propagated related changesEscherichia1-0/+8
2024-03-29Cleanup and fix a mistakeSon Ho1-7/+5
2024-03-29Add some missing error messagesSon Ho1-5/+2
2024-03-29Improve the error messagesSon Ho1-1/+4
2024-03-29formatting and changed save_error condition for failing from b to not bEscherichia1-4/+11
2024-03-29added file and line arg to craise and cassertEscherichia1-25/+25
2024-03-28formattingEscherichia1-111/+185
2024-03-28changes after git rebase mainEscherichia1-6/+8
2024-03-28Should answer all comments, there are still some TODO: error message leftEscherichia1-19/+18
2024-03-28Added sanity_check and sanity_check_opt_meta helpers and changed sanity check...Escherichia1-2/+2
2024-03-28changes to extract_ty and related functions to use the right metaEscherichia1-29/+29
2024-03-28Still need to fill the TODO: error message and check some meta but it buildsEscherichia1-2/+2
2024-03-28WIP: translate.ml and extract.ml do not compile. Some assert left to do and w...Escherichia1-183/+187
2024-03-18Update extract_trait_implSon Ho1-7/+23
2024-03-18Fix the extraction of trait constantsSon Ho1-3/+5
2024-03-18Make good progress on adding generics to global constantsSon Ho1-24/+83
2024-03-17Update following changes in CharonSon Ho1-5/+1
2024-03-11Update the generation of namesSon Ho1-2/+2
2024-03-10Update the name generation and add CLI to print external pat namesSon Ho1-16/+44
2024-03-08Make progress on propagating the changesSon Ho1-287/+157
2024-03-08Update the code generated for tuple projectorsSon Ho1-18/+39
2024-03-08Fix tuple indexing for Lean backendZyad Hassan1-4/+33
2024-03-08Update the generation of constant bodies for LeanSon Ho1-2/+1
2024-02-02Start fixing the testsSon Ho1-1/+1
2023-12-23Fix an issue when deconstructing tuples in CoqSon Ho1-2/+8
2023-12-22Annotate the bound vars in the lambdas for CoqSon Ho1-20/+36
2023-12-22Fix a minor extraction issueSon Ho1-1/+1
2023-12-22Slightly update the formatting of the do blocksSon Ho1-24/+26
2023-12-21Update the formatting of commentsSon Ho1-8/+6
2023-12-21Remove some asserts which are now uselessSon Ho1-4/+0
2023-12-21Make good progress on merging the fwd/back functionsSon Ho1-1/+3
2023-12-18Do not register the names of the back funs if they are merged with the fwd funsSon Ho1-3/+8
2023-12-15Make progress on propagating the changesSon Ho1-4/+4
2023-12-15Make progress on generalizing the signature informationSon Ho1-4/+4
2023-12-13Update Pure.fun_sig_infoSon Ho1-2/+6
2023-12-07Fix minor issues when extracting a structure with one field as a tupleSon Ho1-21/+34
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 19:43:25 +0000