Agda.Syntax.Notation

data HoleName

holeName

type Notation

data GenPart

stringParts

holeTarget

isAHole

isBindingHole

isLambdaHole

mkNotation

defaultNotation

noNotation