Safe Haskell  None 

Language  Haskell2010 
As a concrete name, a notation is a nonempty list of alternating IdPart
s and holes.
In contrast to concrete names, holes can be binders.
Example:
syntax fmap (λ x → e) xs = for x ∈ xs return e
The declared notation for fmap
is for_∈_return_
where the first hole is a binder.
Synopsis
 data HoleName
 = LambdaHole { }
  ExprHole { }
 isLambdaHole :: HoleName > Bool
 stringParts :: Notation > [String]
 holeTarget :: GenPart > Maybe Int
 isAHole :: GenPart > Bool
 isNormalHole :: GenPart > Bool
 isBindingHole :: GenPart > Bool
 data NotationKind
 notationKind :: Notation > NotationKind
 mkNotation :: [NamedArg HoleName] > [RString] > Either String Notation
 data NewNotation = NewNotation {}
 namesToNotation :: QName > Name > NewNotation
 useDefaultFixity :: NewNotation > NewNotation
 notationNames :: NewNotation > [QName]
 syntaxOf :: Name > Notation
 mergeNotations :: [NewNotation] > [NewNotation]
 _notaFixity :: Lens' Fixity NewNotation
 data NotationSection = NotationSection {}
 noSection :: NewNotation > NotationSection
Documentation
Data type constructed in the Happy parser; converted to GenPart
before it leaves the Happy code.
LambdaHole 

 
ExprHole  Simple named hole with hiding. 
isLambdaHole :: HoleName > Bool Source #
Is the hole a binder?
stringParts :: Notation > [String] Source #
Get a flat list of identifier parts of a notation.
holeTarget :: GenPart > Maybe Int Source #
Target argument position of a part (Nothing if it is not a hole).
isAHole :: GenPart > Bool Source #
Is the part a hole? WildHoles don't count since they don't correspond to anything the user writes.
isNormalHole :: GenPart > Bool Source #
Is the part a normal hole?
isBindingHole :: GenPart > Bool Source #
Is the part a binder?
data NotationKind Source #
Classification of notations.
InfixNotation  Ex: 
PrefixNotation  Ex: 
PostfixNotation  Ex: 
NonfixNotation  Ex: 
NoNotation 
Instances
Eq NotationKind Source #  
Defined in Agda.Syntax.Notation (==) :: NotationKind > NotationKind > Bool # (/=) :: NotationKind > NotationKind > Bool #  
Show NotationKind Source #  
Defined in Agda.Syntax.Notation showsPrec :: Int > NotationKind > ShowS # show :: NotationKind > String # showList :: [NotationKind] > ShowS # 
notationKind :: Notation > NotationKind Source #
Classify a notation by presence of leading and/or trailing normal holes.
mkNotation :: [NamedArg HoleName] > [RString] > Either String Notation Source #
From notation with names to notation with indices.
Example:
ids = ["for", "x", "∈", "xs", "return", "e"]
holes = [ LambdaHole "x" "e", ExprHole "xs" ]
creates the notation
[ IdPart "for" , BindHole 0
, IdPart "∈" , NormalHole 1
, IdPart "return" , NormalHole 0
]
data NewNotation Source #
All the notation information related to a name.
NewNotation  

Instances
Show NewNotation Source #  
Defined in Agda.Syntax.Notation showsPrec :: Int > NewNotation > ShowS # show :: NewNotation > String # showList :: [NewNotation] > ShowS #  
LensFixity NewNotation Source #  
Defined in Agda.Syntax.Notation 
namesToNotation :: QName > Name > NewNotation Source #
If an operator has no specific notation, then it is computed from its name.
useDefaultFixity :: NewNotation > NewNotation Source #
Replace noFixity
by defaultFixity
.
notationNames :: NewNotation > [QName] Source #
Return the IdPart
s of a notation, the first part qualified,
the other parts unqualified.
This allows for qualified use of operators, e.g.,
M.for x ∈ xs return e
, or x ℕ.+ y
.
syntaxOf :: Name > Notation Source #
Create a Notation
(without binders) from a concrete Name
.
Does the obvious thing:
Hole
s become NormalHole
s, Id
s become IdParts
.
If Name
has no Hole
s, it returns noNotation
.
mergeNotations :: [NewNotation] > [NewNotation] Source #
Merges NewNotation
s that have the same precedence level and
notation, with two exceptions:
 Operators and notations coming from syntax declarations are kept separate.
 If all instances of a given
NewNotation
have the same precedence level or are "unrelated", then they are merged. They get the given precedence level, if any, and otherwise they become unrelated (but related to each other).
If NewNotation
s that are merged have distinct associativities,
then they get NonAssoc
as their associativity.
Precondition: No Name
may occur in more than one list element.
Every NewNotation
must have the same notaName
.
Postcondition: No Name
occurs in more than one list element.
_notaFixity :: Lens' Fixity NewNotation Source #
Lens for Fixity
in NewNotation
.
Sections
data NotationSection Source #
Sections, as well as nonsectioned operators.
NotationSection  

Instances
Show NotationSection Source #  
Defined in Agda.Syntax.Notation showsPrec :: Int > NotationSection > ShowS # show :: NotationSection > String # showList :: [NotationSection] > ShowS # 
noSection :: NewNotation > NotationSection Source #
Converts a notation to a (non)section.