Mercurial > hg > Members > kono > Proof > category

comparison level-ex.agda @ 153:3249aaddc405

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sync
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 17 Aug 2013 21:09:34 +0900
parents
children d6a6dd305da2
comparison
equal deleted inserted replaced
152:5435469c6cf0 153:3249aaddc405
1 module level-ex where
2
3 open import Level
4
5 postulate ℓ : Level
6
7 postulate A : Set ℓ
8
9 postulate a : A
10
11 lemma1 : Set ℓ -> A
12 lemma1 = \x -> a
13
14 lemma2 : A -> Set ℓ
15 lemma2 = \x -> A
16
17 lemma3 : Set (suc ℓ)
18 lemma3 = A -> Set ℓ