Agda-2.6.2.1.20220327: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Concrete.Attribute

Description

 
Synopsis

Documentation

type LensAttribute a = (LensRelevance a, LensQuantity a, LensCohesion a, LensLock 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.

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