diff --git a/vstte10competition/SumAndMax.scala b/vstte10competition/SumAndMax.scala index 2410dff5d428a0ef9c12687d0f8ec023a8f682a4..973eb3cf7738cab8cd98df77fb81d7be0525b9f1 100644 --- a/vstte10competition/SumAndMax.scala +++ b/vstte10competition/SumAndMax.scala @@ -40,7 +40,8 @@ object SumAndMax { @induct def property(list : List) : Boolean = { - require(allPos(list)) + // This precondition was given in the problem but isn't actually useful :D + // require(allPos(list)) sum(list) <= size(list) * (if(list == Nil()) 0 else max(list)) } holds }