@@ -1269,8 +1269,8 @@ impl DebruijnIndex {
12691269 ///
12701270 /// you would need to shift the index for `'a` into 1 new binder.
12711271 #[ must_use]
1272- pub fn shifted_in ( self , amount : u32 ) -> DebruijnIndex {
1273- DebruijnIndex :: new ( self . index ( ) + amount as usize )
1272+ pub const fn shifted_in ( self , amount : u32 ) -> DebruijnIndex {
1273+ DebruijnIndex ( self . 0 + amount)
12741274 }
12751275
12761276 /// Update this index in place by shifting it "in" through
@@ -1282,8 +1282,8 @@ impl DebruijnIndex {
12821282 /// Returns the resulting index when this value is moved out from
12831283 /// `amount` number of new binders.
12841284 #[ must_use]
1285- pub fn shifted_out ( self , amount : u32 ) -> DebruijnIndex {
1286- DebruijnIndex :: new ( self . index ( ) - amount as usize )
1285+ pub const fn shifted_out ( self , amount : u32 ) -> DebruijnIndex {
1286+ DebruijnIndex ( self . 0 - amount)
12871287 }
12881288
12891289 /// Update in place by shifting out from `amount` binders.
@@ -1312,7 +1312,7 @@ impl DebruijnIndex {
13121312 /// bound by one of the binders we are shifting out of, that is an
13131313 /// error (and should fail an assertion failure).
13141314 pub fn shifted_out_to_binder ( self , to_binder : DebruijnIndex ) -> Self {
1315- self . shifted_out ( ( to_binder. index ( ) - INNERMOST . index ( ) ) as u32 )
1315+ self . shifted_out ( ( to_binder. 0 - INNERMOST . 0 ) as u32 )
13161316 }
13171317}
13181318
0 commit comments