We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent adacb31 commit df81a07Copy full SHA for df81a07
1 file changed
lib/pulse/lib/Pulse.Lib.Vector.fsti
@@ -34,7 +34,7 @@ module SZ = FStar.SizeT
34
val vector (t:Type0) : Type0
35
36
/// Predicate relating a vector to its logical contents and capacity
37
-val is_vector (#t:Type0) ([@@@mkey]v:vector t) (s:Seq.seq t) (cap:SZ.t) : slprop
+val is_vector (#t:Type0) ([@@@mkey]v:vector t) (#[full_default()] p: perm) (s:Seq.seq t) : slprop
38
39
/// Create a new vector with n elements all set to default.
40
/// Capacity is initially n. Requires n > 0.
0 commit comments