rw や simp の共通の構文をどう扱うか？

[Seasawher]

たとえば location の構文は rw でも simp でも push_cast でも同じで、at h で仮定 h に適用し、at h ⊢ で仮定とゴールに適用する。これを、毎回毎回どのタクティクに対してもコード例で確かめていたら大変だし、だからといって省略するのはリファレンスとしていかがなものか。

全く同じ問題が def コマンドと theorem コマンドなどに対しても存在する。これは現状のリファレンスの大きな問題点である。

一つのアイデアは、「location に使われる構文カテゴリを受け入れるかどうか」をまるごとコード例で確かめてしまうというものである。これなら、at ... の構文が使えることを十分示唆するし、そんなに面倒でもない。