src/HOL/Library/Efficient_Nat.thy
changeset 38206 3bf1fffcdd48
parent 38195 9728342bcd56
child 39004 f9cd27cbe8a4
equal deleted inserted replaced
38205:52fdcb76c0af 38206:3bf1fffcdd48
   305   def equals(that: Nat): Boolean = this.value == that.value
   305   def equals(that: Nat): Boolean = this.value == that.value
   306 
   306 
   307   def as_BigInt: BigInt = this.value
   307   def as_BigInt: BigInt = this.value
   308   def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
   308   def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
   309       this.value.intValue
   309       this.value.intValue
   310     else this.value.intValue
   310     else error("Int value out of range: " + this.value.toString)
   311 
   311 
   312   def +(that: Nat): Nat = new Nat(this.value + that.value)
   312   def +(that: Nat): Nat = new Nat(this.value + that.value)
   313   def -(that: Nat): Nat = Nat(this.value - that.value)
   313   def -(that: Nat): Nat = Nat(this.value - that.value)
   314   def *(that: Nat): Nat = new Nat(this.value * that.value)
   314   def *(that: Nat): Nat = new Nat(this.value * that.value)
   315 
   315