構文カテゴリが「それですべて」であることをどうやって知るのか

[Seasawher]

aesop の phase や builder_name が「それですべて」であることを保証したい

declare_syntax_cat hoge_cat

syntax "hoge" : hoge_cat
syntax "fuga" : hoge_cat
syntax "foo" : hoge_cat

Zulip: > how to enumerate all syntax of given sytanx category

[Seasawher]

syntax category は拡張可能なので、全列挙することはできない。（「これですべて」という情報がない） また TSyntax は正当性をチェックしないので、固定された構文でも全列挙は保証できない。

何が入っているのかを列挙することは一応できる。

declare_syntax_cat hoge_cat

syntax "hoge" : hoge_cat
syntax "fuga" : hoge_cat
syntax "foo" : hoge_cat

open Lean

def matchHogeCat : TSyntax `hoge_cat → Unit
  | `(hoge_cat| hoge) => ()
  | `(hoge_cat| fuga) => ()
  | `(hoge_cat| foo) => ()
  | _ => () -- why this line is needed? Without this line, the match is said not to be exhaustive.

[Seasawher]

構文カテゴリを使うからだめ。<|> を使うべき。

syntax hoge := "hoge" <|> "fuga" <|> "foo"