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

Safe HaskellNone

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 String String

(x -> y) ; 1st argument is the bound name (unused for now)

ExprHole String

simple named hole with hiding

holeName :: HoleName -> StringSource

Target of a hole

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 String 

stringParts :: Notation -> [String]Source

Get a flat list of identifier parts of a notation.

holeTarget :: GenPart -> Maybe IntSource

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

isAHole :: GenPart -> BoolSource

Is the part a hole?

mkNotation :: [NamedArg c HoleName] -> [String] -> Either String NotationSource

From notation with names to notation with indices.

defaultNotation :: [a]Source

No notation by default