ushumpei’s blog

生活で気になったことを随時調べて書いていきます。

2023-04-19から1日間の記事一覧

Lean4 学習6

パターンマッチを書いている時、 match xs with | [] => [] | y::ys => _ としたときに二番目にマッチしたケースでは 0 < xs.length が成り立っていて欲しいけどそれはダメみたい?そう言う場合はどうすればいいか?素直に if h : 0 < xs.length then ... el…