File tree Expand file tree Collapse file tree 1 file changed +22
-6
lines changed
experiments/idris/src/Fathom Expand file tree Collapse file tree 1 file changed +22
-6
lines changed Original file line number Diff line number Diff line change @@ -89,33 +89,49 @@ parameters {0 Source, Target : Type}
8989-- --------------------
9090
9191
92- ||| A possibly infinite stream of bits
92+ ||| A potentially infinite stream of bits
9393public export
9494BitStream : Type
9595BitStream = Colist Bool
9696
97- %name BitStream stream
97+ %name BitStream bits
9898
9999
100- ||| A possibly infinite stream of bytes
100+ ||| A potentially infinite stream of bytes
101101public export
102102ByteStream : Type
103103ByteStream = Colist Bits8
104104
105- %name ByteStream stream
105+ %name ByteStream bytes
106106
107107
108108||| A finite bit buffer
109109public export
110110BitBuffer : Type
111111BitBuffer = List Bool
112112
113- %name BitBuffer buffer
113+ %name BitBuffer bits
114114
115115
116116||| A finite byte buffer
117117public export
118118ByteBuffer : Type
119119ByteBuffer = List Bits8
120120
121- %name ByteBuffer buffer
121+ %name ByteBuffer bytes
122+
123+
124+ ||| An array of bits of a known size
125+ public export
126+ BitArray : Nat -> Type
127+ BitArray len = Vect len Bool
128+
129+ %name BitArray bits
130+
131+
132+ ||| An array of bytes of a known size
133+ public export
134+ ByteArray : Nat -> Type
135+ ByteArray len = Vect len Bits8
136+
137+ %name ByteArray bytes
You can’t perform that action at this time.
0 commit comments