aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/Abstr.v
Commit message (Expand)AuthorAgeFilesLines
* [sched] Add combination of equivalent expressionsYann Herklotz2021-10-141-10/+40
* [sched] Finish det proofs of basic Abstr semanticsYann Herklotz2021-10-131-27/+44
* [sched] Add more proof to sem_pred_detYann Herklotz2021-10-131-1/+6
* [sched] Add proofs of sem_pred_detYann Herklotz2021-10-131-8/+44
* [sched] Add start to proof of sem_value_detYann Herklotz2021-10-121-0/+12
* [sched] Add more lemmas into HashTreeYann Herklotz2021-10-121-10/+1
* [sched] Update Abstr.v to use HashTreeYann Herklotz2021-10-121-29/+97
* [sched] Small changes to definitionsYann Herklotz2021-10-121-5/+5
* End section in Abstr.vYann Herklotz2021-10-081-0/+2
* Add proof of beq_check_correctnessYann Herklotz2021-10-081-57/+120
* Add Abstr intermediate languageYann Herklotz2021-10-071-0/+749