/* Copyright 2009-2018 EPFL, Lausanne */

package stainless.lang
import stainless.annotation._

@ignore
class Real(val theReal: scala.math.BigDecimal) {

   def +(a: Real): Real = new Real(theReal + a.theReal)
   def -(a: Real): Real = new Real(theReal - a.theReal)
   def *(a: Real): Real = new Real(theReal * a.theReal)
   def /(a: Real): Real = new Real(theReal / a.theReal)

   def unary_- : Real = new Real(- theReal)

   def > (a: Real): Boolean = theReal >  a.theReal
   def >=(a: Real): Boolean = theReal >= a.theReal
   def < (a: Real): Boolean = theReal <  a.theReal
   def <=(a: Real): Boolean = theReal <= a.theReal

}

@ignore
object Real {
  def apply(n: BigInt, d: BigInt): Real = new Real(scala.math.BigDecimal(n) / scala.math.BigDecimal(d))
  def apply(n: BigInt): Real = new Real(scala.math.BigDecimal(n))
}

/* Copyright 2009-2018 EPFL, Lausanne */

package stainless.lang
import stainless.annotation._

@ignore
class Real {

   def +(a: Real): Real = ???
   def -(a: Real): Real = ???
   def *(a: Real): Real = ???
   def /(a: Real): Real = ???

   def unary_- : Real = ???

   def > (a: Real): Boolean = ???
   def >=(a: Real): Boolean = ???
   def < (a: Real): Boolean = ???
   def <=(a: Real): Boolean = ???

}

@ignore
object Real {
  def apply(n: BigInt, d: BigInt): Real = ???
  def apply(n: BigInt): Real = ???
}

--- 
+++ 
@@ -4,24 +4,24 @@
 import stainless.annotation._
 
 @ignore
-class Real {
+class Real(val theReal: scala.math.BigDecimal) {
 
-   def +(a: Real): Real = ???
-   def -(a: Real): Real = ???
-   def *(a: Real): Real = ???
-   def /(a: Real): Real = ???
+   def +(a: Real): Real = new Real(theReal + a.theReal)
+   def -(a: Real): Real = new Real(theReal - a.theReal)
+   def *(a: Real): Real = new Real(theReal * a.theReal)
+   def /(a: Real): Real = new Real(theReal / a.theReal)
 
-   def unary_- : Real = ???
+   def unary_- : Real = new Real(- theReal)
 
-   def > (a: Real): Boolean = ???
-   def >=(a: Real): Boolean = ???
-   def < (a: Real): Boolean = ???
-   def <=(a: Real): Boolean = ???
+   def > (a: Real): Boolean = theReal >  a.theReal
+   def >=(a: Real): Boolean = theReal >= a.theReal
+   def < (a: Real): Boolean = theReal <  a.theReal
+   def <=(a: Real): Boolean = theReal <= a.theReal
 
 }
 
 @ignore
 object Real {
-  def apply(n: BigInt, d: BigInt): Real = ???
-  def apply(n: BigInt): Real = ???
+  def apply(n: BigInt, d: BigInt): Real = new Real(scala.math.BigDecimal(n) / scala.math.BigDecimal(d))
+  def apply(n: BigInt): Real = new Real(scala.math.BigDecimal(n))
 }
Add underlying operations for library reals
