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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Concrete.Attribute

Contents

Description

Attributes: concrete syntax for ArgInfo, esp. modalities.

Synopsis

Documentation

data Attribute Source #

An attribute is a modifier for ArgInfo.

Instances
Eq Attribute Source # 
Instance details

Defined in Agda.Syntax.Concrete.Attribute

Methods

(==) :: Attribute -> Attribute -> Bool

(/=) :: Attribute -> Attribute -> Bool

Ord Attribute Source # 
Instance details

Defined in Agda.Syntax.Concrete.Attribute

Methods

compare :: Attribute -> Attribute -> Ordering

(<) :: Attribute -> Attribute -> Bool

(<=) :: Attribute -> Attribute -> Bool

(>) :: Attribute -> Attribute -> Bool

(>=) :: Attribute -> Attribute -> Bool

max :: Attribute -> Attribute -> Attribute

min :: Attribute -> Attribute -> 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) Source #

(Conjunctive constraint.)

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

Modifiers for Relevance.

quantityAttributeTable :: [(String, Quantity)] 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.

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.

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

Setting Relevance if unset.

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

Setting Quantity 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