Defbyte-standard-instances
Standard fixtypes of unsigned and signed bytes of various sizes,
with some accompanying theorems.
Here `standard' means that these all have uniform structure and naming.
They are unary counterparts of
(unsigned-byte-p n ...) and (signed-byte-p n ...),
for various values of n.
These are all generated via defbyte.
If standard (in the sense above) fixtypes
of unsigned or signed bytes of a certain size
are needed but are not among the ones defined here,
they can be added here.
Subtopics
- Ubyte8
- Fixtype of unsigned bytes of size 8.
- Ubyte32
- Fixtype of unsigned bytes of size 32.
- Ubyte16
- Fixtype of unsigned bytes of size 16.
- Ubyte128
- Fixtype of unsigned bytes of size 128.
- Sbyte64
- Fixtype of signed bytes of size 64.
- Sbyte32
- Fixtype of signed bytes of size 32.
- Sbyte16
- Fixtype of signed bytes of size 16.
- Sbyte128
- Fixtype of signed bytes of size 128.
- Ubyte64
- Fixtype of unsigned bytes of size 64.
- Ubyte11
- Fixtype of unsigned bytes of size 11.
- Sbyte8
- Fixtype of signed bytes of size 8.
- Ubyte4
- Fixtype of unsigned bytes of size 4.
- Ubyte256
- Fixtype of unsigned bytes of size 256.
- Sbyte256
- Fixtype of signed bytes of size 256.
- Ubyte7
- Fixtype of unsigned bytes of size 7.
- Ubyte6
- Fixtype of unsigned bytes of size 6.
- Ubyte5
- Fixtype of unsigned bytes of size 5.
- Ubyte3
- Fixtype of unsigned bytes of size 3.
- Ubyte20
- Fixtype of unsigned bytes of size 20.
- Ubyte2
- Fixtype of unsigned bytes of size 2.
- Ubyte12
- Fixtype of unsigned bytes of size 12.
- Ubyte1
- Fixtype of unsigned bytes of size 1.
- Sbyte4
- Fixtype of signed bytes of size 4.
- Sbyte3
- Fixtype of signed bytes of size 3.
- Sbyte2
- Fixtype of signed bytes of size 2.
- Sbyte1
- Fixtype of signed bytes of size 1.
- Defbyte-standard-instances-ihs-theorems
- Theorems about defbyte standard instances and IHS functions.
- Defubyte
- Specialized form of defbyte for generating
standard fixtypes of unsigned bytes of explicit integer sizes.
- Defsbyte
- Specialized form of defbyte for generating standard fixtypes
of signed bytes of explicit integer sizes.
