Home > 一般 > Coq の Reserved Notation と戦う

Coq の Reserved Notation と戦う

  • 2018-02-09 (Fri) 22:17
  • 一般

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

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

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

★下記に2つの英単語をスペースで区切って入力してください

Home > 一般 > Coq の Reserved Notation と戦う

Search
Feeds

Page Top