441 |
441 |
442 text \<open>SML\<close> |
442 text \<open>SML\<close> |
443 |
443 |
444 code_printing type_constructor array \<rightharpoonup> (SML) "_/ array" |
444 code_printing type_constructor array \<rightharpoonup> (SML) "_/ array" |
445 code_printing constant Array \<rightharpoonup> (SML) "raise/ (Fail/ \"bare Array\")" |
445 code_printing constant Array \<rightharpoonup> (SML) "raise/ (Fail/ \"bare Array\")" |
446 code_printing constant Array.new' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))" |
446 code_printing constant Array.new' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.array/ (IntInf.toInt _,/ (_)))" |
447 code_printing constant Array.of_list \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.fromList/ _)" |
447 code_printing constant Array.of_list \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.fromList/ _)" |
448 code_printing constant Array.make' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))" |
448 code_printing constant Array.make' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.tabulate/ (IntInf.toInt _,/ _ o IntInf.fromInt))" |
449 code_printing constant Array.len' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.length/ _)" |
449 code_printing constant Array.len' \<rightharpoonup> (SML) "(fn/ ()/ =>/ IntInf.fromInt (Array.length/ _))" |
450 code_printing constant Array.nth' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))" |
450 code_printing constant Array.nth' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.sub/ ((_),/ IntInf.toInt _))" |
451 code_printing constant Array.upd' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))" |
451 code_printing constant Array.upd' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.update/ ((_),/ IntInf.toInt _,/ (_)))" |
452 code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (SML) infixl 6 "=" |
452 code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (SML) infixl 6 "=" |
453 |
453 |
454 code_reserved SML Array |
454 code_reserved SML Array |
455 |
455 |
456 |
456 |
457 text \<open>OCaml\<close> |
457 text \<open>OCaml\<close> |
458 |
458 |