Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Syntax.Notation
Synopsis
data HoleName
= LambdaHole String String
| ExprHole String
type Notation = [GenPart]
data GenPart
= BindHole Int
| NormalHole Int
| IdPart String
isAHole :: GenPart -> Bool
mkNotation :: [HoleName] -> [String] -> Either String Notation
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 String String(x -> y) ; 1st argument is the bound name (unused for now)
ExprHole Stringsimple named hole
type Notation = [GenPart]Source
Target of a hole
data GenPart Source
Part of a Notation
Constructors
BindHole IntArgument is the position of the hole (with binding) where the binding should occur.
NormalHole IntArgument 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.
Produced by Haddock version 2.6.1