リストリテラル

[x₁, x₂, .. , xₙ] は、List α の項を簡単に作るための構文です。

もしこの構文がなければ、List α の項を作るためにはコンストラクタを使用するしかないので、次のように書く必要があります。

/-- 自前で定義したリスト型 -/
inductive MyList (α : Type) where
  | nil
  | cons (head : α) (tail : MyList α)
deriving DecidableEq

/-- 空リスト。標準の`List`のための記法と被るのを避けている。 -/
notation:max " ⟦⟧ " => MyList.nil

/-- `MyList`に要素を追加する。標準の`List`のための記法と被るのを避けている。 -/
infixr:80 " ::: " => MyList.cons

-- 項を作るのが面倒
/- info: 1 ::: 2 ::: 3 ::: ⟦⟧ : MyList Nat -/
#check 1 ::: 2 ::: 3 ::: ⟦⟧

しかし、リストリテラル構文があるおかげで、次のように見やすく簡潔に書くことができます。

/-- 自作のリストリテラル構文。なお末尾のカンマは許可される。
なお標準の`List`のための記法と被るのを避けている。 -/
syntax "⟦" term,*,? "⟧" : term

macro_rules
  | `(⟦ ⟧) => `(⟦⟧)
  | `(⟦$x⟧) => `($x ::: ⟦⟧)
  | `(⟦$x, $xs,*⟧) => `($x ::: (⟦$xs,*⟧))

-- 項を作るのが楽になった！
#guard ⟦1, 2, 3⟧ = 1 ::: 2 ::: 3 ::: ⟦⟧

-- 末尾のコンマは無視される
#guard ⟦1, ⟧ = 1 ::: ⟦⟧

-- 空リストもリストリテラル構文で書ける
#guard ⟦⟧ = MyList.nil (α := Unit)