Agda.Syntax.Notation

Documentation

data HoleName

A name is a non-empty list of alternating Ids and Holes. A normal name is represented by a singleton list, and operators are represented by a list with Holes where the arguments should go. For instance: [Hole,Id +,Hole] 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 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

type Notation = [GenPart]

Target of a hole

data GenPart

Part of a Notation

Constructors

BindHole Int

Argument is the position of the hole (with binding) where the binding should occur.

NormalHole Int

Argument is where the expression should go

IdPart String

Instances

Eq GenPart

Data GenPart

Show GenPart

Typeable GenPart

EmbPrj GenPart

isAHole :: GenPart -> Bool

Target argument position of a part (Nothing if it is not a hole)

Is the part a hole?

mkNotation :: [HoleName] -> [String] -> Either String Notation

From notation with names to notation with indices.