equal
deleted
inserted
replaced
160 (Eval "Integer.max/ 0") |
160 (Eval "Integer.max/ 0") |
161 |
161 |
162 text {* For Haskell and Scala, things are slightly different again. *} |
162 text {* For Haskell and Scala, things are slightly different again. *} |
163 |
163 |
164 code_const int and nat |
164 code_const int and nat |
165 (Haskell "toInteger" and "fromInteger") |
165 (Haskell "Prelude.toInteger" and "Prelude.fromInteger") |
166 (Scala "!_.as'_BigInt" and "Nat") |
166 (Scala "!_.as'_BigInt" and "Nat") |
167 |
167 |
168 text {* Alternativ implementation for @{const of_nat} *} |
168 text {* Alternativ implementation for @{const of_nat} *} |
169 |
169 |
170 lemma [code]: |
170 lemma [code]: |
187 text {* Conversion from and to code numerals *} |
187 text {* Conversion from and to code numerals *} |
188 |
188 |
189 code_const Code_Numeral.of_nat |
189 code_const Code_Numeral.of_nat |
190 (SML "IntInf.toInt") |
190 (SML "IntInf.toInt") |
191 (OCaml "_") |
191 (OCaml "_") |
192 (Haskell "!(fromInteger/ ./ toInteger)") |
192 (Haskell "!(Prelude.fromInteger/ ./ Prelude.toInteger)") |
193 (Scala "!Natural(_.as'_BigInt)") |
193 (Scala "!Natural(_.as'_BigInt)") |
194 (Eval "_") |
194 (Eval "_") |
195 |
195 |
196 code_const Code_Numeral.nat_of |
196 code_const Code_Numeral.nat_of |
197 (SML "IntInf.fromInt") |
197 (SML "IntInf.fromInt") |
198 (OCaml "_") |
198 (OCaml "_") |
199 (Haskell "!(fromInteger/ ./ toInteger)") |
199 (Haskell "!(Prelude.fromInteger/ ./ Prelude.toInteger)") |
200 (Scala "!Nat(_.as'_BigInt)") |
200 (Scala "!Nat(_.as'_BigInt)") |
201 (Eval "_") |
201 (Eval "_") |
202 |
202 |
203 |
203 |
204 subsection {* Target language arithmetic *} |
204 subsection {* Target language arithmetic *} |