Type Alias GhostFn 

pub type GhostFn<I, O> = FnSpec<(I,), O>;

Alias for Verus’s spec function type.

Aliased Type

pub struct GhostFn<I, O> { /* private fields */ }