*) section ‹A Serbian theory› theory Serbian imports Main begin text ‹Serbian cyrillic letters.› datatype azbuka = azbA ( "А" ) | azbB ( "Б" ) | azbV ( "В" ) | azbG ( "Г" ) | azbD ( "Д" ) | azbDj ( "Ђ" ) | azbE ( "Е" ) | azbZv ( "Ж" ) | azbZ ( "З" ) | azbI ( "И" ) | azbJ ( "Ј" ) | azbK ( "К" ) | azbL ( "Л" ) | azbLj ( "Љ" ) | azbM ( "М" ) | azbN ( "Н" ) | azbNj ( "Њ" ) | azbO ( "О" ) | azbP ( "П" ) | azbR ( "Р" ) | azbS ( "С" ) | azbT ( "Т" ) | azbC' ( "Ћ" ) | azbU ( "У" ) | azbF ( "Ф" ) | azbH ( "Х" ) | azbC ( "Ц" ) | azbCv ( "Ч" ) | azbDzv ( "Џ" ) | azbSv ( "Ш" ) | azbSpc thm azbuka.induct text ‹Serbian latin letters.› datatype abeceda = abcA ( "A" ) | abcB ( "B" ) | abcC ( "C" ) | abcCv ( "Č" ) | abcC' ( "Ć" ) | abcD ( "D" ) | abcE ( "E" ) | abcF ( "F" ) | abcG ( "G" ) | abcH ( "H" ) | abcI ( "I" ) | abcJ ( "J" ) | abcK ( "K" ) | abcL ( "L" ) | abcM ( "M" ) | abcN ( "N" ) | abcO ( "O" ) | abcP ( "P" ) | abcR ( "R" ) | abcS ( "S" ) | abcSv ( "Š" ) | abcT ( "T" ) | abcU ( "U" ) | abcV ( "V" ) | abcZ ( "Z" ) | abcvZ ( "Ž" ) | abcSpc thm abeceda.induct text ‹Conversion from cyrillic to latin - this conversion is valid in all cases.› primrec azb2abc_aux :: "azbuka ⇒ abeceda list" where "azb2abc_aux А = " | "azb2abc_aux Б = " | "azb2abc_aux В = " | "azb2abc_aux Г = " | "azb2abc_aux Д = " | "azb2abc_aux Ђ = " | "azb2abc_aux Е = " | "azb2abc_aux Ж = " | "azb2abc_aux З = " | "azb2abc_aux И = " | "azb2abc_aux Ј = " | "azb2abc_aux К = " | "azb2abc_aux Л = " | "azb2abc_aux Љ = " | "azb2abc_aux М = " | "azb2abc_aux Н = " | "azb2abc_aux Њ = " | "azb2abc_aux О = " | "azb2abc_aux П = " | "azb2abc_aux Р = " | "azb2abc_aux С = " | "azb2abc_aux Т = " | "azb2abc_aux Ћ = " | "azb2abc_aux У = " | "azb2abc_aux Ф = " | "azb2abc_aux Х = " | "azb2abc_aux Ц = " | "azb2abc_aux Ч = " | "azb2abc_aux Џ = " | "azb2abc_aux Ш = " | "azb2abc_aux azbSpc = " primrec azb2abc :: "azbuka list ⇒ abeceda list" where "azb2abc = " | "azb2abc (x # xs) = azb2abc_aux x azb2abc xs" value "azb2abc " value "azb2abc " text ‹ Example theory involving Unicode characters (UTF-8 encoding) -Ĭonversion between Serbian cyrillic and latin letters (српска ћирилица и латиница).
0 kommentar(er)
