Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Scope.Flat

Description

Flattened scopes.

Synopsis

data FlatScope
flattenScope :: [[Name]] -> ScopeInfo -> FlatScope
getDefinedNames :: KindsOfNames -> FlatScope -> [List1 NewNotation]
localNames :: FlatScope -> ScopeM ([QName], [NewNotation])

Documentation

data FlatScope Source #

Flattened scopes.

Instances

Instances details

Pretty FlatScope Source #
Instance details Defined in Agda.Syntax.Scope.Flat Methods pretty :: FlatScope -> Doc Source # prettyPrec :: Int -> FlatScope -> Doc Source # prettyList :: [FlatScope] -> Doc Source #

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.