恒等関数

フィッグワン

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日

この記事を高評価した人

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

バッジはありません。

165

コメントはありません。

読み込み中