2018年02月09日
Coq の Reserved Notation と戦う
- 2018-02-09 (Fri)
- 一般
Coq.Init.Notations に Reserved Notation で + が left associativity と定義されてしまっているので結合の仕方を上書きできない．自前のライブラリで no assoc. な + を使いたいと思っても無理．何で Reserved Notation の連中が上書きできないのか知らんけど，ひょっとしてパーサレベルで固定しちゃってるのだろうか．普通には困ることはないだろうけど変なことするには不便．
で，妥協案：全角の ＋（U+FF0B）を使えば良いじゃない．入力面倒だけど見た目は問題ない．
というか，Unicode の数学記号とかも識別子に出来たのか…… oplus とか書いてた部分を Unicode の文字に置き換えてみようかな．
- Comments: 0
- TrackBack (Close): -