Enum Constraint 

pub enum Constraint<T: Types> {
    Pred(Pred<T>, Option<T::Tag>),
    Conj(Vec<Self>),
    ForAll(Bind<T>, Box<Self>),
}

Variants

Pred(Pred<T>, Option<T::Tag>)

Conj(Vec<Self>)

ForAll(Bind<T>, Box<Self>)

Implementations

impl<T: Types> Constraint<T>

pub const TRUE: Self

pub fn foralls(bindings: Vec<Bind<T>>, c: Self) -> Self

pub fn conj(cstrs: Vec<Self>) -> Self

pub fn concrete_head_count(&self) -> usize

Returns true if the constraint has at least one concrete RHS (“head”) predicates. If !c.is_concrete then c is trivially satisfiable and we can avoid calling fixpoint. Returns the number of concrete, non-trivial head predicates in the constraint.

Trait Implementations

impl<T: Types> Clone for Constraint<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 Constraint<T>

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

Formats the value using the given formatter.

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

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

Formats the value using the given formatter.

impl<T: Types> Hash for Constraint<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.