Agda-2.6.2.2: 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

Show Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

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

type Rep Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Delayed = D1 ('MetaData "Delayed" "Agda.Syntax.Common" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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

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

Show FileType Source # 
Instance details

Defined in Agda.Syntax.Common

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

type Rep FileType Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep FileType = D1 ('MetaData "FileType" "Agda.Syntax.Common" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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

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

type Rep Cubical Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Cubical = D1 ('MetaData "Cubical" "Agda.Syntax.Common" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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

Show Language Source # 
Instance details

Defined in Agda.Syntax.Common

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

type Rep Language Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Language = D1 ('MetaData "Language" "Agda.Syntax.Common" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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 #

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

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

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

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

Induction

data Induction Source #

Inductive < Coinductive

Constructors

Inductive 
CoInductive 

Instances

Instances details
Eq Induction Source # 
Instance details

Defined in Agda.Syntax.Common

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

Show Induction Source # 
Instance details

Defined in Agda.Syntax.Common

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

Hiding

data Overlappable Source #

Constructors

YesOverlap 
NoOverlap 

Instances

Instances details
Eq Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

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

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

Show Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup Hiding Source #

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

Instance details

Defined in Agda.Syntax.Common

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

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

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

Defined in Agda.Syntax.Common

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

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 #

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

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

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

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

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

Show Modality Source # 
Instance details

Defined in Agda.Syntax.Common

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

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.2-DXbLWdCWC6QEApzM0094If" '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

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

Show Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

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

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

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

type Rep Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Q0Origin = D1 ('MetaData "Q0Origin" "Agda.Syntax.Common" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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

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

Show Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

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

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

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

type Rep Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Q1Origin = D1 ('MetaData "Q1Origin" "Agda.Syntax.Common" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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

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

Show QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Generic QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep QωOrigin :: Type -> Type #

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

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

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.2-DXbLWdCWC6QEApzM0094If" '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

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

Show Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

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

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

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.

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

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.2-DXbLWdCWC6QEApzM0094If" '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.

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

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

Show Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Generic Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Relevance :: Type -> Type #

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

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.2-DXbLWdCWC6QEApzM0094If" '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

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

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

Generic Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Annotation :: Type -> Type #

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

type Rep Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Annotation = D1 ('MetaData "Annotation" "Agda.Syntax.Common" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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

type Rep Lock Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Lock = D1 ('MetaData "Lock" "Agda.Syntax.Common" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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

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

Show Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

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

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.2-DXbLWdCWC6QEApzM0094If" '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

Show Origin Source # 
Instance details

Defined in Agda.Syntax.Common

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

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

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

Defined in Agda.Syntax.Common

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

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

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

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

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

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

Show ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

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

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

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

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

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 #

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

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

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

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

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

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

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 #

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

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

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

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

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 #

setNameOf :: LensNamed a => Maybe (NameOf a) -> a -> a Source #

mapNameOf :: LensNamed a => (Maybe (NameOf a) -> Maybe (NameOf a)) -> a -> a 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

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

Defined in Agda.Syntax.Concrete.Pretty

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

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

Show ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Generic ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep ConOrigin :: Type -> Type #

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

type Rep ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep ConOrigin = D1 ('MetaData "ConOrigin" "Agda.Syntax.Common" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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

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

Generic ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep ProjOrigin :: Type -> Type #

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

type Rep ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep ProjOrigin = D1 ('MetaData "ProjOrigin" "Agda.Syntax.Common" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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

Show IsInfix Source # 
Instance details

Defined in Agda.Syntax.Common

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

Show Access Source # 
Instance details

Defined in Agda.Syntax.Common

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

abstract blocks

data IsAbstract Source #

Abstract or concrete.

Constructors

AbstractDef 
ConcreteDef 

Instances

Instances details
Eq IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

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

Generic IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep IsAbstract :: Type -> Type #

Semigroup IsAbstract Source #

Semigroup computes if any of several is an AbstractDef.

Instance details

Defined in Agda.Syntax.Common

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

type Rep IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep IsAbstract = D1 ('MetaData "IsAbstract" "Agda.Syntax.Common" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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

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

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

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

Show IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

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.2-DXbLWdCWC6QEApzM0094If" '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

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

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

Show NameId Source # 
Instance details

Defined in Agda.Syntax.Common

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 #

Hashable NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

hashWithSalt :: Int -> NameId -> Int #

hash :: NameId -> Int #

NFData NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: NameId -> () #

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

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.2-DXbLWdCWC6QEApzM0094If" '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

Real MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Show MetaId Source #

Show non-record version of this newtype.

Instance details

Defined in Agda.Syntax.Common

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 #

Hashable MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

hashWithSalt :: Int -> MetaId -> Int #

hash :: MetaId -> Int #

ToJSON MetaId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

NFData MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: MetaId -> () #

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

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

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

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.2-DXbLWdCWC6QEApzM0094If" '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

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

Real ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Show ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

ToJSON ProblemId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

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

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

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

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

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 Source # 
Instance details

Defined in Agda.Interaction.Base

Real InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Show InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

ToJSON InteractionId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

NFData InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: InteractionId -> () #

NFData InteractionPoints Source # 
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 #

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

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

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

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

Pretty Associativity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

EmbPrj Associativity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Show Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Fixity -> () #

Null Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

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

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

NFData Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Fixity' -> () #

Null Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

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

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

(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) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

(HasRange n, HasRange m) => Semigroup (ImportDirective' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

(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) Source # 
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

(Show m, Show n) => Show (ImportedName' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

(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

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) Source # 
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

(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

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

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.2-DXbLWdCWC6QEApzM0094If" '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

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.2-DXbLWdCWC6QEApzM0094If" '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

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.2-DXbLWdCWC6QEApzM0094If" '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

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

Show GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

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