Struct Scope

pub struct Scope {
    params: Vec<(Var, Sort)>,
    bindings: IndexVec<Name, Sort>,
}

A list of refinement variables and their sorts.

Fields

params: Vec<(Var, Sort)>

bindings: IndexVec<Name, Sort>

Implementations

impl Scope

pub(crate) fn iter(&self) -> impl Iterator<Item = (Var, Sort)> + '_

fn into_iter(self) -> impl Iterator<Item = (Var, Sort)>

pub fn has_free_vars<T: TypeFoldable>(&self, t: &T) -> bool

Whether t has any free variables not in this scope

fn contains_all(&self, iter: impl IntoIterator<Item = Name>) -> bool

fn contains(&self, name: Name) -> bool

Trait Implementations

impl Debug for Scope

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

Formats the value using the given formatter.

impl Index<Name> for Scope

type Output = Sort

The returned type after indexing.

fn index(&self, name: Name) -> &Self::Output

Performs the indexing (container[index]) operation.

impl PartialEq for Scope

fn eq(&self, other: &Scope) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Pretty for Scope

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

fn default_cx(tcx: TyCtxt<'_>) -> PrettyCx<'_, '_>

impl Eq for Scope

impl StructuralPartialEq for Scope