blob: 879674584e105f384ea9bb605bfaf10d06323233 (
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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** * Binary Numerical Datatypes *)
Set Implicit Arguments.
(** [positive] is a datatype representing the strictly positive integers
in a binary way. Starting from 1 (represented by [xH]), one can
add a new least significant digit via [xO] (digit 0) or [xI] (digit 1).
Numbers in [positive] will also be denoted using a decimal notation;
e.g. [6%positive] will abbreviate [xO (xI xH)] *)
Inductive positive : Set :=
| xI : positive -> positive
| xO : positive -> positive
| xH : positive.
Declare Scope positive_scope.
Delimit Scope positive_scope with positive.
Bind Scope positive_scope with positive.
Arguments xO _%positive.
Arguments xI _%positive.
Register positive as num.pos.type.
Register xI as num.pos.xI.
Register xO as num.pos.xO.
Register xH as num.pos.xH.
(** [N] is a datatype representing natural numbers in a binary way,
by extending the [positive] datatype with a zero.
Numbers in [N] will also be denoted using a decimal notation;
e.g. [6%N] will abbreviate [Npos (xO (xI xH))] *)
Inductive N : Set :=
| N0 : N
| Npos : positive -> N.
Declare Scope N_scope.
Delimit Scope N_scope with N.
Bind Scope N_scope with N.
Arguments Npos _%positive.
Register N as num.N.type.
Register N0 as num.N.N0.
Register Npos as num.N.Npos.
(** [Z] is a datatype representing the integers in a binary way.
An integer is either zero or a strictly positive number
(coded as a [positive]) or a strictly negative number
(whose opposite is stored as a [positive] value).
Numbers in [Z] will also be denoted using a decimal notation;
e.g. [(-6)%Z] will abbreviate [Zneg (xO (xI xH))] *)
Inductive Z : Set :=
| Z0 : Z
| Zpos : positive -> Z
| Zneg : positive -> Z.
Declare Scope Z_scope.
Delimit Scope Z_scope with Z.
Bind Scope Z_scope with Z.
Arguments Zpos _%positive.
Arguments Zneg _%positive.
Register Z as num.Z.type.
Register Z0 as num.Z.Z0.
Register Zpos as num.Z.Zpos.
Register Zneg as num.Z.Zneg.
|
