CoqでHello, world!（改） - にわとり小屋でのプログラミング
Coqで "Hello, world!" を標準出力させるのはちょっと難しい。 なぜならCoqはプログラミング言語ではなく、システム開発の支援をするツールであり、扱う言語は純粋関数型言語だからだ。 純粋でない部分（外部に標準出力する部分）のために、今回は16行ほどのOCamlの力を借りて実装した。 具体的には次の２つのファイルを作った。 helloworld.v main.ml (16行のOCamlコード) ちなみにCoqでは、文字は8bitのascii型、文字列はasciiのリストみたいな感じで定義されている。 (* Coqのスタンダードライブラリより *) Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool). Inductive string : Set := | EmptyString : string | String :
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
『CSNagoya 第5回GC本読書会』に行ってきました - みずぴー日記
