aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/Predicate.v
Commit message (Expand)AuthorAgeFilesLines
* Finish load proofdev/schedulingYann Herklotz2023-11-051-0/+6
* Changed and proved some more theoremsYann Herklotz2023-10-301-0/+26
* Finish eval_correct proofYann Herklotz2023-10-061-0/+2
* Add equivalence classesYann Herklotz2023-07-111-0/+33
* Finish some proofs and remove unnecessary AdmittedYann Herklotz2023-06-261-3/+3
* Prove more admitted theoremsYann Herklotz2023-05-291-2/+24
* Split proof up into more filesYann Herklotz2023-05-091-0/+6
* Finish forward and backward proofs for predicated proofYann Herklotz2023-05-051-8/+0
* Try and prove equivalence of predicated thingsYann Herklotz2023-05-051-0/+8
* Continue proofs about Abstr.vYann Herklotz2023-05-041-31/+18
* Add structural equality for predicatesYann Herklotz2023-05-021-0/+29
* Update Sat.v namesYann Herklotz2023-04-281-63/+63
* Change nat to positive in Sat proofYann Herklotz2023-04-271-18/+17
* Finish sem_update_instr finallyYann Herklotz2023-02-121-0/+52
* Change evaluation of predicates and remove forest_evaluableYann Herklotz2023-02-111-0/+50
* 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
generated by cgit (git 2.34.1) at 2024-06-08 13:22:34 +0000