aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/GiblePargenproofForward.v
Commit message (Collapse)AuthorAgeFilesLines
* Annonimize submissiondev/asplosYann Herklotz2023-08-101-1/+1
|
* Add equivalence classesYann Herklotz2023-07-111-99/+0
|
* Finish mutual exclusivity checkYann Herklotz2023-06-251-2/+2
|
* Finished the propert version of from_predicated_sem_pred_expr2Yann Herklotz2023-06-021-14/+19
|
* Prove more admitted theoremsYann Herklotz2023-05-291-12/+12
|
* Finish proofs in GiblePargenproofForward.vYann Herklotz2023-05-281-3/+45
|
* Work on forward proofsYann Herklotz2023-05-281-1/+3
|
* Prove evaluable_pred_expr_exists_RBsetpredYann Herklotz2023-05-211-6/+0
|
* Finish evaluability proof of RBopYann Herklotz2023-05-191-190/+1
|
* Add new proofs about semantic identityYann Herklotz2023-05-181-521/+1
|
* Split proof up into more filesYann Herklotz2023-05-091-0/+1568