Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Concrete.Attribute

Description

 
Synopsis

Documentation

data Attribute Source #

An attribute is a modifier for ArgInfo.

Instances

Instances details
HasRange Attribute Source # 
Instance details

Defined in Agda.Syntax.Concrete.Attribute

KillRange Attribute Source # 
Instance details

Defined in Agda.Syntax.Concrete.Attribute

SetRange Attribute Source # 
Instance details

Defined in Agda.Syntax.Concrete.Attribute

Show Attribute Source # 
Instance details

Defined in Agda.Syntax.Concrete.Attribute

Methods

showsPrec :: Int -> Attribute -> ShowS

show :: Attribute -> String

showList :: [Attribute] -> ShowS

type LensAttribute a = (LensRelevance a, LensQuantity a, LensCohesion a, LensLock a) Source #

(Conjunctive constraint.)

relevanceAttributeTable :: [(String, Relevance)] Source #

Modifiers for Relevance.

quantityAttributeTable :: [(String, Quantity)] Source #

Modifiers for Quantity.

type Attributes = [(Attribute, Range, String)] Source #

Information about attributes (attribute, range, printed representation).

This information is returned by the parser. Code that calls the parser should, if appropriate, complain if support for the given attributes has not been enabled. This can be taken care of by checkAttributes, which should not be called until after pragma options have been set.

lockAttributeTable :: [(String, Lock)] Source #

Modifiers for Quantity.

attributesMap :: Map String Attribute Source #

Concrete syntax for all attributes.

stringToAttribute :: String -> Maybe Attribute Source #

Parsing a string into an attribute.

exprToAttribute :: Expr -> Maybe Attribute Source #

Parsing an expression into an attribute.

setAttribute :: LensAttribute a => Attribute -> a -> a Source #

Setting an attribute (in e.g. an Arg). Overwrites previous value.

setAttributes :: LensAttribute a => [Attribute] -> a -> a Source #

Setting some attributes in left-to-right order. Blindly overwrites previous settings.

Applying attributes only if they have not been set already.

setPristineQuantity :: LensQuantity a => Quantity -> a -> Maybe a Source #

Setting Quantity if unset.

setPristineCohesion :: LensCohesion a => Cohesion -> a -> Maybe a Source #

Setting Cohesion if unset.

setPristineLock :: LensLock a => Lock -> a -> Maybe a Source #

Setting Lock if unset.

setPristineAttribute :: LensAttribute a => Attribute -> a -> Maybe a Source #

Setting an unset attribute (to e.g. an Arg).

setPristineAttributes :: LensAttribute a => [Attribute] -> a -> Maybe a Source #

Setting a list of unset attributes.

Filtering attributes