private コマンドの用例を，protected から引っ張ってこない

lean-ja / lean-by-example

コード例で学ぶ Lean 言語

https://lean-ja.github.io/lean-by-example/

MIT License

15 stars 5 forks source link

Closed Seasawher closed 2 days ago

Seasawher commented 3 days ago

protected のページに private のテスト用のコードがあるのは不自然

専用のディレクトリを作るなどして工夫すべき

Seasawher commented 2 days ago

なんと mdbook の #include 機能を使っても上手くいかなかった！

無期限延期