Fix ambiguity

Changes

1 changed files (+6/-6)

• WritingSystem.lean
  • @@ -72,8 +72,8 @@ inductive Vowel where
    def parseVowel : Char → Option Vowel | 'ㄚ' => some <| .medial .a - | 'ㄛ' => some <| .medial .o - | 'ㄜ' => some <| .medial .o + | 'ㄛ' => some <| .medial .e + | 'ㄜ' => some <| .medial .e | 'ㄝ' => some <| .medial .e | 'ㄞ' => some <| .coda true .i | 'ㄟ' => some <| .coda false .i
  • @@ -141,9 +141,9 @@ def convert (s : String) :=
    ㄗㄠˇ ㄕㄤˋ ㄏㄠˇ ㄓㄨㄥ ㄍㄨㄛˊ ， ㄒㄧㄢˋ ㄗㄞˋ ㄨㄛˇ ㄧㄡˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄨㄛˇ ㄏㄣˇ ㄒㄧˇ ㄏㄨㄢ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄉㄢˋ ㄕˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄅㄧˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄨㄛˇ ㄗㄨㄟˋ ㄒㄧˇ ㄏㄨㄢ 。 ㄙㄨㄛˇ ㄧˇ … ㄒㄧㄢˋ ㄗㄞˋ ㄕˋ ㄧㄣ ㄩㄝˋ ㄕˊ ㄐㄧㄢ ， ㄓㄨㄣˇ ㄅㄟˋ 1 2 3， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9。 ㄅㄨˋ ㄧㄠˋ ㄨㄤˋ ㄐㄧˋ ， ㄅㄨˋ ㄧㄠˋ ㄘㄨㄛˋ ㄍㄨㄛˋ ， ㄑㄩˋ ㄉㄧㄢˋ ㄧㄥˇ ㄩㄢˋ ㄎㄢˋ ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄧㄣ ㄨㄟˊ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ㄉㄧㄢˋ ㄧㄥˇ ， ㄉㄨㄥˋ ㄗㄨㄛˋ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ， ㄔㄚˋ ㄅㄨˋ ㄉㄨㄛ ㄧ ㄧㄤˋ 。 ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄗㄞˋ ㄐㄧㄢˋ 。 - C̣o̊̌ṡŋ̊̀ s̄o̊̌ Ċ̣uŋꞇ̣̄uó, s̈ın̊̀c̣ı̊̀ uǒ ıǒ ꞇ̣̓ıŋc̈ı́lıń, uǒ s̄ň s̈ı̌s̄un̊ ꞇ̣̓ıŋc̈ı́lıń, ꞇ̣n̊̀ṡ̀, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, ꞇ̣̓ı̌ ꞇ̣̓ıŋc̈ı́lıń, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, uǒ c̣uı̀ s̈ı̌s̄un̊. Suǒı̌... s̈ın̊̀c̣ı̊̀ ṡ̀ ınyè ṡ́c̣̈ın̊, ċ̣uňꞇ̣̓ı̀ 1 2 3, - Lıŋ̊̌ ꞇ̣̄ò lı̌ꞇ̣̓ı̊̀ ı̌s̄ò, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, lıŋ̊̌ ꞇ̣̄ò lı̌ꞇ̣̓ı̊̀ ı̌s̄ò, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, lıŋ̊̌ ꞇ̣̄ò lı̌ꞇ̣̓ı̊̀ ı̌s̄ò, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9. - Ꞇ̣̓ùıo̊̀ uŋ̊̀c̣̈ı̀, ꞇ̣̓ùıo̊̀ cuòꞇ̣̄uò, c̈ỳ ꞇ̣ın̊̀ıŋ̌yn̊̀ ꞇ̄n̊̀ Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, ınuı́ s̓ıċŋ̊́ s̄o̊̌ ꞇ̣ın̊̀ıŋ̌, ꞇ̣uŋ̀c̣uò s̓ıċŋ̊́ s̄o̊̌, ċàꞇ̣̓ùꞇ̣uo ııŋ̊̀. Ꞇ̣̓ıŋc̈ı́lıń, c̣ı̊̀c̣̈ın̊̀. + C̣o̊̌ṡŋ̊̀ s̄o̊̌ Ċ̣uŋꞇ̣̄uoé, s̈ın̊̀c̣ı̊̀ uě ıǒ ꞇ̣̓ıŋc̈ı́lıń, uě s̄ň s̈ı̌s̄un̊ ꞇ̣̓ıŋc̈ı́lıń, ꞇ̣n̊̀ṡ̀, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, ꞇ̣̓ı̌ ꞇ̣̓ıŋc̈ı́lıń, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, uě c̣uı̀ s̈ı̌s̄un̊. Suěı̌... s̈ın̊̀c̣ı̊̀ ṡ̀ ınyè ṡ́c̣̈ın̊, ċ̣uňꞇ̣̓ı̀ 1 2 3, + Lıŋ̊̌ ꞇ̣̄è lı̌ꞇ̣̓ı̊̀ ı̌s̄ò, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, lıŋ̊̌ ꞇ̣̄è lı̌ꞇ̣̓ı̊̀ ı̌s̄ò, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, lıŋ̊̌ ꞇ̣̄ò lı̌ꞇ̣̓ı̊̀ ı̌s̄ò, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9. + Ꞇ̣̓ùıo̊̀ uŋ̊̀c̣̈ı̀, ꞇ̣̓ùıo̊̀ cuèꞇ̣̄uè, c̈ỳ ꞇ̣ın̊̀ıŋ̌yn̊̀ ꞇ̄n̊̀ Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, ınuı́ s̓ıċŋ̊́ s̄o̊̌ ꞇ̣ın̊̀ıŋ̌, ꞇ̣uŋ̀c̣uè s̓ıċŋ̊́ s̄o̊̌, ċàꞇ̣̓ùꞇ̣ue ııŋ̊̀. Ꞇ̣̓ıŋc̈ı́lıń, c̣ı̊̀c̣̈ın̊̀. -/ - #eval convert "ㄗㄠˇ ㄕㄤˋ ㄏㄠˇ ㄓㄨㄥ ㄍㄨㄛˊ ， ㄒㄧㄢˋ ㄗㄞˋ ㄨㄛˇ ㄧㄡˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄨㄛˇ ㄏㄣˇ ㄒㄧˇ ㄏㄨㄢ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄉㄢˋ ㄕˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄅㄧˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄨㄛˇ ㄗㄨㄟˋ ㄒㄧˇ ㄏㄨㄢ 。 ㄙㄨㄛˇ ㄧˇ … ㄒㄧㄢˋ ㄗㄞˋ ㄕˋ ㄧㄣ ㄩㄝˋ ㄕˊ ㄐㄧㄢ ， ㄓㄨㄣˇ ㄅㄟˋ 1 2 3， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9。 ㄅㄨˋ ㄧㄠˋ ㄨㄤˋ ㄐㄧˋ ， ㄅㄨˋ ㄧㄠˋ ㄘㄨㄛˋ ㄍㄨㄛˋ ， ㄑㄩˋ ㄉㄧㄢˋ ㄧㄥˇ ㄩㄢˋ ㄎㄢˋ ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄧㄣ ㄨㄟˊ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ㄉㄧㄢˋ ㄧㄥˇ ， ㄉㄨㄥˋ ㄗㄨㄛˋ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ， ㄔㄚˋ ㄅㄨˋ ㄉㄨㄛ ㄧ ㄧㄤˋ 。 ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄗㄞˋ ㄐㄧㄢˋ 。 " + #eval convert "ㄗㄠˇ ㄕㄤˋ ㄏㄠˇ ㄓㄨㄥ ㄍㄨㄛˊ ， ㄒㄧㄢˋ ㄗㄞˋ ㄨㄛˇ ㄧㄡˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄨㄛˇ ㄏㄣˇ ㄒㄧˇ ㄏㄨㄢ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄉㄢˋ ㄕˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄅㄧˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄨㄛˇ ㄗㄨㄟˋ ㄒㄧˇ ㄏㄨㄢ 。 ㄙㄨㄛˇ ㄧˇ … ㄒㄧㄢˋ ㄗㄞˋ ㄕˋ ㄧㄣ ㄩㄝˋ ㄕˊ ㄐㄧㄢ ， ㄓㄨㄣˇ ㄅㄟˋ 1 2 3， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9。 ㄅㄨˋ ㄧㄠˋ ㄨㄤˋ ㄐㄧˋ ， ㄅㄨˋ ㄧㄠˋ ㄘㄨㄛˋ ㄍㄨㄛˋ ， ㄑㄩˋ ㄉㄧㄢˋ ㄧㄥˇ ㄩㄢˋ ㄎㄢˋ ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄧㄣ ㄨㄟˊ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ㄉㄧㄢˋ ㄧㄥˇ ， ㄉㄨㄥˋ ㄗㄨㄛˋ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ， ㄔㄚˋ ㄅㄨˋ ㄉㄨㄛ ㄧ ㄧㄤˋ 。 ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄗㄞˋ ㄐㄧㄢˋ 。"