morita_non https://blog.hatena.ne.jp/morita_non/ memo https://morita-non.hatenadiary.org/ なんか読書会がもうすぐあって結構な人気らしい。行って覗いてみたい気もするが、すでに定員一杯らしいし、Haskell知らんし、そもそも勉強会読書会なるものについてける気もしないしちょっと無理だろう。件の本は、オンライン演習は一通りやったけど、そういえば肝心の本本体はほとんど全く読んでなかった。メタ定理を証明せよ。とか謎言葉が最初の方に書いてあって、さっさとあきらめたのであった。そういうわけで再び挑戦のために読んでみることにする。coqで。 まずは第一章の導出システムで、ペアノ自然数の定義だ。 Inductive nat : Type := | Z : nat | S : nat -> nat.「… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmorita-non.hatenadiary.org%2Fentry%2F20150623%2F1435073816" title=" プログラミング言語の基礎概念 - memo" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2015-06-23 00:36:56 rich https://morita-non.hatenadiary.org/entry/20150623/1435073816 1.0 100%