Agda
Safe HaskellNone
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

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 #

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

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

For IsPattern, only constructor-like names are returned.