aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init')
-rw-r--r--theories/Init/Byte.v830
-rw-r--r--theories/Init/Prelude.v5
2 files changed, 835 insertions, 0 deletions
diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v
new file mode 100644
index 0000000000..eede9d5028
--- /dev/null
+++ b/theories/Init/Byte.v
@@ -0,0 +1,830 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+(** * Bytes *)
+
+Require Import Coq.Init.Datatypes.
+Require Import Coq.Init.Logic.
+Require Import Coq.Init.Specif.
+Require Coq.Init.Nat.
+
+Declare ML Module "string_notation_plugin".
+
+(** We define an inductive for use with the [String Notation] command
+ which contains all ascii characters. We use 256 constructors for
+ efficiency and ease of conversion. *)
+
+Declare Scope byte_scope.
+Delimit Scope byte_scope with byte.
+
+Inductive byte :=
+| x00
+| x01
+| x02
+| x03
+| x04
+| x05
+| x06
+| x07
+| x08
+| x09
+| x0a
+| x0b
+| x0c
+| x0d
+| x0e
+| x0f
+| x10
+| x11
+| x12
+| x13
+| x14
+| x15
+| x16
+| x17
+| x18
+| x19
+| x1a
+| x1b
+| x1c
+| x1d
+| x1e
+| x1f
+| x20
+| x21
+| x22
+| x23
+| x24
+| x25
+| x26
+| x27
+| x28
+| x29
+| x2a
+| x2b
+| x2c
+| x2d
+| x2e
+| x2f
+| x30
+| x31
+| x32
+| x33
+| x34
+| x35
+| x36
+| x37
+| x38
+| x39
+| x3a
+| x3b
+| x3c
+| x3d
+| x3e
+| x3f
+| x40
+| x41
+| x42
+| x43
+| x44
+| x45
+| x46
+| x47
+| x48
+| x49
+| x4a
+| x4b
+| x4c
+| x4d
+| x4e
+| x4f
+| x50
+| x51
+| x52
+| x53
+| x54
+| x55
+| x56
+| x57
+| x58
+| x59
+| x5a
+| x5b
+| x5c
+| x5d
+| x5e
+| x5f
+| x60
+| x61
+| x62
+| x63
+| x64
+| x65
+| x66
+| x67
+| x68
+| x69
+| x6a
+| x6b
+| x6c
+| x6d
+| x6e
+| x6f
+| x70
+| x71
+| x72
+| x73
+| x74
+| x75
+| x76
+| x77
+| x78
+| x79
+| x7a
+| x7b
+| x7c
+| x7d
+| x7e
+| x7f
+| x80
+| x81
+| x82
+| x83
+| x84
+| x85
+| x86
+| x87
+| x88
+| x89
+| x8a
+| x8b
+| x8c
+| x8d
+| x8e
+| x8f
+| x90
+| x91
+| x92
+| x93
+| x94
+| x95
+| x96
+| x97
+| x98
+| x99
+| x9a
+| x9b
+| x9c
+| x9d
+| x9e
+| x9f
+| xa0
+| xa1
+| xa2
+| xa3
+| xa4
+| xa5
+| xa6
+| xa7
+| xa8
+| xa9
+| xaa
+| xab
+| xac
+| xad
+| xae
+| xaf
+| xb0
+| xb1
+| xb2
+| xb3
+| xb4
+| xb5
+| xb6
+| xb7
+| xb8
+| xb9
+| xba
+| xbb
+| xbc
+| xbd
+| xbe
+| xbf
+| xc0
+| xc1
+| xc2
+| xc3
+| xc4
+| xc5
+| xc6
+| xc7
+| xc8
+| xc9
+| xca
+| xcb
+| xcc
+| xcd
+| xce
+| xcf
+| xd0
+| xd1
+| xd2
+| xd3
+| xd4
+| xd5
+| xd6
+| xd7
+| xd8
+| xd9
+| xda
+| xdb
+| xdc
+| xdd
+| xde
+| xdf
+| xe0
+| xe1
+| xe2
+| xe3
+| xe4
+| xe5
+| xe6
+| xe7
+| xe8
+| xe9
+| xea
+| xeb
+| xec
+| xed
+| xee
+| xef
+| xf0
+| xf1
+| xf2
+| xf3
+| xf4
+| xf5
+| xf6
+| xf7
+| xf8
+| xf9
+| xfa
+| xfb
+| xfc
+| xfd
+| xfe
+| xff
+.
+
+Bind Scope byte_scope with byte.
+
+Register byte as core.byte.type.
+
+Local Notation "0" := false.
+Local Notation "1" := true.
+
+(** We pick a definition that matches with [Ascii.ascii] *)
+Definition of_bits (b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))) : byte
+ := match b with
+ | (0,(0,(0,(0,(0,(0,(0,0))))))) => x00
+ | (1,(0,(0,(0,(0,(0,(0,0))))))) => x01
+ | (0,(1,(0,(0,(0,(0,(0,0))))))) => x02
+ | (1,(1,(0,(0,(0,(0,(0,0))))))) => x03
+ | (0,(0,(1,(0,(0,(0,(0,0))))))) => x04
+ | (1,(0,(1,(0,(0,(0,(0,0))))))) => x05
+ | (0,(1,(1,(0,(0,(0,(0,0))))))) => x06
+ | (1,(1,(1,(0,(0,(0,(0,0))))))) => x07
+ | (0,(0,(0,(1,(0,(0,(0,0))))))) => x08
+ | (1,(0,(0,(1,(0,(0,(0,0))))))) => x09
+ | (0,(1,(0,(1,(0,(0,(0,0))))))) => x0a
+ | (1,(1,(0,(1,(0,(0,(0,0))))))) => x0b
+ | (0,(0,(1,(1,(0,(0,(0,0))))))) => x0c
+ | (1,(0,(1,(1,(0,(0,(0,0))))))) => x0d
+ | (0,(1,(1,(1,(0,(0,(0,0))))))) => x0e
+ | (1,(1,(1,(1,(0,(0,(0,0))))))) => x0f
+ | (0,(0,(0,(0,(1,(0,(0,0))))))) => x10
+ | (1,(0,(0,(0,(1,(0,(0,0))))))) => x11
+ | (0,(1,(0,(0,(1,(0,(0,0))))))) => x12
+ | (1,(1,(0,(0,(1,(0,(0,0))))))) => x13
+ | (0,(0,(1,(0,(1,(0,(0,0))))))) => x14
+ | (1,(0,(1,(0,(1,(0,(0,0))))))) => x15
+ | (0,(1,(1,(0,(1,(0,(0,0))))))) => x16
+ | (1,(1,(1,(0,(1,(0,(0,0))))))) => x17
+ | (0,(0,(0,(1,(1,(0,(0,0))))))) => x18
+ | (1,(0,(0,(1,(1,(0,(0,0))))))) => x19
+ | (0,(1,(0,(1,(1,(0,(0,0))))))) => x1a
+ | (1,(1,(0,(1,(1,(0,(0,0))))))) => x1b
+ | (0,(0,(1,(1,(1,(0,(0,0))))))) => x1c
+ | (1,(0,(1,(1,(1,(0,(0,0))))))) => x1d
+ | (0,(1,(1,(1,(1,(0,(0,0))))))) => x1e
+ | (1,(1,(1,(1,(1,(0,(0,0))))))) => x1f
+ | (0,(0,(0,(0,(0,(1,(0,0))))))) => x20
+ | (1,(0,(0,(0,(0,(1,(0,0))))))) => x21
+ | (0,(1,(0,(0,(0,(1,(0,0))))))) => x22
+ | (1,(1,(0,(0,(0,(1,(0,0))))))) => x23
+ | (0,(0,(1,(0,(0,(1,(0,0))))))) => x24
+ | (1,(0,(1,(0,(0,(1,(0,0))))))) => x25
+ | (0,(1,(1,(0,(0,(1,(0,0))))))) => x26
+ | (1,(1,(1,(0,(0,(1,(0,0))))))) => x27
+ | (0,(0,(0,(1,(0,(1,(0,0))))))) => x28
+ | (1,(0,(0,(1,(0,(1,(0,0))))))) => x29
+ | (0,(1,(0,(1,(0,(1,(0,0))))))) => x2a
+ | (1,(1,(0,(1,(0,(1,(0,0))))))) => x2b
+ | (0,(0,(1,(1,(0,(1,(0,0))))))) => x2c
+ | (1,(0,(1,(1,(0,(1,(0,0))))))) => x2d
+ | (0,(1,(1,(1,(0,(1,(0,0))))))) => x2e
+ | (1,(1,(1,(1,(0,(1,(0,0))))))) => x2f
+ | (0,(0,(0,(0,(1,(1,(0,0))))))) => x30
+ | (1,(0,(0,(0,(1,(1,(0,0))))))) => x31
+ | (0,(1,(0,(0,(1,(1,(0,0))))))) => x32
+ | (1,(1,(0,(0,(1,(1,(0,0))))))) => x33
+ | (0,(0,(1,(0,(1,(1,(0,0))))))) => x34
+ | (1,(0,(1,(0,(1,(1,(0,0))))))) => x35
+ | (0,(1,(1,(0,(1,(1,(0,0))))))) => x36
+ | (1,(1,(1,(0,(1,(1,(0,0))))))) => x37
+ | (0,(0,(0,(1,(1,(1,(0,0))))))) => x38
+ | (1,(0,(0,(1,(1,(1,(0,0))))))) => x39
+ | (0,(1,(0,(1,(1,(1,(0,0))))))) => x3a
+ | (1,(1,(0,(1,(1,(1,(0,0))))))) => x3b
+ | (0,(0,(1,(1,(1,(1,(0,0))))))) => x3c
+ | (1,(0,(1,(1,(1,(1,(0,0))))))) => x3d
+ | (0,(1,(1,(1,(1,(1,(0,0))))))) => x3e
+ | (1,(1,(1,(1,(1,(1,(0,0))))))) => x3f
+ | (0,(0,(0,(0,(0,(0,(1,0))))))) => x40
+ | (1,(0,(0,(0,(0,(0,(1,0))))))) => x41
+ | (0,(1,(0,(0,(0,(0,(1,0))))))) => x42
+ | (1,(1,(0,(0,(0,(0,(1,0))))))) => x43
+ | (0,(0,(1,(0,(0,(0,(1,0))))))) => x44
+ | (1,(0,(1,(0,(0,(0,(1,0))))))) => x45
+ | (0,(1,(1,(0,(0,(0,(1,0))))))) => x46
+ | (1,(1,(1,(0,(0,(0,(1,0))))))) => x47
+ | (0,(0,(0,(1,(0,(0,(1,0))))))) => x48
+ | (1,(0,(0,(1,(0,(0,(1,0))))))) => x49
+ | (0,(1,(0,(1,(0,(0,(1,0))))))) => x4a
+ | (1,(1,(0,(1,(0,(0,(1,0))))))) => x4b
+ | (0,(0,(1,(1,(0,(0,(1,0))))))) => x4c
+ | (1,(0,(1,(1,(0,(0,(1,0))))))) => x4d
+ | (0,(1,(1,(1,(0,(0,(1,0))))))) => x4e
+ | (1,(1,(1,(1,(0,(0,(1,0))))))) => x4f
+ | (0,(0,(0,(0,(1,(0,(1,0))))))) => x50
+ | (1,(0,(0,(0,(1,(0,(1,0))))))) => x51
+ | (0,(1,(0,(0,(1,(0,(1,0))))))) => x52
+ | (1,(1,(0,(0,(1,(0,(1,0))))))) => x53
+ | (0,(0,(1,(0,(1,(0,(1,0))))))) => x54
+ | (1,(0,(1,(0,(1,(0,(1,0))))))) => x55
+ | (0,(1,(1,(0,(1,(0,(1,0))))))) => x56
+ | (1,(1,(1,(0,(1,(0,(1,0))))))) => x57
+ | (0,(0,(0,(1,(1,(0,(1,0))))))) => x58
+ | (1,(0,(0,(1,(1,(0,(1,0))))))) => x59
+ | (0,(1,(0,(1,(1,(0,(1,0))))))) => x5a
+ | (1,(1,(0,(1,(1,(0,(1,0))))))) => x5b
+ | (0,(0,(1,(1,(1,(0,(1,0))))))) => x5c
+ | (1,(0,(1,(1,(1,(0,(1,0))))))) => x5d
+ | (0,(1,(1,(1,(1,(0,(1,0))))))) => x5e
+ | (1,(1,(1,(1,(1,(0,(1,0))))))) => x5f
+ | (0,(0,(0,(0,(0,(1,(1,0))))))) => x60
+ | (1,(0,(0,(0,(0,(1,(1,0))))))) => x61
+ | (0,(1,(0,(0,(0,(1,(1,0))))))) => x62
+ | (1,(1,(0,(0,(0,(1,(1,0))))))) => x63
+ | (0,(0,(1,(0,(0,(1,(1,0))))))) => x64
+ | (1,(0,(1,(0,(0,(1,(1,0))))))) => x65
+ | (0,(1,(1,(0,(0,(1,(1,0))))))) => x66
+ | (1,(1,(1,(0,(0,(1,(1,0))))))) => x67
+ | (0,(0,(0,(1,(0,(1,(1,0))))))) => x68
+ | (1,(0,(0,(1,(0,(1,(1,0))))))) => x69
+ | (0,(1,(0,(1,(0,(1,(1,0))))))) => x6a
+ | (1,(1,(0,(1,(0,(1,(1,0))))))) => x6b
+ | (0,(0,(1,(1,(0,(1,(1,0))))))) => x6c
+ | (1,(0,(1,(1,(0,(1,(1,0))))))) => x6d
+ | (0,(1,(1,(1,(0,(1,(1,0))))))) => x6e
+ | (1,(1,(1,(1,(0,(1,(1,0))))))) => x6f
+ | (0,(0,(0,(0,(1,(1,(1,0))))))) => x70
+ | (1,(0,(0,(0,(1,(1,(1,0))))))) => x71
+ | (0,(1,(0,(0,(1,(1,(1,0))))))) => x72
+ | (1,(1,(0,(0,(1,(1,(1,0))))))) => x73
+ | (0,(0,(1,(0,(1,(1,(1,0))))))) => x74
+ | (1,(0,(1,(0,(1,(1,(1,0))))))) => x75
+ | (0,(1,(1,(0,(1,(1,(1,0))))))) => x76
+ | (1,(1,(1,(0,(1,(1,(1,0))))))) => x77
+ | (0,(0,(0,(1,(1,(1,(1,0))))))) => x78
+ | (1,(0,(0,(1,(1,(1,(1,0))))))) => x79
+ | (0,(1,(0,(1,(1,(1,(1,0))))))) => x7a
+ | (1,(1,(0,(1,(1,(1,(1,0))))))) => x7b
+ | (0,(0,(1,(1,(1,(1,(1,0))))))) => x7c
+ | (1,(0,(1,(1,(1,(1,(1,0))))))) => x7d
+ | (0,(1,(1,(1,(1,(1,(1,0))))))) => x7e
+ | (1,(1,(1,(1,(1,(1,(1,0))))))) => x7f
+ | (0,(0,(0,(0,(0,(0,(0,1))))))) => x80
+ | (1,(0,(0,(0,(0,(0,(0,1))))))) => x81
+ | (0,(1,(0,(0,(0,(0,(0,1))))))) => x82
+ | (1,(1,(0,(0,(0,(0,(0,1))))))) => x83
+ | (0,(0,(1,(0,(0,(0,(0,1))))))) => x84
+ | (1,(0,(1,(0,(0,(0,(0,1))))))) => x85
+ | (0,(1,(1,(0,(0,(0,(0,1))))))) => x86
+ | (1,(1,(1,(0,(0,(0,(0,1))))))) => x87
+ | (0,(0,(0,(1,(0,(0,(0,1))))))) => x88
+ | (1,(0,(0,(1,(0,(0,(0,1))))))) => x89
+ | (0,(1,(0,(1,(0,(0,(0,1))))))) => x8a
+ | (1,(1,(0,(1,(0,(0,(0,1))))))) => x8b
+ | (0,(0,(1,(1,(0,(0,(0,1))))))) => x8c
+ | (1,(0,(1,(1,(0,(0,(0,1))))))) => x8d
+ | (0,(1,(1,(1,(0,(0,(0,1))))))) => x8e
+ | (1,(1,(1,(1,(0,(0,(0,1))))))) => x8f
+ | (0,(0,(0,(0,(1,(0,(0,1))))))) => x90
+ | (1,(0,(0,(0,(1,(0,(0,1))))))) => x91
+ | (0,(1,(0,(0,(1,(0,(0,1))))))) => x92
+ | (1,(1,(0,(0,(1,(0,(0,1))))))) => x93
+ | (0,(0,(1,(0,(1,(0,(0,1))))))) => x94
+ | (1,(0,(1,(0,(1,(0,(0,1))))))) => x95
+ | (0,(1,(1,(0,(1,(0,(0,1))))))) => x96
+ | (1,(1,(1,(0,(1,(0,(0,1))))))) => x97
+ | (0,(0,(0,(1,(1,(0,(0,1))))))) => x98
+ | (1,(0,(0,(1,(1,(0,(0,1))))))) => x99
+ | (0,(1,(0,(1,(1,(0,(0,1))))))) => x9a
+ | (1,(1,(0,(1,(1,(0,(0,1))))))) => x9b
+ | (0,(0,(1,(1,(1,(0,(0,1))))))) => x9c
+ | (1,(0,(1,(1,(1,(0,(0,1))))))) => x9d
+ | (0,(1,(1,(1,(1,(0,(0,1))))))) => x9e
+ | (1,(1,(1,(1,(1,(0,(0,1))))))) => x9f
+ | (0,(0,(0,(0,(0,(1,(0,1))))))) => xa0
+ | (1,(0,(0,(0,(0,(1,(0,1))))))) => xa1
+ | (0,(1,(0,(0,(0,(1,(0,1))))))) => xa2
+ | (1,(1,(0,(0,(0,(1,(0,1))))))) => xa3
+ | (0,(0,(1,(0,(0,(1,(0,1))))))) => xa4
+ | (1,(0,(1,(0,(0,(1,(0,1))))))) => xa5
+ | (0,(1,(1,(0,(0,(1,(0,1))))))) => xa6
+ | (1,(1,(1,(0,(0,(1,(0,1))))))) => xa7
+ | (0,(0,(0,(1,(0,(1,(0,1))))))) => xa8
+ | (1,(0,(0,(1,(0,(1,(0,1))))))) => xa9
+ | (0,(1,(0,(1,(0,(1,(0,1))))))) => xaa
+ | (1,(1,(0,(1,(0,(1,(0,1))))))) => xab
+ | (0,(0,(1,(1,(0,(1,(0,1))))))) => xac
+ | (1,(0,(1,(1,(0,(1,(0,1))))))) => xad
+ | (0,(1,(1,(1,(0,(1,(0,1))))))) => xae
+ | (1,(1,(1,(1,(0,(1,(0,1))))))) => xaf
+ | (0,(0,(0,(0,(1,(1,(0,1))))))) => xb0
+ | (1,(0,(0,(0,(1,(1,(0,1))))))) => xb1
+ | (0,(1,(0,(0,(1,(1,(0,1))))))) => xb2
+ | (1,(1,(0,(0,(1,(1,(0,1))))))) => xb3
+ | (0,(0,(1,(0,(1,(1,(0,1))))))) => xb4
+ | (1,(0,(1,(0,(1,(1,(0,1))))))) => xb5
+ | (0,(1,(1,(0,(1,(1,(0,1))))))) => xb6
+ | (1,(1,(1,(0,(1,(1,(0,1))))))) => xb7
+ | (0,(0,(0,(1,(1,(1,(0,1))))))) => xb8
+ | (1,(0,(0,(1,(1,(1,(0,1))))))) => xb9
+ | (0,(1,(0,(1,(1,(1,(0,1))))))) => xba
+ | (1,(1,(0,(1,(1,(1,(0,1))))))) => xbb
+ | (0,(0,(1,(1,(1,(1,(0,1))))))) => xbc
+ | (1,(0,(1,(1,(1,(1,(0,1))))))) => xbd
+ | (0,(1,(1,(1,(1,(1,(0,1))))))) => xbe
+ | (1,(1,(1,(1,(1,(1,(0,1))))))) => xbf
+ | (0,(0,(0,(0,(0,(0,(1,1))))))) => xc0
+ | (1,(0,(0,(0,(0,(0,(1,1))))))) => xc1
+ | (0,(1,(0,(0,(0,(0,(1,1))))))) => xc2
+ | (1,(1,(0,(0,(0,(0,(1,1))))))) => xc3
+ | (0,(0,(1,(0,(0,(0,(1,1))))))) => xc4
+ | (1,(0,(1,(0,(0,(0,(1,1))))))) => xc5
+ | (0,(1,(1,(0,(0,(0,(1,1))))))) => xc6
+ | (1,(1,(1,(0,(0,(0,(1,1))))))) => xc7
+ | (0,(0,(0,(1,(0,(0,(1,1))))))) => xc8
+ | (1,(0,(0,(1,(0,(0,(1,1))))))) => xc9
+ | (0,(1,(0,(1,(0,(0,(1,1))))))) => xca
+ | (1,(1,(0,(1,(0,(0,(1,1))))))) => xcb
+ | (0,(0,(1,(1,(0,(0,(1,1))))))) => xcc
+ | (1,(0,(1,(1,(0,(0,(1,1))))))) => xcd
+ | (0,(1,(1,(1,(0,(0,(1,1))))))) => xce
+ | (1,(1,(1,(1,(0,(0,(1,1))))))) => xcf
+ | (0,(0,(0,(0,(1,(0,(1,1))))))) => xd0
+ | (1,(0,(0,(0,(1,(0,(1,1))))))) => xd1
+ | (0,(1,(0,(0,(1,(0,(1,1))))))) => xd2
+ | (1,(1,(0,(0,(1,(0,(1,1))))))) => xd3
+ | (0,(0,(1,(0,(1,(0,(1,1))))))) => xd4
+ | (1,(0,(1,(0,(1,(0,(1,1))))))) => xd5
+ | (0,(1,(1,(0,(1,(0,(1,1))))))) => xd6
+ | (1,(1,(1,(0,(1,(0,(1,1))))))) => xd7
+ | (0,(0,(0,(1,(1,(0,(1,1))))))) => xd8
+ | (1,(0,(0,(1,(1,(0,(1,1))))))) => xd9
+ | (0,(1,(0,(1,(1,(0,(1,1))))))) => xda
+ | (1,(1,(0,(1,(1,(0,(1,1))))))) => xdb
+ | (0,(0,(1,(1,(1,(0,(1,1))))))) => xdc
+ | (1,(0,(1,(1,(1,(0,(1,1))))))) => xdd
+ | (0,(1,(1,(1,(1,(0,(1,1))))))) => xde
+ | (1,(1,(1,(1,(1,(0,(1,1))))))) => xdf
+ | (0,(0,(0,(0,(0,(1,(1,1))))))) => xe0
+ | (1,(0,(0,(0,(0,(1,(1,1))))))) => xe1
+ | (0,(1,(0,(0,(0,(1,(1,1))))))) => xe2
+ | (1,(1,(0,(0,(0,(1,(1,1))))))) => xe3
+ | (0,(0,(1,(0,(0,(1,(1,1))))))) => xe4
+ | (1,(0,(1,(0,(0,(1,(1,1))))))) => xe5
+ | (0,(1,(1,(0,(0,(1,(1,1))))))) => xe6
+ | (1,(1,(1,(0,(0,(1,(1,1))))))) => xe7
+ | (0,(0,(0,(1,(0,(1,(1,1))))))) => xe8
+ | (1,(0,(0,(1,(0,(1,(1,1))))))) => xe9
+ | (0,(1,(0,(1,(0,(1,(1,1))))))) => xea
+ | (1,(1,(0,(1,(0,(1,(1,1))))))) => xeb
+ | (0,(0,(1,(1,(0,(1,(1,1))))))) => xec
+ | (1,(0,(1,(1,(0,(1,(1,1))))))) => xed
+ | (0,(1,(1,(1,(0,(1,(1,1))))))) => xee
+ | (1,(1,(1,(1,(0,(1,(1,1))))))) => xef
+ | (0,(0,(0,(0,(1,(1,(1,1))))))) => xf0
+ | (1,(0,(0,(0,(1,(1,(1,1))))))) => xf1
+ | (0,(1,(0,(0,(1,(1,(1,1))))))) => xf2
+ | (1,(1,(0,(0,(1,(1,(1,1))))))) => xf3
+ | (0,(0,(1,(0,(1,(1,(1,1))))))) => xf4
+ | (1,(0,(1,(0,(1,(1,(1,1))))))) => xf5
+ | (0,(1,(1,(0,(1,(1,(1,1))))))) => xf6
+ | (1,(1,(1,(0,(1,(1,(1,1))))))) => xf7
+ | (0,(0,(0,(1,(1,(1,(1,1))))))) => xf8
+ | (1,(0,(0,(1,(1,(1,(1,1))))))) => xf9
+ | (0,(1,(0,(1,(1,(1,(1,1))))))) => xfa
+ | (1,(1,(0,(1,(1,(1,(1,1))))))) => xfb
+ | (0,(0,(1,(1,(1,(1,(1,1))))))) => xfc
+ | (1,(0,(1,(1,(1,(1,(1,1))))))) => xfd
+ | (0,(1,(1,(1,(1,(1,(1,1))))))) => xfe
+ | (1,(1,(1,(1,(1,(1,(1,1))))))) => xff
+ end.
+
+Definition to_bits (b : byte) : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
+ := match b with
+ | x00 => (0,(0,(0,(0,(0,(0,(0,0)))))))
+ | x01 => (1,(0,(0,(0,(0,(0,(0,0)))))))
+ | x02 => (0,(1,(0,(0,(0,(0,(0,0)))))))
+ | x03 => (1,(1,(0,(0,(0,(0,(0,0)))))))
+ | x04 => (0,(0,(1,(0,(0,(0,(0,0)))))))
+ | x05 => (1,(0,(1,(0,(0,(0,(0,0)))))))
+ | x06 => (0,(1,(1,(0,(0,(0,(0,0)))))))
+ | x07 => (1,(1,(1,(0,(0,(0,(0,0)))))))
+ | x08 => (0,(0,(0,(1,(0,(0,(0,0)))))))
+ | x09 => (1,(0,(0,(1,(0,(0,(0,0)))))))
+ | x0a => (0,(1,(0,(1,(0,(0,(0,0)))))))
+ | x0b => (1,(1,(0,(1,(0,(0,(0,0)))))))
+ | x0c => (0,(0,(1,(1,(0,(0,(0,0)))))))
+ | x0d => (1,(0,(1,(1,(0,(0,(0,0)))))))
+ | x0e => (0,(1,(1,(1,(0,(0,(0,0)))))))
+ | x0f => (1,(1,(1,(1,(0,(0,(0,0)))))))
+ | x10 => (0,(0,(0,(0,(1,(0,(0,0)))))))
+ | x11 => (1,(0,(0,(0,(1,(0,(0,0)))))))
+ | x12 => (0,(1,(0,(0,(1,(0,(0,0)))))))
+ | x13 => (1,(1,(0,(0,(1,(0,(0,0)))))))
+ | x14 => (0,(0,(1,(0,(1,(0,(0,0)))))))
+ | x15 => (1,(0,(1,(0,(1,(0,(0,0)))))))
+ | x16 => (0,(1,(1,(0,(1,(0,(0,0)))))))
+ | x17 => (1,(1,(1,(0,(1,(0,(0,0)))))))
+ | x18 => (0,(0,(0,(1,(1,(0,(0,0)))))))
+ | x19 => (1,(0,(0,(1,(1,(0,(0,0)))))))
+ | x1a => (0,(1,(0,(1,(1,(0,(0,0)))))))
+ | x1b => (1,(1,(0,(1,(1,(0,(0,0)))))))
+ | x1c => (0,(0,(1,(1,(1,(0,(0,0)))))))
+ | x1d => (1,(0,(1,(1,(1,(0,(0,0)))))))
+ | x1e => (0,(1,(1,(1,(1,(0,(0,0)))))))
+ | x1f => (1,(1,(1,(1,(1,(0,(0,0)))))))
+ | x20 => (0,(0,(0,(0,(0,(1,(0,0)))))))
+ | x21 => (1,(0,(0,(0,(0,(1,(0,0)))))))
+ | x22 => (0,(1,(0,(0,(0,(1,(0,0)))))))
+ | x23 => (1,(1,(0,(0,(0,(1,(0,0)))))))
+ | x24 => (0,(0,(1,(0,(0,(1,(0,0)))))))
+ | x25 => (1,(0,(1,(0,(0,(1,(0,0)))))))
+ | x26 => (0,(1,(1,(0,(0,(1,(0,0)))))))
+ | x27 => (1,(1,(1,(0,(0,(1,(0,0)))))))
+ | x28 => (0,(0,(0,(1,(0,(1,(0,0)))))))
+ | x29 => (1,(0,(0,(1,(0,(1,(0,0)))))))
+ | x2a => (0,(1,(0,(1,(0,(1,(0,0)))))))
+ | x2b => (1,(1,(0,(1,(0,(1,(0,0)))))))
+ | x2c => (0,(0,(1,(1,(0,(1,(0,0)))))))
+ | x2d => (1,(0,(1,(1,(0,(1,(0,0)))))))
+ | x2e => (0,(1,(1,(1,(0,(1,(0,0)))))))
+ | x2f => (1,(1,(1,(1,(0,(1,(0,0)))))))
+ | x30 => (0,(0,(0,(0,(1,(1,(0,0)))))))
+ | x31 => (1,(0,(0,(0,(1,(1,(0,0)))))))
+ | x32 => (0,(1,(0,(0,(1,(1,(0,0)))))))
+ | x33 => (1,(1,(0,(0,(1,(1,(0,0)))))))
+ | x34 => (0,(0,(1,(0,(1,(1,(0,0)))))))
+ | x35 => (1,(0,(1,(0,(1,(1,(0,0)))))))
+ | x36 => (0,(1,(1,(0,(1,(1,(0,0)))))))
+ | x37 => (1,(1,(1,(0,(1,(1,(0,0)))))))
+ | x38 => (0,(0,(0,(1,(1,(1,(0,0)))))))
+ | x39 => (1,(0,(0,(1,(1,(1,(0,0)))))))
+ | x3a => (0,(1,(0,(1,(1,(1,(0,0)))))))
+ | x3b => (1,(1,(0,(1,(1,(1,(0,0)))))))
+ | x3c => (0,(0,(1,(1,(1,(1,(0,0)))))))
+ | x3d => (1,(0,(1,(1,(1,(1,(0,0)))))))
+ | x3e => (0,(1,(1,(1,(1,(1,(0,0)))))))
+ | x3f => (1,(1,(1,(1,(1,(1,(0,0)))))))
+ | x40 => (0,(0,(0,(0,(0,(0,(1,0)))))))
+ | x41 => (1,(0,(0,(0,(0,(0,(1,0)))))))
+ | x42 => (0,(1,(0,(0,(0,(0,(1,0)))))))
+ | x43 => (1,(1,(0,(0,(0,(0,(1,0)))))))
+ | x44 => (0,(0,(1,(0,(0,(0,(1,0)))))))
+ | x45 => (1,(0,(1,(0,(0,(0,(1,0)))))))
+ | x46 => (0,(1,(1,(0,(0,(0,(1,0)))))))
+ | x47 => (1,(1,(1,(0,(0,(0,(1,0)))))))
+ | x48 => (0,(0,(0,(1,(0,(0,(1,0)))))))
+ | x49 => (1,(0,(0,(1,(0,(0,(1,0)))))))
+ | x4a => (0,(1,(0,(1,(0,(0,(1,0)))))))
+ | x4b => (1,(1,(0,(1,(0,(0,(1,0)))))))
+ | x4c => (0,(0,(1,(1,(0,(0,(1,0)))))))
+ | x4d => (1,(0,(1,(1,(0,(0,(1,0)))))))
+ | x4e => (0,(1,(1,(1,(0,(0,(1,0)))))))
+ | x4f => (1,(1,(1,(1,(0,(0,(1,0)))))))
+ | x50 => (0,(0,(0,(0,(1,(0,(1,0)))))))
+ | x51 => (1,(0,(0,(0,(1,(0,(1,0)))))))
+ | x52 => (0,(1,(0,(0,(1,(0,(1,0)))))))
+ | x53 => (1,(1,(0,(0,(1,(0,(1,0)))))))
+ | x54 => (0,(0,(1,(0,(1,(0,(1,0)))))))
+ | x55 => (1,(0,(1,(0,(1,(0,(1,0)))))))
+ | x56 => (0,(1,(1,(0,(1,(0,(1,0)))))))
+ | x57 => (1,(1,(1,(0,(1,(0,(1,0)))))))
+ | x58 => (0,(0,(0,(1,(1,(0,(1,0)))))))
+ | x59 => (1,(0,(0,(1,(1,(0,(1,0)))))))
+ | x5a => (0,(1,(0,(1,(1,(0,(1,0)))))))
+ | x5b => (1,(1,(0,(1,(1,(0,(1,0)))))))
+ | x5c => (0,(0,(1,(1,(1,(0,(1,0)))))))
+ | x5d => (1,(0,(1,(1,(1,(0,(1,0)))))))
+ | x5e => (0,(1,(1,(1,(1,(0,(1,0)))))))
+ | x5f => (1,(1,(1,(1,(1,(0,(1,0)))))))
+ | x60 => (0,(0,(0,(0,(0,(1,(1,0)))))))
+ | x61 => (1,(0,(0,(0,(0,(1,(1,0)))))))
+ | x62 => (0,(1,(0,(0,(0,(1,(1,0)))))))
+ | x63 => (1,(1,(0,(0,(0,(1,(1,0)))))))
+ | x64 => (0,(0,(1,(0,(0,(1,(1,0)))))))
+ | x65 => (1,(0,(1,(0,(0,(1,(1,0)))))))
+ | x66 => (0,(1,(1,(0,(0,(1,(1,0)))))))
+ | x67 => (1,(1,(1,(0,(0,(1,(1,0)))))))
+ | x68 => (0,(0,(0,(1,(0,(1,(1,0)))))))
+ | x69 => (1,(0,(0,(1,(0,(1,(1,0)))))))
+ | x6a => (0,(1,(0,(1,(0,(1,(1,0)))))))
+ | x6b => (1,(1,(0,(1,(0,(1,(1,0)))))))
+ | x6c => (0,(0,(1,(1,(0,(1,(1,0)))))))
+ | x6d => (1,(0,(1,(1,(0,(1,(1,0)))))))
+ | x6e => (0,(1,(1,(1,(0,(1,(1,0)))))))
+ | x6f => (1,(1,(1,(1,(0,(1,(1,0)))))))
+ | x70 => (0,(0,(0,(0,(1,(1,(1,0)))))))
+ | x71 => (1,(0,(0,(0,(1,(1,(1,0)))))))
+ | x72 => (0,(1,(0,(0,(1,(1,(1,0)))))))
+ | x73 => (1,(1,(0,(0,(1,(1,(1,0)))))))
+ | x74 => (0,(0,(1,(0,(1,(1,(1,0)))))))
+ | x75 => (1,(0,(1,(0,(1,(1,(1,0)))))))
+ | x76 => (0,(1,(1,(0,(1,(1,(1,0)))))))
+ | x77 => (1,(1,(1,(0,(1,(1,(1,0)))))))
+ | x78 => (0,(0,(0,(1,(1,(1,(1,0)))))))
+ | x79 => (1,(0,(0,(1,(1,(1,(1,0)))))))
+ | x7a => (0,(1,(0,(1,(1,(1,(1,0)))))))
+ | x7b => (1,(1,(0,(1,(1,(1,(1,0)))))))
+ | x7c => (0,(0,(1,(1,(1,(1,(1,0)))))))
+ | x7d => (1,(0,(1,(1,(1,(1,(1,0)))))))
+ | x7e => (0,(1,(1,(1,(1,(1,(1,0)))))))
+ | x7f => (1,(1,(1,(1,(1,(1,(1,0)))))))
+ | x80 => (0,(0,(0,(0,(0,(0,(0,1)))))))
+ | x81 => (1,(0,(0,(0,(0,(0,(0,1)))))))
+ | x82 => (0,(1,(0,(0,(0,(0,(0,1)))))))
+ | x83 => (1,(1,(0,(0,(0,(0,(0,1)))))))
+ | x84 => (0,(0,(1,(0,(0,(0,(0,1)))))))
+ | x85 => (1,(0,(1,(0,(0,(0,(0,1)))))))
+ | x86 => (0,(1,(1,(0,(0,(0,(0,1)))))))
+ | x87 => (1,(1,(1,(0,(0,(0,(0,1)))))))
+ | x88 => (0,(0,(0,(1,(0,(0,(0,1)))))))
+ | x89 => (1,(0,(0,(1,(0,(0,(0,1)))))))
+ | x8a => (0,(1,(0,(1,(0,(0,(0,1)))))))
+ | x8b => (1,(1,(0,(1,(0,(0,(0,1)))))))
+ | x8c => (0,(0,(1,(1,(0,(0,(0,1)))))))
+ | x8d => (1,(0,(1,(1,(0,(0,(0,1)))))))
+ | x8e => (0,(1,(1,(1,(0,(0,(0,1)))))))
+ | x8f => (1,(1,(1,(1,(0,(0,(0,1)))))))
+ | x90 => (0,(0,(0,(0,(1,(0,(0,1)))))))
+ | x91 => (1,(0,(0,(0,(1,(0,(0,1)))))))
+ | x92 => (0,(1,(0,(0,(1,(0,(0,1)))))))
+ | x93 => (1,(1,(0,(0,(1,(0,(0,1)))))))
+ | x94 => (0,(0,(1,(0,(1,(0,(0,1)))))))
+ | x95 => (1,(0,(1,(0,(1,(0,(0,1)))))))
+ | x96 => (0,(1,(1,(0,(1,(0,(0,1)))))))
+ | x97 => (1,(1,(1,(0,(1,(0,(0,1)))))))
+ | x98 => (0,(0,(0,(1,(1,(0,(0,1)))))))
+ | x99 => (1,(0,(0,(1,(1,(0,(0,1)))))))
+ | x9a => (0,(1,(0,(1,(1,(0,(0,1)))))))
+ | x9b => (1,(1,(0,(1,(1,(0,(0,1)))))))
+ | x9c => (0,(0,(1,(1,(1,(0,(0,1)))))))
+ | x9d => (1,(0,(1,(1,(1,(0,(0,1)))))))
+ | x9e => (0,(1,(1,(1,(1,(0,(0,1)))))))
+ | x9f => (1,(1,(1,(1,(1,(0,(0,1)))))))
+ | xa0 => (0,(0,(0,(0,(0,(1,(0,1)))))))
+ | xa1 => (1,(0,(0,(0,(0,(1,(0,1)))))))
+ | xa2 => (0,(1,(0,(0,(0,(1,(0,1)))))))
+ | xa3 => (1,(1,(0,(0,(0,(1,(0,1)))))))
+ | xa4 => (0,(0,(1,(0,(0,(1,(0,1)))))))
+ | xa5 => (1,(0,(1,(0,(0,(1,(0,1)))))))
+ | xa6 => (0,(1,(1,(0,(0,(1,(0,1)))))))
+ | xa7 => (1,(1,(1,(0,(0,(1,(0,1)))))))
+ | xa8 => (0,(0,(0,(1,(0,(1,(0,1)))))))
+ | xa9 => (1,(0,(0,(1,(0,(1,(0,1)))))))
+ | xaa => (0,(1,(0,(1,(0,(1,(0,1)))))))
+ | xab => (1,(1,(0,(1,(0,(1,(0,1)))))))
+ | xac => (0,(0,(1,(1,(0,(1,(0,1)))))))
+ | xad => (1,(0,(1,(1,(0,(1,(0,1)))))))
+ | xae => (0,(1,(1,(1,(0,(1,(0,1)))))))
+ | xaf => (1,(1,(1,(1,(0,(1,(0,1)))))))
+ | xb0 => (0,(0,(0,(0,(1,(1,(0,1)))))))
+ | xb1 => (1,(0,(0,(0,(1,(1,(0,1)))))))
+ | xb2 => (0,(1,(0,(0,(1,(1,(0,1)))))))
+ | xb3 => (1,(1,(0,(0,(1,(1,(0,1)))))))
+ | xb4 => (0,(0,(1,(0,(1,(1,(0,1)))))))
+ | xb5 => (1,(0,(1,(0,(1,(1,(0,1)))))))
+ | xb6 => (0,(1,(1,(0,(1,(1,(0,1)))))))
+ | xb7 => (1,(1,(1,(0,(1,(1,(0,1)))))))
+ | xb8 => (0,(0,(0,(1,(1,(1,(0,1)))))))
+ | xb9 => (1,(0,(0,(1,(1,(1,(0,1)))))))
+ | xba => (0,(1,(0,(1,(1,(1,(0,1)))))))
+ | xbb => (1,(1,(0,(1,(1,(1,(0,1)))))))
+ | xbc => (0,(0,(1,(1,(1,(1,(0,1)))))))
+ | xbd => (1,(0,(1,(1,(1,(1,(0,1)))))))
+ | xbe => (0,(1,(1,(1,(1,(1,(0,1)))))))
+ | xbf => (1,(1,(1,(1,(1,(1,(0,1)))))))
+ | xc0 => (0,(0,(0,(0,(0,(0,(1,1)))))))
+ | xc1 => (1,(0,(0,(0,(0,(0,(1,1)))))))
+ | xc2 => (0,(1,(0,(0,(0,(0,(1,1)))))))
+ | xc3 => (1,(1,(0,(0,(0,(0,(1,1)))))))
+ | xc4 => (0,(0,(1,(0,(0,(0,(1,1)))))))
+ | xc5 => (1,(0,(1,(0,(0,(0,(1,1)))))))
+ | xc6 => (0,(1,(1,(0,(0,(0,(1,1)))))))
+ | xc7 => (1,(1,(1,(0,(0,(0,(1,1)))))))
+ | xc8 => (0,(0,(0,(1,(0,(0,(1,1)))))))
+ | xc9 => (1,(0,(0,(1,(0,(0,(1,1)))))))
+ | xca => (0,(1,(0,(1,(0,(0,(1,1)))))))
+ | xcb => (1,(1,(0,(1,(0,(0,(1,1)))))))
+ | xcc => (0,(0,(1,(1,(0,(0,(1,1)))))))
+ | xcd => (1,(0,(1,(1,(0,(0,(1,1)))))))
+ | xce => (0,(1,(1,(1,(0,(0,(1,1)))))))
+ | xcf => (1,(1,(1,(1,(0,(0,(1,1)))))))
+ | xd0 => (0,(0,(0,(0,(1,(0,(1,1)))))))
+ | xd1 => (1,(0,(0,(0,(1,(0,(1,1)))))))
+ | xd2 => (0,(1,(0,(0,(1,(0,(1,1)))))))
+ | xd3 => (1,(1,(0,(0,(1,(0,(1,1)))))))
+ | xd4 => (0,(0,(1,(0,(1,(0,(1,1)))))))
+ | xd5 => (1,(0,(1,(0,(1,(0,(1,1)))))))
+ | xd6 => (0,(1,(1,(0,(1,(0,(1,1)))))))
+ | xd7 => (1,(1,(1,(0,(1,(0,(1,1)))))))
+ | xd8 => (0,(0,(0,(1,(1,(0,(1,1)))))))
+ | xd9 => (1,(0,(0,(1,(1,(0,(1,1)))))))
+ | xda => (0,(1,(0,(1,(1,(0,(1,1)))))))
+ | xdb => (1,(1,(0,(1,(1,(0,(1,1)))))))
+ | xdc => (0,(0,(1,(1,(1,(0,(1,1)))))))
+ | xdd => (1,(0,(1,(1,(1,(0,(1,1)))))))
+ | xde => (0,(1,(1,(1,(1,(0,(1,1)))))))
+ | xdf => (1,(1,(1,(1,(1,(0,(1,1)))))))
+ | xe0 => (0,(0,(0,(0,(0,(1,(1,1)))))))
+ | xe1 => (1,(0,(0,(0,(0,(1,(1,1)))))))
+ | xe2 => (0,(1,(0,(0,(0,(1,(1,1)))))))
+ | xe3 => (1,(1,(0,(0,(0,(1,(1,1)))))))
+ | xe4 => (0,(0,(1,(0,(0,(1,(1,1)))))))
+ | xe5 => (1,(0,(1,(0,(0,(1,(1,1)))))))
+ | xe6 => (0,(1,(1,(0,(0,(1,(1,1)))))))
+ | xe7 => (1,(1,(1,(0,(0,(1,(1,1)))))))
+ | xe8 => (0,(0,(0,(1,(0,(1,(1,1)))))))
+ | xe9 => (1,(0,(0,(1,(0,(1,(1,1)))))))
+ | xea => (0,(1,(0,(1,(0,(1,(1,1)))))))
+ | xeb => (1,(1,(0,(1,(0,(1,(1,1)))))))
+ | xec => (0,(0,(1,(1,(0,(1,(1,1)))))))
+ | xed => (1,(0,(1,(1,(0,(1,(1,1)))))))
+ | xee => (0,(1,(1,(1,(0,(1,(1,1)))))))
+ | xef => (1,(1,(1,(1,(0,(1,(1,1)))))))
+ | xf0 => (0,(0,(0,(0,(1,(1,(1,1)))))))
+ | xf1 => (1,(0,(0,(0,(1,(1,(1,1)))))))
+ | xf2 => (0,(1,(0,(0,(1,(1,(1,1)))))))
+ | xf3 => (1,(1,(0,(0,(1,(1,(1,1)))))))
+ | xf4 => (0,(0,(1,(0,(1,(1,(1,1)))))))
+ | xf5 => (1,(0,(1,(0,(1,(1,(1,1)))))))
+ | xf6 => (0,(1,(1,(0,(1,(1,(1,1)))))))
+ | xf7 => (1,(1,(1,(0,(1,(1,(1,1)))))))
+ | xf8 => (0,(0,(0,(1,(1,(1,(1,1)))))))
+ | xf9 => (1,(0,(0,(1,(1,(1,(1,1)))))))
+ | xfa => (0,(1,(0,(1,(1,(1,(1,1)))))))
+ | xfb => (1,(1,(0,(1,(1,(1,(1,1)))))))
+ | xfc => (0,(0,(1,(1,(1,(1,(1,1)))))))
+ | xfd => (1,(0,(1,(1,(1,(1,(1,1)))))))
+ | xfe => (0,(1,(1,(1,(1,(1,(1,1)))))))
+ | xff => (1,(1,(1,(1,(1,(1,(1,1)))))))
+ end.
+
+Lemma of_bits_to_bits (b : byte) : of_bits (to_bits b) = b.
+Proof. destruct b; exact eq_refl. Qed.
+
+Lemma to_bits_of_bits (b : _) : to_bits (of_bits b) = b.
+Proof.
+ repeat match goal with
+ | p : prod _ _ |- _ => destruct p
+ | b : bool |- _ => destruct b
+ end;
+ exact eq_refl.
+Qed.
+
+Definition byte_of_byte (b : byte) : byte := b.
+
+Module Export ByteSyntaxNotations.
+ String Notation byte byte_of_byte byte_of_byte : byte_scope.
+End ByteSyntaxNotations.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 6d98bcb34a..5e29f854e8 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -13,6 +13,7 @@ Require Export Logic.
Require Export Logic_Type.
Require Export Datatypes.
Require Export Specif.
+Require Coq.Init.Byte.
Require Coq.Init.Decimal.
Require Coq.Init.Nat.
Require Export Peano.
@@ -26,6 +27,7 @@ Require Export Coq.Init.Tauto.
Declare ML Module "cc_plugin".
Declare ML Module "ground_plugin".
Declare ML Module "numeral_notation_plugin".
+Declare ML Module "string_notation_plugin".
(* Parsing / printing of decimal numbers *)
Arguments Nat.of_uint d%dec_uint_scope.
@@ -38,5 +40,8 @@ Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int
(* Parsing / printing of [nat] numbers *)
Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000).
+(* Printing/Parsing of bytes *)
+Export Byte.ByteSyntaxNotations.
+
(* Default substrings not considered by queries like SearchAbout *)
Add Search Blacklist "_subproof" "_subterm" "Private_".
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 03:42:16 +0000