Agda-2.8.0: A dependently typed functional programming language and proof assistant

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 :: ExprKind -> Maybe QName -> 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 #

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.