diff --git a/prusti-contracts/prusti-contracts/src/core_spec/ops/index.rs b/prusti-contracts/prusti-contracts/src/core_spec/ops/index.rs index ad8106944d8..638464ee4b4 100644 --- a/prusti-contracts/prusti-contracts/src/core_spec/ops/index.rs +++ b/prusti-contracts/prusti-contracts/src/core_spec/ops/index.rs @@ -4,8 +4,10 @@ use crate::*; use core::ops::Index; // FUTURE(#1221): This spec is currently not usable due to issue #1221. +/* #[extern_spec] trait Index { #[pure] fn index(&self, idx: Idx) -> &Self::Output; } +*/ diff --git a/prusti-contracts/prusti-contracts/src/core_spec/slice.rs b/prusti-contracts/prusti-contracts/src/core_spec/slice.rs index 8fa69f6b612..9e13193bc97 100644 --- a/prusti-contracts/prusti-contracts/src/core_spec/slice.rs +++ b/prusti-contracts/prusti-contracts/src/core_spec/slice.rs @@ -42,6 +42,7 @@ impl [T] { } // FUTURE(#1221): This spec is currently not usable due to issue #1221. +/* #[extern_spec] impl Index for [T] where @@ -50,3 +51,4 @@ where #[pure] fn index(&self, index: I) -> &I::Output; } +*/