Agda.Syntax.Notation

data HoleName

isLambdaHole

type Notation

data GenPart

stringParts

holeTarget

isAHole

isNormalHole

isBindingHole

data NotationKind

notationKind

mkNotation

noNotation