以下の内容はhttps://m-hiyama-memo.hatenablog.com/entry/2023/01/28/141456より取得しました。

ノーテーションの名前を知りたいとき

Lean tips 
set_option pp.notation true in #print Eq.trans
set_option pp.notation false in #print Eq.trans
set_option pp.notation false in #check 1 + 3
set_option pp.notation true in #check 1 + 3


以上の内容はhttps://m-hiyama-memo.hatenablog.com/entry/2023/01/28/141456より取得しました。
このページはhttp://font.textar.tv/のウェブフォントを使用してます
不具合報告/要望等はこちらへお願いします。
モバイルやる夫Viewer Ver0.14