Home > Archives > 09 February 2018

09 February 2018

Coq の Reserved Notation と戦う

Coq.Init.Notations に Reserved Notation で + が left associativity と定義されてしまっているので結合の仕方を上書きできない.自前のライブラリで no assoc. な + を使いたいと思っても無理.何で Reserved Notation の連中が上書きできないのか知らんけど,ひょっとしてパーサレベルで固定しちゃってるのだろうか.普通には困ることはないだろうけど変なことするには不便.

で,妥協案:全角の +(U+FF0B)を使えば良いじゃない.入力面倒だけど見た目は問題ない.

というか,Unicode の数学記号とかも識別子に出来たのか…… oplus とか書いてた部分を Unicode の文字に置き換えてみようかな.

Home > Archives > 09 February 2018

Search
Feeds

Page Top