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

Safe HaskellSafe-Infered

Agda.Syntax.Notation

Synopsis

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 

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?

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

From notation with names to notation with indices.

defaultNotation :: [a]

No notation by default

noNotation :: [a]