summaryrefslogtreecommitdiff
path: root/compiler (unfollow)
Commit message (Expand)AuthorFilesLines
2023-08-04Fix issues with the extraction and extend the primitive libraries for Coq and F*Son Ho2-12/+12
2023-08-04Add SliceLen as a primitive function and make minor adjustmentsSon Ho5-35/+62
2023-08-04Start adding support for Arrays/Slices in the Lean librarySon Ho1-10/+12
2023-08-03Fix an issue with the extraction of aggregated arraysSon Ho10-180/+320
2023-08-03Make a minor formatting modification for LeanSon Ho1-1/+1
2023-08-03Fix issuesSon Ho10-57/+139
2023-08-02Make minor modificationsSon Ho3-16/+29
2023-08-02Add the function signatures in Assumed.mlSon Ho1-0/+143
2023-08-02Make more progressSon Ho2-75/+186
2023-08-02Make progressSon Ho5-53/+80
2023-08-02Make progressSon Ho14-76/+178
2023-08-02Make progressSon Ho7-164/+232
2023-08-02Make progress proapagating the changesSon Ho25-273/+407
2023-08-01Start adding support for const genericsSon Ho11-226/+246
2023-07-12Make the `by inlit` implicitSon Ho1-1/+1
2023-07-06Use short names for the structure fields in LeanSon Ho5-19/+78
2023-07-06Improve the generated commentsSon Ho3-24/+102
2023-07-05Simplify the names used in Primitives.leanSon Ho1-16/+33
2023-07-05Simplify the generated names for the types in LeanSon Ho1-5/+12
2023-07-05Start using namespaces in the Lean backendSon Ho5-45/+84
2023-07-04Fix minor issuesSon Ho2-55/+125
2023-07-04Fix some issues with the extraction to LeanSon Ho1-48/+86
2023-07-04Reorganize the Lean testsSon Ho5-43/+62
2023-06-04Make progress on the HOL4 backendSon Ho2-39/+80
2023-06-04Make progress on extracting the HOL4 filesSon Ho3-16/+103
2023-06-04Make the unfolding theorems collection from evalLib persistentSon Ho1-9/+13
2023-06-04Make good progress on generating code for HOL4Son Ho8-487/+1217
2023-06-04Use dune 3.7 and update the flake.lockSon Ho3-5/+5
2023-06-04Add a sanity check in Driver.mlSon Ho1-0/+13
2023-06-04Make more updates for the Lean backendSon Ho2-26/+43
2023-06-04Make minor modificationsSon Ho2-3/+23
2023-06-04Update Extract.mlSon Ho1-15/+35
2023-06-04Make extract_adt_cons call extract_adt_g_valueSon Ho1-54/+15
2023-06-04Make a minor fixSon Ho1-7/+1
2023-06-04Improve the generation of variant names for LeanSon Ho3-15/+33
2023-06-04Improve simplify_aggregates to introduce structure updatesSon Ho2-3/+48
2023-06-04Start updating simplify_aggregatesSon Ho1-2/+43
2023-06-04Add a special expression for structure creation/updateSon Ho9-182/+451
2023-06-04Don't create useless directories in LeanSon Ho1-2/+4
2023-06-04Update the extraction of Lean filesSon Ho2-25/+51
2023-06-04Reorganize the Lean tests and extract the Polonius tests to LeanSon Ho1-1/+1
2023-06-04Remove the symbolic interpreter testsSon Ho2-35/+0
2023-06-04Automate the generation of the lakefile.lean filesSon Ho2-120/+167
2023-06-04Add a check in Driver.mlSon Ho1-0/+12
2023-06-04Handle the "opaque_defs." prefix in a cleaner mannerSon Ho3-95/+253
2023-06-04Make minor modificationsSon Ho1-41/+89
2023-06-04Consistently use the names TerminationMeasure and DecreasesProofSon Ho5-61/+108
2023-06-04Update the generation of termination and decreases_by templates for LeanSon Ho2-28/+39
2023-06-04Add more checks in Driver.mlSon Ho2-3/+8
2023-06-04Print warnings for the Lean backend and loopsSon Ho1-8/+13
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 12:37:00 +0000