Leanに限らず、どんな証明系でも定理ライブラリの構築は熱心。Leanだと自動化タクティクのライブラリも整備されるだろう。だが、特定パターンの証明のやり方をガイダンスするテンプレートみたいなものはない。定型文書作成のテンプレートと同じで、穴埋めす…

エントリの参照点〈中心点〉をずらす !vector 修飾子 アローのカーブ指定に寸法を入れられる。 エントリ座標にホップ以外の方法がある。 エントリーへの枠付け 全体のレイアウト指定、行間の調整とか