Enum Scope 

pub(crate) enum Scope<'a> {
    Implicit {
        kind: BinderKind,
        node_id: NodeId,
        params: &'a [RefineParam],
    },
    Explicit(&'a [RefineParam]),
    Opaque,
}

A scope opened while walking an item. Params are only ever defined when entering the scope that declares them.

Variants

Implicit

A binder with implicitly scoped params (declared with @n, #n, x: T, &strg x). The scope can also declare explicit params, e.g., fn foo[n: int](...).

Fields

kind: BinderKind

node_id: NodeId

params: &'a [RefineParam]

Explicit(&'a [RefineParam])

A scope declaring explicit params, e.g., exists<a: int> ..., |x| ... or forall i in 0..n { ... }.

Opaque

A scope that declares no params. It only prevents binders inside it from being bound in an enclosing binder scope, e.g., @n is illegal in Vec<i32[@n]>.