1	import Base
2	
3	# Neutral datatypes shared by src/containers/bitlist.bend and its spec.
4	
5	type Error is Data:
6	  IndexOutOfRange{}
7	  Full{}
8	  Empty{}
9	
10	# One public operation, for arbitrary finite operation traces.
11	type Op is Data:
12	  Length{}
13	  Limit{}
14	  Get{index: Nat}
15	  Assign{index: Nat, value: Bool}
16	  Push{value: Bool}
17	  Pop{}
18	  Clear{}
19	  Count{}
20	  ToList{}
21	
22	# The observable answer of one operation.
23	type Obs is Data:
24	  ONat{value: Nat}
25	  OLimit{limit: Maybe<&2, Nat>}
26	  OBit{result: Result<&2, &2, Error, Bool>}
27	  OUnit{result: Result<&2, &2, Error, Unit>}
28	  OBits{bits: List<&2, Bool>}