diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-21 14:42:03 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-21 14:42:03 +0100 |
| commit | fc4bc25ca5d986831a02cddd87264b7b51943fc4 (patch) | |
| tree | 075f6cf97f3a35a0c6d34650806b295573288c5f /src/hls/GiblePargenproofForward.v | |
| parent | 28352e0b7c53f7b0d3e610bf8507ee4b0901171d (diff) | |
| download | vericert-fc4bc25ca5d986831a02cddd87264b7b51943fc4.tar.gz vericert-fc4bc25ca5d986831a02cddd87264b7b51943fc4.zip | |
Prove evaluable_pred_expr_exists_RBsetpred
Diffstat (limited to 'src/hls/GiblePargenproofForward.v')
| -rw-r--r-- | src/hls/GiblePargenproofForward.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v index bd18855..6411351 100644 --- a/src/hls/GiblePargenproofForward.v +++ b/src/hls/GiblePargenproofForward.v @@ -332,12 +332,6 @@ all be evaluable. predicated_not_inP pred (forest_exit f). Proof. Admitted. - Lemma from_predicated_sem_pred_expr : - forall A (ctx: @ctx A) preds pe b, - sem_pred_expr preds sem_pred ctx pe b -> - sem_pexpr ctx (from_predicated true preds pe) b. - Proof. Admitted. - Lemma sem_update_Isetpred: forall A (ctx: @ctx A) f pr p0 c args b rs m, valid_mem (ctx_mem ctx) m -> |