Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Int in ghost

You can manipulate values of type Int in ghost code, by using the int suffix on integer literals:

ghost! {
    let x = 42int;
    let y = 58int;
    assert!(x + y == 100int);
};

Ghost containers return their length as an Int, and Seq is indexed by Int as well:

ghost! {
    let s: Seq<_> = ...;
    let m: FMap<_, _> = ...;
    let len: Int = m.len_ghost();
    let x = s[len + 3int];
};