Agda.Syntax.Notation
Documentation
data HoleName
A name is a non-empty list of alternating Id
s and Hole
s. A normal name
is represented by a singleton list, and operators are represented by a list
with Hole
s where the arguments should go. For instance: [Hole,Id +,Hole]
is infix addition.
Equality and ordering on Name
s are defined to ignore range so same names
in different locations are equal.
Data type constructed in the Happy parser; converted to GenPart
before it leaves the Happy code.
Constructors
LambdaHole String String | (x -> y) ; 1st argument is the bound name (unused for now) |
ExprHole String | simple named hole |
data GenPart
Part of a Notation
Target argument position of a part (Nothing if it is not a hole)
Is the part a hole?