lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
15 stars 5 forks source link

対話的コマンドと構文をひとつのカテゴリにまとめる #347

Closed Seasawher closed 1 week ago

Seasawher commented 1 week ago

そもそも # つきのコマンドとそうでないコマンドの間に syntactic な違いはない

使い勝手の観点から分けていたが,今後 attribute や option や type class も紹介していくことを考えると,分ける意味が薄いかもしれない.(あまり違いがはっきりしないため)

また,初心者が見たときに # 付きコマンドとそうでないコマンドが違うものだと思ってしまうかもしれない