creusot_contracts/std/
char.rs

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
use crate::{Default, *};
pub use ::std::char::*;

impl View for char {
    type ViewTy = Int;
    #[logic]
    #[trusted]
    #[creusot::builtins = "creusot.prelude.Char.to_int"]
    fn view(self) -> Self::ViewTy {
        dead
    }
}

impl DeepModel for char {
    type DeepModelTy = Int;
    #[logic]
    #[open]
    fn deep_model(self) -> Self::DeepModelTy {
        pearlite! { self@ }
    }
}

impl Default for char {
    #[predicate]
    #[open]
    fn is_default(self) -> bool {
        pearlite! { self@ == 0 }
    }
}