Mercurial > hg > Members > kono > Proof > automaton

comparison a02/agda/lambda.agda @ 139:3be1afb87f82

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add utm
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 14 Mar 2020 17:34:54 +0900
parents 7a0634a7c25a
children b3f05cd08d24
comparison
equal deleted inserted replaced
138:7a0634a7c25a 139:3be1afb87f82
5 A→A = λ A → λ ( a : A ) → a 5 A→A = λ A → λ ( a : A ) → a
6 6
7 lemma2 : (A : Set ) → A → A 7 lemma2 : (A : Set ) → A → A
8 lemma2 A a = {!!} 8 lemma2 A a = {!!}
9 9
10 →intro : {A B : Set } → A → B → ( A → B )
11 →intro _ b = λ x → b
12
13 →elim : {A B : Set } → A → ( A → B ) → B
14 →elim a f = f a
10 15
11 ex1 : {A B : Set} → Set 16 ex1 : {A B : Set} → Set
12 ex1 {A} {B} = ( A → B ) → A → B 17 ex1 {A} {B} = ( A → B ) → A → B
13 18
14 ex1' : {A B : Set} → Set 19 ex1' : {A B : Set} → Set