From 96449c6134e95378e3edf811f048961ec5fb466c Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 11 Mar 2016 16:41:00 +0100
Subject: [PATCH] no need for isRat postconditions
---
library/lang/Rational.scala | 12 ++++++------
1 file changed, 6 insertions(+), 6 deletions(-)
diff --git a/library/lang/Rational.scala b/library/lang/Rational.scala
index 1bcb679a0..fcdb64cc1 100644
--- a/library/lang/Rational.scala
+++ b/library/lang/Rational.scala
@@ -13,31 +13,31 @@ case class Rational(numerator: BigInt, denominator: BigInt) {
def +(that: Rational): Rational = {
Rational(this.numerator*that.denominator + that.numerator*this.denominator, this.denominator*that.denominator)
- } ensuring(res => res.isRational)
+ }
def -(that: Rational): Rational = {
Rational(this.numerator*that.denominator - that.numerator*this.denominator, this.denominator*that.denominator)
- } ensuring(res => res.isRational)
+ }
def unary_- : Rational = {
Rational(-this.numerator, this.denominator)
- } ensuring(res => res.isRational)
+ }
def *(that: Rational): Rational = {
Rational(this.numerator*that.numerator, this.denominator*that.denominator)
- } ensuring(res => res.isRational)
+ }
def /(that: Rational): Rational = {
require(that.nonZero)
val newNumerator = this.numerator*that.denominator
val newDenominator = this.denominator*that.numerator
normalize(newNumerator, newDenominator)
- } ensuring(res => res.isRational)
+ }
def reciprocal: Rational = {
require(this.nonZero)
normalize(this.denominator, this.numerator)
- } ensuring(res => res.isRational)
+ }
def ~(that: Rational): Boolean = {
--
GitLab