Agda
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Scope.Operator

Description

Computing scopes of names that are relevant to parsing some raw expression.

Synopsis

Documentation

data OperatorScope Source #

Names that are relevant to operator parsing.

Constructors

OpScope 

Fields

Instances

Instances details
Pretty OperatorScope Source # 
Instance details

Defined in Agda.Syntax.Scope.Operator

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.