summaryrefslogtreecommitdiff
path: root/compiler/ExtractTypes.ml (follow)
Commit message (Expand)AuthorAgeFilesLines
* had some fun writing an IsabelleHOL backendstuebinm2024-06-291-40/+65
* Remove redundant `llbc_name` fieldNadrieril2024-06-281-8/+8
* Update charonNadrieril2024-06-241-3/+3
* Support for renaming using the rename attribute in charon (#239)Escherichia2024-06-181-70/+92
* Tiny dedupNadrieril2024-06-181-10/+1
* Update the code extraction and regenerate the testsSon Ho2024-06-121-5/+9
* Revert "Update the scalar notation for the Lean backend"Son Ho2024-06-121-1/+1
* Update the scalar notation for the Lean backendSon Ho2024-06-121-1/+1
* Add an option to run Aeneas as a borrow checkerSon Ho2024-06-051-81/+92
* Factor out the code for Lean and CoqSon Ho2024-05-241-143/+41
* Merge branch 'main' into afromher/recursive_projectorsSon Ho2024-05-241-136/+138
|\
| * Rename meta into spanAymeric Fromherz2024-05-241-129/+131
| * Rename span into raw_spanAymeric Fromherz2024-05-241-8/+8
* | Add simp, reducible attributes to generated Lean projectorsAymeric Fromherz2024-05-231-0/+10
* | Improve formatting of Lean struct projectorsAymeric Fromherz2024-05-231-2/+6
* | Add printing of projectors for recursive structs in Lean backendAymeric Fromherz2024-05-231-3/+130
|/
* Catch new literal variantsNadrieril2024-05-141-0/+3
* Update charonNadrieril2024-05-061-0/+3
* Start adding integer functions to the Lean librarySon Ho2024-04-121-4/+11
* added extract_ty_errors and extract_texpression_errors to deal with the error...Escherichia2024-04-031-1/+8
* added Error and EError to expressions and propagated related changesEscherichia2024-04-031-0/+1
* Add some missing error messagesSon Ho2024-03-291-2/+2
* formatting and changed save_error condition for failing from b to not bEscherichia2024-03-291-3/+6
* added file and line arg to craise and cassertEscherichia2024-03-291-29/+29
* formattingEscherichia2024-03-281-62/+105
* changes after git rebase mainEscherichia2024-03-281-1/+1
* Should answer all comments, there are still some TODO: error message leftEscherichia2024-03-281-17/+16
* Added sanity_check and sanity_check_opt_meta helpers and changed sanity check...Escherichia2024-03-281-3/+3
* changes to extract_ty and related functions to use the right metaEscherichia2024-03-281-12/+12
* Still need to fill the TODO: error message and check some meta but it buildsEscherichia2024-03-281-22/+23
* WIP: translate.ml and extract.ml do not compile. Some assert left to do and w...Escherichia2024-03-281-108/+109
* Update following changes in CharonSon Ho2024-03-171-6/+1
* Update the name generation and add CLI to print external pat namesSon Ho2024-03-101-6/+17
* Make progress on propagating the changesSon Ho2024-03-081-1/+1
* Update the code generationSon Ho2024-03-081-5/+0
* Update the extraction to handle casts between integers/boolsSon Ho2023-12-131-21/+60
* Fix the extraction of the empty typeSon Ho2023-12-071-12/+18
* Fix minor issues when extracting a structure with one field as a tupleSon Ho2023-12-071-0/+11
* Use a better syntax when extracting tuple types (structures with unnamed fields)Son Ho2023-12-071-96/+134
* Fix a minor issue with the extractionSon Ho2023-11-291-4/+5
* Add support for more bitwise operations and update the extractionSon Ho2023-11-291-2/+12
* Merge branch 'main' into afromher_shiftsSon Ho2023-11-291-1/+3
* Fix the issues with the cross-references for OCaml docSon Ho2023-11-271-1/+1
* Improve further the generation of parent clause/trait clause namesSon Ho2023-11-221-2/+3
* Reorganize the "Extract" filesSon Ho2023-11-211-874/+106
* Make minor updates to the extraction of spansSon Ho2023-11-211-4/+5
* Add span information to the generated codeSon Ho2023-11-211-1/+14
* Use the name matcher implemented in CharonSon Ho2023-11-201-84/+22
* Fix a minor issueSon Ho2023-11-161-1/+6
* Finish propagating the changes to the names and cleaningSon Ho2023-11-161-47/+108
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 10:09:31 +0000