aboutsummaryrefslogtreecommitdiffstats
path: root/src/common/NonEmpty.v
Commit message (Expand)AuthorAgeFilesLines
* Finish forward and backward proofs for predicated proofYann Herklotz2023-05-051-0/+5
* Add relations to the NonEmpty moduleYann Herklotz2023-05-021-0/+77
* Add many more proofs about sem_pred_exprYann Herklotz2022-10-261-1/+1
* Add proofs for sem_pexpr and app_predicatedYann Herklotz2022-10-251-0/+1
* Add helper functions to NonEmpty.vYann Herklotz2022-10-101-0/+18
* Add NonEmpty.vYann Herklotz2022-07-311-0/+110