|
153
|
1 module record-ex where
|
|
|
2
|
|
|
3 data _∨_ (A B : Set) : Set where
|
|
|
4 or1 : A -> A ∨ B
|
|
|
5 or2 : B -> A ∨ B
|
|
|
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
|
|
|
16 f : ( A ∨ B ) -> A
|
|
|
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
|
|
|
38 open import Relation.Binary.PropositionalEquality
|
|
|
39
|
|
|
40 data Nat : Set where
|
|
|
41 zero : Nat
|
|
|
42 suc : Nat -> Nat
|
|
|
43
|
|
|
44 record Mod3 (m : Nat) : Set where
|
|
|
45 field
|
|
|
46 mod3 : (suc (suc (suc m ))) ≡ m
|
|
|
47 n : Nat
|
|
|
48 n = m
|
|
|
49
|
|
|
50 open Mod3
|
|
|
51
|
|
|
52 Lemma1 : ( x : Mod3 ( suc (suc (suc (suc zero))))) ( y : Mod3 ( suc zero ) ) -> n x ≡ n y
|
|
|
53 Lemma1 x y = mod3 y
|
|
|
54
|
