Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | Work on finishing the SAT decidability proofs | Yann Herklotz | 2023-04-24 | 1 | -26/+44 | |
| | ||||||
* | Added lemmas about decidability of Sat | Yann Herklotz | 2023-04-24 | 3 | -117/+293 | |
| | ||||||
* | Add temp files | Yann Herklotz | 2023-03-12 | 2 | -10/+24 | |
| | ||||||
* | Work on proof of norm_expression | Yann Herklotz | 2023-02-22 | 3 | -57/+261 | |
| | ||||||
* | Remove aborted evaluable proofs | Yann Herklotz | 2023-02-18 | 1 | -96/+4 | |
| | ||||||
* | Prove abstr_fold_falsy correct | Yann Herklotz | 2023-02-12 | 1 | -21/+100 | |
| | ||||||
* | Prove sem_update_instr_term correct | Yann Herklotz | 2023-02-12 | 1 | -8/+19 | |
| | ||||||
* | Prove abstr_fold_correct inductive case fully | Yann Herklotz | 2023-02-12 | 1 | -12/+15 | |
| | ||||||
* | Finish eval_predf_update_true | Yann Herklotz | 2023-02-12 | 1 | -3/+6 | |
| | ||||||
* | Finish sem_update_instr finally | Yann Herklotz | 2023-02-12 | 4 | -3/+352 | |
| | ||||||
* | Change evaluation of predicates and remove forest_evaluable | Yann Herklotz | 2023-02-11 | 4 | -100/+125 | |
| | ||||||
* | Switch to half lazy evaluation | Yann Herklotz | 2023-02-05 | 3 | -52/+113 | |
| | ||||||
* | Work on intermediate lemma for evaluation | Yann Herklotz | 2023-01-29 | 1 | -5/+12 | |
| | ||||||
* | Prove abstr_fold_correct top-down | Yann Herklotz | 2023-01-29 | 2 | -41/+99 | |
| | ||||||
* | Add documentation and continue on top-down proof | Yann Herklotz | 2023-01-28 | 1 | -6/+54 | |
| | ||||||
* | Work on simplifying seq_app evaluation lemma | Yann Herklotz | 2023-01-02 | 2 | -6/+13 | |
| | ||||||
* | Add all_evaluable lemma for seq_app | Yann Herklotz | 2023-01-01 | 1 | -0/+9 | |
| | ||||||
* | Add proofs about evaluation of body of expressions | Yann Herklotz | 2022-12-27 | 1 | -7/+59 | |
| | ||||||
* | Add proofs about evaluability of predicates in the abstract state | Yann Herklotz | 2022-12-24 | 1 | -23/+55 | |
| | ||||||
* | Add todo | Yann Herklotz | 2022-12-01 | 1 | -76/+163 | |
| | ||||||
* | Prove top level theorems with evaluability | Yann Herklotz | 2022-11-15 | 2 | -43/+344 | |
| | ||||||
* | Add proofs about evaluability of predicates | Yann Herklotz | 2022-11-10 | 1 | -18/+132 | |
| | ||||||
* | Add many more proofs about sem_pred_expr | Yann Herklotz | 2022-10-26 | 2 | -37/+312 | |
| | ||||||
* | Add proofs for sem_pexpr and app_predicated | Yann Herklotz | 2022-10-25 | 2 | -43/+270 | |
| | ||||||
* | Prove sem_update for load and create lemma | Yann Herklotz | 2022-10-24 | 1 | -3/+51 | |
| | ||||||
* | Work on abstract lemmas for update function | Yann Herklotz | 2022-10-20 | 1 | -8/+318 | |
| | ||||||
* | Clean up proofs | Yann Herklotz | 2022-10-11 | 9 | -149/+170 | |
| | ||||||
* | Add helper functions to NonEmpty.v | Yann Herklotz | 2022-10-10 | 1 | -0/+18 | |
| | ||||||
* | [sched] Remove some unprovable lemmas | Yann Herklotz | 2022-10-06 | 5 | -901/+179 | |
| | ||||||
* | Add new if-conversion pass with top-level fold | Yann Herklotz | 2022-09-29 | 3 | -65/+83 | |
| | ||||||
* | Removing duplication in flake.nix file | Yann Herklotz | 2022-09-29 | 1 | -47/+13 | |
| | ||||||
* | Add dune-project fileHEADmasterdev/mac-op | Yann Herklotz | 2022-09-29 | 2 | -1/+2 | |
| | ||||||
* | Fix CI runs using flake | Yann Herklotz | 2022-09-29 | 1 | -5/+3 | |
| | ||||||
* | Remove dependency on man page for install | Yann Herklotz | 2022-09-29 | 1 | -1/+1 | |
| | ||||||
* | Add build flag for BSD architecture | Yann Herklotz | 2022-09-29 | 1 | -0/+3 | |
| | ||||||
* | Add proof using to ifconversionproof | Yann Herklotz | 2022-09-29 | 3 | -171/+30 | |
| | ||||||
* | Add global monad notation using Instances | Yann Herklotz | 2022-09-26 | 10 | -104/+169 | |
| | | | | This was mostly inspired by the std++ library. | |||||
* | Add more monads | Yann Herklotz | 2022-09-24 | 3 | -1/+63 | |
| | ||||||
* | Update and fix the transformation | Yann Herklotz | 2022-08-05 | 5 | -273/+314 | |
| | ||||||
* | Add back changes to Abstr | Yann Herklotz | 2022-08-04 | 3 | -248/+364 | |
| | ||||||
* | Add forest type | Yann Herklotz | 2022-08-01 | 1 | -3/+8 | |
| | ||||||
* | Merge remote-tracking branch 'origin/dev/scheduling' into dev/scheduling | Yann Herklotz | 2022-07-31 | 3 | -112/+115 | |
|\ | ||||||
| * | Add current changes | Yann Herklotz | 2022-07-31 | 2 | -112/+5 | |
| | | ||||||
| * | Add NonEmpty.v | Yann Herklotz | 2022-07-31 | 1 | -0/+110 | |
| | | ||||||
* | | Start refactor in Abstr | Yann Herklotz | 2022-07-31 | 1 | -14/+29 | |
|/ | ||||||
* | Update lemmas with new update function | Yann Herklotz | 2022-07-26 | 1 | -35/+128 | |
| | ||||||
* | Fix main proof | Yann Herklotz | 2022-07-20 | 1 | -21/+27 | |
| | ||||||
* | Add the opion monad file | Yann Herklotz | 2022-07-20 | 1 | -0/+66 | |
| | ||||||
* | Work on implementing abstract predicates | Yann Herklotz | 2022-07-19 | 16 | -388/+528 | |
| | ||||||
* | Add work on abstract predicates | Yann Herklotz | 2022-07-14 | 6 | -96/+377 | |
| |