Coq で遊ぶその9: or について。ジョーカー。Implicit Arguments。 - 言語ゲームこんな日記にもたまにブックマークを付けてくださる方がいらっしゃて有り難い事です。しかし自分が理解した順番に書いてるだけなので、話題が前に後ろに飛びまくって読みづらくて申し訳ない。いつかそのうちちゃんと分かりやすい順番にまとめたいと思っていますので、生暖かく見守り下さい。 さて、今回自分で定理を作ってみます。今回作る定理は「又」です。「True [又] False」のように使います。いわゆる or の事です。今回の目的は、forall と Implicit Arguments の性質に慣れる事です。Implicit Arguments は便利ですが、慣れないと凶悪に難しいです。逆に、これに慣れて forall が単なる関数型と同じように見えてくると断然心が軽くなります。 あと余談ですが、日本語でプログラムを書くのって意外と良いですね。漢字、ひらがな、アルファベットと文字が混ざるとアクセントに
