keenさんが、発した疑問の回答に「Mix-fix operators」とあったので
ググって見ると、下の論文があった。
ですが、どうも違うようです。
http://www.cse.chalmers.se/~nad/publications/danielsson-norell-mixfix.pdf
ただ、keenさんの疑問も、notationのことだったみたいです。
http://keens.github.io/slide/koubunkaisekiarekore/
上記に、下記の記述がある。
Coq
Coqは謎のテクノロジーにより Notationを使えば新しい文法を定義出来る
Notation "'SKIP'" :=
CSkip.
Notation "X '::=' a" :=
(CAss X a) (at level 60).
Notation "c1 ; c2" :=
(CSeq c1 c2) (at level 80, right associativity).
Notation "'WHILE' b 'DO' c 'END'" :=
(CWhile b c) (at level 80, right associativity).
Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" :=
(CIf e1 e2 e3) (at level 80, right associativity).
Definition fact_in_coq : com :=
Z ::= AId X;
Y ::= ANum 1;
WHILE BNot (BEq (AId Z) (ANum 0)) DO
Y ::= AMult (AId Y) (AId Z);
Z ::= AMinus (AId Z) (ANum 1)
END.
Coqは謎のテクで文法を拡張できる。どうやってるかわからん。
(あとの発表でMix-fix operatorsだとのこと)