From 61dd66da0561179f957087942769bd331ef212de Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 26 Oct 2022 19:11:55 +0100 Subject: Add many more proofs about sem_pred_expr --- src/common/NonEmpty.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/common') diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v index 31adbda..5764208 100644 --- a/src/common/NonEmpty.v +++ b/src/common/NonEmpty.v @@ -125,5 +125,5 @@ Fixpoint fold_left {A B} (f: A -> B -> A) (l: non_empty B) (a: A) {struct l} : A Fixpoint fold_right {A B} (f: B -> A -> A) (a: A) (l: non_empty B) {struct l} : A := match l with | singleton a' => f a' a - | b ::| t => fold_right f (f b a) t + | b ::| t => f b (fold_right f a t) end. -- cgit