Struct Int 

pub struct Int;

An unbounded, mathematical integer.

This type cannot be only be constructed in logical or ghost code.

Integers in pearlite

Note that in pearlite, all integer literals are of type Int:

let x = 1i32;
//             ↓ need to use the view operator to convert `i32` to `Int`
proof_assert!(x@ == 1);

You can use the usual operators on integers: +, -, *, / and %.

Note that those operators are not available in ghost code.

Implementations

impl Int

pub fn new(value: i128) -> Ghost<Self>

Create a new Int value

The result is wrapped in a Ghost, so that it can only be access inside a ghost! block.

You should not have to use this method directly: instead, use the int suffix inside of a ghost block:

let x: Ghost<Int> = ghost!(1int);
ghost! {
    let y: Int = 2int;
};

Trait Implementations

impl Add for Int

type Output = Int

The resulting type after applying the + operator.

fn add(self, other: Int) -> Self

Performs the + operation.

impl AddLogic for Int

type Output = Int

impl Clone for Int

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl DeepModel for Int

type DeepModelTy = Int

impl Div for Int

type Output = Int

The resulting type after applying the / operator.

fn div(self, other: Int) -> Self

Performs the / operation.

impl DivLogic for Int

type Output = Int

impl<T> IndexLogic<Int> for [T]

type Item = T

impl<T, const N: usize> IndexLogic<Int> for [T; N]

type Item = T

impl<T> IndexLogic<Int> for Seq<T>

type Item = T

impl<T> IndexLogic<Int> for Vec<T>

Available on non-crate feature nightly only.

Dummy impls that don’t use the unstable trait Allocator

type Item = T

impl<T> IndexLogic<Int> for VecDeque<T>

type Item = T

impl Mul for Int

type Output = Int

The resulting type after applying the * operator.

fn mul(self, other: Int) -> Self

Performs the * operation.

impl MulLogic for Int

type Output = Int

impl Neg for Int

type Output = Int

The resulting type after applying the - operator.

fn neg(self) -> Self

Performs the unary - operation.

impl NegLogic for Int

type Output = Int

impl PartialEq for Int

fn eq(&self, other: &Self) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl PartialOrd for Int

fn partial_cmp(&self, other: &Self) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Self) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Self) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Self) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Self) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl Rem for Int

type Output = Int

The resulting type after applying the % operator.

fn rem(self, other: Int) -> Self

Performs the % operation.

impl RemLogic for Int

type Output = Int

impl Sub for Int

type Output = Int

The resulting type after applying the - operator.

fn sub(self, other: Int) -> Self

Performs the - operation.

impl SubLogic for Int

type Output = Int

impl Copy for Int

impl OrdLogic for Int

impl Plain for Int

impl WellFounded for Int