ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Scope.Flat

Flattened scopes.

newtypenewtype FlatScope

Flattened scopes.

Instances1Pretty

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]

valuelocalNames

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

For IsPattern, only constructor-like names are returned.