エントリーの編集
エントリーの編集は全ユーザーに共通の機能です。
必ずガイドラインを一読の上ご利用ください。
うみねこでまなぶCoq - Yet Another Ranha
記事へのコメント0件
- 注目コメント
- 新着コメント
このエントリーにコメントしてみましょう。
注目コメント算出アルゴリズムの一部にLINEヤフー株式会社の「建設的コメント順位付けモデルAPI」を使用しています
- バナー広告なし
- ミュート機能あり
- ダークモード搭載
関連記事
うみねこでまなぶCoq - Yet Another Ranha
Section うみねこ8のメモ. Definition Pow (S : Set) : Type := S -> Prop. Variable Animal : Set. Def... Section うみねこ8のメモ. Definition Pow (S : Set) : Type := S -> Prop. Variable Animal : Set. Definition animal (a : Animal) : Prop := True. Variable human : Pow Animal. Axiom 人間は1人はいてはる : exists h : Animal , human h. Theorem 人間は動物 : forall (x : Animal) , human x -> animal x. Proof. intro a. intro a_is_human. unfold animal. auto. Qed. Hypothesis アッ動物は人間じゃない : forall (x : Animal) , animal x -> ~(human x).