diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-10-26 19:11:55 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-10-26 19:11:55 +0100 |
| commit | 61dd66da0561179f957087942769bd331ef212de (patch) | |
| tree | 619b98fc5377145e2fd1edf3f18e211d65bf3291 /src/common | |
| parent | f2d2bbd4a759024b716cc7f802427fdb78edfb9d (diff) | |
| download | vericert-61dd66da0561179f957087942769bd331ef212de.tar.gz vericert-61dd66da0561179f957087942769bd331ef212de.zip | |
Add many more proofs about sem_pred_expr
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/NonEmpty.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |