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 is_concrete(&self) -> bool

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.

Trait Implementations

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.