2017-08-15から1日間の記事一覧
最近Lean Prover (Lean 3)で原始再帰的関数について証明を書いているので、それによって得られた知見を一つ紹介する。 gist.github.com inaccessible termとは何か ".(項)"の形のパターンはinaccesible termと呼ばれ、パターンマッチを行う際に、この部分は…
最近Lean Prover (Lean 3)で原始再帰的関数について証明を書いているので、それによって得られた知見を一つ紹介する。 gist.github.com inaccessible termとは何か ".(項)"の形のパターンはinaccesible termと呼ばれ、パターンマッチを行う際に、この部分は…