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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
Set Implicit Arguments.
V7only [Unset Implicit Arguments.].
(** [unit] is a singleton datatype with sole inhabitant [tt] *)
Inductive unit : Set := tt : unit.
(** [bool] is the datatype of the booleans values [true] and [false] *)
Inductive bool : Set := true : bool
| false : bool.
Add Printing If bool.
(** [nat] is the datatype of natural numbers built from [O] and successor [S];
note that zero is the letter O, not the numeral 0 *)
Inductive nat : Set := O : nat
| S : nat->nat.
(** [Empty_set] has no inhabitant *)
Inductive Empty_set:Set :=.
(** [identity A a] is the family of datatypes on [A] whose sole non-empty
member is the singleton datatype [identity A a a] whose
sole inhabitant is denoted [refl_identity A a] *)
Inductive identity [A:Set; a:A] : A->Set :=
refl_identity: (identity A a a).
Hints Resolve refl_identity : core v62.
(** [option A] is the extension of A with a dummy element None *)
Inductive option [A:Set] : Set := Some : A -> (option A) | None : (option A).
Arguments Scope option [ type_scope ].
(** [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *)
(* Syntax defined in Specif.v *)
Inductive sum [A,B:Set] : Set
:= inl : A -> (sum A B)
| inr : B -> (sum A B).
Infix "+" sum (at level 4, left associativity) : type_scope.
Arguments Scope sum [type_scope type_scope].
(** [prod A B], written [A * B], is the product of [A] and [B];
the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *)
Inductive prod [A,B:Set] : Set := pair : A -> B -> (prod A B).
Add Printing Let prod.
Arguments Scope prod [type_scope type_scope].
Notation "x * y" := (prod x y) (at level 3, right associativity) : type_scope
V8only (at level 30, left associativity).
Notation "( x , y )" := (pair ? ? x y) (at level 0)
V8only "x , y" (at level 150, left associativity).
Section projections.
Variables A,B:Set.
Definition fst := [p:(prod A B)]Cases p of (pair x y) => x end.
Definition snd := [p:(prod A B)]Cases p of (pair x y) => y end.
End projections.
Notation Fst := (fst ? ?).
Notation Snd := (snd ? ?).
Hints Resolve pair inl inr : core v62.
(** Parsing only of things in [Datatypes.v] *)
V7only[
Notation "< A , B > ( x , y )" := (pair A B x y) (at level 1, only parsing, A annot).
Notation "< A , B > 'Fst' ( p )" := (fst A B p) (at level 1, only parsing, A annot).
Notation "< A , B > 'Snd' ( p )" := (snd A B p) (at level 1, only parsing, A annot).
].
|
