equal
deleted
inserted
replaced
335 |
335 |
336 code_reserved Scala Nat |
336 code_reserved Scala Nat |
337 |
337 |
338 code_type nat |
338 code_type nat |
339 (Haskell "Nat.Nat") |
339 (Haskell "Nat.Nat") |
340 (Scala "Nat.Nat") |
340 (Scala "Nat") |
341 |
341 |
342 code_instance nat :: eq |
342 code_instance nat :: eq |
343 (Haskell -) |
343 (Haskell -) |
344 |
344 |
345 text {* |
345 text {* |
403 |
403 |
404 text {* For Haskell and Scala, things are slightly different again. *} |
404 text {* For Haskell and Scala, things are slightly different again. *} |
405 |
405 |
406 code_const int and nat |
406 code_const int and nat |
407 (Haskell "toInteger" and "fromInteger") |
407 (Haskell "toInteger" and "fromInteger") |
408 (Scala "!_.as'_BigInt" and "!Nat.Nat((_))") |
408 (Scala "!_.as'_BigInt" and "Nat") |
409 |
409 |
410 text {* Conversion from and to indices. *} |
410 text {* Conversion from and to indices. *} |
411 |
411 |
412 code_const Code_Numeral.of_nat |
412 code_const Code_Numeral.of_nat |
413 (SML "IntInf.toInt") |
413 (SML "IntInf.toInt") |
417 |
417 |
418 code_const Code_Numeral.nat_of |
418 code_const Code_Numeral.nat_of |
419 (SML "IntInf.fromInt") |
419 (SML "IntInf.fromInt") |
420 (OCaml "_") |
420 (OCaml "_") |
421 (Haskell "toEnum") |
421 (Haskell "toEnum") |
422 (Scala "!Nat.Nat((_))") |
422 (Scala "Nat") |
423 |
423 |
424 text {* Using target language arithmetic operations whenever appropriate *} |
424 text {* Using target language arithmetic operations whenever appropriate *} |
425 |
425 |
426 code_const "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" |
426 code_const "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" |
427 (SML "IntInf.+ ((_), (_))") |
427 (SML "IntInf.+ ((_), (_))") |