Mercurial > hg > Members > kono > Proof > category

comparison record-ex.agda @ 300:d6a6dd305da2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
arrow and lambda fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 29 Sep 2013 14:01:07 +0900
parents 3249aaddc405
children 0d7fa6fc5979
comparison
equal deleted inserted replaced
299:8c72f5284bc8 300:d6a6dd305da2
1 module record-ex where 1 module record-ex where
2 2
3 data _∨_ (A B : Set) : Set where 3 data _∨_ (A B : Set) : Set where
4 or1 : A -> A ∨ B 4 or1 : A → A ∨ B
5 or2 : B -> A ∨ B 5 or2 : B → A ∨ B
6 6
7 postulate A B C : Set 7 postulate A B C : Set
8 postulate a1 a2 a3 : A 8 postulate a1 a2 a3 : A
9 postulate b1 b2 b3 : B 9 postulate b1 b2 b3 : B
10 10
11 x : ( A ∨ B ) 11 x : ( A ∨ B )
12 x = or1 a1 12 x = or1 a1
13 y : ( A ∨ B ) 13 y : ( A ∨ B )
14 y = or2 b1 14 y = or2 b1
15 15
16 f : ( A ∨ B ) -> A 16 f : ( A ∨ B ) → A
17 f (or1 a) = a 17 f (or1 a) = a
18 f (or2 b) = a1 18 f (or2 b) = a1
19 19
20 record _∧_ (A B : Set) : Set where 20 record _∧_ (A B : Set) : Set where
21 field 21 field
37 37
38 open import Relation.Binary.PropositionalEquality 38 open import Relation.Binary.PropositionalEquality
39 39
40 data Nat : Set where 40 data Nat : Set where
41 zero : Nat 41 zero : Nat
42 suc : Nat -> Nat 42 suc : Nat → Nat
43 43
44 record Mod3 (m : Nat) : Set where 44 record Mod3 (m : Nat) : Set where
45 field 45 field
46 mod3 : (suc (suc (suc m ))) ≡ m 46 mod3 : (suc (suc (suc m ))) ≡ m
47 n : Nat 47 n : Nat
48 n = m 48 n = m
49 49
50 open Mod3 50 open Mod3
51 51
52 Lemma1 : ( x : Mod3 ( suc (suc (suc (suc zero))))) ( y : Mod3 ( suc zero ) ) -> n x ≡ n y 52 Lemma1 : ( x : Mod3 ( suc (suc (suc (suc zero))))) ( y : Mod3 ( suc zero ) ) → n x ≡ n y
53 Lemma1 x y = mod3 y 53 Lemma1 x y = mod3 y
54 54