@@ -2145,14 +2145,14 @@ mod type_keyword {}
2145
2145
/// contract of `idx_unchecked`. Implementing `Indexable` is safe because when writing
2146
2146
/// `idx_unchecked`, we don't have to worry: our *callers* need to discharge a proof obligation
2147
2147
/// (like `use_indexable` does), but the *implementation* of `get_unchecked` has no proof obligation
2148
- /// to contend with. Note that unlike normal `unsafe fn`, an `unsafe fn` in a trait implementation
2149
- /// does not get to just pick an arbitrary safety contract! It *has * to use the safety contract
2150
- /// defined by the trait (or one with weaker preconditions).
2151
- ///
2152
- /// Of course, the implementation may choose to call other unsafe operations, and then it needs an
2153
- /// `unsafe` *block* to indicate it discharged the proof obligations of its callees. For
2154
- /// that purpose it can make use of the contract that all its callers must uphold -- the fact that
2155
- /// `idx < LEN` .
2148
+ /// to contend with. Of course, the implementation may choose to call other unsafe operations, and
2149
+ /// then it needs an `unsafe` *block * to indicate it discharged the proof obligations of its
2150
+ /// callees. For that purpose it can make use of the contract that all its callers must uphold --
2151
+ /// the fact that `idx < LEN`.
2152
+ ///
2153
+ /// Note that unlike normal `unsafe fn`, an `unsafe fn` in a trait implementation does not get to
2154
+ /// just pick an arbitrary safety contract! It *has* to use the safety contract defined by the trait
2155
+ /// (or one with weaker preconditions) .
2156
2156
///
2157
2157
/// Formally speaking, an `unsafe fn` in a trait is a function with *preconditions* that go beyond
2158
2158
/// those encoded by the argument types (such as `idx < LEN`), whereas an `unsafe trait` can declare
0 commit comments