Leanの構文範疇

• id : an identifier
• expr : an expression
• : a sequence of identifiers and expressions (a : α) where a is an identifier and α is a Type or a Prop.

バインダーズは、列となっている。列とリストの区別はあるのかな？ 列＝構文上のリスト かな？ Leanでは項〈term〉よりは式〈expression〉を使うようだ。