Enum SpecFunc 

pub enum SpecFunc {
    Uif,
    Defined {
        body: Binder<Expr>,
        hide: bool,
    },
}

A spec function (aka flux-def) as written by the user, i.e., before inlining any of the functions it calls.

Variants

Uif

An uninterpreted function

Defined

A function with a body

Fields

body: Binder<Expr>

hide: bool

Whether the function is uninterpreted by default

Implementations

impl SpecFunc

pub fn is_uif(&self) -> bool

Trait Implementations

impl Clone for SpecFunc

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'tcx, __D: TyDecoder<'tcx>> Decodable<__D> for SpecFunc

fn decode(__decoder: &mut __D) -> Self

impl<'tcx, __E: TyEncoder<'tcx>> Encodable<__E> for SpecFunc

fn encode(&self, __encoder: &mut __E)