Hello, World!

Lean には豊かな対話的環境があり，プログラマはお気に入りのテキストエディタを離れることなく，多くのフィードバックを得ることができます．また，Lean は実用的なプログラムを記述することができる言語でもあります．つまり，バッチモードのコンパイラ，ビルドシステム，パッケージマネージャなど，プログラムを書くために不可欠なツールもすべて備えているということです．

前の章では，Lean における関数型プログラミングの基本を紹介しましたが，この章ではプロジェクトを作成し，コンパイルして，その結果を実行する一連の方法を説明します．環境と相互作用するプログラム（例えば，標準入力を読み取ったりファイルを作成したりすること）と，計算を「数学的な式の評価」と解釈する関数型プログラミングは，整合させることが難しいものです．この章では Lean のビルドツールの説明に加え，関数型プログラミングにおいて世界と相互作用するようなプログラムをどのように扱うかについても説明します．