Struct KVarDecl 

pub struct KVarDecl<T: Types> {
    pub kvid: T::KVar,
    pub sorts: Vec<Sort<T>>,
    pub self_args: usize,
}

Fields

kvid: T::KVar

sorts: Vec<Sort<T>>

self_args: usize

Number of leading arguments in sorts that are self arguments. Fixpoint only instantiates qualifiers whose self parameters are bound to self arguments, so a kvar with no self arguments can only be solved to true or false.

Implementations

impl<T: Types> KVarDecl<T>

pub fn new(kvid: T::KVar, sorts: Vec<Sort<T>>, self_args: usize) -> Self

Trait Implementations

impl<T: Types> Clone for KVarDecl<T>

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<T: Types> Debug for KVarDecl<T>

fn fmt(&self, __f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<T: Types> Display for KVarDecl<T>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<T: Types> Hash for KVarDecl<T>

fn hash<__H: Hasher>(&self, __state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.