| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Scope.Operator
Description
Computing scopes of names that are relevant to parsing some raw expression.
Synopsis
- data OperatorScope = OpScope {}
- getOperatorScope :: Set QName -> ScopeInfo -> OperatorScope
- getDefinedNames :: KindsOfNames -> OperatorScope -> [List1 NewNotation]
- localNames :: ExprKind -> Maybe QName -> OperatorScope -> ScopeM ([QName], [NewNotation])
Documentation
data OperatorScope Source #
Names that are relevant to operator parsing.
Constructors
| OpScope | |
Instances
| Pretty OperatorScope Source # | |
Defined in Agda.Syntax.Scope.Operator Methods pretty :: OperatorScope -> Doc Source # prettyPrec :: Int -> OperatorScope -> Doc Source # prettyList :: [OperatorScope] -> Doc Source # | |
getOperatorScope :: Set QName -> ScopeInfo -> OperatorScope Source #
getDefinedNames :: KindsOfNames -> OperatorScope -> [List1 NewNotation] Source #
localNames :: ExprKind -> Maybe QName -> OperatorScope -> ScopeM ([QName], [NewNotation]) Source #
Compute all names (first component) and operators/notations (second component) in scope.
For IsPattern, only constructor-like names are returned.