Commit message (Expand) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| * | | | Update the ci.yml | Son Ho | 2023-11-10 | 1 | -2/+2 | |
| * | | | Update the ci.yml | Son Ho | 2023-11-10 | 1 | -1/+1 | |
| * | | | Update the ci.yml | Son Ho | 2023-11-10 | 1 | -3/+5 | |
| * | | | Update the ci.yml | Son Ho | 2023-11-10 | 1 | -1/+1 | |
| * | | | Update the ci.yml | Son Ho | 2023-11-10 | 1 | -3/+3 | |
| * | | | Update the ci.yml | Son Ho | 2023-11-10 | 1 | -1/+5 | |
| * | | | Make a minor fix | Son Ho | 2023-11-10 | 1 | -1/+1 | |
| * | | | Make a minor update | Son Ho | 2023-11-10 | 1 | -2/+2 | |
| * | | | Update the ci.yml | Son Ho | 2023-11-10 | 1 | -0/+5 | |
| * | | | Update the flake.lock | Son Ho | 2023-11-10 | 1 | -93/+44 | |
| * | | | Merge branch 'main' into son_traits_types | Son Ho | 2023-11-09 | 2 | -1/+19 | |
| |\ \ \ | |/ / / |/| | | | ||||||
* | | | | Merge pull request #43 from AeneasVerif/pnmadelaine-ci | Son HO | 2023-10-23 | 2 | -1/+19 | |
|\ \ \ \ | ||||||
| * | | | | ci: hydra -> github runner | Paul-Nicolas Madelaine | 2023-10-23 | 2 | -1/+19 | |
|/ / / / | ||||||
| * | | | Update the rule build-bin-dir in the Makefile | Son Ho | 2023-11-09 | 1 | -3/+6 | |
| * | | | Make administrative updates in the tests | Son Ho | 2023-11-09 | 2 | -405/+49 | |
| * | | | Update the failing proofs | Son Ho | 2023-11-09 | 16 | -1710/+1049 | |
| * | | | Regenerate the Coq test files | Son Ho | 2023-11-09 | 14 | -80/+1403 | |
| * | | | Make the traits work for Coq | Son Ho | 2023-11-09 | 7 | -194/+354 | |
| * | | | Deactivate the HOL4 tests | Son Ho | 2023-11-09 | 1 | -2/+10 | |
| * | | | Remove a file | Son Ho | 2023-11-09 | 1 | -387/+0 | |
| * | | | Update the Makefile for the F* array test | Son Ho | 2023-11-09 | 1 | -1/+1 | |
| * | | | Regenerate the tests | Son Ho | 2023-11-09 | 2 | -94/+37 | |
| * | | | Extract the trait parent clauses after the types and the constants | Son Ho | 2023-11-09 | 1 | -24/+25 | |
| * | | | Progress on making the traits work for F* | Son Ho | 2023-11-09 | 6 | -36/+1616 | |
| * | | | Modify some options and update the Makefile | Son Ho | 2023-11-09 | 11 | -1082/+2280 | |
| * | | | Update the Makefile to rename the "trans-" rules to "test-" | Son Ho | 2023-11-09 | 1 | -46/+46 | |
| * | | | Regenerate some Lean tests | Son Ho | 2023-11-09 | 2 | -0/+39 | |
| * | | | Fix a small issue in AssociatedTypes | Son Ho | 2023-11-09 | 7 | -15/+21 | |
| * | | | Update the Makefile and regenerate some tests | Son Ho | 2023-11-08 | 4 | -0/+40 | |
| * | | | Update the extraction | Son Ho | 2023-11-07 | 3 | -2/+15 | |
| * | | | Update the normalization of associated types | Son Ho | 2023-11-07 | 4 | -50/+126 | |
| * | | | Fix a naming issue | Son Ho | 2023-11-06 | 1 | -1/+3 | |
| * | | | Regenerate part of the trait tests for Lean | Son Ho | 2023-11-06 | 2 | -16/+65 | |
| * | | | Fix some issues when extracting references to Self | Son Ho | 2023-11-06 | 1 | -30/+57 | |
| * | | | Update following some changes in Charon | Son Ho | 2023-11-06 | 5 | -58/+68 | |
| * | | | Make minor updates following changes in Charon | Son Ho | 2023-10-30 | 2 | -6/+2 | |
| * | | | Add some files for the Coq trait tests | Son Ho | 2023-10-27 | 2 | -0/+28 | |
| * | | | Fix minor issues in the name collision detection | Son Ho | 2023-10-27 | 2 | -10/+23 | |
| * | | | Regenerate the Coq test files | Son Ho | 2023-10-27 | 24 | -2118/+3589 | |
| * | | | Update Primitives.v | Son Ho | 2023-10-27 | 1 | -60/+342 | |
| * | | | Regenerate more F* files | Son Ho | 2023-10-27 | 18 | -1549/+1427 | |
| * | | | Fix a minor issue and regenerate some F* test files | Son Ho | 2023-10-27 | 10 | -602/+646 | |
| * | | | Regenerate some of the F* test files | Son Ho | 2023-10-27 | 19 | -440/+549 | |
| * | | | Make minor modifications and update the array test for F* | Son Ho | 2023-10-26 | 6 | -188/+200 | |
| * | | | Update Primitives.fst | Son Ho | 2023-10-26 | 8 | -318/+2757 | |
| * | | | Fix some issues and regenerate the HashmapMain example for Lean | Son Ho | 2023-10-26 | 5 | -106/+147 | |
| * | | | Regenerate the betree example for Lean | Son Ho | 2023-10-26 | 1 | -40/+39 | |
| * | | | Regenerate several test files for Lean | Son Ho | 2023-10-26 | 4 | -122/+132 | |
| * | | | Improve the handling of saved function effects in ExtractBuiltin.ml | Son Ho | 2023-10-26 | 2 | -24/+44 | |
| * | | | Regenerate the array files for Lean | Son Ho | 2023-10-26 | 2 | -111/+103 |