From e4e615ede80e813647947bdff67453b4cc788ce2 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 6 Oct 2023 18:23:43 +0200
Subject: Finish eval_correct proof

---
 src/hls/Predicate.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/hls/Predicate.v')

diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v
index d4bc80a..7786c5d 100644
--- a/src/hls/Predicate.v
+++ b/src/hls/Predicate.v
@@ -161,6 +161,8 @@ Section PRED_DEFINITION.
 
 End PRED_DEFINITION.
 
+Definition dfltp {A} (p: option (@Predicate.pred_op A)) := Option.default Ptrue p.
+
 Notation "A ∧ B" := (Pand A B) (at level 20) : pred_op.
 Notation "A ∨ B" := (Por A B) (at level 25) : pred_op.
 Notation "⟂" := (Pfalse) : pred_op.
-- 
cgit