blob: 0e557aee07722d9c273ace86c1a1b14b8d0631c6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
(* Simple let-patterns *)
Variable A B : Type.
Definition l1 (t : A * B * B) : A := let '(x, y, z) := t in x.
Print l1.
Definition l2 (t : (A * B) * B) : A := let '((x, y), z) := t in x.
Definition l3 (t : A * (B * B)) : A := let '(x, (y, z)) := t in x.
Print l3.
Record someT (A : Type) := mkT { a : nat; b: A }.
Definition l4 A (t : someT A) : nat := let 'mkT _ x y := t in x.
Print l4.
Print sigT.
Definition l5 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
let 'existT _ x y := t return B (projT1 t) in y.
Definition l6 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
let 'existT _ x y as t' := t return B (projT1 t') in y.
Definition l7 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
let 'existT _ x y as t' in sigT _ := t return B (projT1 t') in y.
Definition l8 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
match t with
existT _ x y => y
end.
(** An example from algebra, using let' and inference of return clauses
to deconstruct contexts. *)
Record a_category (A : Type) (hom : A -> A -> Type) := { }.
Definition category := { A : Type & { hom : A -> A -> Type & a_category A hom } }.
Record a_functor (A : Type) (hom : A -> A -> Type) (C : a_category A hom) := { }.
Notation " x :& y " := (@existT _ _ x y) (right associativity, at level 55) : core_scope.
Definition functor (c d : category) :=
let ' A :& homA :& CA := c in
let ' B :& homB :& CB := d in
A -> B.
Definition identity_functor (c : category) : functor c c :=
let 'A :& homA :& CA := c in
fun x => x.
Definition functor_composition (a b c : category) : functor a b -> functor b c -> functor a c :=
let 'A :& homA :& CA := a in
let 'B :& homB :& CB := b in
let 'C :& homB :& CB := c in
fun f g =>
fun x => g (f x).
|
