blob: f8b3d9e1d98beb97288d3f1a188fe2a62165e54b (
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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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.
Declare ML Module "z_syntax_plugin".
(** [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] can also be denoted using a decimal notation;
e.g. [6%positive] abbreviates [xO (xI xH)] *)
Inductive positive : Set :=
| xI : positive -> positive
| xO : positive -> positive
| xH : positive.
Delimit Scope positive_scope with positive.
Bind Scope positive_scope with positive.
Arguments xO _%positive.
Arguments xI _%positive.
(** [N] is a datatype representing natural numbers in a binary way,
by extending the [positive] datatype with a zero.
Numbers in [N] can also be denoted using a decimal notation;
e.g. [6%N] abbreviates [Npos (xO (xI xH))] *)
Inductive N : Set :=
| N0 : N
| Npos : positive -> N.
Delimit Scope N_scope with N.
Bind Scope N_scope with N.
Arguments Npos _%positive.
(** [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] can also be denoted using a decimal notation;
e.g. [(-6)%Z] abbreviates [Zneg (xO (xI xH))] *)
Inductive Z : Set :=
| Z0 : Z
| Zpos : positive -> Z
| Zneg : positive -> Z.
Delimit Scope Z_scope with Z.
Bind Scope Z_scope with Z.
Arguments Zpos _%positive.
Arguments Zneg _%positive.
|
