Agda.Syntax.Concrete.Attribute

Attributes: concrete syntax for ArgInfo, esp. modalities.

Documentation

data Attribute

An attribute is a modifier for ArgInfo.

Constructors

RelevanceAttribute Relevance

QuantityAttribute Quantity

TacticAttribute Expr

CohesionAttribute Cohesion

Instances

Show Attribute

Defined in Agda.Syntax.Concrete.Attribute

Methods

showsPrec :: Int -> Attribute -> ShowS

show :: Attribute -> String

showList :: [Attribute] -> ShowS

KillRange Attribute

Defined in Agda.Syntax.Concrete.Attribute

Methods

killRange :: KillRangeT Attribute

SetRange Attribute

Defined in Agda.Syntax.Concrete.Attribute

Methods

setRange :: Range -> Attribute -> Attribute

HasRange Attribute

Defined in Agda.Syntax.Concrete.Attribute

Methods

getRange :: Attribute -> Range

type LensAttribute a = (LensRelevance a, LensQuantity a, LensCohesion a)

(Conjunctive constraint.)

relevanceAttributeTable :: [(String, Relevance)]

Modifiers for Relevance.

quantityAttributeTable :: [(String, Quantity)]

Modifiers for Quantity.

cohesionAttributeTable :: [(String, Cohesion)]

attributesMap :: Map String Attribute

Concrete syntax for all attributes.

stringToAttribute :: String -> Maybe Attribute

Parsing a string into an attribute.

exprToAttribute :: Expr -> Maybe Attribute

Parsing an expression into an attribute.

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

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

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

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

Applying attributes only if they have not been set already.

setPristineRelevance :: LensRelevance a => Relevance -> a -> Maybe a

Setting Relevance if unset.

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

Setting Quantity if unset.

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

Setting Cohesion if unset.

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

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

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

Setting a list of unset attributes.

Filtering attributes

isRelevanceAttribute :: Attribute -> Maybe Relevance

isQuantityAttribute :: Attribute -> Maybe Quantity

isTacticAttribute :: Attribute -> Maybe Expr

relevanceAttributes :: [Attribute] -> [Attribute]

quantityAttributes :: [Attribute] -> [Attribute]

tacticAttributes :: [Attribute] -> [Attribute]