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

Agda.Syntax.Common

Description

Some common syntactic entities are defined in this module.

Synopsis

Documentation

type Nat = Int Source #

type Arity = Nat Source #

Delayed

data Delayed Source #

Used to specify whether something should be delayed.

Constructors

Delayed 
NotDelayed 

Instances

Instances details
Eq Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Delayed -> Delayed -> Bool

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

Data Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Delayed -> c Delayed

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Delayed

toConstr :: Delayed -> Constr

dataTypeOf :: Delayed -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Delayed)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Delayed)

gmapT :: (forall b. Data b => b -> b) -> Delayed -> Delayed

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Delayed -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Delayed -> r

gmapQ :: (forall d. Data d => d -> u) -> Delayed -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Delayed -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed

Ord Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Delayed -> Delayed -> Ordering

(<) :: Delayed -> Delayed -> Bool

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

(>) :: Delayed -> Delayed -> Bool

(>=) :: Delayed -> Delayed -> Bool

max :: Delayed -> Delayed -> Delayed

min :: Delayed -> Delayed -> Delayed

Show Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Delayed -> ShowS

show :: Delayed -> String

showList :: [Delayed] -> ShowS

Generic Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Delayed :: Type -> Type

Methods

from :: Delayed -> Rep Delayed x

to :: Rep Delayed x -> Delayed

NFData Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Delayed -> ()

KillRange Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Delayed Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Delayed -> S Int32 Source #

icod_ :: Delayed -> S Int32 Source #

value :: Int32 -> R Delayed Source #

type Rep Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Delayed = D1 ('MetaData "Delayed" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "Delayed" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotDelayed" 'PrefixI 'False) (U1 :: Type -> Type))

File

data FileType Source #

Instances

Instances details
Eq FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: FileType -> FileType -> Bool

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

Data FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FileType -> c FileType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FileType

toConstr :: FileType -> Constr

dataTypeOf :: FileType -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FileType)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FileType)

gmapT :: (forall b. Data b => b -> b) -> FileType -> FileType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FileType -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FileType -> r

gmapQ :: (forall d. Data d => d -> u) -> FileType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> FileType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FileType -> m FileType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FileType -> m FileType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FileType -> m FileType

Ord FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: FileType -> FileType -> Ordering

(<) :: FileType -> FileType -> Bool

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

(>) :: FileType -> FileType -> Bool

(>=) :: FileType -> FileType -> Bool

max :: FileType -> FileType -> FileType

min :: FileType -> FileType -> FileType

Show FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> FileType -> ShowS

show :: FileType -> String

showList :: [FileType] -> ShowS

Generic FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep FileType :: Type -> Type

Methods

from :: FileType -> Rep FileType x

to :: Rep FileType x -> FileType

NFData FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: FileType -> ()

Pretty FileType Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj FileType Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FileType -> S Int32 Source #

icod_ :: FileType -> S Int32 Source #

value :: Int32 -> R FileType Source #

type Rep FileType Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep FileType = D1 ('MetaData "FileType" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) ((C1 ('MetaCons "AgdaFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MdFileType" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RstFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TexFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OrgFileType" 'PrefixI 'False) (U1 :: Type -> Type))))

Agda variants

data Cubical Source #

Variants of Cubical Agda.

Constructors

CErased 
CFull 

Instances

Instances details
Eq Cubical Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Cubical -> Cubical -> Bool

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

Show Cubical Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Cubical -> ShowS

show :: Cubical -> String

showList :: [Cubical] -> ShowS

Generic Cubical Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Cubical :: Type -> Type

Methods

from :: Cubical -> Rep Cubical x

to :: Rep Cubical x -> Cubical

NFData Cubical Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Cubical -> ()

EmbPrj Cubical Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Cubical -> S Int32 Source #

icod_ :: Cubical -> S Int32 Source #

value :: Int32 -> R Cubical Source #

type Rep Cubical Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Cubical = D1 ('MetaData "Cubical" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "CErased" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CFull" 'PrefixI 'False) (U1 :: Type -> Type))

data Language Source #

Agda variants.

Only some variants are tracked.

Constructors

WithoutK 
WithK 
Cubical Cubical 

Instances

Instances details
Eq Language Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Language -> Language -> Bool

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

Show Language Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Language -> ShowS

show :: Language -> String

showList :: [Language] -> ShowS

Generic Language Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Language :: Type -> Type

Methods

from :: Language -> Rep Language x

to :: Rep Language x -> Language

NFData Language Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Language -> ()

KillRange Language Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Language Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Language -> S Int32 Source #

icod_ :: Language -> S Int32 Source #

value :: Int32 -> R Language Source #

type Rep Language Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Language = D1 ('MetaData "Language" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "WithoutK" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WithK" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Cubical" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cubical))))

Record Directives

data RecordDirectives' a Source #

Constructors

RecordDirectives 

Fields

Instances

Instances details
Functor RecordDirectives' Source # 
Instance details

Defined in Agda.Syntax.Common

DeclaredNames RecordDirectives Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Eq a => Eq (RecordDirectives' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Data a => Data (RecordDirectives' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RecordDirectives' a -> c (RecordDirectives' a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RecordDirectives' a)

toConstr :: RecordDirectives' a -> Constr

dataTypeOf :: RecordDirectives' a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RecordDirectives' a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RecordDirectives' a))

gmapT :: (forall b. Data b => b -> b) -> RecordDirectives' a -> RecordDirectives' a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RecordDirectives' a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RecordDirectives' a -> r

gmapQ :: (forall d. Data d => d -> u) -> RecordDirectives' a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> RecordDirectives' a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RecordDirectives' a -> m (RecordDirectives' a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RecordDirectives' a -> m (RecordDirectives' a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RecordDirectives' a -> m (RecordDirectives' a)

Show a => Show (RecordDirectives' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> RecordDirectives' a -> ShowS

show :: RecordDirectives' a -> String

showList :: [RecordDirectives' a] -> ShowS

NFData a => NFData (RecordDirectives' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: RecordDirectives' a -> ()

KillRange a => KillRange (RecordDirectives' a) Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange a => HasRange (RecordDirectives' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Eta-equality

data HasEta' a Source #

Does a record come with eta-equality?

Constructors

YesEta 
NoEta a 

Instances

Instances details
Functor HasEta' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> HasEta' a -> HasEta' b

(<$) :: a -> HasEta' b -> HasEta' a #

Foldable HasEta' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => HasEta' m -> m

foldMap :: Monoid m => (a -> m) -> HasEta' a -> m

foldMap' :: Monoid m => (a -> m) -> HasEta' a -> m

foldr :: (a -> b -> b) -> b -> HasEta' a -> b

foldr' :: (a -> b -> b) -> b -> HasEta' a -> b

foldl :: (b -> a -> b) -> b -> HasEta' a -> b

foldl' :: (b -> a -> b) -> b -> HasEta' a -> b

foldr1 :: (a -> a -> a) -> HasEta' a -> a

foldl1 :: (a -> a -> a) -> HasEta' a -> a

toList :: HasEta' a -> [a]

null :: HasEta' a -> Bool

length :: HasEta' a -> Int

elem :: Eq a => a -> HasEta' a -> Bool

maximum :: Ord a => HasEta' a -> a

minimum :: Ord a => HasEta' a -> a

sum :: Num a => HasEta' a -> a

product :: Num a => HasEta' a -> a

Traversable HasEta' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverse :: Applicative f => (a -> f b) -> HasEta' a -> f (HasEta' b)

sequenceA :: Applicative f => HasEta' (f a) -> f (HasEta' a)

mapM :: Monad m => (a -> m b) -> HasEta' a -> m (HasEta' b)

sequence :: Monad m => HasEta' (m a) -> m (HasEta' a)

CopatternMatchingAllowed HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

PatternMatchingAllowed HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

Eq a => Eq (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: HasEta' a -> HasEta' a -> Bool

(/=) :: HasEta' a -> HasEta' a -> Bool

Data a => Data (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HasEta' a -> c (HasEta' a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (HasEta' a)

toConstr :: HasEta' a -> Constr

dataTypeOf :: HasEta' a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (HasEta' a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (HasEta' a))

gmapT :: (forall b. Data b => b -> b) -> HasEta' a -> HasEta' a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HasEta' a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HasEta' a -> r

gmapQ :: (forall d. Data d => d -> u) -> HasEta' a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> HasEta' a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HasEta' a -> m (HasEta' a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HasEta' a -> m (HasEta' a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HasEta' a -> m (HasEta' a)

Ord a => Ord (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: HasEta' a -> HasEta' a -> Ordering

(<) :: HasEta' a -> HasEta' a -> Bool

(<=) :: HasEta' a -> HasEta' a -> Bool

(>) :: HasEta' a -> HasEta' a -> Bool

(>=) :: HasEta' a -> HasEta' a -> Bool

max :: HasEta' a -> HasEta' a -> HasEta' a

min :: HasEta' a -> HasEta' a -> HasEta' a

Show a => Show (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> HasEta' a -> ShowS

show :: HasEta' a -> String

showList :: [HasEta' a] -> ShowS

NFData a => NFData (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: HasEta' a -> ()

KillRange a => KillRange (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange a => HasRange (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: HasEta' a -> Range Source #

EmbPrj a => EmbPrj (HasEta' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: HasEta' a -> S Int32 Source #

icod_ :: HasEta' a -> S Int32 Source #

value :: Int32 -> R (HasEta' a) Source #

type HasEta = HasEta' PatternOrCopattern Source #

Pattern and copattern matching is allowed in the presence of eta.

In the absence of eta, we have to choose whether we want to allow matching on the constructor or copattern matching with the projections. Having both leads to breakage of subject reduction (issue #4560).

data PatternOrCopattern Source #

For a record without eta, which type of matching do we allow?

Constructors

PatternMatching

Can match on the record constructor.

CopatternMatching

Can copattern match using the projections. (Default.)

Instances

Instances details
Bounded PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

Enum PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

Eq PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

Data PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PatternOrCopattern -> c PatternOrCopattern

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PatternOrCopattern

toConstr :: PatternOrCopattern -> Constr

dataTypeOf :: PatternOrCopattern -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PatternOrCopattern)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatternOrCopattern)

gmapT :: (forall b. Data b => b -> b) -> PatternOrCopattern -> PatternOrCopattern

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PatternOrCopattern -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PatternOrCopattern -> r

gmapQ :: (forall d. Data d => d -> u) -> PatternOrCopattern -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> PatternOrCopattern -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PatternOrCopattern -> m PatternOrCopattern

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PatternOrCopattern -> m PatternOrCopattern

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PatternOrCopattern -> m PatternOrCopattern

Ord PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

Show PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> PatternOrCopattern -> ShowS

show :: PatternOrCopattern -> String

showList :: [PatternOrCopattern] -> ShowS

NFData PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: PatternOrCopattern -> ()

KillRange PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

CopatternMatchingAllowed PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

CopatternMatchingAllowed HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

PatternMatchingAllowed PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

PatternMatchingAllowed HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj PatternOrCopattern Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

class PatternMatchingAllowed a where Source #

Can we pattern match on the record constructor?

Methods

patternMatchingAllowed :: a -> Bool Source #

class CopatternMatchingAllowed a where Source #

Can we construct a record by copattern matching?

Methods

copatternMatchingAllowed :: a -> Bool Source #

Induction

data Induction Source #

Inductive < Coinductive

Constructors

Inductive 
CoInductive 

Instances

Instances details
Eq Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Induction -> Induction -> Bool

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

Data Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Induction -> c Induction

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Induction

toConstr :: Induction -> Constr

dataTypeOf :: Induction -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Induction)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Induction)

gmapT :: (forall b. Data b => b -> b) -> Induction -> Induction

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Induction -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Induction -> r

gmapQ :: (forall d. Data d => d -> u) -> Induction -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Induction -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Induction -> m Induction

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Induction -> m Induction

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Induction -> m Induction

Ord Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Induction -> Induction -> Ordering

(<) :: Induction -> Induction -> Bool

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

(>) :: Induction -> Induction -> Bool

(>=) :: Induction -> Induction -> Bool

max :: Induction -> Induction -> Induction

min :: Induction -> Induction -> Induction

Show Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Induction -> ShowS

show :: Induction -> String

showList :: [Induction] -> ShowS

NFData Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Induction -> ()

Pretty Induction Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

PatternMatchingAllowed Induction Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Induction Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Induction -> S Int32 Source #

icod_ :: Induction -> S Int32 Source #

value :: Int32 -> R Induction Source #

Hiding

data Overlappable Source #

Constructors

YesOverlap 
NoOverlap 

Instances

Instances details
Eq Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Overlappable -> Overlappable -> Bool

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

Data Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Overlappable -> c Overlappable

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Overlappable

toConstr :: Overlappable -> Constr

dataTypeOf :: Overlappable -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Overlappable)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Overlappable)

gmapT :: (forall b. Data b => b -> b) -> Overlappable -> Overlappable

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Overlappable -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Overlappable -> r

gmapQ :: (forall d. Data d => d -> u) -> Overlappable -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Overlappable -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Overlappable -> m Overlappable

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Overlappable -> m Overlappable

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Overlappable -> m Overlappable

Ord Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Show Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Overlappable -> ShowS

show :: Overlappable -> String

showList :: [Overlappable] -> ShowS

Semigroup Overlappable Source #

Just for the Hiding instance. Should never combine different overlapping.

Instance details

Defined in Agda.Syntax.Common

Monoid Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Overlappable -> ()

data Hiding Source #

Instances

Instances details
Eq Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Hiding -> Hiding -> Bool

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

Data Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Hiding -> c Hiding

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Hiding

toConstr :: Hiding -> Constr

dataTypeOf :: Hiding -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Hiding)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Hiding)

gmapT :: (forall b. Data b => b -> b) -> Hiding -> Hiding

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Hiding -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Hiding -> r

gmapQ :: (forall d. Data d => d -> u) -> Hiding -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Hiding -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding

Ord Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Hiding -> Hiding -> Ordering

(<) :: Hiding -> Hiding -> Bool

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

(>) :: Hiding -> Hiding -> Bool

(>=) :: Hiding -> Hiding -> Bool

max :: Hiding -> Hiding -> Hiding

min :: Hiding -> Hiding -> Hiding

Show Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Hiding -> ShowS

show :: Hiding -> String

showList :: [Hiding] -> ShowS

Semigroup Hiding Source #

Hiding is an idempotent partial monoid, with unit NotHidden. Instance and NotHidden are incompatible.

Instance details

Defined in Agda.Syntax.Common

Methods

(<>) :: Hiding -> Hiding -> Hiding #

sconcat :: NonEmpty Hiding -> Hiding

stimes :: Integral b => b -> Hiding -> Hiding

Monoid Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Hiding -> ()

Pretty Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Hiding -> S Int32 Source #

icod_ :: Hiding -> S Int32 Source #

value :: Int32 -> R Hiding Source #

ChooseFlex Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Unquote Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Arg a -> TOM (Hiding, b) Source #

data WithHiding a Source #

Decorating something with Hiding information.

Constructors

WithHiding 

Fields

Instances

Instances details
Functor WithHiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> WithHiding a -> WithHiding b

(<$) :: a -> WithHiding b -> WithHiding a #

Applicative WithHiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pure :: a -> WithHiding a

(<*>) :: WithHiding (a -> b) -> WithHiding a -> WithHiding b #

liftA2 :: (a -> b -> c) -> WithHiding a -> WithHiding b -> WithHiding c

(*>) :: WithHiding a -> WithHiding b -> WithHiding b

(<*) :: WithHiding a -> WithHiding b -> WithHiding a

Foldable WithHiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => WithHiding m -> m

foldMap :: Monoid m => (a -> m) -> WithHiding a -> m

foldMap' :: Monoid m => (a -> m) -> WithHiding a -> m

foldr :: (a -> b -> b) -> b -> WithHiding a -> b

foldr' :: (a -> b -> b) -> b -> WithHiding a -> b

foldl :: (b -> a -> b) -> b -> WithHiding a -> b

foldl' :: (b -> a -> b) -> b -> WithHiding a -> b

foldr1 :: (a -> a -> a) -> WithHiding a -> a

foldl1 :: (a -> a -> a) -> WithHiding a -> a

toList :: WithHiding a -> [a]

null :: WithHiding a -> Bool

length :: WithHiding a -> Int

elem :: Eq a => a -> WithHiding a -> Bool

maximum :: Ord a => WithHiding a -> a

minimum :: Ord a => WithHiding a -> a

sum :: Num a => WithHiding a -> a

product :: Num a => WithHiding a -> a

Traversable WithHiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverse :: Applicative f => (a -> f b) -> WithHiding a -> f (WithHiding b)

sequenceA :: Applicative f => WithHiding (f a) -> f (WithHiding a)

mapM :: Monad m => (a -> m b) -> WithHiding a -> m (WithHiding b)

sequence :: Monad m => WithHiding (m a) -> m (WithHiding a)

Decoration WithHiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverseF :: Functor m => (a -> m b) -> WithHiding a -> m (WithHiding b) Source #

distributeF :: Functor m => WithHiding (m a) -> m (WithHiding a) Source #

Eq a => Eq (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: WithHiding a -> WithHiding a -> Bool

(/=) :: WithHiding a -> WithHiding a -> Bool

Data a => Data (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WithHiding a -> c (WithHiding a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WithHiding a)

toConstr :: WithHiding a -> Constr

dataTypeOf :: WithHiding a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WithHiding a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WithHiding a))

gmapT :: (forall b. Data b => b -> b) -> WithHiding a -> WithHiding a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WithHiding a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WithHiding a -> r

gmapQ :: (forall d. Data d => d -> u) -> WithHiding a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> WithHiding a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> WithHiding a -> m (WithHiding a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WithHiding a -> m (WithHiding a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WithHiding a -> m (WithHiding a)

Ord a => Ord (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: WithHiding a -> WithHiding a -> Ordering

(<) :: WithHiding a -> WithHiding a -> Bool

(<=) :: WithHiding a -> WithHiding a -> Bool

(>) :: WithHiding a -> WithHiding a -> Bool

(>=) :: WithHiding a -> WithHiding a -> Bool

max :: WithHiding a -> WithHiding a -> WithHiding a

min :: WithHiding a -> WithHiding a -> WithHiding a

Show a => Show (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> WithHiding a -> ShowS

show :: WithHiding a -> String

showList :: [WithHiding a] -> ShowS

NFData a => NFData (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: WithHiding a -> ()

Pretty a => Pretty (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange a => KillRange (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange a => SetRange (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange a => HasRange (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

ExprLike a => ExprLike (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> WithHiding a -> WithHiding a Source #

foldExpr :: Monoid m => (Expr -> m) -> WithHiding a -> m Source #

traverseExpr :: Monad m => (Expr -> m Expr) -> WithHiding a -> m (WithHiding a) Source #

Free t => Free (WithHiding t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => WithHiding t -> FreeM a c Source #

Subst a => Subst (WithHiding a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (WithHiding a) Source #

TermLike a => TermLike (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> WithHiding a -> m (WithHiding a) Source #

foldTerm :: Monoid m => (Term -> m) -> WithHiding a -> m Source #

ExprLike a => ExprLike (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

EmbPrj a => EmbPrj (WithHiding a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: WithHiding a -> S Int32 Source #

icod_ :: WithHiding a -> S Int32 Source #

value :: Int32 -> R (WithHiding a) Source #

PrettyTCM a => PrettyTCM (WithHiding a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => WithHiding a -> m Doc Source #

ToConcrete a => ToConcrete (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (WithHiding a) Source #

Normalise t => Normalise (WithHiding t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

ToAbstract c => ToAbstract (WithHiding c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (WithHiding c) Source #

AddContext ([WithHiding Name], Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext (List1 (WithHiding Name), Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

type SubstArg (WithHiding a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type ConOfAbs (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfCon (WithHiding c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

class LensHiding a where Source #

A lens to access the Hiding attribute in data structures. Minimal implementation: getHiding and mapHiding or LensArgInfo.

Minimal complete definition

Nothing

Methods

getHiding :: a -> Hiding Source #

default getHiding :: LensArgInfo a => a -> Hiding Source #

setHiding :: Hiding -> a -> a Source #

mapHiding :: (Hiding -> Hiding) -> a -> a Source #

default mapHiding :: LensArgInfo a => (Hiding -> Hiding) -> a -> a Source #

Instances

Instances details
LensHiding ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

LensHiding (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getHiding :: Arg e -> Hiding Source #

setHiding :: Hiding -> Arg e -> Arg e Source #

mapHiding :: (Hiding -> Hiding) -> Arg e -> Arg e Source #

LensHiding (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

LensHiding a => LensHiding (Named nm a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getHiding :: Named nm a -> Hiding Source #

setHiding :: Hiding -> Named nm a -> Named nm a Source #

mapHiding :: (Hiding -> Hiding) -> Named nm a -> Named nm a Source #

LensHiding (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

getHiding :: Dom' t e -> Hiding Source #

setHiding :: Hiding -> Dom' t e -> Dom' t e Source #

mapHiding :: (Hiding -> Hiding) -> Dom' t e -> Dom' t e Source #

mergeHiding :: LensHiding a => WithHiding a -> a Source #

Monoidal composition of Hiding information in some data.

visible :: LensHiding a => a -> Bool Source #

NotHidden arguments are visible.

notVisible :: LensHiding a => a -> Bool Source #

Instance and Hidden arguments are notVisible.

hidden :: LensHiding a => a -> Bool Source #

Hidden arguments are hidden.

hide :: LensHiding a => a -> a Source #

isOverlappable :: LensHiding a => a -> Bool Source #

isInstance :: LensHiding a => a -> Bool Source #

sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool Source #

Ignores Overlappable.

Modalities

newtype UnderAddition t Source #

Type wrapper to indicate additive monoid/semigroup context.

Constructors

UnderAddition t 

Instances

Instances details
Functor UnderAddition Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> UnderAddition a -> UnderAddition b

(<$) :: a -> UnderAddition b -> UnderAddition a #

Applicative UnderAddition Source # 
Instance details

Defined in Agda.Syntax.Common

Eq t => Eq (UnderAddition t) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: UnderAddition t -> UnderAddition t -> Bool

(/=) :: UnderAddition t -> UnderAddition t -> Bool

Ord t => Ord (UnderAddition t) Source # 
Instance details

Defined in Agda.Syntax.Common

Show t => Show (UnderAddition t) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> UnderAddition t -> ShowS

show :: UnderAddition t -> String

showList :: [UnderAddition t] -> ShowS

Semigroup (UnderAddition Cohesion) Source #

Cohesion forms a semigroup under addition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Modality) Source #

Pointwise addition.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Cohesion) Source #

Squash is the additive unit.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Modality) Source #

Pointwise additive unit.

Instance details

Defined in Agda.Syntax.Common

PartialOrd t => PartialOrd (UnderAddition t) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

newtype UnderComposition t Source #

Type wrapper to indicate composition or multiplicative monoid/semigroup context.

Constructors

UnderComposition t 

Instances

Instances details
Functor UnderComposition Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> UnderComposition a -> UnderComposition b

(<$) :: a -> UnderComposition b -> UnderComposition a #

Applicative UnderComposition Source # 
Instance details

Defined in Agda.Syntax.Common

Eq t => Eq (UnderComposition t) Source # 
Instance details

Defined in Agda.Syntax.Common

Ord t => Ord (UnderComposition t) Source # 
Instance details

Defined in Agda.Syntax.Common

Show t => Show (UnderComposition t) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> UnderComposition t -> ShowS

show :: UnderComposition t -> String

showList :: [UnderComposition t] -> ShowS

Semigroup (UnderComposition Cohesion) Source #

Cohesion forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Relevance) Source #

Relevance forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Erased) Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Quantity) Source #

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Right-biased for origin.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Modality) Source #

Pointwise composition.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Cohesion) Source #

Continous is the multiplicative unit.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Relevance) Source #

Relevant is the unit under composition.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Quantity) Source #

In the absense of finite quantities besides 0, ω is the unit. Otherwise, 1 is the unit.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Modality) Source #

Pointwise composition unit.

Instance details

Defined in Agda.Syntax.Common

PartialOrd t => PartialOrd (UnderComposition t) Source # 
Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid (UnderComposition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid (UnderComposition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid (UnderComposition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid (UnderComposition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

data Modality Source #

We have a tuple of modalities, which might not be fully orthogonal. For instance, irrelevant stuff is also run-time irrelevant.

Constructors

Modality 

Fields

  • modRelevance :: Relevance

    Legacy irrelevance. See Pfenning, LiCS 2001; AbelVezzosiWinterhalter, ICFP 2017.

  • modQuantity :: Quantity

    Cardinality / runtime erasure. See Conor McBride, I got plenty o' nutting, Wadlerfest 2016. See Bob Atkey, Syntax and Semantics of Quantitative Type Theory, LiCS 2018.

  • modCohesion :: Cohesion

    Cohesion/what was in Agda-flat. see "Brouwer's fixed-point theorem in real-cohesive homotopy type theory" (arXiv:1509.07584) Currently only the comonad is implemented.

Instances

Instances details
Eq Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Modality -> Modality -> Bool

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

Data Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Modality -> c Modality

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Modality

toConstr :: Modality -> Constr

dataTypeOf :: Modality -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Modality)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Modality)

gmapT :: (forall b. Data b => b -> b) -> Modality -> Modality

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Modality -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Modality -> r

gmapQ :: (forall d. Data d => d -> u) -> Modality -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Modality -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Modality -> m Modality

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Modality -> m Modality

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Modality -> m Modality

Ord Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Modality -> Modality -> Ordering

(<) :: Modality -> Modality -> Bool

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

(>) :: Modality -> Modality -> Bool

(>=) :: Modality -> Modality -> Bool

max :: Modality -> Modality -> Modality

min :: Modality -> Modality -> Modality

Show Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Modality -> ShowS

show :: Modality -> String

showList :: [Modality] -> ShowS

Generic Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Modality :: Type -> Type

Methods

from :: Modality -> Rep Modality x

to :: Rep Modality x -> Modality

NFData Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Modality -> ()

PartialOrd Modality Source #

Dominance ordering.

Instance details

Defined in Agda.Syntax.Common

Pretty Modality Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Modality Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensCohesion Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality Modality Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Modality Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Modality -> S Int32 Source #

icod_ :: Modality -> S Int32 Source #

value :: Int32 -> R Modality Source #

PrettyTCM Modality Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Unquote Modality Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

IsVarSet () AllowedVar Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Semigroup (UnderComposition Modality) Source #

Pointwise composition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Modality) Source #

Pointwise addition.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Modality) Source #

Pointwise composition unit.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Modality) Source #

Pointwise additive unit.

Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid (UnderComposition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Modality Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Modality = D1 ('MetaData "Modality" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "Modality" 'PrefixI 'True) (S1 ('MetaSel ('Just "modRelevance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Relevance) :*: (S1 ('MetaSel ('Just "modQuantity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Quantity) :*: S1 ('MetaSel ('Just "modCohesion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cohesion))))

moreUsableModality :: Modality -> Modality -> Bool Source #

m moreUsableModality m' means that an m can be used where ever an m' is required.

composeModality :: Modality -> Modality -> Modality Source #

Multiplicative monoid (standard monoid).

applyModality :: LensModality a => Modality -> a -> a Source #

Compose with modality flag from the left. This function is e.g. used to update the modality information on pattern variables a after a match against something of modality q.

inverseComposeModality :: Modality -> Modality -> Modality Source #

inverseComposeModality r x returns the least modality y such that forall x, y we have x `moreUsableModality` (r `composeModality` y) iff (r `inverseComposeModality` x) `moreUsableModality` y (Galois connection).

inverseApplyModalityButNotQuantity :: LensModality a => Modality -> a -> a Source #

Left division by a Modality. Used e.g. to modify context when going into a m argument.

Note that this function does not change quantities.

addModality :: Modality -> Modality -> Modality Source #

Modality forms a pointwise additive monoid.

zeroModality :: Modality Source #

Identity under addition

unitModality :: Modality Source #

Identity under composition

topModality :: Modality Source #

Absorptive element under addition.

defaultModality :: Modality Source #

The default Modality Beware that this is neither the additive unit nor the unit under composition, because the default quantity is ω.

sameModality :: (LensModality a, LensModality b) => a -> b -> Bool Source #

Equality ignoring origin.

class LensModality a where Source #

Minimal complete definition

Nothing

Methods

getModality :: a -> Modality Source #

default getModality :: LensArgInfo a => a -> Modality Source #

setModality :: Modality -> a -> a Source #

mapModality :: (Modality -> Modality) -> a -> a Source #

default mapModality :: LensArgInfo a => (Modality -> Modality) -> a -> a Source #

Instances

Instances details
LensModality ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality MetaInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality MetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality (VarOcc' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

LensModality (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

LensModality (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

getModality :: Dom' t e -> Modality Source #

setModality :: Modality -> Dom' t e -> Dom' t e Source #

mapModality :: (Modality -> Modality) -> Dom' t e -> Dom' t e Source #

LensModality (FreeEnv' a b c) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Quantities

Quantity origin.

data Q0Origin Source #

Origin of Quantity0.

Constructors

Q0Inferred

User wrote nothing.

Q0 Range

User wrote "@0".

Q0Erased Range

User wrote "@erased".

Instances

Instances details
Eq Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Q0Origin -> Q0Origin -> Bool

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

Data Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Q0Origin -> c Q0Origin

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Q0Origin

toConstr :: Q0Origin -> Constr

dataTypeOf :: Q0Origin -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Q0Origin)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Q0Origin)

gmapT :: (forall b. Data b => b -> b) -> Q0Origin -> Q0Origin

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Q0Origin -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Q0Origin -> r

gmapQ :: (forall d. Data d => d -> u) -> Q0Origin -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Q0Origin -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Q0Origin -> m Q0Origin

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Q0Origin -> m Q0Origin

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Q0Origin -> m Q0Origin

Ord Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Q0Origin -> Q0Origin -> Ordering

(<) :: Q0Origin -> Q0Origin -> Bool

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

(>) :: Q0Origin -> Q0Origin -> Bool

(>=) :: Q0Origin -> Q0Origin -> Bool

max :: Q0Origin -> Q0Origin -> Q0Origin

min :: Q0Origin -> Q0Origin -> Q0Origin

Show Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Q0Origin -> ShowS

show :: Q0Origin -> String

showList :: [Q0Origin] -> ShowS

Generic Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Q0Origin :: Type -> Type

Methods

from :: Q0Origin -> Rep Q0Origin x

to :: Rep Q0Origin x -> Q0Origin

Semigroup Q0Origin Source #

Right-biased composition, because the left quantity acts as context, and the right one as occurrence.

Instance details

Defined in Agda.Syntax.Common

Methods

(<>) :: Q0Origin -> Q0Origin -> Q0Origin #

sconcat :: NonEmpty Q0Origin -> Q0Origin

stimes :: Integral b => b -> Q0Origin -> Q0Origin

Monoid Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Q0Origin -> ()

Null Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

empty :: Q0Origin Source #

null :: Q0Origin -> Bool Source #

Pretty Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Q0Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Q0Origin -> S Int32 Source #

icod_ :: Q0Origin -> S Int32 Source #

value :: Int32 -> R Q0Origin Source #

type Rep Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Q0Origin = D1 ('MetaData "Q0Origin" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "Q0Inferred" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Q0" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Q0Erased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data Q1Origin Source #

Origin of Quantity1.

Constructors

Q1Inferred

User wrote nothing.

Q1 Range

User wrote "@1".

Q1Linear Range

User wrote "@linear".

Instances

Instances details
Eq Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Q1Origin -> Q1Origin -> Bool

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

Data Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Q1Origin -> c Q1Origin

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Q1Origin

toConstr :: Q1Origin -> Constr

dataTypeOf :: Q1Origin -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Q1Origin)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Q1Origin)

gmapT :: (forall b. Data b => b -> b) -> Q1Origin -> Q1Origin

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Q1Origin -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Q1Origin -> r

gmapQ :: (forall d. Data d => d -> u) -> Q1Origin -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Q1Origin -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Q1Origin -> m Q1Origin

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Q1Origin -> m Q1Origin

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Q1Origin -> m Q1Origin

Ord Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Q1Origin -> Q1Origin -> Ordering

(<) :: Q1Origin -> Q1Origin -> Bool

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

(>) :: Q1Origin -> Q1Origin -> Bool

(>=) :: Q1Origin -> Q1Origin -> Bool

max :: Q1Origin -> Q1Origin -> Q1Origin

min :: Q1Origin -> Q1Origin -> Q1Origin

Show Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Q1Origin -> ShowS

show :: Q1Origin -> String

showList :: [Q1Origin] -> ShowS

Generic Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Q1Origin :: Type -> Type

Methods

from :: Q1Origin -> Rep Q1Origin x

to :: Rep Q1Origin x -> Q1Origin

Semigroup Q1Origin Source #

Right-biased composition, because the left quantity acts as context, and the right one as occurrence.

Instance details

Defined in Agda.Syntax.Common

Methods

(<>) :: Q1Origin -> Q1Origin -> Q1Origin #

sconcat :: NonEmpty Q1Origin -> Q1Origin

stimes :: Integral b => b -> Q1Origin -> Q1Origin

Monoid Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Q1Origin -> ()

Null Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

empty :: Q1Origin Source #

null :: Q1Origin -> Bool Source #

Pretty Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Q1Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Q1Origin -> S Int32 Source #

icod_ :: Q1Origin -> S Int32 Source #

value :: Int32 -> R Q1Origin Source #

type Rep Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Q1Origin = D1 ('MetaData "Q1Origin" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "Q1Inferred" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Q1" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Q1Linear" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data QωOrigin Source #

Origin of Quantityω.

Constructors

QωInferred

User wrote nothing.

Range

User wrote "@ω".

QωPlenty Range

User wrote "@plenty".

Instances

Instances details
Eq QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: QωOrigin -> QωOrigin -> Bool

(/=) :: QωOrigin -> QωOrigin -> Bool

Data QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QωOrigin -> c QωOrigin

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QωOrigin

toConstr :: QωOrigin -> Constr

dataTypeOf :: QωOrigin -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QωOrigin)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QωOrigin)

gmapT :: (forall b. Data b => b -> b) -> QωOrigin -> QωOrigin

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QωOrigin -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QωOrigin -> r

gmapQ :: (forall d. Data d => d -> u) -> QωOrigin -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> QωOrigin -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> QωOrigin -> m QωOrigin

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QωOrigin -> m QωOrigin

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QωOrigin -> m QωOrigin

Ord QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: QωOrigin -> QωOrigin -> Ordering

(<) :: QωOrigin -> QωOrigin -> Bool

(<=) :: QωOrigin -> QωOrigin -> Bool

(>) :: QωOrigin -> QωOrigin -> Bool

(>=) :: QωOrigin -> QωOrigin -> Bool

max :: QωOrigin -> QωOrigin -> QωOrigin

min :: QωOrigin -> QωOrigin -> QωOrigin

Show QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> QωOrigin -> ShowS

show :: QωOrigin -> String

showList :: [QωOrigin] -> ShowS

Generic QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep QωOrigin :: Type -> Type

Methods

from :: QωOrigin -> Rep QωOrigin x

to :: Rep QωOrigin x -> QωOrigin

Semigroup QωOrigin Source #

Right-biased composition, because the left quantity acts as context, and the right one as occurrence.

Instance details

Defined in Agda.Syntax.Common

Methods

(<>) :: QωOrigin -> QωOrigin -> QωOrigin #

sconcat :: NonEmpty QωOrigin -> QωOrigin

stimes :: Integral b => b -> QωOrigin -> QωOrigin

Monoid QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

NFData QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: QωOrigin -> ()

Null QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj QωOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QωOrigin -> S Int32 Source #

icod_ :: QωOrigin -> S Int32 Source #

value :: Int32 -> R QωOrigin Source #

type Rep QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep QωOrigin = D1 ('MetaData "Q\969Origin" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "Q\969Inferred" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Q\969" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Q\969Plenty" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

Instances for Q0Origin.

Instances for Q1Origin.

Instances for QωOrigin.

Quantity.

data Quantity Source #

Quantity for linearity.

A quantity is a set of natural numbers, indicating possible semantic uses of a variable. A singleton set {n} requires that the corresponding variable is used exactly n times.

Constructors

Quantity0 Q0Origin

Zero uses {0}, erased at runtime.

Quantity1 Q1Origin

Linear use {1} (could be updated destructively). Mostly TODO (needs postponable constraints between quantities to compute uses).

Quantityω QωOrigin

Unrestricted use .

Instances

Instances details
Eq Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Quantity -> Quantity -> Bool

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

Data Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Quantity -> c Quantity

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quantity

toConstr :: Quantity -> Constr

dataTypeOf :: Quantity -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Quantity)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quantity)

gmapT :: (forall b. Data b => b -> b) -> Quantity -> Quantity

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quantity -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quantity -> r

gmapQ :: (forall d. Data d => d -> u) -> Quantity -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Quantity -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity

Ord Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Quantity -> Quantity -> Ordering

(<) :: Quantity -> Quantity -> Bool

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

(>) :: Quantity -> Quantity -> Bool

(>=) :: Quantity -> Quantity -> Bool

max :: Quantity -> Quantity -> Quantity

min :: Quantity -> Quantity -> Quantity

Show Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Quantity -> ShowS

show :: Quantity -> String

showList :: [Quantity] -> ShowS

Generic Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Quantity :: Type -> Type

Methods

from :: Quantity -> Rep Quantity x

to :: Rep Quantity x -> Quantity

NFData Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Quantity -> ()

PartialOrd Quantity Source #

Note that the order is ω ≤ 0,1, more options is smaller.

Instance details

Defined in Agda.Syntax.Common

Pretty Quantity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Quantity -> S Int32 Source #

icod_ :: Quantity -> S Int32 Source #

value :: Int32 -> R Quantity Source #

PrettyTCM Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Unquote Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Semigroup (UnderComposition Quantity) Source #

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Right-biased for origin.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Quantity) Source #

In the absense of finite quantities besides 0, ω is the unit. Otherwise, 1 is the unit.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid (UnderComposition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Quantity = D1 ('MetaData "Quantity" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "Quantity0" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Q0Origin)) :+: (C1 ('MetaCons "Quantity1" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Q1Origin)) :+: C1 ('MetaCons "Quantity\969" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QωOrigin))))

sameQuantity :: Quantity -> Quantity -> Bool Source #

Equality ignoring origin.

addQuantity :: Quantity -> Quantity -> Quantity Source #

Quantity forms an additive monoid with zero Quantity0.

zeroQuantity :: Quantity Source #

Identity element under addition

defaultQuantity :: Quantity Source #

Absorptive element! This differs from Relevance and Cohesion whose default is the multiplicative unit.

unitQuantity :: Quantity Source #

Identity element under composition

topQuantity :: Quantity Source #

Absorptive element is ω.

moreQuantity :: Quantity -> Quantity -> Bool Source #

m moreUsableQuantity m' means that an m can be used where ever an m' is required.

composeQuantity :: Quantity -> Quantity -> Quantity Source #

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Right-biased for origin.

applyQuantity :: LensQuantity a => Quantity -> a -> a Source #

Compose with quantity flag from the left. This function is e.g. used to update the quantity information on pattern variables a after a match against something of quantity q.

inverseComposeQuantity :: Quantity -> Quantity -> Quantity Source #

inverseComposeQuantity r x returns the least quantity y such that forall x, y we have x `moreQuantity` (r `composeQuantity` y) iff (r `inverseComposeQuantity` x) `moreQuantity` y (Galois connection).

inverseApplyQuantity :: LensQuantity a => Quantity -> a -> a Source #

Left division by a Quantity. Used e.g. to modify context when going into a q argument.

hasQuantity0 :: LensQuantity a => a -> Bool Source #

Check for Quantity0.

hasQuantity1 :: LensQuantity a => a -> Bool Source #

Check for Quantity1.

hasQuantityω :: LensQuantity a => a -> Bool Source #

Check for Quantityω.

noUserQuantity :: LensQuantity a => a -> Bool Source #

Did the user supply a quantity annotation?

usableQuantity :: LensQuantity a => a -> Bool Source #

A thing of quantity 0 is unusable, all others are usable.

class LensQuantity a where Source #

Minimal complete definition

Nothing

Methods

getQuantity :: a -> Quantity Source #

setQuantity :: Quantity -> a -> a Source #

mapQuantity :: (Quantity -> Quantity) -> a -> a Source #

default mapQuantity :: LensModality a => (Quantity -> Quantity) -> a -> a Source #

Instances

Instances details
LensQuantity ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity MetaInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity MetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity (VarOcc' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

LensQuantity (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

getQuantity :: Dom' t e -> Quantity Source #

setQuantity :: Quantity -> Dom' t e -> Dom' t e Source #

mapQuantity :: (Quantity -> Quantity) -> Dom' t e -> Dom' t e Source #

LensQuantity (FreeEnv' a b c) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Erased.

data Erased Source #

A special case of Quantity: erased or not.

Instances

Instances details
Eq Erased Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Erased -> Erased -> Bool

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

Data Erased Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Erased -> c Erased

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Erased

toConstr :: Erased -> Constr

dataTypeOf :: Erased -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Erased)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Erased)

gmapT :: (forall b. Data b => b -> b) -> Erased -> Erased

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Erased -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Erased -> r

gmapQ :: (forall d. Data d => d -> u) -> Erased -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Erased -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Erased -> m Erased

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Erased -> m Erased

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Erased -> m Erased

Show Erased Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Erased -> ShowS

show :: Erased -> String

showList :: [Erased] -> ShowS

Generic Erased Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Erased :: Type -> Type

Methods

from :: Erased -> Rep Erased x

to :: Rep Erased x -> Erased

NFData Erased Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Erased -> ()

KillRange Erased Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Erased Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Erased) Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Erased Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Erased = D1 ('MetaData "Erased" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "Erased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Q0Origin)) :+: C1 ('MetaCons "NotErased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QωOrigin)))

defaultErased :: Erased Source #

The default value of type Erased: not erased.

asQuantity :: Erased -> Quantity Source #

Erased can be embedded into Quantity.

erasedFromQuantity :: Quantity -> Maybe Erased Source #

Quantity can be projected onto Erased.

sameErased :: Erased -> Erased -> Bool Source #

Equality ignoring origin.

isErased :: Erased -> Bool Source #

Is the value "erased"?

composeErased :: Erased -> Erased -> Erased Source #

Composition of values of type Erased.

Erased is dominant. NotErased is neutral.

Right-biased for the origin.

Relevance

data Relevance Source #

A function argument can be relevant or irrelevant. See Agda.TypeChecking.Irrelevance.

Constructors

Relevant

The argument is (possibly) relevant at compile-time.

NonStrict

The argument may never flow into evaluation position. Therefore, it is irrelevant at run-time. It is treated relevantly during equality checking.

Irrelevant

The argument is irrelevant at compile- and runtime.

Instances

Instances details
Bounded Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Enum Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Eq Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Relevance -> Relevance -> Bool

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

Data Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Relevance -> c Relevance

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Relevance

toConstr :: Relevance -> Constr

dataTypeOf :: Relevance -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Relevance)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Relevance)

gmapT :: (forall b. Data b => b -> b) -> Relevance -> Relevance

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Relevance -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Relevance -> r

gmapQ :: (forall d. Data d => d -> u) -> Relevance -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Relevance -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Relevance -> m Relevance

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Relevance -> m Relevance

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Relevance -> m Relevance

Ord Relevance Source #

More relevant is smaller.

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Relevance -> Relevance -> Ordering

(<) :: Relevance -> Relevance -> Bool

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

(>) :: Relevance -> Relevance -> Bool

(>=) :: Relevance -> Relevance -> Bool

max :: Relevance -> Relevance -> Relevance

min :: Relevance -> Relevance -> Relevance

Show Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Relevance -> ShowS

show :: Relevance -> String

showList :: [Relevance] -> ShowS

Generic Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Relevance :: Type -> Type

Methods

from :: Relevance -> Rep Relevance x

to :: Rep Relevance x -> Relevance

NFData Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Relevance -> ()

PartialOrd Relevance Source #

More relevant is smaller.

Instance details

Defined in Agda.Syntax.Common

Pretty Relevance Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Relevance -> S Int32 Source #

icod_ :: Relevance -> S Int32 Source #

value :: Int32 -> R Relevance Source #

PrettyTCM Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Unquote Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Semigroup (UnderComposition Relevance) Source #

Relevance forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Relevance) Source #

Relevant is the unit under composition.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid (UnderComposition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Relevance = D1 ('MetaData "Relevance" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "Relevant" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NonStrict" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Irrelevant" 'PrefixI 'False) (U1 :: Type -> Type)))

class LensRelevance a where Source #

A lens to access the Relevance attribute in data structures. Minimal implementation: getRelevance and mapRelevance or LensModality.

Minimal complete definition

Nothing

Instances

Instances details
LensRelevance ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensRelevance TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensRelevance Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensRelevance (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance (VarOcc' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

LensRelevance (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

LensRelevance (FreeEnv' a b c) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

isRelevant :: LensRelevance a => a -> Bool Source #

isNonStrict :: LensRelevance a => a -> Bool Source #

moreRelevant :: Relevance -> Relevance -> Bool Source #

Information ordering. Relevant `moreRelevant` NonStrict `moreRelevant` Irrelevant

sameRelevance :: Relevance -> Relevance -> Bool Source #

Equality ignoring origin.

usableRelevance :: LensRelevance a => a -> Bool Source #

usableRelevance rel == False iff we cannot use a variable of rel.

composeRelevance :: Relevance -> Relevance -> Relevance Source #

Relevance composition. Irrelevant is dominant, Relevant is neutral. Composition coincides with max.

applyRelevance :: LensRelevance a => Relevance -> a -> a Source #

Compose with relevance flag from the left. This function is e.g. used to update the relevance information on pattern variables a after a match against something rel.

inverseComposeRelevance :: Relevance -> Relevance -> Relevance Source #

inverseComposeRelevance r x returns the most irrelevant y such that forall x, y we have x `moreRelevant` (r `composeRelevance` y) iff (r `inverseComposeRelevance` x) `moreRelevant` y (Galois connection).

inverseApplyRelevance :: LensRelevance a => Relevance -> a -> a Source #

Left division by a Relevance. Used e.g. to modify context when going into a rel argument.

addRelevance :: Relevance -> Relevance -> Relevance Source #

Combine inferred Relevance. The unit is Irrelevant.

zeroRelevance :: Relevance Source #

Relevance forms a monoid under addition, and even a semiring.

unitRelevance :: Relevance Source #

Identity element under composition

topRelevance :: Relevance Source #

Absorptive element under addition.

defaultRelevance :: Relevance Source #

Default Relevance is the identity element under composition

irrToNonStrict :: Relevance -> Relevance Source #

Irrelevant function arguments may appear non-strictly in the codomain type.

nonStrictToRel :: Relevance -> Relevance Source #

Applied when working on types (unless --experimental-irrelevance).

Annotations

data Annotation Source #

We have a tuple of annotations, which might not be fully orthogonal.

Constructors

Annotation 

Fields

  • annLock :: Lock

    Fitch-style dependent right adjoints. See Modal Dependent Type Theory and Dependent Right Adjoints, arXiv:1804.05236.

Instances

Instances details
Eq Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Annotation -> Annotation -> Bool

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

Data Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Annotation -> c Annotation

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Annotation

toConstr :: Annotation -> Constr

dataTypeOf :: Annotation -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Annotation)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annotation)

gmapT :: (forall b. Data b => b -> b) -> Annotation -> Annotation

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annotation -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annotation -> r

gmapQ :: (forall d. Data d => d -> u) -> Annotation -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Annotation -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Annotation -> m Annotation

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotation -> m Annotation

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotation -> m Annotation

Ord Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

Show Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Annotation -> ShowS

show :: Annotation -> String

showList :: [Annotation] -> ShowS

Generic Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Annotation :: Type -> Type

Methods

from :: Annotation -> Rep Annotation x

to :: Rep Annotation x -> Annotation

NFData Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Annotation -> ()

KillRange Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

LensAnnotation Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Annotation Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Annotation -> S Int32 Source #

icod_ :: Annotation -> S Int32 Source #

value :: Int32 -> R Annotation Source #

type Rep Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Annotation = D1 ('MetaData "Annotation" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "Annotation" 'PrefixI 'True) (S1 ('MetaSel ('Just "annLock") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Lock)))

Locks

data Lock Source #

Constructors

IsNotLock 
IsLock

In the future there might be different kinds of them. For now we assume lock weakening.

Instances

Instances details
Bounded Lock Source # 
Instance details

Defined in Agda.Syntax.Common

Enum Lock Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

succ :: Lock -> Lock

pred :: Lock -> Lock

toEnum :: Int -> Lock

fromEnum :: Lock -> Int

enumFrom :: Lock -> [Lock]

enumFromThen :: Lock -> Lock -> [Lock]

enumFromTo :: Lock -> Lock -> [Lock]

enumFromThenTo :: Lock -> Lock -> Lock -> [Lock]

Eq Lock Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Lock -> Lock -> Bool

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

Data Lock Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Lock -> c Lock

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Lock

toConstr :: Lock -> Constr

dataTypeOf :: Lock -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Lock)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Lock)

gmapT :: (forall b. Data b => b -> b) -> Lock -> Lock

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Lock -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Lock -> r

gmapQ :: (forall d. Data d => d -> u) -> Lock -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Lock -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Lock -> m Lock

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Lock -> m Lock

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Lock -> m Lock

Ord Lock Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Lock -> Lock -> Ordering

(<) :: Lock -> Lock -> Bool

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

(>) :: Lock -> Lock -> Bool

(>=) :: Lock -> Lock -> Bool

max :: Lock -> Lock -> Lock

min :: Lock -> Lock -> Lock

Show Lock Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Lock -> ShowS

show :: Lock -> String

showList :: [Lock] -> ShowS

Generic Lock Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Lock :: Type -> Type

Methods

from :: Lock -> Rep Lock x

to :: Rep Lock x -> Lock

NFData Lock Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Lock -> ()

LensLock Lock Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Lock Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Lock -> S Int32 Source #

icod_ :: Lock -> S Int32 Source #

value :: Int32 -> R Lock Source #

type Rep Lock Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Lock = D1 ('MetaData "Lock" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "IsNotLock" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsLock" 'PrefixI 'False) (U1 :: Type -> Type))

class LensLock a where Source #

Minimal complete definition

getLock

Methods

getLock :: a -> Lock Source #

setLock :: Lock -> a -> a Source #

mapLock :: (Lock -> Lock) -> a -> a Source #

Instances

Instances details
LensLock ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensLock Lock Source # 
Instance details

Defined in Agda.Syntax.Common

LensLock (Arg t) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getLock :: Arg t -> Lock Source #

setLock :: Lock -> Arg t -> Arg t Source #

mapLock :: (Lock -> Lock) -> Arg t -> Arg t Source #

Cohesion

data Cohesion Source #

Cohesion modalities see "Brouwer's fixed-point theorem in real-cohesive homotopy type theory" (arXiv:1509.07584) types are now given an additional topological layer which the modalities interact with.

Constructors

Flat

same points, discrete topology, idempotent comonad, box-like.

Continuous

identity modality. | Sharp -- ^ same points, codiscrete topology, idempotent monad, diamond-like.

Squash

single point space, artificially added for Flat left-composition.

Instances

Instances details
Bounded Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Enum Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Eq Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Cohesion -> Cohesion -> Bool

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

Data Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Cohesion -> c Cohesion

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Cohesion

toConstr :: Cohesion -> Constr

dataTypeOf :: Cohesion -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Cohesion)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Cohesion)

gmapT :: (forall b. Data b => b -> b) -> Cohesion -> Cohesion

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Cohesion -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Cohesion -> r

gmapQ :: (forall d. Data d => d -> u) -> Cohesion -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Cohesion -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Cohesion -> m Cohesion

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Cohesion -> m Cohesion

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Cohesion -> m Cohesion

Ord Cohesion Source #

Order is given by implication: flatter is smaller.

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Cohesion -> Cohesion -> Ordering

(<) :: Cohesion -> Cohesion -> Bool

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

(>) :: Cohesion -> Cohesion -> Bool

(>=) :: Cohesion -> Cohesion -> Bool

max :: Cohesion -> Cohesion -> Cohesion

min :: Cohesion -> Cohesion -> Cohesion

Show Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Cohesion -> ShowS

show :: Cohesion -> String

showList :: [Cohesion] -> ShowS

Generic Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Cohesion :: Type -> Type

Methods

from :: Cohesion -> Rep Cohesion x

to :: Rep Cohesion x -> Cohesion

NFData Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Cohesion -> ()

PartialOrd Cohesion Source #

Flatter is smaller.

Instance details

Defined in Agda.Syntax.Common

Pretty Cohesion Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

LensCohesion Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Cohesion Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Cohesion -> S Int32 Source #

icod_ :: Cohesion -> S Int32 Source #

value :: Int32 -> R Cohesion Source #

Semigroup (UnderComposition Cohesion) Source #

Cohesion forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Cohesion) Source #

Cohesion forms a semigroup under addition.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Cohesion) Source #

Continous is the multiplicative unit.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Cohesion) Source #

Squash is the additive unit.

Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid (UnderComposition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Cohesion = D1 ('MetaData "Cohesion" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "Flat" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Continuous" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Squash" 'PrefixI 'False) (U1 :: Type -> Type)))

class LensCohesion a where Source #

A lens to access the Cohesion attribute in data structures. Minimal implementation: getCohesion and mapCohesion or LensModality.

Minimal complete definition

Nothing

Methods

getCohesion :: a -> Cohesion Source #

setCohesion :: Cohesion -> a -> a Source #

mapCohesion :: (Cohesion -> Cohesion) -> a -> a Source #

default mapCohesion :: LensModality a => (Cohesion -> Cohesion) -> a -> a Source #

moreCohesion :: Cohesion -> Cohesion -> Bool Source #

Information ordering. Flat `moreCohesion` Continuous `moreCohesion` Sharp `moreCohesion` Squash

sameCohesion :: Cohesion -> Cohesion -> Bool Source #

Equality ignoring origin.

usableCohesion :: LensCohesion a => a -> Bool Source #

usableCohesion rel == False iff we cannot use a variable of rel.

composeCohesion :: Cohesion -> Cohesion -> Cohesion Source #

Cohesion composition. Squash is dominant, Continuous is neutral.

applyCohesion :: LensCohesion a => Cohesion -> a -> a Source #

Compose with cohesion flag from the left. This function is e.g. used to update the cohesion information on pattern variables a after a match against something of cohesion rel.

inverseComposeCohesion :: Cohesion -> Cohesion -> Cohesion Source #

inverseComposeCohesion r x returns the least y such that forall x, y we have x `moreCohesion` (r `composeCohesion` y) iff (r `inverseComposeCohesion` x) `moreCohesion` y (Galois connection). The above law fails for r = Squash.

inverseApplyCohesion :: LensCohesion a => Cohesion -> a -> a Source #

Left division by a Cohesion. Used e.g. to modify context when going into a rel argument.

addCohesion :: Cohesion -> Cohesion -> Cohesion Source #

Combine inferred Cohesion. The unit is Squash.

zeroCohesion :: Cohesion Source #

Cohesion forms a monoid under addition, and even a semiring.

unitCohesion :: Cohesion Source #

Identity under composition

topCohesion :: Cohesion Source #

Absorptive element under addition.

defaultCohesion :: Cohesion Source #

Default Cohesion is the identity element under composition

Origin of arguments (user-written, inserted or reflected)

data Origin Source #

Origin of arguments.

Constructors

UserWritten

From the source file / user input. (Preserve!)

Inserted

E.g. inserted hidden arguments.

Reflected

Produced by the reflection machinery.

CaseSplit

Produced by an interactive case split.

Substitution

Named application produced to represent a substitution. E.g. "?0 (x = n)" instead of "?0 n"

Instances

Instances details
Eq Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Origin -> Origin -> Bool

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

Data Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Origin -> c Origin

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Origin

toConstr :: Origin -> Constr

dataTypeOf :: Origin -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Origin)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Origin)

gmapT :: (forall b. Data b => b -> b) -> Origin -> Origin

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Origin -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Origin -> r

gmapQ :: (forall d. Data d => d -> u) -> Origin -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Origin -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Origin -> m Origin

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Origin -> m Origin

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Origin -> m Origin

Ord Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Origin -> Origin -> Ordering

(<) :: Origin -> Origin -> Bool

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

(>) :: Origin -> Origin -> Bool

(>=) :: Origin -> Origin -> Bool

max :: Origin -> Origin -> Origin

min :: Origin -> Origin -> Origin

Show Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Origin -> ShowS

show :: Origin -> String

showList :: [Origin] -> ShowS

NFData Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Origin -> ()

KillRange Origin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Origin Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin Origin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Origin -> S Int32 Source #

icod_ :: Origin -> S Int32 Source #

value :: Int32 -> R Origin Source #

ChooseFlex Origin Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

data WithOrigin a Source #

Decorating something with Origin information.

Constructors

WithOrigin 

Fields

Instances

Instances details
Functor WithOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> WithOrigin a -> WithOrigin b

(<$) :: a -> WithOrigin b -> WithOrigin a #

Foldable WithOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => WithOrigin m -> m

foldMap :: Monoid m => (a -> m) -> WithOrigin a -> m

foldMap' :: Monoid m => (a -> m) -> WithOrigin a -> m

foldr :: (a -> b -> b) -> b -> WithOrigin a -> b

foldr' :: (a -> b -> b) -> b -> WithOrigin a -> b

foldl :: (b -> a -> b) -> b -> WithOrigin a -> b

foldl' :: (b -> a -> b) -> b -> WithOrigin a -> b

foldr1 :: (a -> a -> a) -> WithOrigin a -> a

foldl1 :: (a -> a -> a) -> WithOrigin a -> a

toList :: WithOrigin a -> [a]

null :: WithOrigin a -> Bool

length :: WithOrigin a -> Int

elem :: Eq a => a -> WithOrigin a -> Bool

maximum :: Ord a => WithOrigin a -> a

minimum :: Ord a => WithOrigin a -> a

sum :: Num a => WithOrigin a -> a

product :: Num a => WithOrigin a -> a

Traversable WithOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverse :: Applicative f => (a -> f b) -> WithOrigin a -> f (WithOrigin b)

sequenceA :: Applicative f => WithOrigin (f a) -> f (WithOrigin a)

mapM :: Monad m => (a -> m b) -> WithOrigin a -> m (WithOrigin b)

sequence :: Monad m => WithOrigin (m a) -> m (WithOrigin a)

Decoration WithOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverseF :: Functor m => (a -> m b) -> WithOrigin a -> m (WithOrigin b) Source #

distributeF :: Functor m => WithOrigin (m a) -> m (WithOrigin a) Source #

MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #

MapNamedArgPattern a (NamedArg (Pattern' a)) Source #

Modify the content of VarP, and the closest surrounding NamedArg.

Note: the mapNamedArg for Pattern' is not expressible simply by fmap or traverse etc., since ConP has NamedArg subpatterns, which are taken into account by mapNamedArg.

Instance details

Defined in Agda.Syntax.Internal.Pattern

Eq a => Eq (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: WithOrigin a -> WithOrigin a -> Bool

(/=) :: WithOrigin a -> WithOrigin a -> Bool

Data a => Data (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WithOrigin a -> c (WithOrigin a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WithOrigin a)

toConstr :: WithOrigin a -> Constr

dataTypeOf :: WithOrigin a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WithOrigin a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WithOrigin a))

gmapT :: (forall b. Data b => b -> b) -> WithOrigin a -> WithOrigin a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WithOrigin a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WithOrigin a -> r

gmapQ :: (forall d. Data d => d -> u) -> WithOrigin a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> WithOrigin a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> WithOrigin a -> m (WithOrigin a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WithOrigin a -> m (WithOrigin a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WithOrigin a -> m (WithOrigin a)

Ord a => Ord (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: WithOrigin a -> WithOrigin a -> Ordering

(<) :: WithOrigin a -> WithOrigin a -> Bool

(<=) :: WithOrigin a -> WithOrigin a -> Bool

(>) :: WithOrigin a -> WithOrigin a -> Bool

(>=) :: WithOrigin a -> WithOrigin a -> Bool

max :: WithOrigin a -> WithOrigin a -> WithOrigin a

min :: WithOrigin a -> WithOrigin a -> WithOrigin a

Show a => Show (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> WithOrigin a -> ShowS

show :: WithOrigin a -> String

showList :: [WithOrigin a] -> ShowS

NFData a => NFData (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: WithOrigin a -> ()

Pretty e => Pretty (Named_ e) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Named_ e -> Doc Source #

prettyPrec :: Int -> Named_ e -> Doc Source #

prettyList :: [Named_ e] -> Doc Source #

Pretty a => Pretty (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange a => KillRange (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange a => SetRange (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange a => HasRange (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

IsNoName a => IsNoName (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: WithOrigin a -> Bool Source #

PatternVars (NamedArg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (NamedArg (Pattern' a)) Source #

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj a => EmbPrj (WithOrigin a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: WithOrigin a -> S Int32 Source #

icod_ :: WithOrigin a -> S Int32 Source #

value :: Int32 -> R (WithOrigin a) Source #

PrettyTCM (NamedArg Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (NamedArg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Named_ Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

NormaliseProjP a => NormaliseProjP (Named_ a) Source # 
Instance details

Defined in Agda.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source #

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

AddContext ([NamedArg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source #

contextSize :: ([NamedArg Name], Type) -> Nat Source #

AddContext (List1 (NamedArg Name), Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

type PatternVarOut (NamedArg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

class LensOrigin a where Source #

A lens to access the Origin attribute in data structures. Minimal implementation: getOrigin and mapOrigin or LensArgInfo.

Minimal complete definition

Nothing

Methods

getOrigin :: a -> Origin Source #

default getOrigin :: LensArgInfo a => a -> Origin Source #

setOrigin :: Origin -> a -> a Source #

mapOrigin :: (Origin -> Origin) -> a -> a Source #

default mapOrigin :: LensArgInfo a => (Origin -> Origin) -> a -> a Source #

Instances

Instances details
LensOrigin ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin Origin Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

LensOrigin (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getOrigin :: Arg e -> Origin Source #

setOrigin :: Origin -> Arg e -> Arg e Source #

mapOrigin :: (Origin -> Origin) -> Arg e -> Arg e Source #

LensOrigin (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin (Elim' a) Source #

This instance cheats on Proj, use with care. Projs are always assumed to be UserWritten, since they have no ArgInfo. Same for IApply

Instance details

Defined in Agda.Syntax.Internal.Elim

LensOrigin (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

LensOrigin (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

getOrigin :: Dom' t e -> Origin Source #

setOrigin :: Origin -> Dom' t e -> Dom' t e Source #

mapOrigin :: (Origin -> Origin) -> Dom' t e -> Dom' t e Source #

Free variable annotations

data FreeVariables Source #

Constructors

UnknownFVs 
KnownFVs IntSet 

Instances

Instances details
Eq FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Data FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FreeVariables -> c FreeVariables

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FreeVariables

toConstr :: FreeVariables -> Constr

dataTypeOf :: FreeVariables -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FreeVariables)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FreeVariables)

gmapT :: (forall b. Data b => b -> b) -> FreeVariables -> FreeVariables

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FreeVariables -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FreeVariables -> r

gmapQ :: (forall d. Data d => d -> u) -> FreeVariables -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> FreeVariables -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FreeVariables -> m FreeVariables

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FreeVariables -> m FreeVariables

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FreeVariables -> m FreeVariables

Ord FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Show FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> FreeVariables -> ShowS

show :: FreeVariables -> String

showList :: [FreeVariables] -> ShowS

Semigroup FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

NFData FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: FreeVariables -> ()

KillRange FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

LensFreeVariables FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj FreeVariables Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FreeVariables -> S Int32 Source #

icod_ :: FreeVariables -> S Int32 Source #

value :: Int32 -> R FreeVariables Source #

class LensFreeVariables a where Source #

A lens to access the FreeVariables attribute in data structures. Minimal implementation: getFreeVariables and mapFreeVariables or LensArgInfo.

Minimal complete definition

Nothing

Argument decoration

data ArgInfo Source #

A function argument can be hidden and/or irrelevant.

Constructors

ArgInfo 

Fields

Instances

Instances details
Eq ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: ArgInfo -> ArgInfo -> Bool

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

Data ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ArgInfo -> c ArgInfo

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ArgInfo

toConstr :: ArgInfo -> Constr

dataTypeOf :: ArgInfo -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ArgInfo)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ArgInfo)

gmapT :: (forall b. Data b => b -> b) -> ArgInfo -> ArgInfo

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ArgInfo -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ArgInfo -> r

gmapQ :: (forall d. Data d => d -> u) -> ArgInfo -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ArgInfo -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ArgInfo -> m ArgInfo

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgInfo -> m ArgInfo

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgInfo -> m ArgInfo

Ord ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: ArgInfo -> ArgInfo -> Ordering

(<) :: ArgInfo -> ArgInfo -> Bool

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

(>) :: ArgInfo -> ArgInfo -> Bool

(>=) :: ArgInfo -> ArgInfo -> Bool

max :: ArgInfo -> ArgInfo -> ArgInfo

min :: ArgInfo -> ArgInfo -> ArgInfo

Show ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ArgInfo -> ShowS

show :: ArgInfo -> String

showList :: [ArgInfo] -> ShowS

NFData ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ArgInfo -> ()

KillRange ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensArgInfo ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensFreeVariables ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensCohesion ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensLock ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensAnnotation ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ArgInfo -> S Int32 Source #

icod_ :: ArgInfo -> S Int32 Source #

value :: Int32 -> R ArgInfo Source #

SynEq ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: ArgInfo -> ArgInfo -> SynEqM (ArgInfo, ArgInfo)

synEq' :: ArgInfo -> ArgInfo -> SynEqM (ArgInfo, ArgInfo)

ToTerm ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ChooseFlex ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Unquote ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

EqualSy ArgInfo Source #

Ignore origin and free variables.

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: ArgInfo -> ArgInfo -> Bool Source #

class LensArgInfo a where Source #

Minimal complete definition

getArgInfo

Methods

getArgInfo :: a -> ArgInfo Source #

setArgInfo :: ArgInfo -> a -> a Source #

mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a Source #

Arguments

data Arg e Source #

Constructors

Arg 

Fields

Instances

Instances details
Functor Arg Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> Arg a -> Arg b

(<$) :: a -> Arg b -> Arg a #

Foldable Arg Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => Arg m -> m

foldMap :: Monoid m => (a -> m) -> Arg a -> m

foldMap' :: Monoid m => (a -> m) -> Arg a -> m

foldr :: (a -> b -> b) -> b -> Arg a -> b

foldr' :: (a -> b -> b) -> b -> Arg a -> b

foldl :: (b -> a -> b) -> b -> Arg a -> b

foldl' :: (b -> a -> b) -> b -> Arg a -> b

foldr1 :: (a -> a -> a) -> Arg a -> a

foldl1 :: (a -> a -> a) -> Arg a -> a

toList :: Arg a -> [a]

null :: Arg a -> Bool

length :: Arg a -> Int

elem :: Eq a => a -> Arg a -> Bool

maximum :: Ord a => Arg a -> a

minimum :: Ord a => Arg a -> a

sum :: Num a => Arg a -> a

product :: Num a => Arg a -> a

Traversable Arg Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverse :: Applicative f => (a -> f b) -> Arg a -> f (Arg b)

sequenceA :: Applicative f => Arg (f a) -> f (Arg a)

mapM :: Monad m => (a -> m b) -> Arg a -> m (Arg b)

sequence :: Monad m => Arg (m a) -> m (Arg a)

Decoration Arg Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverseF :: Functor m => (a -> m b) -> Arg a -> m (Arg b) Source #

distributeF :: Functor m => Arg (m a) -> m (Arg a) Source #

MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #

IsPrefixOf Args Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Args -> Args -> Maybe Elims Source #

Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #

Conversion TOM Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O) Source #

Conversion TOM Term (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O) Source #

Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #

PatternLike a b => PatternLike a (Arg b) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Arg b -> m Source #

traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Arg b -> m (Arg b) Source #

MapNamedArgPattern a (NamedArg (Pattern' a)) Source #

Modify the content of VarP, and the closest surrounding NamedArg.

Note: the mapNamedArg for Pattern' is not expressible simply by fmap or traverse etc., since ConP has NamedArg subpatterns, which are taken into account by mapNamedArg.

Instance details

Defined in Agda.Syntax.Internal.Pattern

Conversion MOT (Exp O) Type Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type Source #

Conversion MOT (Exp O) Term Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Term Source #

Conversion TOM [Clause] [([Pat O], MExp O)] Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #

Conversion TOM (Arg Pattern) (Pat O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Arg Pattern -> TOM (Pat O) Source #

Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Arg a -> TOM (Hiding, b) Source #

Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: MM a (RefInfo O) -> MOT b Source #

Eq e => Eq (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Arg e -> Arg e -> Bool

(/=) :: Arg e -> Arg e -> Bool

Data e => Data (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Arg e -> c (Arg e)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Arg e)

toConstr :: Arg e -> Constr

dataTypeOf :: Arg e -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Arg e))

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (Arg e))

gmapT :: (forall b. Data b => b -> b) -> Arg e -> Arg e

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Arg e -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Arg e -> r

gmapQ :: (forall d. Data d => d -> u) -> Arg e -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Arg e -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Arg e -> m (Arg e)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Arg e -> m (Arg e)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Arg e -> m (Arg e)

Ord e => Ord (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Arg e -> Arg e -> Ordering

(<) :: Arg e -> Arg e -> Bool

(<=) :: Arg e -> Arg e -> Bool

(>) :: Arg e -> Arg e -> Bool

(>=) :: Arg e -> Arg e -> Bool

max :: Arg e -> Arg e -> Arg e

min :: Arg e -> Arg e -> Arg e

Show e => Show (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Arg e -> ShowS

show :: Arg e -> String

showList :: [Arg e] -> ShowS

NFData e => NFData (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Arg e -> ()

Pretty a => Pretty (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Arg a -> Doc Source #

prettyPrec :: Int -> Arg a -> Doc Source #

prettyList :: [Arg a] -> Doc Source #

KillRange a => KillRange (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange a => SetRange (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Arg a -> Arg a Source #

HasRange a => HasRange (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Arg a -> Range Source #

LensNamed a => LensNamed (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type NameOf (Arg a) Source #

Methods

lensNamed :: Lens' (Maybe (NameOf (Arg a))) (Arg a) Source #

LensArgInfo (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

LensFreeVariables (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getOrigin :: Arg e -> Origin Source #

setOrigin :: Origin -> Arg e -> Arg e Source #

mapOrigin :: (Origin -> Origin) -> Arg e -> Arg e Source #

LensCohesion (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensLock (Arg t) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getLock :: Arg t -> Lock Source #

setLock :: Lock -> Arg t -> Arg t Source #

mapLock :: (Lock -> Lock) -> Arg t -> Arg t Source #

LensAnnotation (Arg t) Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getHiding :: Arg e -> Hiding Source #

setHiding :: Hiding -> Arg e -> Arg e Source #

mapHiding :: (Hiding -> Hiding) -> Arg e -> Arg e Source #

IsProjP a => IsProjP (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

isProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName) Source #

CPatternLike p => CPatternLike (Arg p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Arg p -> m Source #

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Arg p -> m (Arg p) Source #

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Arg p -> m (Arg p) Source #

IsWithP p => IsWithP (Arg p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

isWithP :: Arg p -> Maybe (Arg p) Source #

ExprLike a => ExprLike (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> Arg a -> Arg a Source #

foldExpr :: Monoid m => (Expr -> m) -> Arg a -> m Source #

traverseExpr :: Monad m => (Expr -> m Expr) -> Arg a -> m (Arg a) Source #

PatternVars (NamedArg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (NamedArg (Pattern' a)) Source #

PatternVars (Arg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (Arg (Pattern' a)) Source #

Methods

patternVars :: Arg (Pattern' a) -> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)] Source #

LensSort a => LensSort (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal

PrecomputeFreeVars a => PrecomputeFreeVars (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Arg a -> FV (Arg a) Source #

Free t => Free (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Arg t -> FreeM a c Source #

Subst a => Subst (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Arg a) Source #

Methods

applySubst :: Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a Source #

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

PatternVarModalities a => PatternVarModalities (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar (Arg a) Source #

CountPatternVars a => CountPatternVars (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

countPatternVars :: Arg a -> Int Source #

TermLike a => TermLike (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Arg a -> m (Arg a) Source #

foldTerm :: Monoid m => (Term -> m) -> Arg a -> m Source #

AllMetas a => AllMetas (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> Arg a -> m Source #

GetDefs a => GetDefs (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => Arg a -> m () Source #

SubstExpr a => SubstExpr (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> Arg a -> Arg a Source #

DeclaredNames a => DeclaredNames (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => Arg a -> m Source #

ExprLike a => ExprLike (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

APatternLike a => APatternLike (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Arg a) Source #

Methods

foldrAPattern :: Monoid m => (Pattern' (ADotT (Arg a)) -> m -> m) -> Arg a -> m Source #

traverseAPatternM :: Monad m => (Pattern' (ADotT (Arg a)) -> m (Pattern' (ADotT (Arg a)))) -> (Pattern' (ADotT (Arg a)) -> m (Pattern' (ADotT (Arg a)))) -> Arg a -> m (Arg a) Source #

EmbPrj a => EmbPrj (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Arg a -> S Int32 Source #

icod_ :: Arg a -> S Int32 Source #

value :: Int32 -> R (Arg a) Source #

PrettyTCM (NamedArg Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (NamedArg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Arg Bool) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Arg Bool -> m Doc Source #

PrettyTCM (Arg Type) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Arg Type -> m Doc Source #

PrettyTCM (Arg Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Arg Term -> m Doc Source #

PrettyTCM (Arg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Arg Expr -> m Doc Source #

NamesIn a => NamesIn (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Arg a -> m Source #

PiApplyM a => PiApplyM (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Telescope

Methods

piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> Arg a -> m Type Source #

piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> Arg a -> m Type Source #

ToConcrete a => ToConcrete (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Arg a) Source #

IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Arg a -> m Bool Source #

ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

MentionsMeta t => MentionsMeta (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Arg t -> Bool Source #

InstantiateFull t => InstantiateFull (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Arg t -> ReduceM (Arg t) Source #

Normalise t => Normalise (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Arg t -> ReduceM (Arg t) Source #

Simplify t => Simplify (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Arg t -> ReduceM (Arg t) Source #

Reduce t => Reduce (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Arg t -> ReduceM (Arg t) Source #

reduceB' :: Arg t -> ReduceM (Blocked (Arg t)) Source #

IsMeta a => IsMeta (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Arg a -> Maybe MetaId Source #

Instantiate t => Instantiate (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Arg t -> ReduceM (Arg t) Source #

SynEq a => SynEq (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Arg a -> Arg a -> SynEqM (Arg a, Arg a)

synEq' :: Arg a -> Arg a -> SynEqM (Arg a, Arg a)

(Reduce a, ForceNotFree a) => ForceNotFree (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Arg a -> m (Arg a)

ToAbstract r => ToAbstract [Arg r] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef [Arg r] Source #

ToAbstract r => ToAbstract (Arg r) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Arg r) Source #

Reify i => Reify (Arg i) Source #

Skip reification of implicit and irrelevant args if option is off.

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Arg i) Source #

Methods

reify :: MonadReify m => Arg i -> m (ReifiesTo (Arg i)) Source #

reifyWhen :: MonadReify m => Bool -> Arg i -> m (ReifiesTo (Arg i)) Source #

UsableModality a => UsableModality (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Arg a -> m Bool Source #

UsableRelevance a => UsableRelevance (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

NormaliseProjP a => NormaliseProjP (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => Arg a -> m (Arg a) Source #

GetMatchables a => GetMatchables (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Arg a -> [QName] Source #

ComputeOccurrences a => ComputeOccurrences (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

AnyRigid a => AnyRigid (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Arg a -> tcm Bool Source #

Occurs a => Occurs (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Arg a -> OccursM (Arg a) Source #

metaOccurs :: MetaId -> Arg a -> TCM () Source #

ReduceAndEtaContract a => ReduceAndEtaContract (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars

Methods

reduceAndEtaContract :: Arg a -> TCM (Arg a) Source #

NoProjectedVar a => NoProjectedVar (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars

Methods

noProjectedVar :: Arg a -> Either ProjectedVar () Source #

Unquote a => Unquote (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Arg a) Source #

EqualSy a => EqualSy (Arg a) Source #

Ignores irrelevant arguments and modality. (And, of course, origin and free variables).

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Arg a -> Arg a -> Bool Source #

AbsTerm a => AbsTerm (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Arg a -> Arg a Source #

IsFlexiblePattern a => IsFlexiblePattern (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Arg a -> MaybeT m FlexibleVarKind Source #

isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Arg a -> m Bool Source #

ToAbstract c => ToAbstract (Arg c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Arg c) Source #

Methods

toAbstract :: Arg c -> ScopeM (AbsOfCon (Arg c)) Source #

LabelPatVars a b => LabelPatVars (Arg a) (Arg b) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel (Arg b) Source #

Methods

labelPatVars :: Arg a -> State [PatVarLabel (Arg b)] (Arg b) Source #

unlabelPatVars :: Arg b -> Arg a Source #

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

TermToPattern a b => TermToPattern (Arg a) (Arg b) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Internal

Methods

termToPattern :: Arg a -> TCM (Arg b) Source #

NLPatToTerm p a => NLPatToTerm (Arg p) (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatToTerm :: PureTCM m => Arg p -> m (Arg a) Source #

PatternFrom t a b => PatternFrom (Dom t) (Arg a) (Arg b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> Dom t -> Arg a -> TCM (Arg b) Source #

Match t a b => Match (Dom t) (Arg a) (Arg b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Dom t -> Arg a -> Arg b -> NLM () Source #

AddContext ([NamedArg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source #

contextSize :: ([NamedArg Name], Type) -> Nat Source #

AddContext ([Arg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source #

contextSize :: ([Arg Name], Type) -> Nat Source #

AddContext (List1 (NamedArg Name), Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext (List1 (Arg Name), Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (List1 (Arg Name), Type) -> m a -> m a Source #

contextSize :: (List1 (Arg Name), Type) -> Nat Source #

type NameOf (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

type NameOf (Arg a) = NameOf a
type PatternVarOut (NamedArg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

type PatternVarOut (Arg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

type PatternVarOut (Arg (Pattern' a)) = a
type SubstArg (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Arg a) = SubstArg a
type PatVar (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

type PatVar (Arg a) = PatVar a
type PatVarLabel (Arg b) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

type ADotT (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ADotT (Arg a) = ADotT a
type ConOfAbs (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Arg a) = Arg (ConOfAbs a)
type AbsOfRef [Arg r] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef [Arg r] = [NamedArg (AbsOfRef r)]
type AbsOfRef (Arg r) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Arg r) = NamedArg (AbsOfRef r)
type ReifiesTo (Arg i) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Arg i) = Arg (ReifiesTo i)
type AbsOfCon (Arg c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Arg c) = Arg (AbsOfCon c)

withArgsFrom :: [a] -> [Arg b] -> [Arg a] Source #

xs `withArgsFrom` args translates xs into a list of Args, using the elements in args to fill in the non-unArg fields.

Precondition: The two lists should have equal length.

Names

class Eq a => Underscore a where Source #

Minimal complete definition

underscore

Methods

underscore :: a Source #

isUnderscore :: a -> Bool Source #

Instances

Instances details
Underscore String Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

underscore :: String Source #

isUnderscore :: String -> Bool Source #

Underscore ByteString Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

underscore :: ByteString Source #

isUnderscore :: ByteString -> Bool Source #

Underscore Doc Source # 
Instance details

Defined in Agda.Syntax.Common

Underscore QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Underscore Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Underscore Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Named arguments

data Named name a Source #

Something potentially carrying a name.

Constructors

Named 

Fields

Instances

Instances details
MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #

MapNamedArgPattern a (NamedArg (Pattern' a)) Source #

Modify the content of VarP, and the closest surrounding NamedArg.

Note: the mapNamedArg for Pattern' is not expressible simply by fmap or traverse etc., since ConP has NamedArg subpatterns, which are taken into account by mapNamedArg.

Instance details

Defined in Agda.Syntax.Internal.Pattern

PatternLike a b => PatternLike a (Named x b) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Named x b -> m Source #

traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Named x b -> m (Named x b) Source #

Functor (Named name) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> Named name a -> Named name b

(<$) :: a -> Named name b -> Named name a #

Foldable (Named name) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => Named name m -> m

foldMap :: Monoid m => (a -> m) -> Named name a -> m

foldMap' :: Monoid m => (a -> m) -> Named name a -> m

foldr :: (a -> b -> b) -> b -> Named name a -> b

foldr' :: (a -> b -> b) -> b -> Named name a -> b

foldl :: (b -> a -> b) -> b -> Named name a -> b

foldl' :: (b -> a -> b) -> b -> Named name a -> b

foldr1 :: (a -> a -> a) -> Named name a -> a

foldl1 :: (a -> a -> a) -> Named name a -> a

toList :: Named name a -> [a]

null :: Named name a -> Bool

length :: Named name a -> Int

elem :: Eq a => a -> Named name a -> Bool

maximum :: Ord a => Named name a -> a

minimum :: Ord a => Named name a -> a

sum :: Num a => Named name a -> a

product :: Num a => Named name a -> a

Traversable (Named name) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverse :: Applicative f => (a -> f b) -> Named name a -> f (Named name b)

sequenceA :: Applicative f => Named name (f a) -> f (Named name a)

mapM :: Monad m => (a -> m b) -> Named name a -> m (Named name b)

sequence :: Monad m => Named name (m a) -> m (Named name a)

Decoration (Named name) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverseF :: Functor m => (a -> m b) -> Named name a -> m (Named name b) Source #

distributeF :: Functor m => Named name (m a) -> m (Named name a) Source #

Pretty e => Pretty (Named_ e) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Named_ e -> Doc Source #

prettyPrec :: Int -> Named_ e -> Doc Source #

prettyList :: [Named_ e] -> Doc Source #

PatternVars (NamedArg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (NamedArg (Pattern' a)) Source #

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

PrettyTCM (NamedArg Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (NamedArg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Named_ Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

NormaliseProjP a => NormaliseProjP (Named_ a) Source # 
Instance details

Defined in Agda.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source #

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

(Eq name, Eq a) => Eq (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Named name a -> Named name a -> Bool

(/=) :: Named name a -> Named name a -> Bool

(Data name, Data a) => Data (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Named name a -> c (Named name a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Named name a)

toConstr :: Named name a -> Constr

dataTypeOf :: Named name a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Named name a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Named name a))

gmapT :: (forall b. Data b => b -> b) -> Named name a -> Named name a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Named name a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Named name a -> r

gmapQ :: (forall d. Data d => d -> u) -> Named name a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Named name a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a)

(Ord name, Ord a) => Ord (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Named name a -> Named name a -> Ordering

(<) :: Named name a -> Named name a -> Bool

(<=) :: Named name a -> Named name a -> Bool

(>) :: Named name a -> Named name a -> Bool

(>=) :: Named name a -> Named name a -> Bool

max :: Named name a -> Named name a -> Named name a

min :: Named name a -> Named name a -> Named name a

(Show name, Show a) => Show (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Named name a -> ShowS

show :: Named name a -> String

showList :: [Named name a] -> ShowS

(NFData name, NFData a) => NFData (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Named name a -> ()

(KillRange name, KillRange a) => KillRange (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Named name a) Source #

SetRange a => SetRange (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Named name a -> Named name a Source #

HasRange a => HasRange (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Named name a -> Range Source #

LensNamed (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type NameOf (Named name a) Source #

Methods

lensNamed :: Lens' (Maybe (NameOf (Named name a))) (Named name a) Source #

LensHiding a => LensHiding (Named nm a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getHiding :: Named nm a -> Hiding Source #

setHiding :: Hiding -> Named nm a -> Named nm a Source #

mapHiding :: (Hiding -> Hiding) -> Named nm a -> Named nm a Source #

IsProjP a => IsProjP (Named n a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) Source #

CPatternLike p => CPatternLike (Named n p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Named n p -> m Source #

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Named n p -> m (Named n p) Source #

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Named n p -> m (Named n p) Source #

IsWithP p => IsWithP (Named n p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

isWithP :: Named n p -> Maybe (Named n p) Source #

ExprLike a => ExprLike (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> Named name a -> Named name a Source #

foldExpr :: Monoid m => (Expr -> m) -> Named name a -> m Source #

traverseExpr :: Monad m => (Expr -> m Expr) -> Named name a -> m (Named name a) Source #

Free t => Free (Named nm t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Named nm t -> FreeM a c Source #

Subst a => Subst (Named name a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Named name a) Source #

Methods

applySubst :: Substitution' (SubstArg (Named name a)) -> Named name a -> Named name a Source #

PatternVarModalities a => PatternVarModalities (Named s a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar (Named s a) Source #

Methods

patternVarModalities :: Named s a -> [(PatVar (Named s a), Modality)] Source #

CountPatternVars a => CountPatternVars (Named x a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

countPatternVars :: Named x a -> Int Source #

SubstExpr a => SubstExpr (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> Named name a -> Named name a Source #

DeclaredNames a => DeclaredNames (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => Named name a -> m Source #

ExprLike a => ExprLike (Named x a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

APatternLike a => APatternLike (Named n a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Named n a) Source #

Methods

foldrAPattern :: Monoid m => (Pattern' (ADotT (Named n a)) -> m -> m) -> Named n a -> m Source #

traverseAPatternM :: Monad m => (Pattern' (ADotT (Named n a)) -> m (Pattern' (ADotT (Named n a)))) -> (Pattern' (ADotT (Named n a)) -> m (Pattern' (ADotT (Named n a)))) -> Named n a -> m (Named n a) Source #

(EmbPrj s, EmbPrj t) => EmbPrj (Named s t) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Named s t -> S Int32 Source #

icod_ :: Named s t -> S Int32 Source #

value :: Int32 -> R (Named s t) Source #

NamesIn a => NamesIn (Named n a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Named n a -> m Source #

AddContext ([NamedArg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source #

contextSize :: ([NamedArg Name], Type) -> Nat Source #

AddContext (List1 (NamedArg Name), Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

PiApplyM a => PiApplyM (Named n a) Source # 
Instance details

Defined in Agda.TypeChecking.Telescope

Methods

piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> Named n a -> m Type Source #

piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> Named n a -> m Type Source #

ToConcrete a => ToConcrete (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Named name a) Source #

Methods

toConcrete :: Named name a -> AbsToCon (ConOfAbs (Named name a)) Source #

bindToConcrete :: Named name a -> (ConOfAbs (Named name a) -> AbsToCon b) -> AbsToCon b Source #

ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

expandPatternSynonyms :: Named n a -> TCM (Named n a) Source #

InstantiateFull t => InstantiateFull (Named name t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Named name t -> ReduceM (Named name t) Source #

Normalise t => Normalise (Named name t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Named name t -> ReduceM (Named name t) Source #

Simplify t => Simplify (Named name t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Named name t -> ReduceM (Named name t) Source #

ToAbstract r => ToAbstract (Named name r) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Named name r) Source #

Methods

toAbstract :: MonadReflectedToAbstract m => Named name r -> m (AbsOfRef (Named name r)) Source #

Reify i => Reify (Named n i) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Named n i) Source #

Methods

reify :: MonadReify m => Named n i -> m (ReifiesTo (Named n i)) Source #

reifyWhen :: MonadReify m => Bool -> Named n i -> m (ReifiesTo (Named n i)) Source #

IsFlexiblePattern a => IsFlexiblePattern (Named name a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Named name a -> MaybeT m FlexibleVarKind Source #

isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Named name a -> m Bool Source #

ToAbstract c => ToAbstract (Named name c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Named name c) Source #

Methods

toAbstract :: Named name c -> ScopeM (AbsOfCon (Named name c)) Source #

LabelPatVars a b => LabelPatVars (Named x a) (Named x b) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel (Named x b) Source #

Methods

labelPatVars :: Named x a -> State [PatVarLabel (Named x b)] (Named x b) Source #

unlabelPatVars :: Named x b -> Named x a Source #

TermToPattern a b => TermToPattern (Named c a) (Named c b) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Internal

Methods

termToPattern :: Named c a -> TCM (Named c b) Source #

type PatternVarOut (NamedArg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

type NameOf (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

type NameOf (Named name a) = name
type SubstArg (Named name a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Named name a) = SubstArg a
type PatVar (Named s a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

type PatVar (Named s a) = PatVar a
type PatVarLabel (Named x b) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

type ADotT (Named n a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ADotT (Named n a) = ADotT a
type ConOfAbs (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Named name a) = Named name (ConOfAbs a)
type AbsOfRef (Named name r) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Named name r) = Named name (AbsOfRef r)
type ReifiesTo (Named n i) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Named n i) = Named n (ReifiesTo i)
type AbsOfCon (Named name c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Named name c) = Named name (AbsOfCon c)

type Named_ = Named NamedName Source #

Standard naming.

type NamedName = WithOrigin (Ranged ArgName) Source #

Standard argument names.

sameName :: NamedName -> NamedName -> Bool Source #

Equality of argument names of things modulo Range and Origin.

unnamed :: a -> Named name a Source #

isUnnamed :: Named name a -> Maybe a Source #

named :: name -> a -> Named name a Source #

class LensNamed a where Source #

Accessor/editor for the nameOf component.

Minimal complete definition

Nothing

Associated Types

type NameOf a Source #

The type of the name

Methods

lensNamed :: Lens' (Maybe (NameOf a)) a Source #

default lensNamed :: (Decoration f, LensNamed b, NameOf b ~ NameOf a, f b ~ a) => Lens' (Maybe (NameOf a)) a Source #

Instances

Instances details
LensNamed (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type NameOf (Maybe a) Source #

Methods

lensNamed :: Lens' (Maybe (NameOf (Maybe a))) (Maybe a) Source #

LensNamed a => LensNamed (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type NameOf (Arg a) Source #

Methods

lensNamed :: Lens' (Maybe (NameOf (Arg a))) (Arg a) Source #

LensNamed (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type NameOf (Named name a) Source #

Methods

lensNamed :: Lens' (Maybe (NameOf (Named name a))) (Named name a) Source #

LensNamed (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

type NameOf (Dom' t e) Source #

Methods

lensNamed :: Lens' (Maybe (NameOf (Dom' t e))) (Dom' t e) Source #

getNameOf :: LensNamed a => a -> Maybe (NameOf a) Source #

setNameOf :: LensNamed a => Maybe (NameOf a) -> a -> a Source #

mapNameOf :: LensNamed a => (Maybe (NameOf a) -> Maybe (NameOf a)) -> a -> a Source #

bareNameOf :: (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName Source #

namedSame :: (LensNamed a, LensNamed b, NameOf a ~ NamedName, NameOf b ~ NamedName) => a -> b -> Bool Source #

Equality of argument names of things modulo Range and Origin.

fittingNamedArg :: (LensNamed arg, NameOf arg ~ NamedName, LensHiding arg, LensNamed dom, NameOf dom ~ NamedName, LensHiding dom) => arg -> dom -> Maybe Bool Source #

Does an argument arg fit the shape dom of the next expected argument?

The hiding has to match, and if the argument has a name, it should match the name of the domain.

Nothing should be __IMPOSSIBLE__, so use as @ fromMaybe IMPOSSIBLE $ fittingNamedArg arg dom @

type NamedArg a = Arg (Named_ a) Source #

Only Hidden arguments can have names.

namedArg :: NamedArg a -> a Source #

Get the content of a NamedArg.

updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b Source #

The functor instance for NamedArg would be ambiguous, so we give it another name here.

updateNamedArgA :: Applicative f => (a -> f b) -> NamedArg a -> f (NamedArg b) Source #

setNamedArg :: NamedArg a -> b -> NamedArg b Source #

setNamedArg a b = updateNamedArg (const b) a

ArgName

type ArgName = String Source #

Names in binders and arguments.

Range decoration.

data Ranged a Source #

Thing with range info.

Constructors

Ranged 

Fields

Instances

Instances details
Functor Ranged Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> Ranged a -> Ranged b

(<$) :: a -> Ranged b -> Ranged a #

Foldable Ranged Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => Ranged m -> m

foldMap :: Monoid m => (a -> m) -> Ranged a -> m

foldMap' :: Monoid m => (a -> m) -> Ranged a -> m

foldr :: (a -> b -> b) -> b -> Ranged a -> b

foldr' :: (a -> b -> b) -> b -> Ranged a -> b

foldl :: (b -> a -> b) -> b -> Ranged a -> b

foldl' :: (b -> a -> b) -> b -> Ranged a -> b

foldr1 :: (a -> a -> a) -> Ranged a -> a

foldl1 :: (a -> a -> a) -> Ranged a -> a

toList :: Ranged a -> [a]

null :: Ranged a -> Bool

length :: Ranged a -> Int

elem :: Eq a => a -> Ranged a -> Bool

maximum :: Ord a => Ranged a -> a

minimum :: Ord a => Ranged a -> a

sum :: Num a => Ranged a -> a

product :: Num a => Ranged a -> a

Traversable Ranged Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverse :: Applicative f => (a -> f b) -> Ranged a -> f (Ranged b)

sequenceA :: Applicative f => Ranged (f a) -> f (Ranged a)

mapM :: Monad m => (a -> m b) -> Ranged a -> m (Ranged b)

sequence :: Monad m => Ranged (m a) -> m (Ranged a)

Decoration Ranged Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverseF :: Functor m => (a -> m b) -> Ranged a -> m (Ranged b) Source #

distributeF :: Functor m => Ranged (m a) -> m (Ranged a) Source #

MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #

MapNamedArgPattern a (NamedArg (Pattern' a)) Source #

Modify the content of VarP, and the closest surrounding NamedArg.

Note: the mapNamedArg for Pattern' is not expressible simply by fmap or traverse etc., since ConP has NamedArg subpatterns, which are taken into account by mapNamedArg.

Instance details

Defined in Agda.Syntax.Internal.Pattern

Eq a => Eq (Ranged a) Source #

Ignores range.

Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Ranged a -> Ranged a -> Bool

(/=) :: Ranged a -> Ranged a -> Bool

Data a => Data (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ranged a -> c (Ranged a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Ranged a)

toConstr :: Ranged a -> Constr

dataTypeOf :: Ranged a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Ranged a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ranged a))

gmapT :: (forall b. Data b => b -> b) -> Ranged a -> Ranged a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r

gmapQ :: (forall d. Data d => d -> u) -> Ranged a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Ranged a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a)

Ord a => Ord (Ranged a) Source #

Ignores range.

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Ranged a -> Ranged a -> Ordering

(<) :: Ranged a -> Ranged a -> Bool

(<=) :: Ranged a -> Ranged a -> Bool

(>) :: Ranged a -> Ranged a -> Bool

(>=) :: Ranged a -> Ranged a -> Bool

max :: Ranged a -> Ranged a -> Ranged a

min :: Ranged a -> Ranged a -> Ranged a

Show a => Show (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Ranged a -> ShowS

show :: Ranged a -> String

showList :: [Ranged a] -> ShowS

NFData a => NFData (Ranged a) Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Ranged a -> ()

Pretty a => Pretty (Ranged a) Source #

Ignores range.

Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: Ranged a -> Doc Source #

prettyPrec :: Int -> Ranged a -> Doc Source #

prettyList :: [Ranged a] -> Doc Source #

Pretty e => Pretty (Named_ e) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Named_ e -> Doc Source #

prettyPrec :: Int -> Named_ e -> Doc Source #

prettyList :: [Named_ e] -> Doc Source #

KillRange (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Ranged a -> Range Source #

IsNoName a => IsNoName (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Ranged a -> Bool Source #

PatternVars (NamedArg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (NamedArg (Pattern' a)) Source #

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj a => EmbPrj (Ranged a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Ranged a -> S Int32 Source #

icod_ :: Ranged a -> S Int32 Source #

value :: Int32 -> R (Ranged a) Source #

PrettyTCM (NamedArg Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (NamedArg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Named_ Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

NormaliseProjP a => NormaliseProjP (Named_ a) Source # 
Instance details

Defined in Agda.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source #

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

AddContext ([NamedArg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source #

contextSize :: ([NamedArg Name], Type) -> Nat Source #

AddContext (List1 (NamedArg Name), Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

type PatternVarOut (NamedArg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

unranged :: a -> Ranged a Source #

Thing with no range info.

Raw names (before parsing into name parts).

type RawName = String Source #

A RawName is some sort of string.

type RString = Ranged RawName Source #

String with range info.

Further constructor and projection info

data ConOrigin Source #

Where does the ConP or Con come from?

Constructors

ConOSystem

Inserted by system or expanded from an implicit pattern.

ConOCon

User wrote a constructor (pattern).

ConORec

User wrote a record (pattern).

ConOSplit

Generated by interactive case splitting.

Instances

Instances details
Bounded ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Enum ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Eq ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: ConOrigin -> ConOrigin -> Bool

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

Data ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConOrigin -> c ConOrigin

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConOrigin

toConstr :: ConOrigin -> Constr

dataTypeOf :: ConOrigin -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConOrigin)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConOrigin)

gmapT :: (forall b. Data b => b -> b) -> ConOrigin -> ConOrigin

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConOrigin -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConOrigin -> r

gmapQ :: (forall d. Data d => d -> u) -> ConOrigin -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ConOrigin -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin

Ord ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: ConOrigin -> ConOrigin -> Ordering

(<) :: ConOrigin -> ConOrigin -> Bool

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

(>) :: ConOrigin -> ConOrigin -> Bool

(>=) :: ConOrigin -> ConOrigin -> Bool

max :: ConOrigin -> ConOrigin -> ConOrigin

min :: ConOrigin -> ConOrigin -> ConOrigin

Show ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ConOrigin -> ShowS

show :: ConOrigin -> String

showList :: [ConOrigin] -> ShowS

Generic ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep ConOrigin :: Type -> Type

Methods

from :: ConOrigin -> Rep ConOrigin x

to :: Rep ConOrigin x -> ConOrigin

NFData ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ConOrigin -> ()

KillRange ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj ConOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ConOrigin -> S Int32 Source #

icod_ :: ConOrigin -> S Int32 Source #

value :: Int32 -> R ConOrigin Source #

type Rep ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep ConOrigin = D1 ('MetaData "ConOrigin" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) ((C1 ('MetaCons "ConOSystem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConOCon" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ConORec" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConOSplit" 'PrefixI 'False) (U1 :: Type -> Type)))

bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin Source #

Prefer user-written over system-inserted.

data ProjOrigin Source #

Where does a projection come from?

Constructors

ProjPrefix

User wrote a prefix projection.

ProjPostfix

User wrote a postfix projection.

ProjSystem

Projection was generated by the system.

Instances

Instances details
Bounded ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Enum ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Eq ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: ProjOrigin -> ProjOrigin -> Bool

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

Data ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProjOrigin -> c ProjOrigin

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProjOrigin

toConstr :: ProjOrigin -> Constr

dataTypeOf :: ProjOrigin -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProjOrigin)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProjOrigin)

gmapT :: (forall b. Data b => b -> b) -> ProjOrigin -> ProjOrigin

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProjOrigin -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProjOrigin -> r

gmapQ :: (forall d. Data d => d -> u) -> ProjOrigin -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProjOrigin -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProjOrigin -> m ProjOrigin

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjOrigin -> m ProjOrigin

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjOrigin -> m ProjOrigin

Ord ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Show ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ProjOrigin -> ShowS

show :: ProjOrigin -> String

showList :: [ProjOrigin] -> ShowS

Generic ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep ProjOrigin :: Type -> Type

Methods

from :: ProjOrigin -> Rep ProjOrigin x

to :: Rep ProjOrigin x -> ProjOrigin

NFData ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ProjOrigin -> ()

KillRange ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj ProjOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ProjOrigin -> S Int32 Source #

icod_ :: ProjOrigin -> S Int32 Source #

value :: Int32 -> R ProjOrigin Source #

type Rep ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep ProjOrigin = D1 ('MetaData "ProjOrigin" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "ProjPrefix" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ProjPostfix" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ProjSystem" 'PrefixI 'False) (U1 :: Type -> Type)))

Infixity, access, abstract, etc.

data IsInfix Source #

Functions can be defined in both infix and prefix style. See LHS.

Constructors

InfixDef 
PrefixDef 

Instances

Instances details
Eq IsInfix Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: IsInfix -> IsInfix -> Bool

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

Data IsInfix Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsInfix -> c IsInfix

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsInfix

toConstr :: IsInfix -> Constr

dataTypeOf :: IsInfix -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsInfix)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsInfix)

gmapT :: (forall b. Data b => b -> b) -> IsInfix -> IsInfix

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsInfix -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsInfix -> r

gmapQ :: (forall d. Data d => d -> u) -> IsInfix -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsInfix -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix

Ord IsInfix Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: IsInfix -> IsInfix -> Ordering

(<) :: IsInfix -> IsInfix -> Bool

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

(>) :: IsInfix -> IsInfix -> Bool

(>=) :: IsInfix -> IsInfix -> Bool

max :: IsInfix -> IsInfix -> IsInfix

min :: IsInfix -> IsInfix -> IsInfix

Show IsInfix Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> IsInfix -> ShowS

show :: IsInfix -> String

showList :: [IsInfix] -> ShowS

private blocks, public imports

data Access Source #

Access modifier.

Constructors

PrivateAccess Origin

Store the Origin of the private block that lead to this qualifier. This is needed for more faithful printing of declarations.

PublicAccess 

Instances

Instances details
Eq Access Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Access -> Access -> Bool

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

Data Access Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Access -> c Access

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Access

toConstr :: Access -> Constr

dataTypeOf :: Access -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Access)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Access)

gmapT :: (forall b. Data b => b -> b) -> Access -> Access

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Access -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Access -> r

gmapQ :: (forall d. Data d => d -> u) -> Access -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Access -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Access -> m Access

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Access -> m Access

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Access -> m Access

Ord Access Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Access -> Access -> Ordering

(<) :: Access -> Access -> Bool

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

(>) :: Access -> Access -> Bool

(>=) :: Access -> Access -> Bool

max :: Access -> Access -> Access

min :: Access -> Access -> Access

Show Access Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Access -> ShowS

show :: Access -> String

showList :: [Access] -> ShowS

NFData Access Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Access -> ()

Pretty Access Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Access Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Access Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Access Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Access -> S Int32 Source #

icod_ :: Access -> S Int32 Source #

value :: Int32 -> R Access Source #

abstract blocks

data IsAbstract Source #

Abstract or concrete.

Constructors

AbstractDef 
ConcreteDef 

Instances

Instances details
Eq IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: IsAbstract -> IsAbstract -> Bool

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

Data IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsAbstract -> c IsAbstract

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsAbstract

toConstr :: IsAbstract -> Constr

dataTypeOf :: IsAbstract -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsAbstract)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsAbstract)

gmapT :: (forall b. Data b => b -> b) -> IsAbstract -> IsAbstract

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsAbstract -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsAbstract -> r

gmapQ :: (forall d. Data d => d -> u) -> IsAbstract -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsAbstract -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsAbstract -> m IsAbstract

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsAbstract -> m IsAbstract

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsAbstract -> m IsAbstract

Ord IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Show IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> IsAbstract -> ShowS

show :: IsAbstract -> String

showList :: [IsAbstract] -> ShowS

Generic IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep IsAbstract :: Type -> Type

Methods

from :: IsAbstract -> Rep IsAbstract x

to :: Rep IsAbstract x -> IsAbstract

Semigroup IsAbstract Source #

Semigroup computes if any of several is an AbstractDef.

Instance details

Defined in Agda.Syntax.Common

Methods

(<>) :: IsAbstract -> IsAbstract -> IsAbstract #

sconcat :: NonEmpty IsAbstract -> IsAbstract

stimes :: Integral b => b -> IsAbstract -> IsAbstract

Monoid IsAbstract Source #

Default is ConcreteDef.

Instance details

Defined in Agda.Syntax.Common

NFData IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: IsAbstract -> ()

KillRange IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

AnyIsAbstract IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

LensIsAbstract IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj IsAbstract Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: IsAbstract -> S Int32 Source #

icod_ :: IsAbstract -> S Int32 Source #

value :: Int32 -> R IsAbstract Source #

type Rep IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep IsAbstract = D1 ('MetaData "IsAbstract" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "AbstractDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConcreteDef" 'PrefixI 'False) (U1 :: Type -> Type))

class AnyIsAbstract a where Source #

Is any element of a collection an AbstractDef.

Minimal complete definition

Nothing

Methods

anyIsAbstract :: a -> IsAbstract Source #

default anyIsAbstract :: (Foldable t, AnyIsAbstract b, t b ~ a) => a -> IsAbstract Source #

Instances

Instances details
AnyIsAbstract IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

AnyIsAbstract a => AnyIsAbstract [a] Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

anyIsAbstract :: [a] -> IsAbstract Source #

AnyIsAbstract a => AnyIsAbstract (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

anyIsAbstract :: Maybe a -> IsAbstract Source #

AnyIsAbstract (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

instance blocks

data IsInstance Source #

Is this definition eligible for instance search?

Constructors

InstanceDef Range

Range of the instance keyword.

NotInstanceDef 

Instances

Instances details
Eq IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: IsInstance -> IsInstance -> Bool

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

Data IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsInstance -> c IsInstance

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsInstance

toConstr :: IsInstance -> Constr

dataTypeOf :: IsInstance -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsInstance)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsInstance)

gmapT :: (forall b. Data b => b -> b) -> IsInstance -> IsInstance

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsInstance -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsInstance -> r

gmapQ :: (forall d. Data d => d -> u) -> IsInstance -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsInstance -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsInstance -> m IsInstance

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInstance -> m IsInstance

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInstance -> m IsInstance

Ord IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Show IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> IsInstance -> ShowS

show :: IsInstance -> String

showList :: [IsInstance] -> ShowS

NFData IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: IsInstance -> ()

KillRange IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

macro blocks

data IsMacro Source #

Is this a macro definition?

Constructors

MacroDef 
NotMacroDef 

Instances

Instances details
Eq IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: IsMacro -> IsMacro -> Bool

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

Data IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsMacro -> c IsMacro

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsMacro

toConstr :: IsMacro -> Constr

dataTypeOf :: IsMacro -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsMacro)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsMacro)

gmapT :: (forall b. Data b => b -> b) -> IsMacro -> IsMacro

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsMacro -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsMacro -> r

gmapQ :: (forall d. Data d => d -> u) -> IsMacro -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsMacro -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro

Ord IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: IsMacro -> IsMacro -> Ordering

(<) :: IsMacro -> IsMacro -> Bool

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

(>) :: IsMacro -> IsMacro -> Bool

(>=) :: IsMacro -> IsMacro -> Bool

max :: IsMacro -> IsMacro -> IsMacro

min :: IsMacro -> IsMacro -> IsMacro

Show IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> IsMacro -> ShowS

show :: IsMacro -> String

showList :: [IsMacro] -> ShowS

Generic IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep IsMacro :: Type -> Type

Methods

from :: IsMacro -> Rep IsMacro x

to :: Rep IsMacro x -> IsMacro

NFData IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: IsMacro -> ()

KillRange IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep IsMacro = D1 ('MetaData "IsMacro" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "MacroDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotMacroDef" 'PrefixI 'False) (U1 :: Type -> Type))

NameId

newtype ModuleNameHash Source #

Constructors

ModuleNameHash Word64 

Instances

Instances details
Eq ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.Common

Data ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleNameHash -> c ModuleNameHash

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleNameHash

toConstr :: ModuleNameHash -> Constr

dataTypeOf :: ModuleNameHash -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleNameHash)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleNameHash)

gmapT :: (forall b. Data b => b -> b) -> ModuleNameHash -> ModuleNameHash

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleNameHash -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleNameHash -> r

gmapQ :: (forall d. Data d => d -> u) -> ModuleNameHash -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleNameHash -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleNameHash -> m ModuleNameHash

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleNameHash -> m ModuleNameHash

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleNameHash -> m ModuleNameHash

Ord ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.Common

Show ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ModuleNameHash -> ShowS

show :: ModuleNameHash -> String

showList :: [ModuleNameHash] -> ShowS

NFData ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ModuleNameHash -> ()

EmbPrj ModuleNameHash Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ModuleNameHash -> S Int32 Source #

icod_ :: ModuleNameHash -> S Int32 Source #

value :: Int32 -> R ModuleNameHash Source #

data NameId Source #

The unique identifier of a name. Second argument is the top-level module identifier.

Constructors

NameId !Word64 !ModuleNameHash 

Instances

Instances details
Enum NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Eq NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: NameId -> NameId -> Bool

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

Data NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameId -> c NameId

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameId

toConstr :: NameId -> Constr

dataTypeOf :: NameId -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameId)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameId)

gmapT :: (forall b. Data b => b -> b) -> NameId -> NameId

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r

gmapQ :: (forall d. Data d => d -> u) -> NameId -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NameId -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameId -> m NameId

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId

Ord NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: NameId -> NameId -> Ordering

(<) :: NameId -> NameId -> Bool

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

(>) :: NameId -> NameId -> Bool

(>=) :: NameId -> NameId -> Bool

max :: NameId -> NameId -> NameId

min :: NameId -> NameId -> NameId

Show NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> NameId -> ShowS

show :: NameId -> String

showList :: [NameId] -> ShowS

Generic NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep NameId :: Type -> Type

Methods

from :: NameId -> Rep NameId x

to :: Rep NameId x -> NameId

NFData NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: NameId -> ()

Hashable NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

hashWithSalt :: Int -> NameId -> Int

hash :: NameId -> Int

Pretty NameId Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange NameId Source # 
Instance details

Defined in Agda.Syntax.Common

HasFresh NameId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj NameId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NameId -> S Int32 Source #

icod_ :: NameId -> S Int32 Source #

value :: Int32 -> R NameId Source #

Monad m => MonadFresh NameId (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

type Rep NameId Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep NameId = D1 ('MetaData "NameId" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "NameId" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash)))

Meta variables

newtype MetaId Source #

A meta variable identifier is just a natural number.

Constructors

MetaId 

Fields

Instances

Instances details
Enum MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Eq MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: MetaId -> MetaId -> Bool

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

Integral MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Data MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MetaId -> c MetaId

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MetaId

toConstr :: MetaId -> Constr

dataTypeOf :: MetaId -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MetaId)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MetaId)

gmapT :: (forall b. Data b => b -> b) -> MetaId -> MetaId

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r

gmapQ :: (forall d. Data d => d -> u) -> MetaId -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> MetaId -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId

Num MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Ord MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: MetaId -> MetaId -> Ordering

(<) :: MetaId -> MetaId -> Bool

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

(>) :: MetaId -> MetaId -> Bool

(>=) :: MetaId -> MetaId -> Bool

max :: MetaId -> MetaId -> MetaId

min :: MetaId -> MetaId -> MetaId

Real MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

toRational :: MetaId -> Rational

Show MetaId Source #

Show non-record version of this newtype.

Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> MetaId -> ShowS

show :: MetaId -> String

showList :: [MetaId] -> ShowS

Generic MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep MetaId :: Type -> Type

Methods

from :: MetaId -> Rep MetaId x

to :: Rep MetaId x -> MetaId

NFData MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: MetaId -> ()

Hashable MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

hashWithSalt :: Int -> MetaId -> Int

hash :: MetaId -> Int

Pretty MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

GetDefs MetaId Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => MetaId -> m () Source #

HasFresh MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: MetaId -> S Int32 Source #

icod_ :: MetaId -> S Int32 Source #

value :: Int32 -> R MetaId Source #

PrettyTCM MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => MetaId -> m Doc Source #

UnFreezeMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source #

IsInstantiatedMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool Source #

Reify MetaId Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo MetaId Source #

FromTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimType MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Unquote MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

ToJSON MetaId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

EncodeTCM MetaId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Singleton MetaId () Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

singleton :: MetaId -> () Source #

Singleton MetaId MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

type Rep MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep MetaId = D1 ('MetaData "MetaId" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'True) (C1 ('MetaCons "MetaId" 'PrefixI 'True) (S1 ('MetaSel ('Just "metaId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat)))
type ReifiesTo MetaId Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Problems

newtype ProblemId Source #

A "problem" consists of a set of constraints and the same constraint can be part of multiple problems.

Constructors

ProblemId Nat 

Instances

Instances details
Enum ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Eq ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: ProblemId -> ProblemId -> Bool

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

Integral ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Data ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemId -> c ProblemId

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemId

toConstr :: ProblemId -> Constr

dataTypeOf :: ProblemId -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemId)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemId)

gmapT :: (forall b. Data b => b -> b) -> ProblemId -> ProblemId

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r

gmapQ :: (forall d. Data d => d -> u) -> ProblemId -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemId -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId

Num ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Ord ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: ProblemId -> ProblemId -> Ordering

(<) :: ProblemId -> ProblemId -> Bool

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

(>) :: ProblemId -> ProblemId -> Bool

(>=) :: ProblemId -> ProblemId -> Bool

max :: ProblemId -> ProblemId -> ProblemId

min :: ProblemId -> ProblemId -> ProblemId

Real ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

toRational :: ProblemId -> Rational

Show ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ProblemId -> ShowS

show :: ProblemId -> String

showList :: [ProblemId] -> ShowS

NFData ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ProblemId -> ()

Pretty ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

HasFresh ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

ToJSON ProblemId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

EncodeTCM ProblemId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Monad m => MonadFresh ProblemId (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Placeholders (used to parse sections)

data PositionInName Source #

The position of a name part or underscore in a name.

Constructors

Beginning

The following underscore is at the beginning of the name: _foo.

Middle

The following underscore is in the middle of the name: foo_bar.

End

The following underscore is at the end of the name: foo_.

Instances

Instances details
Eq PositionInName Source # 
Instance details

Defined in Agda.Syntax.Common

Data PositionInName Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PositionInName -> c PositionInName

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PositionInName

toConstr :: PositionInName -> Constr

dataTypeOf :: PositionInName -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PositionInName)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PositionInName)

gmapT :: (forall b. Data b => b -> b) -> PositionInName -> PositionInName

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PositionInName -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PositionInName -> r

gmapQ :: (forall d. Data d => d -> u) -> PositionInName -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> PositionInName -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PositionInName -> m PositionInName

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PositionInName -> m PositionInName

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PositionInName -> m PositionInName

Ord PositionInName Source # 
Instance details

Defined in Agda.Syntax.Common

Show PositionInName Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> PositionInName -> ShowS

show :: PositionInName -> String

showList :: [PositionInName] -> ShowS

data MaybePlaceholder e Source #

Placeholders are used to represent the underscores in a section.

Constructors

Placeholder !PositionInName 
NoPlaceholder !(Maybe PositionInName) e

The second argument is used only (but not always) for name parts other than underscores.

Instances

Instances details
Functor MaybePlaceholder Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> MaybePlaceholder a -> MaybePlaceholder b

(<$) :: a -> MaybePlaceholder b -> MaybePlaceholder a #

Foldable MaybePlaceholder Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => MaybePlaceholder m -> m

foldMap :: Monoid m => (a -> m) -> MaybePlaceholder a -> m

foldMap' :: Monoid m => (a -> m) -> MaybePlaceholder a -> m

foldr :: (a -> b -> b) -> b -> MaybePlaceholder a -> b

foldr' :: (a -> b -> b) -> b -> MaybePlaceholder a -> b

foldl :: (b -> a -> b) -> b -> MaybePlaceholder a -> b

foldl' :: (b -> a -> b) -> b -> MaybePlaceholder a -> b

foldr1 :: (a -> a -> a) -> MaybePlaceholder a -> a

foldl1 :: (a -> a -> a) -> MaybePlaceholder a -> a

toList :: MaybePlaceholder a -> [a]

null :: MaybePlaceholder a -> Bool

length :: MaybePlaceholder a -> Int

elem :: Eq a => a -> MaybePlaceholder a -> Bool

maximum :: Ord a => MaybePlaceholder a -> a

minimum :: Ord a => MaybePlaceholder a -> a

sum :: Num a => MaybePlaceholder a -> a

product :: Num a => MaybePlaceholder a -> a

Traversable MaybePlaceholder Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverse :: Applicative f => (a -> f b) -> MaybePlaceholder a -> f (MaybePlaceholder b)

sequenceA :: Applicative f => MaybePlaceholder (f a) -> f (MaybePlaceholder a)

mapM :: Monad m => (a -> m b) -> MaybePlaceholder a -> m (MaybePlaceholder b)

sequence :: Monad m => MaybePlaceholder (m a) -> m (MaybePlaceholder a)

Eq e => Eq (MaybePlaceholder e) Source # 
Instance details

Defined in Agda.Syntax.Common

Data e => Data (MaybePlaceholder e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MaybePlaceholder e -> c (MaybePlaceholder e)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (MaybePlaceholder e)

toConstr :: MaybePlaceholder e -> Constr

dataTypeOf :: MaybePlaceholder e -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (MaybePlaceholder e))

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (MaybePlaceholder e))

gmapT :: (forall b. Data b => b -> b) -> MaybePlaceholder e -> MaybePlaceholder e

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MaybePlaceholder e -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MaybePlaceholder e -> r

gmapQ :: (forall d. Data d => d -> u) -> MaybePlaceholder e -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> MaybePlaceholder e -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MaybePlaceholder e -> m (MaybePlaceholder e)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MaybePlaceholder e -> m (MaybePlaceholder e)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MaybePlaceholder e -> m (MaybePlaceholder e)

Ord e => Ord (MaybePlaceholder e) Source # 
Instance details

Defined in Agda.Syntax.Common

Show e => Show (MaybePlaceholder e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> MaybePlaceholder e -> ShowS

show :: MaybePlaceholder e -> String

showList :: [MaybePlaceholder e] -> ShowS

NFData a => NFData (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: MaybePlaceholder a -> ()

Pretty a => Pretty (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange a => KillRange (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange a => HasRange (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Common

ExprLike a => ExprLike (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> MaybePlaceholder a -> MaybePlaceholder a Source #

foldExpr :: Monoid m => (Expr -> m) -> MaybePlaceholder a -> m Source #

traverseExpr :: Monad m => (Expr -> m Expr) -> MaybePlaceholder a -> m (MaybePlaceholder a) Source #

noPlaceholder :: e -> MaybePlaceholder e Source #

An abbreviation: noPlaceholder = NoPlaceholder Nothing.

Interaction meta variables

newtype InteractionId Source #

Constructors

InteractionId 

Fields

Instances

Instances details
Enum InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Eq InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Integral InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Data InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> InteractionId -> c InteractionId

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c InteractionId

toConstr :: InteractionId -> Constr

dataTypeOf :: InteractionId -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c InteractionId)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InteractionId)

gmapT :: (forall b. Data b => b -> b) -> InteractionId -> InteractionId

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> InteractionId -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InteractionId -> r

gmapQ :: (forall d. Data d => d -> u) -> InteractionId -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> InteractionId -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> InteractionId -> m InteractionId

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InteractionId -> m InteractionId

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InteractionId -> m InteractionId

Num InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Ord InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Read InteractionId 
Instance details

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS InteractionId

readList :: ReadS [InteractionId]

readPrec :: ReadPrec InteractionId

readListPrec :: ReadPrec [InteractionId]

Real InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

toRational :: InteractionId -> Rational

Show InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> InteractionId -> ShowS

show :: InteractionId -> String

showList :: [InteractionId] -> ShowS

NFData InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: InteractionId -> ()

NFData InteractionPoints 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

rnf :: InteractionPoints -> ()

Pretty InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

HasFresh InteractionId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

ToConcrete InteractionId Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs InteractionId Source #

ToJSON InteractionId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

EncodeTCM InteractionId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

type ConOfAbs InteractionId Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Fixity

type PrecedenceLevel = Double Source #

Precedence levels for operators.

data FixityLevel Source #

Constructors

Unrelated

No fixity declared.

Related !PrecedenceLevel

Fixity level declared as the number.

Instances

Instances details
Eq FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: FixityLevel -> FixityLevel -> Bool

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

Data FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FixityLevel -> c FixityLevel

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FixityLevel

toConstr :: FixityLevel -> Constr

dataTypeOf :: FixityLevel -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FixityLevel)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FixityLevel)

gmapT :: (forall b. Data b => b -> b) -> FixityLevel -> FixityLevel

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FixityLevel -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FixityLevel -> r

gmapQ :: (forall d. Data d => d -> u) -> FixityLevel -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> FixityLevel -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FixityLevel -> m FixityLevel

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FixityLevel -> m FixityLevel

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FixityLevel -> m FixityLevel

Ord FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

Show FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> FixityLevel -> ShowS

show :: FixityLevel -> String

showList :: [FixityLevel] -> ShowS

NFData FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: FixityLevel -> ()

Null FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

EmbPrj FixityLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FixityLevel -> S Int32 Source #

icod_ :: FixityLevel -> S Int32 Source #

value :: Int32 -> R FixityLevel Source #

ToTerm FixityLevel Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

data Associativity Source #

Associativity.

Constructors

NonAssoc 
LeftAssoc 
RightAssoc 

Instances

Instances details
Eq Associativity Source # 
Instance details

Defined in Agda.Syntax.Common

Data Associativity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Associativity -> c Associativity

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Associativity

toConstr :: Associativity -> Constr

dataTypeOf :: Associativity -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Associativity)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Associativity)

gmapT :: (forall b. Data b => b -> b) -> Associativity -> Associativity

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r

gmapQ :: (forall d. Data d => d -> u) -> Associativity -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Associativity -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity

Ord Associativity Source # 
Instance details

Defined in Agda.Syntax.Common

Show Associativity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Associativity -> ShowS

show :: Associativity -> String

showList :: [Associativity] -> ShowS

Pretty Associativity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

EmbPrj Associativity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Associativity -> S Int32 Source #

icod_ :: Associativity -> S Int32 Source #

value :: Int32 -> R Associativity Source #

ToTerm Associativity Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

data Fixity Source #

Fixity of operators.

Constructors

Fixity 

Fields

Instances

Instances details
Eq Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Fixity -> Fixity -> Bool

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

Data Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Fixity -> c Fixity

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity

toConstr :: Fixity -> Constr

dataTypeOf :: Fixity -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Fixity)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity)

gmapT :: (forall b. Data b => b -> b) -> Fixity -> Fixity

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r

gmapQ :: (forall d. Data d => d -> u) -> Fixity -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity

Ord Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Fixity -> Fixity -> Ordering

(<) :: Fixity -> Fixity -> Bool

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

(>) :: Fixity -> Fixity -> Bool

(>=) :: Fixity -> Fixity -> Bool

max :: Fixity -> Fixity -> Fixity

min :: Fixity -> Fixity -> Fixity

Show Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Fixity -> ShowS

show :: Fixity -> String

showList :: [Fixity] -> ShowS

NFData Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Fixity -> ()

Null Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

empty :: Fixity Source #

null :: Fixity -> Bool Source #

Pretty Fixity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

LensFixity Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Fixity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Fixity -> S Int32 Source #

icod_ :: Fixity -> S Int32 Source #

value :: Int32 -> R Fixity Source #

ToTerm Fixity Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Notation coupled with Fixity

data Fixity' Source #

The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.

Constructors

Fixity' 

Fields

Instances

Instances details
Eq Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Fixity' -> Fixity' -> Bool

(/=) :: Fixity' -> Fixity' -> Bool

Data Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Fixity' -> c Fixity'

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity'

toConstr :: Fixity' -> Constr

dataTypeOf :: Fixity' -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Fixity')

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity')

gmapT :: (forall b. Data b => b -> b) -> Fixity' -> Fixity'

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r

gmapQ :: (forall d. Data d => d -> u) -> Fixity' -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity' -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity'

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity'

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity'

Show Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Fixity' -> ShowS

show :: Fixity' -> String

showList :: [Fixity'] -> ShowS

NFData Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Fixity' -> ()

Null Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

empty :: Fixity' Source #

null :: Fixity' -> Bool Source #

Pretty Fixity' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

LensFixity' Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

LensFixity Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Fixity' -> S Int32 Source #

icod_ :: Fixity' -> S Int32 Source #

value :: Int32 -> R Fixity' Source #

ToTerm Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimType Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

class LensFixity' a where Source #

Instances

Instances details
LensFixity' Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

LensFixity' QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

LensFixity' Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

LensFixity' (ThingWithFixity a) Source # 
Instance details

Defined in Agda.Syntax.Fixity

Import directive

data ImportDirective' n m Source #

The things you are allowed to say when you shuffle names between name spaces (i.e. in import, namespace, or open declarations).

Constructors

ImportDirective 

Fields

Instances

Instances details
(Eq m, Eq n) => Eq (ImportDirective' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: ImportDirective' n m -> ImportDirective' n m -> Bool

(/=) :: ImportDirective' n m -> ImportDirective' n m -> Bool

(Data n, Data m) => Data (ImportDirective' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ImportDirective' n m -> c (ImportDirective' n m)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ImportDirective' n m)

toConstr :: ImportDirective' n m -> Constr

dataTypeOf :: ImportDirective' n m -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ImportDirective' n m))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ImportDirective' n m))

gmapT :: (forall b. Data b => b -> b) -> ImportDirective' n m -> ImportDirective' n m

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportDirective' n m -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportDirective' n m -> r

gmapQ :: (forall d. Data d => d -> u) -> ImportDirective' n m -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportDirective' n m -> u

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m)

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m)

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m)

(Show a, Show b) => Show (ImportDirective' a b) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> ImportDirective' a b -> ShowS

show :: ImportDirective' a b -> String

showList :: [ImportDirective' a b] -> ShowS

(HasRange n, HasRange m) => Semigroup (ImportDirective' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(<>) :: ImportDirective' n m -> ImportDirective' n m -> ImportDirective' n m #

sconcat :: NonEmpty (ImportDirective' n m) -> ImportDirective' n m

stimes :: Integral b => b -> ImportDirective' n m -> ImportDirective' n m

(HasRange n, HasRange m) => Monoid (ImportDirective' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

(NFData a, NFData b) => NFData (ImportDirective' a b) Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ImportDirective' a b -> ()

Null (ImportDirective' n m) Source #

null for import directives holds when everything is imported unchanged (no names are hidden or renamed).

Instance details

Defined in Agda.Syntax.Common

(Pretty a, Pretty b) => Pretty (ImportDirective' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

(KillRange a, KillRange b) => KillRange (ImportDirective' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(HasRange a, HasRange b) => HasRange (ImportDirective' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

defaultImportDir :: ImportDirective' n m Source #

Default is directive is private (use everything, but do not export).

isDefaultImportDir :: ImportDirective' n m -> Bool Source #

isDefaultImportDir implies null, but not the other way round.

data Using' n m Source #

The using clause of import directive.

Constructors

UseEverything

No using clause given.

Using [ImportedName' n m]

using the specified names.

Instances

Instances details
(Eq m, Eq n) => Eq (Using' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Using' n m -> Using' n m -> Bool

(/=) :: Using' n m -> Using' n m -> Bool

(Data n, Data m) => Data (Using' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Using' n m -> c (Using' n m)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Using' n m)

toConstr :: Using' n m -> Constr

dataTypeOf :: Using' n m -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Using' n m))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Using' n m))

gmapT :: (forall b. Data b => b -> b) -> Using' n m -> Using' n m

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Using' n m -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Using' n m -> r

gmapQ :: (forall d. Data d => d -> u) -> Using' n m -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Using' n m -> u

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m)

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m)

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m)

(Show a, Show b) => Show (Using' a b) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Using' a b -> ShowS

show :: Using' a b -> String

showList :: [Using' a b] -> ShowS

Semigroup (Using' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(<>) :: Using' n m -> Using' n m -> Using' n m #

sconcat :: NonEmpty (Using' n m) -> Using' n m

stimes :: Integral b => b -> Using' n m -> Using' n m

Monoid (Using' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

mempty :: Using' n m

mappend :: Using' n m -> Using' n m -> Using' n m

mconcat :: [Using' n m] -> Using' n m

(NFData a, NFData b) => NFData (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Using' a b -> ()

Null (Using' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

empty :: Using' n m Source #

null :: Using' n m -> Bool Source #

(Pretty a, Pretty b) => Pretty (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Using' a b -> Doc Source #

prettyPrec :: Int -> Using' a b -> Doc Source #

prettyList :: [Using' a b] -> Doc Source #

(KillRange a, KillRange b) => KillRange (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(HasRange a, HasRange b) => HasRange (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Using' a b -> Range Source #

mapUsing :: ([ImportedName' n1 m1] -> [ImportedName' n2 m2]) -> Using' n1 m1 -> Using' n2 m2 Source #

data ImportedName' n m Source #

An imported name can be a module or a defined name.

Constructors

ImportedModule m

Imported module name of type m.

ImportedName n

Imported name of type n.

Instances

Instances details
(Eq m, Eq n) => Eq (ImportedName' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: ImportedName' n m -> ImportedName' n m -> Bool

(/=) :: ImportedName' n m -> ImportedName' n m -> Bool

(Data n, Data m) => Data (ImportedName' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ImportedName' n m -> c (ImportedName' n m)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ImportedName' n m)

toConstr :: ImportedName' n m -> Constr

dataTypeOf :: ImportedName' n m -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ImportedName' n m))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ImportedName' n m))

gmapT :: (forall b. Data b => b -> b) -> ImportedName' n m -> ImportedName' n m

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportedName' n m -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportedName' n m -> r

gmapQ :: (forall d. Data d => d -> u) -> ImportedName' n m -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportedName' n m -> u

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m)

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m)

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m)

(Ord m, Ord n) => Ord (ImportedName' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: ImportedName' n m -> ImportedName' n m -> Ordering

(<) :: ImportedName' n m -> ImportedName' n m -> Bool

(<=) :: ImportedName' n m -> ImportedName' n m -> Bool

(>) :: ImportedName' n m -> ImportedName' n m -> Bool

(>=) :: ImportedName' n m -> ImportedName' n m -> Bool

max :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m

min :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m

(Show m, Show n) => Show (ImportedName' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ImportedName' n m -> ShowS

show :: ImportedName' n m -> String

showList :: [ImportedName' n m] -> ShowS

(NFData a, NFData b) => NFData (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ImportedName' a b -> ()

(Pretty a, Pretty b) => Pretty (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

(KillRange a, KillRange b) => KillRange (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(HasRange a, HasRange b) => HasRange (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ImportedName' a b -> S Int32 Source #

icod_ :: ImportedName' a b -> S Int32 Source #

value :: Int32 -> R (ImportedName' a b) Source #

partitionImportedNames :: [ImportedName' n m] -> ([n], [m]) Source #

Like partitionEithers.

data Renaming' n m Source #

Constructors

Renaming 

Fields

Instances

Instances details
(Eq m, Eq n) => Eq (Renaming' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Renaming' n m -> Renaming' n m -> Bool

(/=) :: Renaming' n m -> Renaming' n m -> Bool

(Data n, Data m) => Data (Renaming' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Renaming' n m -> c (Renaming' n m)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Renaming' n m)

toConstr :: Renaming' n m -> Constr

dataTypeOf :: Renaming' n m -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Renaming' n m))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Renaming' n m))

gmapT :: (forall b. Data b => b -> b) -> Renaming' n m -> Renaming' n m

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' n m -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' n m -> r

gmapQ :: (forall d. Data d => d -> u) -> Renaming' n m -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Renaming' n m -> u

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m)

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m)

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m)

(Show a, Show b) => Show (Renaming' a b) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Renaming' a b -> ShowS

show :: Renaming' a b -> String

showList :: [Renaming' a b] -> ShowS

(NFData a, NFData b) => NFData (Renaming' a b) Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Renaming' a b -> ()

(Pretty a, Pretty b) => Pretty (Renaming' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Renaming' a b -> Doc Source #

prettyPrec :: Int -> Renaming' a b -> Doc Source #

prettyList :: [Renaming' a b] -> Doc Source #

(KillRange a, KillRange b) => KillRange (Renaming' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(HasRange a, HasRange b) => HasRange (Renaming' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Renaming' a b -> Range Source #

HasRange instances

KillRange instances

NFData instances

Termination

data TerminationCheck m Source #

Termination check? (Default = TerminationCheck).

Constructors

TerminationCheck

Run the termination checker.

NoTerminationCheck

Skip termination checking (unsafe).

NonTerminating

Treat as non-terminating.

Terminating

Treat as terminating (unsafe). Same effect as NoTerminationCheck.

TerminationMeasure Range m

Skip termination checking but use measure instead.

Instances

Instances details
Functor TerminationCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> TerminationCheck a -> TerminationCheck b

(<$) :: a -> TerminationCheck b -> TerminationCheck a #

Eq m => Eq (TerminationCheck m) Source # 
Instance details

Defined in Agda.Syntax.Common

Data m => Data (TerminationCheck m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TerminationCheck m -> c (TerminationCheck m)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TerminationCheck m)

toConstr :: TerminationCheck m -> Constr

dataTypeOf :: TerminationCheck m -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TerminationCheck m))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TerminationCheck m))

gmapT :: (forall b. Data b => b -> b) -> TerminationCheck m -> TerminationCheck m

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TerminationCheck m -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TerminationCheck m -> r

gmapQ :: (forall d. Data d => d -> u) -> TerminationCheck m -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TerminationCheck m -> u

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> TerminationCheck m -> m0 (TerminationCheck m)

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> TerminationCheck m -> m0 (TerminationCheck m)

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> TerminationCheck m -> m0 (TerminationCheck m)

Show m => Show (TerminationCheck m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> TerminationCheck m -> ShowS

show :: TerminationCheck m -> String

showList :: [TerminationCheck m] -> ShowS

NFData a => NFData (TerminationCheck a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: TerminationCheck a -> ()

KillRange m => KillRange (TerminationCheck m) Source # 
Instance details

Defined in Agda.Syntax.Common

Positivity

data PositivityCheck Source #

Positivity check? (Default = True).

Instances

Instances details
Bounded PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Enum PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Eq PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Data PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PositivityCheck -> c PositivityCheck

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PositivityCheck

toConstr :: PositivityCheck -> Constr

dataTypeOf :: PositivityCheck -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PositivityCheck)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PositivityCheck)

gmapT :: (forall b. Data b => b -> b) -> PositivityCheck -> PositivityCheck

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PositivityCheck -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PositivityCheck -> r

gmapQ :: (forall d. Data d => d -> u) -> PositivityCheck -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> PositivityCheck -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PositivityCheck -> m PositivityCheck

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PositivityCheck -> m PositivityCheck

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PositivityCheck -> m PositivityCheck

Ord PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Show PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> PositivityCheck -> ShowS

show :: PositivityCheck -> String

showList :: [PositivityCheck] -> ShowS

Generic PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep PositivityCheck :: Type -> Type

Semigroup PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

NFData PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: PositivityCheck -> ()

KillRange PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep PositivityCheck = D1 ('MetaData "PositivityCheck" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "YesPositivityCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoPositivityCheck" 'PrefixI 'False) (U1 :: Type -> Type))

Universe checking

data UniverseCheck Source #

Universe check? (Default is yes).

Instances

Instances details
Bounded UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Enum UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Eq UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Data UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UniverseCheck -> c UniverseCheck

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UniverseCheck

toConstr :: UniverseCheck -> Constr

dataTypeOf :: UniverseCheck -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UniverseCheck)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UniverseCheck)

gmapT :: (forall b. Data b => b -> b) -> UniverseCheck -> UniverseCheck

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UniverseCheck -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UniverseCheck -> r

gmapQ :: (forall d. Data d => d -> u) -> UniverseCheck -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> UniverseCheck -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UniverseCheck -> m UniverseCheck

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UniverseCheck -> m UniverseCheck

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UniverseCheck -> m UniverseCheck

Ord UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Show UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> UniverseCheck -> ShowS

show :: UniverseCheck -> String

showList :: [UniverseCheck] -> ShowS

Generic UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep UniverseCheck :: Type -> Type

NFData UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: UniverseCheck -> ()

KillRange UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep UniverseCheck = D1 ('MetaData "UniverseCheck" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "YesUniverseCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoUniverseCheck" 'PrefixI 'False) (U1 :: Type -> Type))

Universe checking

data CoverageCheck Source #

Coverage check? (Default is yes).

Instances

Instances details
Bounded CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Enum CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Eq CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Data CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoverageCheck -> c CoverageCheck

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoverageCheck

toConstr :: CoverageCheck -> Constr

dataTypeOf :: CoverageCheck -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CoverageCheck)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoverageCheck)

gmapT :: (forall b. Data b => b -> b) -> CoverageCheck -> CoverageCheck

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoverageCheck -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoverageCheck -> r

gmapQ :: (forall d. Data d => d -> u) -> CoverageCheck -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> CoverageCheck -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoverageCheck -> m CoverageCheck

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoverageCheck -> m CoverageCheck

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoverageCheck -> m CoverageCheck

Ord CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Show CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> CoverageCheck -> ShowS

show :: CoverageCheck -> String

showList :: [CoverageCheck] -> ShowS

Generic CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep CoverageCheck :: Type -> Type

Semigroup CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

NFData CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: CoverageCheck -> ()

KillRange CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep CoverageCheck = D1 ('MetaData "CoverageCheck" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "YesCoverageCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoCoverageCheck" 'PrefixI 'False) (U1 :: Type -> Type))

Rewrite Directives on the LHS

data RewriteEqn' qn nm p e Source #

RewriteEqn' qn p e represents the rewrite and irrefutable with clauses of the LHS. qn stands for the QName of the auxiliary function generated to implement the feature nm is the type of names for pattern variables p is the type of patterns e is the type of expressions

Constructors

Rewrite (List1 (qn, e))
rewrite e
Invert qn (List1 (Named nm (p, e)))
with p <- e in eq

Instances

Instances details
ToAbstract RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RewriteEqn Source #

Functor (RewriteEqn' qn nm p) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> RewriteEqn' qn nm p a -> RewriteEqn' qn nm p b

(<$) :: a -> RewriteEqn' qn nm p b -> RewriteEqn' qn nm p a #

Foldable (RewriteEqn' qn nm p) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => RewriteEqn' qn nm p m -> m

foldMap :: Monoid m => (a -> m) -> RewriteEqn' qn nm p a -> m

foldMap' :: Monoid m => (a -> m) -> RewriteEqn' qn nm p a -> m

foldr :: (a -> b -> b) -> b -> RewriteEqn' qn nm p a -> b

foldr' :: (a -> b -> b) -> b -> RewriteEqn' qn nm p a -> b

foldl :: (b -> a -> b) -> b -> RewriteEqn' qn nm p a -> b

foldl' :: (b -> a -> b) -> b -> RewriteEqn' qn nm p a -> b

foldr1 :: (a -> a -> a) -> RewriteEqn' qn nm p a -> a

foldl1 :: (a -> a -> a) -> RewriteEqn' qn nm p a -> a

toList :: RewriteEqn' qn nm p a -> [a]

null :: RewriteEqn' qn nm p a -> Bool

length :: RewriteEqn' qn nm p a -> Int

elem :: Eq a => a -> RewriteEqn' qn nm p a -> Bool

maximum :: Ord a => RewriteEqn' qn nm p a -> a

minimum :: Ord a => RewriteEqn' qn nm p a -> a

sum :: Num a => RewriteEqn' qn nm p a -> a

product :: Num a => RewriteEqn' qn nm p a -> a

Traversable (RewriteEqn' qn nm p) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverse :: Applicative f => (a -> f b) -> RewriteEqn' qn nm p a -> f (RewriteEqn' qn nm p b)

sequenceA :: Applicative f => RewriteEqn' qn nm p (f a) -> f (RewriteEqn' qn nm p a)

mapM :: Monad m => (a -> m b) -> RewriteEqn' qn nm p a -> m (RewriteEqn' qn nm p b)

sequence :: Monad m => RewriteEqn' qn nm p (m a) -> m (RewriteEqn' qn nm p a)

(Eq qn, Eq e, Eq nm, Eq p) => Eq (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e -> Bool

(/=) :: RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e -> Bool

(Data qn, Data nm, Data p, Data e) => Data (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RewriteEqn' qn nm p e -> c (RewriteEqn' qn nm p e)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RewriteEqn' qn nm p e)

toConstr :: RewriteEqn' qn nm p e -> Constr

dataTypeOf :: RewriteEqn' qn nm p e -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RewriteEqn' qn nm p e))

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (RewriteEqn' qn nm p e))

gmapT :: (forall b. Data b => b -> b) -> RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RewriteEqn' qn nm p e -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RewriteEqn' qn nm p e -> r

gmapQ :: (forall d. Data d => d -> u) -> RewriteEqn' qn nm p e -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> RewriteEqn' qn nm p e -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e)

(Show qn, Show e, Show nm, Show p) => Show (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> RewriteEqn' qn nm p e -> ShowS

show :: RewriteEqn' qn nm p e -> String

showList :: [RewriteEqn' qn nm p e] -> ShowS

(NFData qn, NFData nm, NFData p, NFData e) => NFData (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: RewriteEqn' qn nm p e -> ()

(Pretty nm, Pretty p, Pretty e) => Pretty (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: RewriteEqn' qn nm p e -> Doc Source #

prettyPrec :: Int -> RewriteEqn' qn nm p e -> Doc Source #

prettyList :: [RewriteEqn' qn nm p e] -> Doc Source #

(KillRange qn, KillRange nm, KillRange e, KillRange p) => KillRange (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (RewriteEqn' qn nm p e) Source #

(HasRange qn, HasRange nm, HasRange p, HasRange e) => HasRange (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: RewriteEqn' qn nm p e -> Range Source #

(ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e Source #

foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn nm p e -> m Source #

traverseExpr :: Monad m => (Expr -> m Expr) -> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e) Source #

(ExprLike qn, ExprLike nm, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (RewriteEqn' qn BindName p a) Source #

ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source #

type AbsOfCon RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type ConOfAbs (RewriteEqn' qn BindName p a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Information on expanded ellipsis (...)

data ExpandedEllipsis Source #

Instances

Instances details
Eq ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

Data ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExpandedEllipsis -> c ExpandedEllipsis

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExpandedEllipsis

toConstr :: ExpandedEllipsis -> Constr

dataTypeOf :: ExpandedEllipsis -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExpandedEllipsis)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExpandedEllipsis)

gmapT :: (forall b. Data b => b -> b) -> ExpandedEllipsis -> ExpandedEllipsis

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExpandedEllipsis -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExpandedEllipsis -> r

gmapQ :: (forall d. Data d => d -> u) -> ExpandedEllipsis -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ExpandedEllipsis -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExpandedEllipsis -> m ExpandedEllipsis

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandedEllipsis -> m ExpandedEllipsis

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandedEllipsis -> m ExpandedEllipsis

Show ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ExpandedEllipsis -> ShowS

show :: ExpandedEllipsis -> String

showList :: [ExpandedEllipsis] -> ShowS

Semigroup ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

NFData ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ExpandedEllipsis -> ()

Null ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj ExpandedEllipsis Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

type Notation = [GenPart] Source #

Notation as provided by the syntax declaration.

data GenPart Source #

Part of a Notation

Constructors

BindHole Range (Ranged Int)

Argument is the position of the hole (with binding) where the binding should occur. First range is the rhs range and second is the binder.

NormalHole Range (NamedArg (Ranged Int))

Argument is where the expression should go.

WildHole (Ranged Int)

An underscore in binding position.

IdPart RString 

Instances

Instances details
Eq GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: GenPart -> GenPart -> Bool

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

Data GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GenPart -> c GenPart

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GenPart

toConstr :: GenPart -> Constr

dataTypeOf :: GenPart -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GenPart)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GenPart)

gmapT :: (forall b. Data b => b -> b) -> GenPart -> GenPart

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GenPart -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GenPart -> r

gmapQ :: (forall d. Data d => d -> u) -> GenPart -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> GenPart -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart

Ord GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: GenPart -> GenPart -> Ordering

(<) :: GenPart -> GenPart -> Bool

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

(>) :: GenPart -> GenPart -> Bool

(>=) :: GenPart -> GenPart -> Bool

max :: GenPart -> GenPart -> GenPart

min :: GenPart -> GenPart -> GenPart

Show GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> GenPart -> ShowS

show :: GenPart -> String

showList :: [GenPart] -> ShowS

NFData GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: GenPart -> ()

Pretty GenPart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj GenPart Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: GenPart -> S Int32 Source #

icod_ :: GenPart -> S Int32 Source #

value :: Int32 -> R GenPart Source #