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

Safe Haskell | None

Agda.Syntax.Notation

Synopsis

- data HoleName
  - = LambdaHole String String
  - | ExprHole String
- holeName :: HoleName -> String
- type Notation = [GenPart]
- data GenPart
  - = BindHole Int
  - | NormalHole Int
  - | IdPart String
- stringParts :: Notation -> [String]
- holeTarget :: GenPart -> Maybe Int
- isAHole :: GenPart -> Bool
- isBindingHole :: GenPart -> Bool
- isLambdaHole :: HoleName -> Bool
- mkNotation :: [HoleName] -> [String] -> Either String Notation
- defaultNotation :: [a]
- noNotation :: [a]

# Documentation

data HoleName

A name is a non-empty list of alternating `Id`s and `Hole`s. A normal name is represented by a singleton list, and operators are represented by a list with `Hole`s where the arguments should go. For instance: `[Hole,Id +,Hole]` is infix addition.

Equality and ordering on `Name`s 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]