Struct OpenClause 

pub struct OpenClause {
    pub namespace: Name,
    pub only: Option<Vec<Name>>,
    pub hiding: Vec<Name>,
    pub renaming: Vec<(Name, Name)>,
}

One open clause: a namespace, and WHICH of its names it brings in, under WHICH spelling.

Lean’s four forms (Lean/Elab/Open.lean:63-96), and they are not sugar for one another: Open Alpha. brings in all of them; Open Alpha (a b). brings in exactly those two; Open Alpha hiding (a). brings in the rest; Open Alpha renaming a -> b. brings in a under the local spelling b and brings in nothing else. Opening a namespace WHOLESALE is what makes short names ambiguous in the first place, so the three narrowing forms are the tools for AVOIDING an ambiguity rather than being told about one — and renaming is the only one of them that can bring in a name whose short spelling already means something else here.

Fields

namespace: Name

The namespace. As written when the clause is parsed; resolved against the current namespace when it is applied.

only: Option<Vec<Name>>

Open Alpha (a b). — ONLY these names are brought in. None is the wholesale opening.

hiding: Vec<Name>

Open Alpha hiding (a b). — every name EXCEPT these.

renaming: Vec<(Name, Name)>

Open Alpha renaming a -> b. — (the member, the local spelling). A clause with any renaming brings in EXACTLY these, which is why it is its own form and not a modifier on the others: Lean’s renaming arm emits only OpenDecl.explicit entries and no simple open (Lean/Elab/Open.lean:89-96), so open Baz renaming orig → ali leaves untouched unknown.

Implementations

impl OpenClause

pub fn all(namespace: Name) -> OpenClause

Open Alpha. — the wholesale opening.

Trait Implementations

impl Clone for OpenClause

fn clone(&self) -> OpenClause

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for OpenClause

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

Formats the value using the given formatter.

impl PartialEq for OpenClause

fn eq(&self, other: &OpenClause) -> 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 Eq for OpenClause

impl StructuralPartialEq for OpenClause