diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-02-27 11:55:10 -0500 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-02-27 11:55:34 -0500 |
| commit | b94f708b8ee634da2c6920f9417a7e72ca47814c (patch) | |
| tree | 19f2828e16992a663729c1b1d11007444188b0cd /src/Util | |
| parent | 1fb1958d505974a3864322d3f10f5dfa042f363a (diff) | |
added Positional wrappers for Associational operations, added correctness proof of
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/ListUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 88fb815b2..4d6555778 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1101,7 +1101,7 @@ Proof. intuition (subst; auto). Qed. -Lemma fold_right_invariant : forall {A} P (f: A -> A -> A) l x, +Lemma fold_right_invariant : forall {A B} P (f: A -> B -> B) l x, P x -> (forall y, In y l -> forall z, P z -> P (f y z)) -> P (fold_right f x l). Proof. |