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

holeName :: HoleName -> String

Target of a hole

type Notation = [GenPart]

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

Show GenPart

Typeable GenPart

EmbPrj GenPart

stringParts :: Notation -> [String]

Get a flat list of identifier parts of a notation.

holeTarget :: GenPart -> Maybe Int

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

isAHole :: GenPart -> Bool

Is the part a hole?

isBindingHole :: GenPart -> Bool

isLambdaHole :: HoleName -> Bool

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

From notation with names to notation with indices.

defaultNotation :: [a]

No notation by default

noNotation :: [a]