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

Safe HaskellNone




Attributes: concrete syntax for ArgInfo, esp. modalities.



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

(Conjunctive constraint.)

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.

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