Trait Base

pub trait Base {
    // Required methods
    spec fn base() -> nat;
    proof fn base_min();
}

Expand description

Represents a base with value Self::base().

Required Methods§

ensures

Self::base() > 1,

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

{ u8::MAX as nat + 1 }

{ u64::MAX as nat + 1 }

{ usize::MAX as nat + 1 }