演習問題

この章の演習では，Lean の内部構造と，VS Code を介さない Lean との相互作用を確認します． 証明を作るだけでなく，実際にターミナルで出力を読むことを目標にしてください．

1. VS Code を使わずに，この章を単体でチェックしてください．

   lake env lean LeanMathNote/basic/chapter06.lean
   lake lean LeanMathNote/basic/chapter06.lean
   

2. 標準入力から Lean にコードを渡してください．

   printf '#check Nat\n#eval 2 + 3\n' | lake env lean --stdin
   

3. --json を付けて Lean を実行し，通常の出力との違いを確認してください．

   lake env lean --json LeanMathNote/basic/chapter06.lean
   

4. --deps と --src-deps を使って，依存関係の出力を比較してください．

   lake env lean --deps LeanMathNote/basic/chapter06.lean
   lake env lean --src-deps LeanMathNote/basic/chapter06.lean
   

5. Syntax，Expr，Environment の型を確認してください．

   #check Lean.Syntax
   #check Lean.Expr
   #check Lean.Environment
   

6. pretty printer の出力を詳しくして，暗黙引数や型クラス引数が表示されることを確認してください．

   set_option pp.all true in
   #check (fun n : Nat => n + 1)
   

7. lake build を実行した後，生成される .olean と .ilean を探してください．

   lake build
   find .lake/build/lib -name '*.olean' | head
   find .lake/build/lib -name '*.ilean' | head
   

8. module 名とファイルパスの対応を説明してください．

   LeanMathNote.lean
   LeanMathNote/basic/chapter01.lean
   LeanMathNote/basic/chapter06.lean
   LeanMathNote/practice/chapter01.lean