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文の略記という位置付け。ノーテーション宣言では、裸の && が書ける。