hitotakuchan https://blog.hatena.ne.jp/hitotakuchan/ 俺の Colimit を越えてゆけ https://www.orecoli.com/ Coq はじめに length関数を実装する Gallina 風の実装 Ltac から Gallina へ Gallina の項を Ltac 呼び出しの結果として受け取る 気持ち悪い点 map関数(Ltac引数)を実装する map関数(Gallina引数)を実装する 最後に 参考書籍 はじめに Ltac は、Coq において証明の探索を自動化するための Domain Specific Language です。Coq においてプログラムを記述する言語は Gallina と呼ばれていて、これは依存型を持つ普通の関数型言語で意味論も目的も Ltac とは全く別物です。 Gallina で map関数を実装す… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fwww.orecoli.com%2Fentry%2F2016%2F03%2F04%2F143058" title="CoqのLtacでmap関数を実装する - 俺の Colimit を越えてゆけ" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> http://ecx.images-amazon.com/images/I/41RmEb-xqxL.jpg Hatena Blog https://hatena.blog 2016-03-04 14:30:58 rich https://www.orecoli.com/entry/2016/03/04/143058 1.0 100%