- data HoleName
- holeName :: HoleName -> String
- type Notation = [GenPart]
- data GenPart
- stringParts :: Notation -> [String]
- holeTarget :: GenPart -> Maybe Int
- isAHole :: GenPart -> Bool
- isBindingHole :: GenPart -> Bool
- isLambdaHole :: HoleName -> Bool
- mkNotation :: [HoleName] -> [String] -> Either String Notation
- defaultNotation :: [a]
- noNotation :: [a]
A name is a non-empty list of alternating
Holes. A normal name
is represented by a singleton list, and operators are represented by a list
Holes where the arguments should go. For instance:
is infix addition.
Equality and ordering on
Names are defined to ignore range so same names
in different locations are equal.
Data type constructed in the Happy parser; converted to
before it leaves the Happy code.
Part of a Notation
Argument is the position of the hole (with binding) where the binding should occur.
Argument is where the expression should go
Target argument position of a part (Nothing if it is not a hole)
From notation with names to notation with indices.