diff options
| -rw-r--r-- | src/hls/Scheduleoracle.v | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v index 09b1355..b5aa86d 100644 --- a/src/hls/Scheduleoracle.v +++ b/src/hls/Scheduleoracle.v @@ -1,3 +1,7 @@ +(*| +.. coq:: none +|*) + (* * Vericert: Verified high-level synthesis. * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com> @@ -368,12 +372,6 @@ Definition empty : forest := Rtree.empty _. This function checks if all the elements in [fa] are in [fb], but not the other way round. |*) -Definition check_partial (fa fb : forest) : bool := - PTree.fold (fun b i el => b && (match PTree.get i fb with - | Some el' => beq_expression el el' - | None => false - end)) fa true. - Definition check := Rtree.beq beq_expression. Lemma check_correct: forall (fa fb : forest) (x : resource), |