借用したいHaskell記法／Coq記法

Haskell演算には、加減乗除（+, -, *, /）、累乗（整数の^と実数の**）、余り mod がある。これを例とする。

• 中置→前置変換 (+) 3 2 、(-) 3 2
• 前置→後置変換 10 `mod` 3 、 10 `div` 3

セクション記法

• (^2) 、 (2^) 、(*3)
• 例外 (-2) は -2 のこと。部分適用 (subtract 2) またはセクション (+ (-2))

CoqのNotation宣言

• Notation "A /\ B" := (and A B).

変数名（A, B）と演算子記号を含む文字列に意味を割り当てる。

変数を無名ラムダ変数にして、簡易ラムダ記法（関数記法）に使う。

• "_ /\ _" = λ(A, B).(and A B)
• "_ /\ _"(A, B) = (and A B)

演算子記号の記法情報〈notatinal information〉が事前にあるときは、無名ラムダ変数を省略してよい。

• "!"(n) = n! = fact(n)
• "+"(2, 3) = 2 + 3
• "+2"(3) = 3 + 2
• "3^"(5) = 3^5

記法情報とは：

1. 演算子記号、空記号も可能
2. 引数の個数〈項数〉
3. 演算子記号とそれぞれの引数の位置（レイアウト）、親文字と飾り六位置（入れ子も可能）外側になると、真上位置と真下位置が 1, 3, 5, 7, ... と奇数個で増える。ひとつ外側で十位置になり、さらに十四位置になる。位置数は、飾り四段レイアウトで (奇数×2 + 4)
4. 引数の順番、位置に前順序を入れる

TeXでのレンダリングでは、飾り六位置をすべて同時に使うのは難しい。