恒等関数

フィッグワン

imp

$$ imp \ a \ b:=a\rightarrow b $$

ref

$$ ref \ U \ R:= \forall x:U,R \ x \ x $$

$$ ref \ imp $$

      Require Import Utf8.

Set Implicit Arguments.

Definition imp a b:=a → b.

Definition ref U R:=∀x:U,R x x.

Goal ref imp.
Abort.

投稿日：2020年11月24日

更新日：2020年11月24日

投稿者

高評価したユーザはいません

バッジはありません。

バッチを贈って投稿者を応援しよう

バッチを贈ると投稿者に現金やAmazonのギフトカードが還元されます。