Module ghost

Definitions for ghost code

Ghost code is code that will be erased during the normal compilation of the program. To use ghost code in creusot, you must use the ghost! macro:

let x: Ghost<i32> = ghost!(1);
ghost! {
    let y: i32 = *x;
    assert!(y == 1);
};

There are restrictions on the values that can enter/exit a ghost! block: see Ghost and ghost! for more details.

Structs

Ghost

A type that can be used in ghost! context.