Agda.Syntax.Notation
data HoleName
isLambdaHole
type Notation
data GenPart
stringParts
holeTarget
isAHole
isNormalHole
isBindingHole
data NotationKind
notationKind
mkNotation
noNotation