diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-12 20:27:20 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-12 20:27:20 +0000 |
| commit | 86c9c7cec60a2e302a317acadc559cb6e3c481f5 (patch) | |
| tree | d455814d236b0bfdaa28ca45e04434a2ec10e284 /src/hls | |
| parent | f77ef7aa3ecda17e3280846419223f24e4685f5f (diff) | |
| download | vericert-86c9c7cec60a2e302a317acadc559cb6e3c481f5.tar.gz vericert-86c9c7cec60a2e302a317acadc559cb6e3c481f5.zip | |
Remove unnecessary definition of check
Diffstat (limited to 'src/hls')
| -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), |