case文の書き方など

core.lean 内の定義:

@[inline] def band : bool → bool → bool
| ff _  := ff
| tt ff := ff
| tt tt := tt

notation x && y := band x y

[inline] というアトリビュートがある。その場で展開されるのかな?アンダスコアは無名変数〈匿名変数〉で、パターンマッチしても捨てるときに使われる。場合分けは、mathc/with/end文の略記という位置付け。ノーテーション宣言では、裸の && が書ける。