diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-10-12 13:38:13 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-12 13:38:13 +0100 |
| commit | 06b24257359305114b868b5b78971cc4c6e30db1 (patch) | |
| tree | d676691919d01c48640a19fbd9887ef0c1440270 | |
| parent | ce3adde4b50ba04430a1cf0ffb0ea85168091746 (diff) | |
| download | vericert-06b24257359305114b868b5b78971cc4c6e30db1.tar.gz vericert-06b24257359305114b868b5b78971cc4c6e30db1.zip | |
[sched] Small changes to definitions
| -rw-r--r-- | src/hls/Abstr.v | 10 |
1 files changed, 5 insertions, 5 deletions
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; |