Char

Char 型は、Unicode 文字を表します。二重引用符 " ではなくてシングルクォート ' で囲んで表されます。

-- Char はシングルクォートで囲む
#check ('a' : Char)
#check ("a" : String)

-- Unicode 文字を含む
#check ('あ' : Char)
#check ('∀' : Char)
#check ('∅' : Char)

Char は、以下のように structure として定義されています。

structure Char where
  /-- Unicode スカラー値 -/
  val : UInt32

  /-- `val` が正しいコードポイントであること -/
  valid : val.isValidChar

したがって Char.val 関数によりコードポイントを取得することができます。

#guard 'a'.val = 97
#guard '⨅'.val = 10757