More comments

Changes

1 changed files (+16/-16)

• WritingSystem.lean
  • @@ -50,14 +50,14 @@ instance : ToString Consonant where
    | .s => "s" | .l => "l") ++ ((match c.place, asp with - | .la, true => some 0x304 + | .la, true => some 0x304 -- ̄ | .da, true => none - | .rf, true => some 0x307 - | .ve, true => some 0x308 - | .la, false => some 0x331 - | .da, false => some 0x32F - | .rf, false => some 0x323 - | .ve, false => some 0x324) + | .rf, true => some 0x307 -- ̇ + | .ve, true => some 0x308 -- ̈ + | .la, false => some 0x331 -- ̱ + | .da, false => some 0x32F -- ̯ + | .rf, false => some 0x323 -- ̣ + | .ve, false => some 0x324) -- ̤ |>.map Char.ofNat |>.map toString |>.getD "")
  • @@ -122,16 +122,16 @@ def parseTone : Char → Fin 5
    instance : ToString (Fin 5 × Bool) where toString t := (match t with - | ⟨0, true⟩ => some 0x304 - | ⟨1, true⟩ => some 0x301 - | ⟨2, true⟩ => some 0x30C + | ⟨0, true⟩ => some 0x304 -- ̄ + | ⟨1, true⟩ => some 0x301 -- ́ + | ⟨2, true⟩ => some 0x30C -- ̌ | ⟨3, true⟩ => none -- Falling tone is most common - | ⟨4, true⟩ => some 0x30A - | ⟨0, false⟩ => some 0x331 - | ⟨1, false⟩ => some 0x317 - | ⟨2, false⟩ => some 0x32C - | ⟨3, false⟩ => some 0x316 - | ⟨4, false⟩ => some 0x325) + | ⟨4, true⟩ => some 0x30A -- ̊ + | ⟨0, false⟩ => some 0x331 -- ̱ + | ⟨1, false⟩ => some 0x317 -- ̗ + | ⟨2, false⟩ => some 0x32C -- ̬ + | ⟨3, false⟩ => some 0x316 -- ̖ + | ⟨4, false⟩ => some 0x325) -- ̥ |>.map Char.ofNat |>.map toString |>.getD ""