From fc4bc25ca5d986831a02cddd87264b7b51943fc4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 21 May 2023 14:42:03 +0100 Subject: Prove evaluable_pred_expr_exists_RBsetpred --- src/hls/GiblePargenproofForward.v | 6 ------ 1 file changed, 6 deletions(-) (limited to 'src/hls/GiblePargenproofForward.v') 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 -> -- cgit