Agda-2.6.3.20230914: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Scope.Flat

Description

Flattened scopes.

Synopsis

Documentation

data FlatScope Source #

Flattened scopes.

Instances

Instances details
Pretty FlatScope Source # 
Instance details

Defined in Agda.Syntax.Scope.Flat

flattenScope :: [[Name]] -> ScopeInfo -> FlatScope Source #

Compute a flattened scope. Only include unqualified names or names qualified by modules in the first argument.

getDefinedNames :: KindsOfNames -> FlatScope -> [List1 NewNotation] Source #

Compute all defined names in scope and their fixities/notations. Note that overloaded names (constructors) can have several fixities/notations. Then we mergeNotations. (See issue 1194.)

localNames :: FlatScope -> ScopeM ([QName], [NewNotation]) Source #

Compute all names (first component) and operators/notations (second component) in scope.