Traits§
- AddAssign
Spec - AddAssign
Spec Impl - AddSpec
- AddSpec
Impl - BitAnd
Assign Spec - BitAnd
Assign Spec Impl - BitAnd
Spec - BitAnd
Spec Impl - BitOr
Assign Spec - BitOr
Assign Spec Impl - BitOr
Spec - BitOr
Spec Impl - BitXor
Assign Spec - BitXor
Assign Spec Impl - BitXor
Spec - BitXor
Spec Impl - DivAssign
Spec - DivAssign
Spec Impl - DivSpec
- DivSpec
Impl - ExAdd
- ExAdd
Assign - ExBit
And - ExBit
AndAssign - ExBitOr
- ExBit
OrAssign - ExBit
Xor - ExBit
XorAssign - ExDiv
- ExDiv
Assign - ExMul
- ExMul
Assign - ExNeg
- ExNot
- ExRem
- ExRem
Assign - ExShl
- ExShl
Assign - ExShr
- ExShr
Assign - ExSub
- ExSub
Assign - MulAssign
Spec - MulAssign
Spec Impl - MulSpec
- MulSpec
Impl - NegSpec
- NegSpec
Impl - NotSpec
- NotSpec
Impl - RemAssign
Spec - RemAssign
Spec Impl - RemSpec
- RemSpec
Impl - ShlAssign
Spec - ShlAssign
Spec Impl - ShlSpec
- ShlSpec
Impl - ShrAssign
Spec - ShrAssign
Spec Impl - ShrSpec
- ShrSpec
Impl - SubAssign
Spec - SubAssign
Spec Impl - SubSpec
- SubSpec
Impl
Functions§
- _verus_
external_ ⚠fn_ specification_ 388__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - _verus_
external_ ⚠fn_ specification_ 389__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - _verus_
external_ ⚠fn_ specification_ 390__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - _verus_
external_ ⚠fn_ specification_ 391__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - _verus_
external_ ⚠fn_ specification_ 392__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - _verus_
external_ ⚠fn_ specification_ 393__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - _verus_
external_ ⚠fn_ specification_ 394__ 60__ 32_ bool_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 395__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 396__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 397__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 398__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 399__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 400__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 401__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 402__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 403__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 404__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 405__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 406__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 407__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 408__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 409__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 410__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 411__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 412__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 413__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 414__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 415__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 416__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 417__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 418__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 419__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ AddAssign_ 32__ 62__ 32__ 58__ 58__ 32_ add__ assign - _verus_
external_ ⚠fn_ specification_ 420__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ AddAssign_ 32__ 62__ 32__ 58__ 58__ 32_ add__ assign - _verus_
external_ ⚠fn_ specification_ 421__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ AddAssign_ 32__ 62__ 32__ 58__ 58__ 32_ add__ assign - _verus_
external_ ⚠fn_ specification_ 422__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ AddAssign_ 32__ 62__ 32__ 58__ 58__ 32_ add__ assign - _verus_
external_ ⚠fn_ specification_ 423__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ AddAssign_ 32__ 62__ 32__ 58__ 58__ 32_ add__ assign - _verus_
external_ ⚠fn_ specification_ 424__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ AddAssign_ 32__ 62__ 32__ 58__ 58__ 32_ add__ assign - _verus_
external_ ⚠fn_ specification_ 425__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ AddAssign_ 32__ 62__ 32__ 58__ 58__ 32_ add__ assign - _verus_
external_ ⚠fn_ specification_ 426__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ AddAssign_ 32__ 62__ 32__ 58__ 58__ 32_ add__ assign - _verus_
external_ ⚠fn_ specification_ 427__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ AddAssign_ 32__ 62__ 32__ 58__ 58__ 32_ add__ assign - _verus_
external_ ⚠fn_ specification_ 428__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ AddAssign_ 32__ 62__ 32__ 58__ 58__ 32_ add__ assign - _verus_
external_ ⚠fn_ specification_ 429__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ AddAssign_ 32__ 62__ 32__ 58__ 58__ 32_ add__ assign - _verus_
external_ ⚠fn_ specification_ 430__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ AddAssign_ 32__ 62__ 32__ 58__ 58__ 32_ add__ assign - _verus_
external_ ⚠fn_ specification_ 431__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 432__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 433__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 434__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 435__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 436__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 437__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 438__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 439__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 440__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 441__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 442__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 443__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ SubAssign_ 32__ 62__ 32__ 58__ 58__ 32_ sub__ assign - _verus_
external_ ⚠fn_ specification_ 444__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ SubAssign_ 32__ 62__ 32__ 58__ 58__ 32_ sub__ assign - _verus_
external_ ⚠fn_ specification_ 445__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ SubAssign_ 32__ 62__ 32__ 58__ 58__ 32_ sub__ assign - _verus_
external_ ⚠fn_ specification_ 446__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ SubAssign_ 32__ 62__ 32__ 58__ 58__ 32_ sub__ assign - _verus_
external_ ⚠fn_ specification_ 447__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ SubAssign_ 32__ 62__ 32__ 58__ 58__ 32_ sub__ assign - _verus_
external_ ⚠fn_ specification_ 448__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ SubAssign_ 32__ 62__ 32__ 58__ 58__ 32_ sub__ assign - _verus_
external_ ⚠fn_ specification_ 449__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ SubAssign_ 32__ 62__ 32__ 58__ 58__ 32_ sub__ assign - _verus_
external_ ⚠fn_ specification_ 450__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ SubAssign_ 32__ 62__ 32__ 58__ 58__ 32_ sub__ assign - _verus_
external_ ⚠fn_ specification_ 451__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ SubAssign_ 32__ 62__ 32__ 58__ 58__ 32_ sub__ assign - _verus_
external_ ⚠fn_ specification_ 452__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ SubAssign_ 32__ 62__ 32__ 58__ 58__ 32_ sub__ assign - _verus_
external_ ⚠fn_ specification_ 453__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ SubAssign_ 32__ 62__ 32__ 58__ 58__ 32_ sub__ assign - _verus_
external_ ⚠fn_ specification_ 454__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ SubAssign_ 32__ 62__ 32__ 58__ 58__ 32_ sub__ assign - _verus_
external_ ⚠fn_ specification_ 455__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 456__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 457__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 458__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 459__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 460__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 461__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 462__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 463__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 464__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 465__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 466__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 467__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ MulAssign_ 32__ 62__ 32__ 58__ 58__ 32_ mul__ assign - _verus_
external_ ⚠fn_ specification_ 468__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ MulAssign_ 32__ 62__ 32__ 58__ 58__ 32_ mul__ assign - _verus_
external_ ⚠fn_ specification_ 469__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ MulAssign_ 32__ 62__ 32__ 58__ 58__ 32_ mul__ assign - _verus_
external_ ⚠fn_ specification_ 470__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ MulAssign_ 32__ 62__ 32__ 58__ 58__ 32_ mul__ assign - _verus_
external_ ⚠fn_ specification_ 471__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ MulAssign_ 32__ 62__ 32__ 58__ 58__ 32_ mul__ assign - _verus_
external_ ⚠fn_ specification_ 472__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ MulAssign_ 32__ 62__ 32__ 58__ 58__ 32_ mul__ assign - _verus_
external_ ⚠fn_ specification_ 473__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ MulAssign_ 32__ 62__ 32__ 58__ 58__ 32_ mul__ assign - _verus_
external_ ⚠fn_ specification_ 474__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ MulAssign_ 32__ 62__ 32__ 58__ 58__ 32_ mul__ assign - _verus_
external_ ⚠fn_ specification_ 475__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ MulAssign_ 32__ 62__ 32__ 58__ 58__ 32_ mul__ assign - _verus_
external_ ⚠fn_ specification_ 476__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ MulAssign_ 32__ 62__ 32__ 58__ 58__ 32_ mul__ assign - _verus_
external_ ⚠fn_ specification_ 477__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ MulAssign_ 32__ 62__ 32__ 58__ 58__ 32_ mul__ assign - _verus_
external_ ⚠fn_ specification_ 478__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ MulAssign_ 32__ 62__ 32__ 58__ 58__ 32_ mul__ assign - _verus_
external_ ⚠fn_ specification_ 479__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 480__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 481__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 482__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 483__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 484__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 485__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ DivAssign_ 32__ 62__ 32__ 58__ 58__ 32_ div__ assign - _verus_
external_ ⚠fn_ specification_ 486__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ DivAssign_ 32__ 62__ 32__ 58__ 58__ 32_ div__ assign - _verus_
external_ ⚠fn_ specification_ 487__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ DivAssign_ 32__ 62__ 32__ 58__ 58__ 32_ div__ assign - _verus_
external_ ⚠fn_ specification_ 488__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ DivAssign_ 32__ 62__ 32__ 58__ 58__ 32_ div__ assign - _verus_
external_ ⚠fn_ specification_ 489__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ DivAssign_ 32__ 62__ 32__ 58__ 58__ 32_ div__ assign - _verus_
external_ ⚠fn_ specification_ 490__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ DivAssign_ 32__ 62__ 32__ 58__ 58__ 32_ div__ assign - _verus_
external_ ⚠fn_ specification_ 491__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 492__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 493__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 494__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 495__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 496__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 497__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ DivAssign_ 32__ 62__ 32__ 58__ 58__ 32_ div__ assign - _verus_
external_ ⚠fn_ specification_ 498__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ DivAssign_ 32__ 62__ 32__ 58__ 58__ 32_ div__ assign - _verus_
external_ ⚠fn_ specification_ 499__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ DivAssign_ 32__ 62__ 32__ 58__ 58__ 32_ div__ assign - _verus_
external_ ⚠fn_ specification_ 500__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ DivAssign_ 32__ 62__ 32__ 58__ 58__ 32_ div__ assign - _verus_
external_ ⚠fn_ specification_ 501__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ DivAssign_ 32__ 62__ 32__ 58__ 58__ 32_ div__ assign - _verus_
external_ ⚠fn_ specification_ 502__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ DivAssign_ 32__ 62__ 32__ 58__ 58__ 32_ div__ assign - _verus_
external_ ⚠fn_ specification_ 503__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 504__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 505__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 506__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 507__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 508__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 509__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ RemAssign_ 32__ 62__ 32__ 58__ 58__ 32_ rem__ assign - _verus_
external_ ⚠fn_ specification_ 510__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ RemAssign_ 32__ 62__ 32__ 58__ 58__ 32_ rem__ assign - _verus_
external_ ⚠fn_ specification_ 511__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ RemAssign_ 32__ 62__ 32__ 58__ 58__ 32_ rem__ assign - _verus_
external_ ⚠fn_ specification_ 512__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ RemAssign_ 32__ 62__ 32__ 58__ 58__ 32_ rem__ assign - _verus_
external_ ⚠fn_ specification_ 513__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ RemAssign_ 32__ 62__ 32__ 58__ 58__ 32_ rem__ assign - _verus_
external_ ⚠fn_ specification_ 514__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ RemAssign_ 32__ 62__ 32__ 58__ 58__ 32_ rem__ assign - _verus_
external_ ⚠fn_ specification_ 515__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 516__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 517__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 518__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 519__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 520__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 521__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ RemAssign_ 32__ 62__ 32__ 58__ 58__ 32_ rem__ assign - _verus_
external_ ⚠fn_ specification_ 522__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ RemAssign_ 32__ 62__ 32__ 58__ 58__ 32_ rem__ assign - _verus_
external_ ⚠fn_ specification_ 523__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ RemAssign_ 32__ 62__ 32__ 58__ 58__ 32_ rem__ assign - _verus_
external_ ⚠fn_ specification_ 524__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ RemAssign_ 32__ 62__ 32__ 58__ 58__ 32_ rem__ assign - _verus_
external_ ⚠fn_ specification_ 525__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ RemAssign_ 32__ 62__ 32__ 58__ 58__ 32_ rem__ assign - _verus_
external_ ⚠fn_ specification_ 526__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ RemAssign_ 32__ 62__ 32__ 58__ 58__ 32_ rem__ assign - _verus_
external_ ⚠fn_ specification_ 527__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 528__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 529__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 530__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 531__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 532__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 533__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 534__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 535__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 536__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 537__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 538__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 539__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitand__ assign - _verus_
external_ ⚠fn_ specification_ 540__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitand__ assign - _verus_
external_ ⚠fn_ specification_ 541__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitand__ assign - _verus_
external_ ⚠fn_ specification_ 542__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitand__ assign - _verus_
external_ ⚠fn_ specification_ 543__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitand__ assign - _verus_
external_ ⚠fn_ specification_ 544__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitand__ assign - _verus_
external_ ⚠fn_ specification_ 545__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitand__ assign - _verus_
external_ ⚠fn_ specification_ 546__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitand__ assign - _verus_
external_ ⚠fn_ specification_ 547__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitand__ assign - _verus_
external_ ⚠fn_ specification_ 548__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitand__ assign - _verus_
external_ ⚠fn_ specification_ 549__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitand__ assign - _verus_
external_ ⚠fn_ specification_ 550__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitand__ assign - _verus_
external_ ⚠fn_ specification_ 551__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 552__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 553__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 554__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 555__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 556__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 557__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 558__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 559__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 560__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 561__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 562__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 563__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitor__ assign - _verus_
external_ ⚠fn_ specification_ 564__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitor__ assign - _verus_
external_ ⚠fn_ specification_ 565__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitor__ assign - _verus_
external_ ⚠fn_ specification_ 566__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitor__ assign - _verus_
external_ ⚠fn_ specification_ 567__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitor__ assign - _verus_
external_ ⚠fn_ specification_ 568__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitor__ assign - _verus_
external_ ⚠fn_ specification_ 569__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitor__ assign - _verus_
external_ ⚠fn_ specification_ 570__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitor__ assign - _verus_
external_ ⚠fn_ specification_ 571__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitor__ assign - _verus_
external_ ⚠fn_ specification_ 572__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitor__ assign - _verus_
external_ ⚠fn_ specification_ 573__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitor__ assign - _verus_
external_ ⚠fn_ specification_ 574__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitor__ assign - _verus_
external_ ⚠fn_ specification_ 575__ 60__ 32_ bool_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 576__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 577__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 578__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 579__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 580__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 581__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 582__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 583__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 584__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 585__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 586__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 587__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 588__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor__ assign - _verus_
external_ ⚠fn_ specification_ 589__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor__ assign - _verus_
external_ ⚠fn_ specification_ 590__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor__ assign - _verus_
external_ ⚠fn_ specification_ 591__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor__ assign - _verus_
external_ ⚠fn_ specification_ 592__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor__ assign - _verus_
external_ ⚠fn_ specification_ 593__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor__ assign - _verus_
external_ ⚠fn_ specification_ 594__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor__ assign - _verus_
external_ ⚠fn_ specification_ 595__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor__ assign - _verus_
external_ ⚠fn_ specification_ 596__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor__ assign - _verus_
external_ ⚠fn_ specification_ 597__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor__ assign - _verus_
external_ ⚠fn_ specification_ 598__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor__ assign - _verus_
external_ ⚠fn_ specification_ 599__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor Assign_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor__ assign - _verus_
external_ ⚠fn_ specification_ 600__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 601__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 602__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 603__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 604__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 605__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 606__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 607__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 608__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 609__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 610__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 611__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 612__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShlAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shl__ assign - _verus_
external_ ⚠fn_ specification_ 613__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShlAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shl__ assign - _verus_
external_ ⚠fn_ specification_ 614__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShlAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shl__ assign - _verus_
external_ ⚠fn_ specification_ 615__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShlAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shl__ assign - _verus_
external_ ⚠fn_ specification_ 616__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShlAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shl__ assign - _verus_
external_ ⚠fn_ specification_ 617__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShlAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shl__ assign - _verus_
external_ ⚠fn_ specification_ 618__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShlAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shl__ assign - _verus_
external_ ⚠fn_ specification_ 619__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShlAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shl__ assign - _verus_
external_ ⚠fn_ specification_ 620__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShlAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shl__ assign - _verus_
external_ ⚠fn_ specification_ 621__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShlAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shl__ assign - _verus_
external_ ⚠fn_ specification_ 622__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShlAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shl__ assign - _verus_
external_ ⚠fn_ specification_ 623__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShlAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shl__ assign - _verus_
external_ ⚠fn_ specification_ 624__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 625__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 626__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 627__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 628__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 629__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 630__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 631__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 632__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 633__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 634__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 635__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 636__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShrAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shr__ assign - _verus_
external_ ⚠fn_ specification_ 637__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShrAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shr__ assign - _verus_
external_ ⚠fn_ specification_ 638__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShrAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shr__ assign - _verus_
external_ ⚠fn_ specification_ 639__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShrAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shr__ assign - _verus_
external_ ⚠fn_ specification_ 640__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShrAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shr__ assign - _verus_
external_ ⚠fn_ specification_ 641__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShrAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shr__ assign - _verus_
external_ ⚠fn_ specification_ 642__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShrAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shr__ assign - _verus_
external_ ⚠fn_ specification_ 643__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShrAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shr__ assign - _verus_
external_ ⚠fn_ specification_ 644__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShrAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shr__ assign - _verus_
external_ ⚠fn_ specification_ 645__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShrAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shr__ assign - _verus_
external_ ⚠fn_ specification_ 646__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShrAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shr__ assign - _verus_
external_ ⚠fn_ specification_ 647__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ ShrAssign_ 32__ 62__ 32__ 58__ 58__ 32_ shr__ assign - _verus_
external_ ⚠fn_ specification_ 648__ 60__ 32_ f32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - _verus_
external_ ⚠fn_ specification_ 649__ 60__ 32_ f32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 650__ 60__ 32_ f32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 651__ 60__ 32_ f32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 652__ 60__ 32_ f32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 653__ 60__ 32_ f64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - _verus_
external_ ⚠fn_ specification_ 654__ 60__ 32_ f64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 655__ 60__ 32_ f64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 656__ 60__ 32_ f64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 657__ 60__ 32_ f64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - add_
ensures - div_
ensures - mul_
ensures - neg_
ensures - sub_
ensures