このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

探すのが不便

Isabelle ダメ出し

infix operatorの優先度の一覧が欲しいだけど、isabelle infix operator precedence とかでググッてもあんまり分からん。Coqだと、公開されているHTMLマニュアルが引っかかったけど、Isabelleは粒度がでかいPDFだからなーー。

[追記]

  • introの"4.1.1 Infix Annotations"に演算子の優先度：50が等号で、50を超えて100未満で算術演算子、らしい。
  • isar-refの"8.2.1 The general mixfix form"にmixfix宣言について詳しい。

[/追記]