creusot_std/std/
default.rs

1use crate::prelude::*;
2use core::default::*;
3
4#[cfg(creusot)]
5pub use creusot_std_proc::Default;
6
7#[cfg(not(creusot))]
8pub use core::default::Default;
9
10extern_spec! {
11    mod core {
12        mod default {
13            trait Default {
14                // #[requires(true)]
15                fn default() -> Self;
16            }
17        }
18    }
19
20    impl Default for bool {
21        #[check(ghost)]
22        #[ensures(result == false)]
23        fn default() -> bool;
24    }
25}