creusot_contracts/std/
convert.rs

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