ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Scope.Flat

Flattened scopes.

1 type
3 values

PackageAgda-2.7.0.1
Exports4
LanguageHaskell2010
LicenceMIT
SourceFlat.hs

newtypenewtype FlatScope

Flattened scopes.

Instances1Pretty

Pretty FlatScopeDefined in Agda-2.7.0.1 · Agda.Syntax.Scope.Flat

valueflattenScope :: [[Name]] -> ScopeInfo -> FlatScope

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

valuegetDefinedNames :: KindsOfNames -> FlatScope -> [List1 NewNotation]

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.)

valuelocalNames :: FlatScope -> ScopeM ([QName], [NewNotation])

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