|
153
|
1 module record-ex where
|
|
|
2
|
|
|
3 data _∨_ (A B : Set) : Set where
|
|
300
|
4 or1 : A → A ∨ B
|
|
|
5 or2 : B → A ∨ B
|
|
153
|
6
|
|
|
7 postulate A B C : Set
|
|
|
8 postulate a1 a2 a3 : A
|
|
|
9 postulate b1 b2 b3 : B
|
|
|
10
|
|
|
11 x : ( A ∨ B )
|
|
|
12 x = or1 a1
|
|
|
13 y : ( A ∨ B )
|
|
|
14 y = or2 b1
|
|
|
15
|
|
300
|
16 f : ( A ∨ B ) → A
|
|
153
|
17 f (or1 a) = a
|
|
|
18 f (or2 b) = a1
|
|
|
19
|
|
|
20 record _∧_ (A B : Set) : Set where
|
|
|
21 field
|
|
|
22 and1 : A
|
|
|
23 and2 : B
|
|
|
24
|
|
|
25 z : A ∧ B
|
|
|
26 z = record { and1 = a1 ; and2 = b2 }
|
|
|
27
|
|
|
28 xa : A
|
|
|
29 xa = _∧_.and1 z
|
|
|
30 xb : B
|
|
|
31 xb = _∧_.and2 z
|
|
|
32
|
|
|
33 open _∧_
|
|
|
34
|
|
|
35 ya : A
|
|
|
36 ya = and1 z
|
|
|
37
|
|
315
|
38 lemma1 : A ∧ B → A
|
|
|
39 lemma1 a = and1 a
|
|
|
40
|
|
|
41 lemma2 : A → B → A ∧ B
|
|
|
42 lemma2 a b = record { and1 = a ; and2 = b }
|
|
|
43
|
|
153
|
44 open import Relation.Binary.PropositionalEquality
|
|
|
45
|
|
|
46 data Nat : Set where
|
|
|
47 zero : Nat
|
|
300
|
48 suc : Nat → Nat
|
|
153
|
49
|
|
|
50 record Mod3 (m : Nat) : Set where
|
|
|
51 field
|
|
|
52 mod3 : (suc (suc (suc m ))) ≡ m
|
|
|
53 n : Nat
|
|
|
54 n = m
|
|
|
55
|
|
|
56 open Mod3
|
|
|
57
|
|
300
|
58 Lemma1 : ( x : Mod3 ( suc (suc (suc (suc zero))))) ( y : Mod3 ( suc zero ) ) → n x ≡ n y
|
|
153
|
59 Lemma1 x y = mod3 y
|
|
|
60
|
