src/HOL/Library/Efficient_Nat.thy
changeset 34902 780172c006e1
parent 34899 8674bb6f727b
child 34944 970e1466028d
equal deleted inserted replaced
34901:0d6a2ae86525 34902:780172c006e1
   307   override def toString(): String = this.value.toString
   307   override def toString(): String = this.value.toString
   308 
   308 
   309   def equals(that: Nat): Boolean = this.value == that.value
   309   def equals(that: Nat): Boolean = this.value == that.value
   310 
   310 
   311   def as_BigInt: BigInt = this.value
   311   def as_BigInt: BigInt = this.value
       
   312   def as_Int: Int = this.value
   312 
   313 
   313   def +(that: Nat): Nat = new Nat(this.value + that.value)
   314   def +(that: Nat): Nat = new Nat(this.value + that.value)
   314   def -(that: Nat): Nat = Nat(this.value + that.value)
   315   def -(that: Nat): Nat = Nat(this.value + that.value)
   315   def *(that: Nat): Nat = new Nat(this.value * that.value)
   316   def *(that: Nat): Nat = new Nat(this.value * that.value)
   316 
   317 
   405 
   406 
   406 code_const Code_Numeral.of_nat
   407 code_const Code_Numeral.of_nat
   407   (SML "IntInf.toInt")
   408   (SML "IntInf.toInt")
   408   (OCaml "_")
   409   (OCaml "_")
   409   (Haskell "fromEnum")
   410   (Haskell "fromEnum")
   410   (Scala "!_.as'_BigInt")
   411   (Scala "!_.as'_Int")
   411 
   412 
   412 code_const Code_Numeral.nat_of
   413 code_const Code_Numeral.nat_of
   413   (SML "IntInf.fromInt")
   414   (SML "IntInf.fromInt")
   414   (OCaml "_")
   415   (OCaml "_")
   415   (Haskell "toEnum")
   416   (Haskell "toEnum")