aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/AbstrSemIdent.v
Commit message (Expand)AuthorAgeFilesLines
* Finished the propert version of from_predicated_sem_pred_expr2Yann Herklotz2023-06-021-24/+98
* Finish from_predicated_sem_pred_exprYann Herklotz2023-05-311-8/+97
* Remove unnecessary assumption from sem_merge_listYann Herklotz2023-05-301-4/+3
* Fix other proofs and attempt from_predicated proofYann Herklotz2023-05-301-7/+26
* Prove merge list_translationYann Herklotz2023-05-301-2/+16
* Prove fold_right over ElistYann Herklotz2023-05-301-4/+74
* Finish second flap2 proofYann Herklotz2023-05-301-1/+9
* Finished painful product proofYann Herklotz2023-05-301-4/+115
* Prove more admitted theoremsYann Herklotz2023-05-291-18/+108
* Finish two AbstrSemIdent false proofsYann Herklotz2023-05-281-11/+50
* Prove evaluable_pred_expr_exists_RBsetpredYann Herklotz2023-05-211-1/+19
* Finish evaluability proof of RBopYann Herklotz2023-05-191-3/+4
* Add new proofs about semantic identityYann Herklotz2023-05-181-0/+665