The data associated with a name in context. This includes:

• Whether the name is a constructor, pattern synonym, or ordinary definition.
• A list of ranges associated with the name, which includes the site of the original definition, as well as any relevant import or open statements.
• Alternative syntax for the name, if any.

The data associated with a module in context. This includes:

• A list of ranges associated with the module, which includes the site of the original definition, as well as any relevant import or open statements.
• The inner context of the module.

Like Module, but also recording whether the module is public or private.

A namespace of definitions. Any Agda module produces a Context.

A namespace of definitions, which may be public or private. Any collection of Agda declarations produces an AccessContext, for example.

Like (<>), but public items take precedence over private items. This is important when combining contexts from successive declarations; for example:

module M where

  postulate
    A : Set

module N where

  postulate
    A : Set

  open M

x : N.A
x = ?

This code type-checks, and the identifier N.A refers to the postulate declared in the definition of N, not the definition opened from M.

A description of failure for an AccessContext lookup.

Get the ranges for the given name, or Nothing if not in context.

Get the item for the given name, or Nothing if not in context.

Get the inner module for the given name, or Nothing if not in context.

Get the ranges for the given name, or produce a LookupError.

Get the inner module for the given name, or produce a LookupError.

Like accessContextLookup, but also return a boolean indicating whether we are currently defining the referenced item.

Determine whether a name represents a constructor or pattern synonym. Return Nothing if the name is not in context.

Insert a range for the given name, if present.

Insert a range for all names in the given module, if present.

Insert a range for all names in a context.

Insert a range for all names in an access context.

Delete an item from the context.

Delete a module from the context.

Rename an item, if present.

Rename a module, if present.

Mark an existing name as in process of being defined.

Get all ranges associated with names in the given module, including ranges associated with the module itself.

Get all ranges associated with names in the given context.

Find all operators matching the given list of tokens.

Construct an Item representing an ordinary definition.

Construct an Item representing a pattern synonym.

Construct an Item representing a constructor.

Construct a Context with a single item.

Construct a Context with a single module.

Construct an AccessContext with a single item, along with the relevant syntax item if applicable.

Construct an AccessContext with a single access module.

Like accessContextModule, but taking an access context. We convert the given access context to an ordinary context using toContext:

accessContextModule' n a rs c
  = accessContextModule n (AccessModule a rs (toContext c))

Construct an access context with a single import.

Convert a Context to AccessContext. Give all items the given access.

Convert an AccessContext to Context. Discard private items and imports.