aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/Predicate.v
Commit message (Expand)AuthorAgeFilesLines
* Add proof using to ifconversionproofYann Herklotz2022-09-291-1/+1
* Add global monad notation using InstancesYann Herklotz2022-09-261-1/+1
* Work on implementing abstract predicatesYann Herklotz2022-07-191-140/+193
* Rearrange definitions and create IfConversion templateYann Herklotz2022-06-061-0/+12
* Fix many more lemmasYann Herklotz2022-06-051-0/+9
* Work on CondElim proofYann Herklotz2022-06-031-3/+3
* Abstract useful function into Predicate.vYann Herklotz2022-05-311-0/+7
* Improve simplification of predicatesYann Herklotz2021-11-141-2/+10
* Add the tseytin transformation insteadYann Herklotz2021-11-141-210/+359
* Improve simplification of predicatesYann Herklotz2021-11-131-57/+80
* Add simplify operation and simplify IfConversionYann Herklotz2021-11-111-0/+58
* Add intermediate step in proof of sem presYann Herklotz2021-10-271-0/+26
* Work more on equivalence of SATYann Herklotz2021-10-261-0/+15
* Add type-class proofs to Predicate.vYann Herklotz2021-10-241-4/+207
* Add work towards decidability of SAT solverYann Herklotz2021-10-211-0/+201