From 1167bcef629e9875499cf94037f0c2dc13798b6b Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 5 Oct 2015 19:21:17 +0200
Subject: [PATCH] Remove warning
---
library/collection/List.scala | 15 +++++++--------
1 file changed, 7 insertions(+), 8 deletions(-)
diff --git a/library/collection/List.scala b/library/collection/List.scala
index 436886cca..74a0f0c66 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -673,14 +673,13 @@ object ListSpecs {
def headReverseLast[T](l: List[T]): Boolean = {
require (!l.isEmpty)
(l.head == l.reverse.last) because {
- l match {
- case Cons(x, xs) => {
- (x :: xs).head ==| trivial |
- x ==| snocLast(xs.reverse, x) |
- (xs.reverse :+ x).last ==| trivial |
- (x :: xs).reverse.last
- }.qed
- }
+ val Cons(x, xs) = l;
+ {
+ (x :: xs).head ==| trivial |
+ x ==| snocLast(xs.reverse, x) |
+ (xs.reverse :+ x).last ==| trivial |
+ (x :: xs).reverse.last
+ }.qed
}
}.holds
--
GitLab