Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Newer
Older
100644 32 lines (26 sloc) 0.513 kb
652478c Added 'where' keyword in Data declarations
eb authored
1 Data Eq (A:*)(a:A) : (b:A)* where refl : Eq A a a;
4a53940 Initial version
eb authored
2
3 repl : (A:*)(a:A)(b:A)(q:Eq _ a b)(P:(a:A)*)(p:P a)(P b);
4 intros;
5 induction q;
6 fill p;
7 Qed;
8 Freeze repl;
9
10 trans : (A:*)(a:A)(b:A)(c:A)(p:Eq _ a b)(q:Eq _ b c)(Eq _ a c);
11 intros;
12 induction q;
13 fill p;
14 Qed;
15 Freeze trans;
16
17 sym : (A:*)(a:A)(b:A)(p:Eq _ a b)(Eq _ b a);
18 intros;
19 induction p;
20 refine refl;
21 Qed;
22 Freeze sym;
23
24 Repl Eq repl sym;
25
26 eq_resp_f:(A,B:*)(f:(a:A)B)(x:A)(y:A)(q:Eq _ x y)(Eq _ (f x) (f y));
27 intros;
28 induction q;
29 refine refl;
30 Qed;
31 Freeze eq_resp_f;
Something went wrong with that request. Please try again.