From 06b24257359305114b868b5b78971cc4c6e30db1 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 12 Oct 2021 13:38:13 +0100 Subject: [sched] Small changes to definitions --- src/hls/Abstr.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src/hls') diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 957e265..271355d 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -290,7 +290,7 @@ Import NE.NonEmptyNotation. Definition predicated_ne A := NE.non_empty (pred_op * A). -Inductive predicated A := +Variant predicated A := | Psingle : A -> predicated A | Plist : predicated_ne A -> predicated A. @@ -666,8 +666,8 @@ Qed. Lemma sat_equiv : forall a b, - unsat (Por (Pand a (Pnot b)) (Pand (Pnot a) b)) -> - forall c, sat_predicate a c = sat_predicate b c. + unsat (Por (Pand a (Pnot b)) (Pand (Pnot a) b)) -> + forall c, sat_predicate a c = sat_predicate b c. Proof. unfold unsat. intros. specialize (H c); simplify. destruct (sat_predicate b c) eqn:X; @@ -677,8 +677,8 @@ Qed. Lemma sat_equiv2 : forall a b, - unsat (Por (Pand a (Pnot b)) (Pand b (Pnot a))) -> - forall c, sat_predicate a c = sat_predicate b c. + unsat (Por (Pand a (Pnot b)) (Pand b (Pnot a))) -> + forall c, sat_predicate a c = sat_predicate b c. Proof. unfold unsat. intros. specialize (H c); simplify. destruct (sat_predicate b c) eqn:X; -- cgit