Skip to main content

creusot_std/std/
convert.rs

1use crate::prelude::*;
2
3extern_spec! {
4    mod core {
5        mod convert {
6            trait From<T> where Self: From<T> {
7                // #[requires(true)]
8                fn from(value: T) -> Self;
9            }
10        }
11    }
12
13    impl<T> From<T> for T {
14        #[ensures(result == self)]
15        fn from(self) -> T;
16    }
17}