Lean4 学習9 - ushumpei’s blog こちらで定義した range' : (n : Nat) → Vector (Fin n) n という関数、もっと簡単に定義できた。 range を定義してから型の対応関係を考えるというのが逆で、型の対応関係を考えたら自然と range に相当するものが出てきた感…

Lean4 で有限個の要素をいい感じに扱いたくてどうすればいいか悩んでいて、Fin n → α がそれに当たるかなーとか考えたのですが、プログラミングにおいては Vector α n (長さ固定の List α) が使いやすいのでその間を埋めることができないかなと色々していま…

Lean4 で証明とプログラムをうまく組み合わせたものが書けないか色々試している。証明を書いて、その具体的な値を使って何かするといったことがなかなかうまく出来ず、何となくこれでいいんじゃないかな、という方法が少しわかったのでメモしておく。単体を…