背景
Xでバズってたから。 あとRustが比較に出されていて、なんとなく面白そうに感じたから。
やってみる
- めざせHello world
あと湯婆婆- また今度。
Zedを使ってLeanをかける環境を整える
Zedが好きなので今回はZedを使ってLeanを書いていく。
ZedにはデフォルトでLeanをサポートする機能が入っていないので、下記拡張機能を入れた。
lean4
leanprover/elan: リーンバージョンマネージャー がないとインストールできないので入れる
- github の Readmeにある通りにコマンドを実行する。
- インストールに成功したら、
source $HOME/.elan/envを実行してパスを通す。 - その後に、lean4をインストールすると正常にインストールされる。
初めての lean
leanは拡張子が .leanらしい。試しにhello.lean という名前でファイルを作ってみる。
下記にある通りに写経して、 #eval にカーソルを合わせると確かに3が出てくる。
これはダメらしい。 代わりに次のように書く
()なしでいけた。何がダメなんだろう。（カッコないのにちゃんと読まれているのも不思議な感じ）
もう少し楽しみたいんだけど、まだ難しい
一旦ここまで。もしこういうの面白いよ、などあればまた書きます。
