Skip to main content

creusot_std/std/
default.rs

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