Trait Default

pub trait Default: Default {
    // Required method
    fn is_default(self) -> bool;
}

Extension of the standard Default trait.

This allows Creusot to specify the behavior of default.

Derive macro

Similarly to std, Creusot defines a derive macro for Default:

use creusot_contracts::Default;

#[derive(Default)]
struct S(i32);

This will implement both Default traits, and generate a proof obligation to show that they agree.

Required Methods

fn is_default(self) -> bool

logic(prophetic)

Dyn Compatibility

This trait is not dyn compatible.

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

Implementations on Foreign Types

impl Default for bool

fn is_default(self) -> bool

logic

pearlite! { self == false }

impl Default for char

fn is_default(self) -> bool

logic

pearlite! { self@ == 0 }

impl Default for i8

fn is_default(self) -> bool

logic

pearlite! { self == $zero }

impl Default for i16

fn is_default(self) -> bool

logic

pearlite! { self == $zero }

impl Default for i32

fn is_default(self) -> bool

logic

pearlite! { self == $zero }

impl Default for i64

fn is_default(self) -> bool

logic

pearlite! { self == $zero }

impl Default for i128

fn is_default(self) -> bool

logic

pearlite! { self == $zero }

impl Default for isize

fn is_default(self) -> bool

logic

pearlite! { self == $zero }

impl Default for u8

fn is_default(self) -> bool

logic

pearlite! { self == $zero }

impl Default for u16

fn is_default(self) -> bool

logic

pearlite! { self == $zero }

impl Default for u32

fn is_default(self) -> bool

logic

pearlite! { self == $zero }

impl Default for u64

fn is_default(self) -> bool

logic

pearlite! { self == $zero }

impl Default for u128

fn is_default(self) -> bool

logic

pearlite! { self == $zero }

impl Default for ()

fn is_default(self) -> bool

logic

pearlite! { true }

impl Default for usize

fn is_default(self) -> bool

logic

pearlite! { self == $zero }

impl<A: Default> Default for (A,)

fn is_default(self) -> bool

logic(prophetic)

pearlite! { $(self.$idx.is_default())&&+ }

impl<A: Default, B: Default> Default for (A, B)

fn is_default(self) -> bool

logic(prophetic)

pearlite! { $(self.$idx.is_default())&&+ }

impl<A: Default, B: Default, C: Default> Default for (A, B, C)

fn is_default(self) -> bool

logic(prophetic)

pearlite! { $(self.$idx.is_default())&&+ }

impl<A: Default, B: Default, C: Default, D: Default> Default for (A, B, C, D)

fn is_default(self) -> bool

logic(prophetic)

pearlite! { $(self.$idx.is_default())&&+ }

impl<A: Default, B: Default, C: Default, D: Default, E: Default> Default for (A, B, C, D, E)

fn is_default(self) -> bool

logic(prophetic)

pearlite! { $(self.$idx.is_default())&&+ }

impl<A: Default, B: Default, C: Default, D: Default, E: Default, F: Default> Default for (A, B, C, D, E, F)

fn is_default(self) -> bool

logic(prophetic)

pearlite! { $(self.$idx.is_default())&&+ }

impl<A: Default, B: Default, C: Default, D: Default, E: Default, F: Default, G: Default> Default for (A, B, C, D, E, F, G)

fn is_default(self) -> bool

logic(prophetic)

pearlite! { $(self.$idx.is_default())&&+ }

impl<A: Default, B: Default, C: Default, D: Default, E: Default, F: Default, G: Default, H: Default> Default for (A, B, C, D, E, F, G, H)

fn is_default(self) -> bool

logic(prophetic)

pearlite! { $(self.$idx.is_default())&&+ }

impl<A: Default, B: Default, C: Default, D: Default, E: Default, F: Default, G: Default, H: Default, I: Default> Default for (A, B, C, D, E, F, G, H, I)

fn is_default(self) -> bool

logic(prophetic)

pearlite! { $(self.$idx.is_default())&&+ }

impl<A: Default, B: Default, C: Default, D: Default, E: Default, F: Default, G: Default, H: Default, I: Default, J: Default> Default for (A, B, C, D, E, F, G, H, I, J)

fn is_default(self) -> bool

logic(prophetic)

pearlite! { $(self.$idx.is_default())&&+ }

impl<A: Default, B: Default, C: Default, D: Default, E: Default, F: Default, G: Default, H: Default, I: Default, J: Default, K: Default> Default for (A, B, C, D, E, F, G, H, I, J, K)

fn is_default(self) -> bool

logic(prophetic)

pearlite! { $(self.$idx.is_default())&&+ }

impl<A: Default, B: Default, C: Default, D: Default, E: Default, F: Default, G: Default, H: Default, I: Default, J: Default, K: Default, L: Default> Default for (A, B, C, D, E, F, G, H, I, J, K, L)

fn is_default(self) -> bool

logic(prophetic)

pearlite! { $(self.$idx.is_default())&&+ }

impl<T> Default for &[T]

fn is_default(self) -> bool

logic

pearlite! { self@ == Seq::EMPTY }

impl<T> Default for &mut [T]

fn is_default(self) -> bool

logic(prophetic)

pearlite! { self@ == Seq::EMPTY && (^self)@ == Seq::EMPTY }

Implementors

impl Default for PeanoInt

impl Default for RandomState

impl<T> Default for Option<T>

impl<T> Default for Vec<T>