fix comment

source/pervasive/std_specs/vec.rs

@@ -72,9 +72,12 @@ impl<T, A: Allocator> VecAdditionalExecFns<T> for Vec<T, A> {
 // TODO this should really be a 'external_fn_specification' function
 // but it's difficult to handle vec.index right now because
 // it uses more trait polymorphism than we can handle right now.
-// And `index` is too important that I don't want do
+//
 // So this is a bit of a hack, but I'm just manually redirecting
-// `vec.index` to this function here from rust_to_vir_expr.
+// `vec[i]` to this function here from rust_to_vir_expr.
+//
+// It's not ideal, but I think it's better than the alternative, which would
+// be to have users call some function with a nonstandard name to perform indexing.
 
 #[verifier::external_body]
 pub fn vec_index<T, A: Allocator>(vec: &Vec<T, A>, i: usize) -> (element: &T)

source/pervasive/string.rs

@@ -1,12 +1,11 @@
 #![feature(rustc_attrs)]
+#![allow(unused_imports)]
 
 extern crate alloc;
 use alloc::string;
 
 use crate::view::*;
-#[allow(unused_imports)]
 use super::seq::Seq;
-#[allow(unused_imports)]
 use builtin::*;
 use builtin_macros::verus;
 use crate::prelude::*;