Agda.Syntax.Notation

data HoleName

type Notation

data GenPart

isAHole

mkNotation