yoshihiro503 https://blog.hatena.ne.jp/yoshihiro503/ にわとり小屋でのプログラミング https://yosh.hateblo.jp/ Require Import Inductive Definition Extraction Coqで "Hello, world!" を標準出力させるのはちょっと難しい。 なぜならCoqはプログラミング言語ではなく、システム開発の支援をするツールであり、扱う言語は純粋関数型言語だからだ。純粋でない部分（外部に標準出力する部分）のために、今回は16行ほどのOCamlの力を借りて実装した。 具体的には次の２つのファイルを作った。 helloworld.v main.ml (16行のOCamlコード) ちなみにCoqでは、文字は8bitのascii型、文字列はasciiのリストみたいな感じで定義されている。 (* Coqのスタンダードライブラリより *) Inductive ascii :… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fyosh.hateblo.jp%2Fentry%2F20070618%2Fp1" title="CoqでHello, world!（改） - にわとり小屋でのプログラミング" 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 2007-06-18 00:00:00 rich https://yosh.hateblo.jp/entry/20070618/p1 1.0 100%