Agda-2.2.8: A dependently typed functional programming language and proof assistant




data HoleName Source

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.


LambdaHole String String

(x -> y) ; 1st argument is the bound name (unused for now)

ExprHole String

simple named hole

type Notation = [GenPart]Source

Target of a hole

data GenPart Source

Part of a Notation


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 

isAHole :: GenPart -> BoolSource

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

Is the part a hole?

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

From notation with names to notation with indices.