Safe Haskell	None
Language	Haskell98

Agda.Syntax.Notation

Synopsis

Documentation

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.

Constructors

LambdaHole RawName RawName	(x -> y) ; 1st argument is the bound name (unused for now)
ExprHole RawName	simple named hole with hiding

holeName :: HoleName -> RawName Source

Target of a hole

type Notation = [GenPart] Source

data GenPart Source

Part of a Notation

Constructors

BindHole Int	Argument is the position of the hole (with binding) where the binding should occur.
NormalHole (NamedArg () Int)	Argument is where the expression should go
IdPart RawName

Instances

Eq GenPart
Show GenPart
EmbPrj GenPart
Typeable * GenPart

stringParts :: Notation -> [RawName] Source

Get a flat list of identifier parts of a notation.

holeTarget :: GenPart -> Maybe Int Source

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

isAHole :: GenPart -> Bool Source

Is the part a hole?

isBindingHole :: GenPart -> Bool Source

isLambdaHole :: HoleName -> Bool Source

mkNotation :: [NamedArg c HoleName] -> [RawName] -> Either String Notation Source

From notation with names to notation with indices.

defaultNotation :: [t] Source

No notation by default

noNotation :: [t] Source