Lines Matching refs:Capacity
68 type List (Capacity : Count_Type) is private with
96 Pre => Target.Capacity >= Length (Source);
98 function Copy (Source : List; Capacity : Count_Type := 0) return List with
100 Pre => Capacity = 0 or else Capacity >= Source.Capacity;
119 Pre => Target.Capacity >= Length (Source);
128 Pre => Length (Container) + Count <= Container.Capacity
140 Pre => Length (Container) + Count <= Container.Capacity
151 Pre => Length (Container) + Count <= Container.Capacity
161 Pre => Length (Container) + Count <= Container.Capacity;
169 Pre => Length (Container) + Count <= Container.Capacity;
214 Pre => Length (Source) + Length (Target) <= Target.Capacity
225 Pre => Length (Source) + Length (Target) <= Target.Capacity
236 Pre => 2 * Length (Container) <= Container.Capacity
347 type List (Capacity : Count_Type) is tagged record
348 Nodes : Node_Array (1 .. Capacity) := (others => <>);