1	import Base
2	
3	# Neutral datatypes shared by src/dynamic_array.bend and spec/dynamic_array.bend.
4	
5	type Error is Data:
6	  IndexOutOfRange{}
7	  EmptyArray{}
8	  CapacityExceeded{}
9	
10	# One public operation, for arbitrary finite operation traces.
11	type Op<-T: Data> is Data:
12	  Length{}
13	  Capacity{}
14	  Get{index: Nat}
15	  Set{index: Nat, value: T}
16	  Push{value: T}
17	  Pop{}
18	  Reserve{wanted: Nat}
19	  Clear{}
20	  ToList{}
21	
22	# The observable answer of one operation.
23	type Obs<-T: Data> is Data:
24	  ONat{value: Nat}
25	  OItem{result: Result<&2, &2, Error, T>}
26	  OUnit{result: Result<&2, &2, Error, Unit>}
27	  OList{items: List<&2, T>}
28	
29	# A rejected owning write returns its input value to the caller.
30	type Rejected<-T: Type> is Type:
31	  Rejected{error: Error, value: T}