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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Common

Contents

Description

Some common syntactic entities are defined in this module.

Synopsis

Delayed

data Delayed Source #

Used to specify whether something should be delayed.

Constructors

Delayed 
NotDelayed 
Instances
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Delayed -> r

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

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

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

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

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

Ord Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Delayed -> Delayed -> Ordering

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

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

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

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

max :: Delayed -> Delayed -> Delayed

min :: Delayed -> Delayed -> Delayed

Show Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Delayed -> ShowS

show :: Delayed -> String

showList :: [Delayed] -> ShowS

KillRange Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Delayed Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Delayed -> S Int32 Source #

icod_ :: Delayed -> S Int32 Source #

value :: Int32 -> R Delayed Source #

File

data FileType Source #

Instances
Eq FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Data FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: FileType -> Constr

dataTypeOf :: FileType -> DataType

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

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

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

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

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

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

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

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

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

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

Ord FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: FileType -> FileType -> Ordering

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

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

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

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

max :: FileType -> FileType -> FileType

min :: FileType -> FileType -> FileType

Show FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> FileType -> ShowS

show :: FileType -> String

showList :: [FileType] -> ShowS

Pretty FileType Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj FileType Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FileType -> S Int32 Source #

icod_ :: FileType -> S Int32 Source #

value :: Int32 -> R FileType Source #

Eta-equality

data HasEta Source #

Constructors

NoEta 
YesEta 
Instances
Eq HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Data HasEta 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 -> c HasEta

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

toConstr :: HasEta -> Constr

dataTypeOf :: HasEta -> DataType

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

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

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

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

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

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

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

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

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

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

Ord HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: HasEta -> HasEta -> Ordering

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

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

(>) :: HasEta -> HasEta -> Bool

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

max :: HasEta -> HasEta -> HasEta

min :: HasEta -> HasEta -> HasEta

Show HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> HasEta -> ShowS

show :: HasEta -> String

showList :: [HasEta] -> ShowS

NFData HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: HasEta -> ()

KillRange HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj HasEta Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: HasEta -> S Int32 Source #

icod_ :: HasEta -> S Int32 Source #

value :: Int32 -> R HasEta Source #

Induction

data Induction Source #

Constructors

Inductive 
CoInductive 
Instances
Eq Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Data Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Induction -> Constr

dataTypeOf :: Induction -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Induction -> Induction -> Ordering

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

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

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

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

max :: Induction -> Induction -> Induction

min :: Induction -> Induction -> Induction

Show Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Induction -> ShowS

show :: Induction -> String

showList :: [Induction] -> ShowS

NFData Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Induction -> ()

Pretty Induction Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Induction Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Induction -> S Int32 Source #

icod_ :: Induction -> S Int32 Source #

value :: Int32 -> R Induction Source #

Hiding

data Overlappable Source #

Constructors

YesOverlap 
NoOverlap 
Instances
Eq Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Data Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Overlappable -> Constr

dataTypeOf :: Overlappable -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Show Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Overlappable -> ShowS

show :: Overlappable -> String

showList :: [Overlappable] -> ShowS

Semigroup Overlappable Source #

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

Instance details

Defined in Agda.Syntax.Common

Monoid Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Overlappable -> ()

data Hiding Source #

Instances
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Hiding -> r

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

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

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

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

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

Ord Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Hiding -> Hiding -> Ordering

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

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

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

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

max :: Hiding -> Hiding -> Hiding

min :: Hiding -> Hiding -> Hiding

Show Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Hiding -> ShowS

show :: Hiding -> String

showList :: [Hiding] -> ShowS

Semigroup Hiding Source #

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

Instance details

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Hiding -> Hiding

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

Monoid Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Hiding -> ()

Pretty Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Hiding -> S Int32 Source #

icod_ :: Hiding -> S Int32 Source #

value :: Int32 -> R Hiding Source #

ChooseFlex Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Unquote Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

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

Defined in Agda.Auto.Convert

Methods

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

data WithHiding a Source #

Decorating something with Hiding information.

Constructors

WithHiding 

Fields

Instances
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

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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WithHiding a -> r

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

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

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

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

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

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

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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

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

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

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

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> WithHiding a -> ShowS

show :: WithHiding a -> String

showList :: [WithHiding a] -> ShowS

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

Defined in Agda.Syntax.Common

Methods

rnf :: WithHiding a -> ()

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

Defined in Agda.Syntax.Concrete.Pretty

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

LensHiding (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: WithHiding a -> S Int32 Source #

icod_ :: WithHiding a -> S Int32 Source #

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

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

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([WithHiding Name], Dom Type) -> tcm a -> tcm a Source #

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

class LensHiding a where Source #

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

Minimal complete definition

getHiding

Methods

getHiding :: a -> Hiding Source #

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

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

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

Defined in Agda.Syntax.Common

Methods

getHiding :: Dom e -> Hiding Source #

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

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

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

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

Monoidal composition of Hiding information in some data.

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

NotHidden arguments are visible.

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

Instance and Hidden arguments are notVisible.

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

Hidden arguments are hidden.

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

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

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

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

Ignores Overlappable.

Modalities

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.

Instances
Eq Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Data Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Modality -> Constr

dataTypeOf :: Modality -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Modality -> Modality -> Ordering

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

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

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

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

max :: Modality -> Modality -> Modality

min :: Modality -> Modality -> Modality

Show Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Modality -> ShowS

show :: Modality -> String

showList :: [Modality] -> ShowS

Generic Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Modality :: Type -> Type

Methods

from :: Modality -> Rep Modality x

to :: Rep Modality x -> Modality

Semigroup Modality Source #

Pointwise composition.

Instance details

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Modality -> Modality

stimes :: Integral b => b -> Modality -> Modality

Monoid Modality Source #

Pointwise unit.

Instance details

Defined in Agda.Syntax.Common

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

LeftClosedPOMonoid Modality Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid Modality Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup Modality Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality Modality Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Modality Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Modality -> S Int32 Source #

icod_ :: Modality -> S Int32 Source #

value :: Int32 -> R Modality Source #

Unquote Modality Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

type Rep Modality Source # 
Instance details

Defined in Agda.Syntax.Common

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

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

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

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).

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

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

Quantities

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

Zero uses {0}, erased at runtime.

Quantity1

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

Quantityω

Unrestricted use .

Instances
Bounded Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Enum Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Eq Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Data Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Quantity -> Constr

dataTypeOf :: Quantity -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Quantity -> Quantity -> Ordering

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

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

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

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

max :: Quantity -> Quantity -> Quantity

min :: Quantity -> Quantity -> Quantity

Show Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Quantity -> ShowS

show :: Quantity -> String

showList :: [Quantity] -> ShowS

Generic Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Quantity :: Type -> Type

Methods

from :: Quantity -> Rep Quantity x

to :: Rep Quantity x -> Quantity

Semigroup Quantity Source #

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Instance details

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Quantity -> Quantity

stimes :: Integral b => b -> Quantity -> Quantity

Monoid 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

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

LeftClosedPOMonoid Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Quantity -> S Int32 Source #

icod_ :: Quantity -> S Int32 Source #

value :: Int32 -> R Quantity Source #

type Rep Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Quantity = D1 (MetaData "Quantity" "Agda.Syntax.Common" "Agda-2.6.0.1-B0t7sLPZhcP4jvj0wGvNPO" False) (C1 (MetaCons "Quantity0" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Quantity1" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Quantity\969" PrefixI False) (U1 :: Type -> Type)))

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

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

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

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

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.

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

Defined in Agda.Syntax.Common

Enum Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Eq Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Data Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Relevance -> Constr

dataTypeOf :: Relevance -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Relevance Source #

More relevant is smaller.

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Relevance -> Relevance -> Ordering

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

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

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

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

max :: Relevance -> Relevance -> Relevance

min :: Relevance -> Relevance -> Relevance

Show Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Relevance -> ShowS

show :: Relevance -> String

showList :: [Relevance] -> ShowS

Generic Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Relevance :: Type -> Type

Methods

from :: Relevance -> Rep Relevance x

to :: Rep Relevance x -> Relevance

Semigroup Relevance Source #

Relevance forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Relevance -> Relevance

stimes :: Integral b => b -> Relevance -> Relevance

Monoid Relevance Source #

Relevant is the unit.

Instance details

Defined in Agda.Syntax.Common

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

LeftClosedPOMonoid Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup Relevance Source # 
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

LensRelevance Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Relevance -> S Int32 Source #

icod_ :: Relevance -> S Int32 Source #

value :: Int32 -> R Relevance Source #

PrettyTCM Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Unquote Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

type Rep Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Relevance = D1 (MetaData "Relevance" "Agda.Syntax.Common" "Agda-2.6.0.1-B0t7sLPZhcP4jvj0wGvNPO" 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 one of setRelevance or mapRelevance.

Minimal complete definition

getRelevance

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

Defined in Agda.Syntax.Concrete

LensRelevance VarOcc Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

LensRelevance (Dom e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

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

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

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

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

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.

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.

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).

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
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Origin -> r

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

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

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

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

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

Ord Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Origin -> Origin -> Ordering

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

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

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

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

max :: Origin -> Origin -> Origin

min :: Origin -> Origin -> Origin

Show Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Origin -> ShowS

show :: Origin -> String

showList :: [Origin] -> ShowS

NFData Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Origin -> ()

KillRange Origin Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin Origin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Origin -> S Int32 Source #

icod_ :: Origin -> S Int32 Source #

value :: Int32 -> R Origin Source #

ChooseFlex Origin Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

data WithOrigin a Source #

Decorating something with Origin information.

Constructors

WithOrigin 

Fields

Instances
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

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 #

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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WithOrigin a -> r

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

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

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

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

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

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

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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

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

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

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

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> WithOrigin a -> ShowS

show :: WithOrigin a -> String

showList :: [WithOrigin a] -> ShowS

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

Defined in Agda.Syntax.Common

Methods

rnf :: WithOrigin a -> ()

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

class LensOrigin a where Source #

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

Minimal complete definition

getOrigin

Methods

getOrigin :: a -> Origin Source #

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

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

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

Defined in Agda.Syntax.Common

Methods

getOrigin :: Dom e -> Origin Source #

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

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

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

LensOrigin (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Free variable annotations

data FreeVariables Source #

Constructors

UnknownFVs 
KnownFVs IntSet 
Instances
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FreeVariables -> r

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

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

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

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

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

Ord FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Show FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> FreeVariables -> ShowS

show :: FreeVariables -> String

showList :: [FreeVariables] -> ShowS

Semigroup FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

NFData FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: FreeVariables -> ()

LensFreeVariables FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj FreeVariables Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FreeVariables -> S Int32 Source #

icod_ :: FreeVariables -> S Int32 Source #

value :: Int32 -> R FreeVariables Source #

class LensFreeVariables a where Source #

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

Minimal complete definition

getFreeVariables

Argument decoration

data ArgInfo Source #

A function argument can be hidden and/or irrelevant.

Instances
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ArgInfo -> r

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

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

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

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

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

Ord ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: ArgInfo -> ArgInfo -> Ordering

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

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

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

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

max :: ArgInfo -> ArgInfo -> ArgInfo

min :: ArgInfo -> ArgInfo -> ArgInfo

Show ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ArgInfo -> ShowS

show :: ArgInfo -> String

showList :: [ArgInfo] -> ShowS

NFData ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ArgInfo -> ()

KillRange ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

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

LensRelevance ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ArgInfo -> S Int32 Source #

icod_ :: ArgInfo -> S Int32 Source #

value :: Int32 -> R ArgInfo Source #

SynEq ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

ToTerm ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Unquote ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

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 #

Instances
LensArgInfo ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensArgInfo (Dom e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensArgInfo (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

Arguments

data Arg e Source #

Constructors

Arg 

Fields

Instances
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

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

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

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

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

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

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

toList :: Arg a -> [a]

null :: Arg a -> Bool

length :: Arg a -> Int

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

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

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

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

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

Traversable Arg Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

Decoration Arg Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

IsPrefixOf Args Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

UniverseBi Args Pattern Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

universeBi :: Args -> [Pattern] Source #

UniverseBi Args Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

universeBi :: Args -> [Term] 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 #

UniverseBi Declaration (NamedArg Pattern) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg LHSCore) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg Expr) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg BindName) Source # 
Instance details

Defined in Agda.Syntax.Abstract

LensNamed name a => LensNamed name (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

lensNamed :: Lens' (Maybe name) (Arg a) Source #

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

Defined in Agda.Syntax.Internal

Methods

patternVars :: NamedArg (Pattern' a) -> [Arg (Either a Term)] Source #

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

Defined in Agda.Syntax.Internal

Methods

patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)] Source #

Subst t a => Subst t (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> Arg a -> Arg a 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

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

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Arg b -> m (Arg b) 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 #

Eq a => Eq (Arg a) Source #

Ignores Quantity, Relevance, Origin, and FreeVariables. Ignores content of argument if Irrelevant.

Instance details

Defined in Agda.Syntax.Common

Methods

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

(/=) :: Arg a -> Arg a -> 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 :: (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 #

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 #

LensRelevance (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getHiding :: Arg e -> Hiding Source #

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

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

IsProjP a => IsProjP (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

isProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName) Source #

CPatternLike p => CPatternLike (Arg p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Arg p -> m Source #

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Arg p -> m (Arg p) Source #

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Arg p -> m (Arg p) Source #

IsWithP p => IsWithP (Arg p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

isWithP :: Arg p -> Maybe (Arg p) Source #

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

foldExpr :: Monoid m => (Expr -> m) -> Arg a -> m 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 a => Free (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

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 #

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 #

AllNames a => AllNames (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

allNames :: Arg a -> Seq QName Source #

CountPatternVars a => CountPatternVars (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

countPatternVars :: Arg a -> Int Source #

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

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Arg a -> m (Arg a) Source #

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

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Arg a -> m (Arg a) Source #

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

Free a => Free (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Arg a -> FreeT

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 #

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Arg a -> TCM Doc Source #

NamesIn a => NamesIn (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Arg a -> Set QName Source #

PiApplyM a => PiApplyM (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Telescope

Methods

piApplyM :: MonadReduce m => Type -> Arg a -> m Type Source #

IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: Arg a -> TCM Bool Source #

ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

MentionsMeta t => MentionsMeta (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Arg t -> Bool Source #

InstantiateFull t => InstantiateFull (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Arg t -> ReduceM (Arg t) Source #

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

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Arg t -> ReduceM (Arg t) Source #

Simplify t => Simplify (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Arg t -> ReduceM (Arg t) Source #

Reduce t => Reduce (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Arg t -> ReduceM (Arg t) Source #

reduceB' :: Arg t -> ReduceM (Blocked (Arg t)) Source #

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)

SubstWithOrigin (Arg Term) Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

SubstWithOrigin (Arg DisplayTerm) Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

Match a => Match (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

Methods

match :: Arg a -> Arg a -> MaybeT TCM [WithOrigin Term] Source #

UsableModality a => UsableModality (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: Modality -> Arg a -> TCM Bool Source #

UsableRelevance a => UsableRelevance (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Arg a -> TCM Bool Source #

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

Defined in Agda.TypeChecking.Records

Methods

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

ForcedVariables a => ForcedVariables (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Forcing

Methods

forcedVariables :: Arg a -> [(Modality, Nat)] Source #

ComputeOccurrences a => ComputeOccurrences (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

HasPolarity a => HasPolarity (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Polarity

Methods

polarities :: Nat -> Arg a -> TCM [Polarity] Source #

FoldRigid a => FoldRigid (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Arg a -> TCM m Source #

Occurs a => Occurs (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Arg a -> TCM (Arg a) Source #

metaOccurs :: MetaId -> Arg a -> TCM () Source #

ReduceAndEtaContract a => ReduceAndEtaContract (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars

Methods

reduceAndEtaContract :: Arg a -> TCM (Arg a) Source #

NoProjectedVar a => NoProjectedVar (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars

Methods

noProjectedVar :: Arg a -> Either ProjVarExc () Source #

Unquote a => Unquote (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Arg a) 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

PatternVarModalities a x => PatternVarModalities (Arg a) x Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

patternVarModalities :: Arg a -> [(x, Modality)] Source #

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 #

ToAbstract [Arg Term] [NamedArg Expr] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToConcrete a c => ToConcrete (Arg a) (Arg c) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Arg a -> AbsToCon (Arg c) Source #

bindToConcrete :: Arg a -> (Arg c -> AbsToCon b) -> AbsToCon b Source #

Reify i a => Reify (Dom i) (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Dom i -> TCM (Arg a) Source #

reifyWhen :: Bool -> Dom i -> TCM (Arg a) Source #

Reify i a => Reify (Arg i) (Arg a) Source #

Skip reification of implicit and irrelevant args if option is off.

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Arg i -> TCM (Arg a) Source #

reifyWhen :: Bool -> Arg i -> TCM (Arg a) Source #

ToAbstract c a => ToAbstract (Arg c) (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: Arg c -> ScopeM (Arg a) Source #

LabelPatVars a b i => LabelPatVars (Arg a) (Arg b) i Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

labelPatVars :: Arg a -> State [i] (Arg b) Source #

unlabelPatVars :: Arg b -> Arg a 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 #

PatternFrom t a b => PatternFrom (Dom t) (Arg a) (Arg b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> Dom t -> Arg a -> TCM (Arg b) Source #

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([NamedArg Name], Type) -> tcm a -> tcm a Source #

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Arg Name], Type) -> tcm a -> tcm a Source #

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

withArgsFrom :: [a] -> [Arg b] -> [Arg a] Source #

xs `withArgsFrom` args translates xs into a list of Args, using the elements in args to fill in the non-unArg fields.

Precondition: The two lists should have equal length.

Names

class Eq a => Underscore a where Source #

Minimal complete definition

underscore

Methods

underscore :: a Source #

isUnderscore :: a -> Bool Source #

Instances
Underscore String Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

underscore :: String Source #

isUnderscore :: String -> Bool Source #

Underscore ByteString Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

underscore :: ByteString Source #

isUnderscore :: ByteString -> Bool Source #

Underscore Doc Source # 
Instance details

Defined in Agda.Syntax.Common

Underscore QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Underscore Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Underscore Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Function type domain

data Dom e Source #

Similar to Arg, but we need to distinguish an irrelevance annotation in a function domain (the domain itself is not irrelevant!) from an irrelevant argument.

Dom is used in Pi of internal syntax, in Context and Telescope. Arg is used for actual arguments (Var, Con, Def etc.) and in Abstract syntax and other situations.

cubical
When domFinite = True for the domain of a Pi type, the elements should be compared by tabulating the domain type. Only supported in case the domain type is primIsOne, to obtain the correct equality for partial elements.

Constructors

Dom 

Fields

Instances
Functor Dom Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Foldable Dom Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => Dom m -> m

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

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

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

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

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

foldr1 :: (a -> a -> a) -> Dom a -> a

foldl1 :: (a -> a -> a) -> Dom a -> a

toList :: Dom a -> [a]

null :: Dom a -> Bool

length :: Dom a -> Int

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

maximum :: Ord a => Dom a -> a

minimum :: Ord a => Dom a -> a

sum :: Num a => Dom a -> a

product :: Num a => Dom a -> a

Traversable Dom Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

Decoration Dom Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

TelToArgs ListTel Source # 
Instance details

Defined in Agda.Syntax.Internal

TelToArgs Telescope Source # 
Instance details

Defined in Agda.Syntax.Internal

Abstract Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

PrettyTCM Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

TeleNoAbs ListTel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: ListTel -> Term -> Term Source #

TeleNoAbs Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

DropArgs Telescope Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Telescope -> Telescope Source #

AddContext Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Telescope -> tcm a -> tcm a Source #

contextSize :: Telescope -> Nat Source #

Reduce Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reify Telescope Telescope Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Subst t a => Subst t (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> Dom a -> Dom a Source #

Match t a b => Match t (Dom a) (Dom b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> t -> Dom a -> Dom b -> NLM () Source #

PatternFrom t a b => PatternFrom t (Dom a) (Dom b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> t -> Dom a -> TCM (Dom b) Source #

Eq a => Eq (Dom a) Source #

Ignores Origin and FreeVariables.

Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Data e => Data (Dom 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) -> Dom e -> c (Dom e)

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

toConstr :: Dom e -> Constr

dataTypeOf :: Dom e -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Dom e -> Dom e

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

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

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

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

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

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

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

Ord e => Ord (Dom e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Dom e -> Dom e -> Ordering

(<) :: Dom e -> Dom e -> Bool

(<=) :: Dom e -> Dom e -> Bool

(>) :: Dom e -> Dom e -> Bool

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

max :: Dom e -> Dom e -> Dom e

min :: Dom e -> Dom e -> Dom e

Show e => Show (Dom e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Dom e -> ShowS

show :: Dom e -> String

showList :: [Dom e] -> ShowS

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

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Dom a -> Doc Source #

prettyPrec :: Int -> Dom a -> Doc Source #

prettyList :: [Dom a] -> Doc Source #

Pretty a => Pretty (Tele (Dom a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Tele (Dom a) -> Doc Source #

prettyPrec :: Int -> Tele (Dom a) -> Doc Source #

prettyList :: [Tele (Dom a)] -> Doc Source #

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

Methods

getRange :: Dom a -> Range Source #

LensArgInfo (Dom e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensFreeVariables (Dom e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin (Dom e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getOrigin :: Dom e -> Origin Source #

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

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

LensRelevance (Dom e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity (Dom e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality (Dom e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding (Dom e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getHiding :: Dom e -> Hiding Source #

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

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

SgTel (Dom (ArgName, Type)) Source # 
Instance details

Defined in Agda.Syntax.Internal

SgTel (Dom Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

LensSort a => LensSort (Dom a) Source # 
Instance details

Defined in Agda.Syntax.Internal

PrecomputeFreeVars a => PrecomputeFreeVars (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Dom a -> FV (Dom a) Source #

Free a => Free (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

GetDefs a => GetDefs (Dom a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => Dom a -> m () Source #

Free a => Free (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Dom a -> FreeT

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Dom a -> S Int32 Source #

icod_ :: Dom a -> S Int32 Source #

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

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Dom a -> TCM Doc Source #

NamesIn a => NamesIn (Dom a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Dom a -> Set QName Source #

IsSizeType a => IsSizeType (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: Dom a -> TCM (Maybe BoundedSize) Source #

AddContext (Dom (String, Type)) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (String, Type) -> tcm a -> tcm a Source #

contextSize :: Dom (String, Type) -> Nat Source #

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (Name, Type) -> tcm a -> tcm a Source #

contextSize :: Dom (Name, Type) -> Nat Source #

AddContext (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom Type -> tcm a -> tcm a Source #

contextSize :: Dom Type -> Nat Source #

AddContext (KeepNames Telescope) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

MentionsMeta t => MentionsMeta (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Dom t -> Bool Source #

InstantiateFull t => InstantiateFull (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Dom t -> ReduceM (Dom t) Source #

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

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Dom t -> ReduceM (Dom t) Source #

Simplify t => Simplify (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Dom t -> ReduceM (Dom t) Source #

Reduce t => Reduce (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Dom t -> ReduceM (Dom t) Source #

reduceB' :: Dom t -> ReduceM (Blocked (Dom t)) Source #

Instantiate t => Instantiate (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Dom t -> ReduceM (Dom t) Source #

SynEq a => SynEq (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Dom a -> Dom a -> SynEqM (Dom a, Dom a)

synEq' :: Dom a -> Dom a -> SynEqM (Dom a, Dom a)

(Reduce a, ForceNotFree a) => ForceNotFree (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Dom a -> m (Dom a)

UsableModality a => UsableModality (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: Modality -> Dom a -> TCM Bool Source #

UsableRelevance a => UsableRelevance (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Dom a -> TCM Bool Source #

ComputeOccurrences a => ComputeOccurrences (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

HasPolarity a => HasPolarity (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Polarity

Methods

polarities :: Nat -> Dom a -> TCM [Polarity] Source #

FoldRigid a => FoldRigid (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Dom a -> TCM m Source #

Occurs a => Occurs (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Dom a -> TCM (Dom a) Source #

metaOccurs :: MetaId -> Dom a -> TCM () Source #

Unquote a => Unquote (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Dom a) Source #

AbsTerm a => AbsTerm (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Dom a -> Dom a Source #

Reify i a => Reify (Dom i) (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Dom i -> TCM (Arg a) Source #

reifyWhen :: Bool -> Dom i -> TCM (Arg a) 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 #

PatternFrom t a b => PatternFrom (Dom t) (Arg a) (Arg b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> Dom t -> Arg a -> TCM (Arg b) Source #

SgTel (ArgName, Dom Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([WithHiding Name], Dom Type) -> tcm a -> tcm a Source #

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Name], Dom Type) -> tcm a -> tcm a Source #

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

AddContext (String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => (String, Dom Type) -> tcm a -> tcm a Source #

contextSize :: (String, Dom Type) -> Nat Source #

AddContext (Name, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => (Name, Dom Type) -> tcm a -> tcm a Source #

contextSize :: (Name, Dom Type) -> Nat Source #

AddContext (KeepNames String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => (KeepNames String, Dom Type) -> tcm a -> tcm a Source #

contextSize :: (KeepNames String, Dom Type) -> Nat Source #

ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a Source #

Named arguments

data Named name a Source #

Something potentially carrying a name.

Constructors

Named 

Fields

Instances
MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

UniverseBi Declaration (NamedArg Pattern) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg LHSCore) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg Expr) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg BindName) Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Internal

Methods

patternVars :: NamedArg (Pattern' a) -> [Arg (Either a Term)] 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

LensNamed name (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

lensNamed :: Lens' (Maybe name) (Named name a) Source #

Subst t a => Subst t (Named name a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> Named name a -> Named name a Source #

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 #

APatternLike a b => APatternLike a (Named n b) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> Named n b -> m Source #

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Named n b -> m (Named n 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

foldr :: (a -> b -> b) -> b -> Named name a -> b

foldr' :: (a -> b -> b) -> b -> Named name a -> b

foldl :: (b -> a -> b) -> b -> Named name a -> b

foldl' :: (b -> a -> b) -> b -> Named name a -> b

foldr1 :: (a -> a -> a) -> Named name a -> a

foldl1 :: (a -> a -> a) -> Named name a -> a

toList :: Named name a -> [a]

null :: Named name a -> Bool

length :: Named name a -> Int

elem :: Eq a => a -> Named name a -> Bool

maximum :: Ord a => Named name a -> a

minimum :: Ord a => Named name a -> a

sum :: Num a => Named name a -> a

product :: Num a => Named name a -> a

Traversable (Named name) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverse :: Applicative f => (a -> f b) -> Named name a -> f (Named name b)

sequenceA :: Applicative f => Named name (f a) -> f (Named name a)

mapM :: Monad m => (a -> m b) -> Named name a -> m (Named name b)

sequence :: Monad m => Named name (m a) -> m (Named name a)

Decoration (Named name) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Named_ e -> Doc Source #

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

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

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Named_ a -> TCM Doc Source #

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

Defined in Agda.TypeChecking.Records

Methods

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

ToAbstract [Arg Term] [NamedArg Expr] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

(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 :: (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 #

IsProjP a => IsProjP (Named n a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) Source #

CPatternLike p => CPatternLike (Named n p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Named n p -> m Source #

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Named n p -> m (Named n p) Source #

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Named n p -> m (Named n p) Source #

IsWithP p => IsWithP (Named n p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

isWithP :: Named n p -> Maybe (Named n p) Source #

ExprLike a => ExprLike (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> Named name a -> Named name a Source #

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

foldExpr :: Monoid m => (Expr -> m) -> Named name a -> m 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 #

AllNames a => AllNames (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

allNames :: Named name a -> Seq QName Source #

CountPatternVars a => CountPatternVars (Named x a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

countPatternVars :: Named x a -> Int Source #

ExprLike a => ExprLike (Named x a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Named x a -> m (Named x a) Source #

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

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Named x a -> m (Named x a) Source #

mapExpr :: (Expr -> Expr) -> Named x a -> Named x 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 :: Named n a -> Set QName Source #

PiApplyM a => PiApplyM (Named n a) Source # 
Instance details

Defined in Agda.TypeChecking.Telescope

Methods

piApplyM :: MonadReduce m => Type -> Named n a -> m Type Source #

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([NamedArg Name], Type) -> tcm a -> tcm a Source #

contextSize :: ([NamedArg Name], Type) -> Nat 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 #

IsFlexiblePattern a => IsFlexiblePattern (Named name a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

PatternVarModalities a x => PatternVarModalities (Named s a) x Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

patternVarModalities :: Named s a -> [(x, Modality)] 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 #

ToAbstract r a => ToAbstract (Named name r) (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: Named name r -> WithNames (Named name a) Source #

ToConcrete a c => ToConcrete (Named name a) (Named name c) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Named name a -> AbsToCon (Named name c) Source #

bindToConcrete :: Named name a -> (Named name c -> AbsToCon b) -> AbsToCon b Source #

Reify i a => Reify (Named n i) (Named n a) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Named n i -> TCM (Named n a) Source #

reifyWhen :: Bool -> Named n i -> TCM (Named n a) Source #

ToAbstract c a => ToAbstract (Named name c) (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: Named name c -> ScopeM (Named name a) Source #

LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

labelPatVars :: Named x a -> State [i] (Named x b) Source #

unlabelPatVars :: Named x b -> Named x a Source #

type Named_ = Named RString Source #

Standard naming.

unnamed :: a -> Named name a Source #

named :: name -> a -> Named name a Source #

class LensNamed name a | a -> name where Source #

Accessor/editor for the nameOf component.

Methods

lensNamed :: Lens' (Maybe name) a Source #

Instances
LensNamed name a => LensNamed name (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

lensNamed :: Lens' (Maybe name) (Arg a) Source #

LensNamed name (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

lensNamed :: Lens' (Maybe name) (Named name a) Source #

getNameOf :: LensNamed name a => a -> Maybe name Source #

setNameOf :: LensNamed name a => Maybe name -> a -> a Source #

mapNameOf :: LensNamed name a => (Maybe name -> Maybe name) -> a -> a Source #

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.

setNamedArg :: NamedArg a -> b -> NamedArg b Source #

setNamedArg a b = updateNamedArg (const b) a

Range decoration.

data Ranged a Source #

Thing with range info.

Constructors

Ranged 

Fields

Instances
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

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 #

UniverseBi Declaration (NamedArg Pattern) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg LHSCore) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg Expr) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg BindName) Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Internal

Methods

patternVars :: NamedArg (Pattern' a) -> [Arg (Either a Term)] 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 # 
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 :: (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 # 
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 # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: Ranged a -> Doc Source #

prettyPrec :: Int -> Ranged a -> Doc Source #

prettyList :: [Ranged a] -> Doc Source #

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

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Named_ e -> Doc Source #

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

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

KillRange (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Ranged a -> Range Source #

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 #

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Named_ a -> TCM Doc Source #

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

Defined in Agda.TypeChecking.Records

Methods

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

ToAbstract [Arg Term] [NamedArg Expr] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([NamedArg Name], Type) -> tcm a -> tcm a Source #

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

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

Defined in Agda.Syntax.Common

Enum ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Eq ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: ConOrigin -> ConOrigin -> Bool

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

Data ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: ConOrigin -> Constr

dataTypeOf :: ConOrigin -> DataType

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

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

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

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

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

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

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

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

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

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

Ord ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: ConOrigin -> ConOrigin -> Ordering

(<) :: ConOrigin -> ConOrigin -> Bool

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

(>) :: ConOrigin -> ConOrigin -> Bool

(>=) :: ConOrigin -> ConOrigin -> Bool

max :: ConOrigin -> ConOrigin -> ConOrigin

min :: ConOrigin -> ConOrigin -> ConOrigin

Show ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ConOrigin -> ShowS

show :: ConOrigin -> String

showList :: [ConOrigin] -> ShowS

KillRange ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj ConOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ConOrigin -> S Int32 Source #

icod_ :: ConOrigin -> S Int32 Source #

value :: Int32 -> R ConOrigin Source #

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

Defined in Agda.Syntax.Common

Enum ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Eq ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: ProjOrigin -> ProjOrigin -> Bool

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

Data ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: ProjOrigin -> Constr

dataTypeOf :: ProjOrigin -> DataType

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

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

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

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

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

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

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

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

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

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

Ord ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Show ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ProjOrigin -> ShowS

show :: ProjOrigin -> String

showList :: [ProjOrigin] -> ShowS

KillRange ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj ProjOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ProjOrigin -> S Int32 Source #

icod_ :: ProjOrigin -> S Int32 Source #

value :: Int32 -> R ProjOrigin Source #

data DataOrRecord Source #

Constructors

IsData 
IsRecord 
Instances
Eq DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: DataOrRecord -> DataOrRecord -> Bool

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

Data DataOrRecord 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) -> DataOrRecord -> c DataOrRecord

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

toConstr :: DataOrRecord -> Constr

dataTypeOf :: DataOrRecord -> DataType

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

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

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

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

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

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

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

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

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

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

Ord DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Common

Show DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> DataOrRecord -> ShowS

show :: DataOrRecord -> String

showList :: [DataOrRecord] -> ShowS

EmbPrj DataOrRecord Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: DataOrRecord -> S Int32 Source #

icod_ :: DataOrRecord -> S Int32 Source #

value :: Int32 -> R DataOrRecord Source #

Infixity, access, abstract, etc.

data IsInfix Source #

Functions can be defined in both infix and prefix style. See LHS.

Constructors

InfixDef 
PrefixDef 
Instances
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsInfix -> r

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

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

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

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

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

Ord IsInfix Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: IsInfix -> IsInfix -> Ordering

(<) :: IsInfix -> IsInfix -> Bool

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

(>) :: IsInfix -> IsInfix -> Bool

(>=) :: IsInfix -> IsInfix -> Bool

max :: IsInfix -> IsInfix -> IsInfix

min :: IsInfix -> IsInfix -> IsInfix

Show IsInfix Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> IsInfix -> ShowS

show :: IsInfix -> String

showList :: [IsInfix] -> ShowS

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 
OnlyQualified

Visible from outside, but not exported when opening the module Used for qualified constructors.

Instances
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Access -> r

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

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

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

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

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

Ord Access Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Access -> Access -> Ordering

(<) :: Access -> Access -> Bool

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

(>) :: Access -> Access -> Bool

(>=) :: Access -> Access -> Bool

max :: Access -> Access -> Access

min :: Access -> Access -> Access

Show Access Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Access -> ShowS

show :: Access -> String

showList :: [Access] -> ShowS

NFData Access Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Access -> ()

Pretty Access Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Access Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Access Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Access Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Access -> S Int32 Source #

icod_ :: Access -> S Int32 Source #

value :: Int32 -> R Access Source #

data IsAbstract Source #

Abstract or concrete

Constructors

AbstractDef 
ConcreteDef 
Instances
Eq IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: IsAbstract -> IsAbstract -> Bool

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

Data IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: IsAbstract -> Constr

dataTypeOf :: IsAbstract -> DataType

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

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

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

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

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

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

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

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

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

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

Ord IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Show IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> IsAbstract -> ShowS

show :: IsAbstract -> String

showList :: [IsAbstract] -> ShowS

KillRange IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj IsAbstract Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: IsAbstract -> S Int32 Source #

icod_ :: IsAbstract -> S Int32 Source #

value :: Int32 -> R IsAbstract Source #

data IsInstance Source #

Is this definition eligible for instance search?

Instances
Eq IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: IsInstance -> IsInstance -> Bool

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

Data IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: IsInstance -> Constr

dataTypeOf :: IsInstance -> DataType

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

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

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

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

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

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

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

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

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

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

Ord IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Show IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> IsInstance -> ShowS

show :: IsInstance -> String

showList :: [IsInstance] -> ShowS

NFData IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: IsInstance -> ()

KillRange IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

data IsMacro Source #

Is this a macro definition?

Constructors

MacroDef 
NotMacroDef 
Instances
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsMacro -> r

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

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

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

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

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

Ord IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: IsMacro -> IsMacro -> Ordering

(<) :: IsMacro -> IsMacro -> Bool

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

(>) :: IsMacro -> IsMacro -> Bool

(>=) :: IsMacro -> IsMacro -> Bool

max :: IsMacro -> IsMacro -> IsMacro

min :: IsMacro -> IsMacro -> IsMacro

Show IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> IsMacro -> ShowS

show :: IsMacro -> String

showList :: [IsMacro] -> ShowS

KillRange IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

type Nat = Int Source #

type Arity = Nat Source #

NameId

data NameId Source #

The unique identifier of a name. Second argument is the top-level module identifier.

Constructors

NameId !Word64 !Word64 
Instances
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r

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

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

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

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

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

Ord NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: NameId -> NameId -> Ordering

(<) :: NameId -> NameId -> Bool

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

(>) :: NameId -> NameId -> Bool

(>=) :: NameId -> NameId -> Bool

max :: NameId -> NameId -> NameId

min :: NameId -> NameId -> NameId

Show NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> NameId -> ShowS

show :: NameId -> String

showList :: [NameId] -> ShowS

Generic NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep NameId :: Type -> Type

Methods

from :: NameId -> Rep NameId x

to :: Rep NameId x -> NameId

NFData NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: NameId -> ()

Hashable NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

hashWithSalt :: Int -> NameId -> Int

hash :: NameId -> Int

Pretty NameId Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange NameId Source # 
Instance details

Defined in Agda.Syntax.Common

HasFresh NameId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj NameId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NameId -> S Int32 Source #

icod_ :: NameId -> S Int32 Source #

value :: Int32 -> R NameId Source #

type Rep NameId Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep NameId = D1 (MetaData "NameId" "Agda.Syntax.Common" "Agda-2.6.0.1-B0t7sLPZhcP4jvj0wGvNPO" 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 Word64)))

Meta variables

newtype MetaId Source #

A meta variable identifier is just a natural number.

Constructors

MetaId 

Fields

Instances
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r

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

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

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

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

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

Num MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Ord MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: MetaId -> MetaId -> Ordering

(<) :: MetaId -> MetaId -> Bool

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

(>) :: MetaId -> MetaId -> Bool

(>=) :: MetaId -> MetaId -> Bool

max :: MetaId -> MetaId -> MetaId

min :: MetaId -> MetaId -> MetaId

Real MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

toRational :: MetaId -> Rational

Show MetaId Source #

Show non-record version of this newtype.

Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> MetaId -> ShowS

show :: MetaId -> String

showList :: [MetaId] -> ShowS

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

Methods

icode :: MetaId -> S Int32 Source #

icod_ :: MetaId -> S Int32 Source #

value :: Int32 -> R MetaId Source #

PrettyTCM MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

UnFreezeMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MetaId -> TCM () Source #

IsInstantiatedMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

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

Unquote MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Reify MetaId Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MetaId -> TCM Expr Source #

reifyWhen :: Bool -> MetaId -> TCM Expr Source #

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
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PositionInName -> r

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

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

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

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

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

Ord PositionInName Source # 
Instance details

Defined in Agda.Syntax.Common

Show PositionInName Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> PositionInName -> ShowS

show :: PositionInName -> String

showList :: [PositionInName] -> ShowS

data MaybePlaceholder e Source #

Placeholders are used to represent the underscores in a section.

Constructors

Placeholder !PositionInName 
NoPlaceholder !(Maybe PositionInName) e

The second argument is used only (but not always) for name parts other than underscores.

Instances
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

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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MaybePlaceholder e -> r

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

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

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

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

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

Ord e => Ord (MaybePlaceholder e) Source # 
Instance details

Defined in Agda.Syntax.Common

Show e => Show (MaybePlaceholder e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> MaybePlaceholder e -> ShowS

show :: MaybePlaceholder e -> String

showList :: [MaybePlaceholder e] -> ShowS

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

Defined in Agda.Syntax.Common

Methods

rnf :: MaybePlaceholder a -> ()

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

Defined in Agda.Syntax.Concrete.Pretty

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

noPlaceholder :: e -> MaybePlaceholder e Source #

An abbreviation: noPlaceholder = NoPlaceholder Nothing.

Interaction meta variables

newtype InteractionId Source #

Constructors

InteractionId 

Fields

Instances
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InteractionId -> r

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

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

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

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

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

Num InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Ord InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Read InteractionId 
Instance details

Defined in Agda.Interaction.InteractionTop

Methods

readsPrec :: Int -> ReadS InteractionId

readList :: ReadS [InteractionId]

readPrec :: ReadPrec InteractionId

readListPrec :: ReadPrec [InteractionId]

Real InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

toRational :: InteractionId -> Rational

Show InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> InteractionId -> ShowS

show :: InteractionId -> String

showList :: [InteractionId] -> ShowS

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

ToJSON InteractionId 
Instance details

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: InteractionId -> Value

toEncoding :: InteractionId -> Encoding

toJSONList :: [InteractionId] -> Value

toEncodingList :: [InteractionId] -> Encoding

ToConcrete InteractionId Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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
(Eq m, Eq n) => Eq (ImportDirective' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: ImportDirective' n m -> ImportDirective' n m -> Bool

(/=) :: ImportDirective' n m -> ImportDirective' n m -> Bool

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

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ImportDirective' n m -> c (ImportDirective' n m)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ImportDirective' n m)

toConstr :: ImportDirective' n m -> Constr

dataTypeOf :: ImportDirective' n m -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ImportDirective' n m))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ImportDirective' n m))

gmapT :: (forall b. Data b => b -> b) -> ImportDirective' n m -> ImportDirective' n m

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportDirective' n m -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportDirective' n m -> r

gmapQ :: (forall d. Data d => d -> u) -> ImportDirective' n m -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportDirective' n m -> u

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m)

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m)

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m)

(Show a, Show b) => Show (ImportDirective' a b) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> ImportDirective' a b -> ShowS

show :: ImportDirective' a b -> String

showList :: [ImportDirective' a b] -> ShowS

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

(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

data Using' n m Source #

Constructors

UseEverything 
Using [ImportedName' n m] 
Instances
(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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Using' n m -> r

gmapQ :: (forall d. Data d => d -> u) -> Using' n m -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Using' n m -> u

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m)

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m)

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m)

(Show a, Show b) => Show (Using' a b) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Using' a b -> ShowS

show :: Using' a b -> String

showList :: [Using' a b] -> ShowS

Semigroup (Using' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(<>) :: Using' n m -> Using' n m -> Using' n m

sconcat :: NonEmpty (Using' n m) -> Using' n m

stimes :: Integral b => b -> Using' n m -> Using' n m

Monoid (Using' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

mempty :: Using' n m

mappend :: Using' n m -> Using' n m -> Using' n m

mconcat :: [Using' n m] -> Using' n m

(NFData a, NFData b) => NFData (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Using' a b -> ()

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

defaultImportDir :: ImportDirective' n m Source #

Default is directive is private (use everything, but do not export).

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
(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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportedName' n m -> r

gmapQ :: (forall d. Data d => d -> u) -> ImportedName' n m -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportedName' n m -> u

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m)

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m)

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m)

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

Defined in Agda.Syntax.Common

Methods

compare :: ImportedName' n m -> ImportedName' n m -> Ordering

(<) :: ImportedName' n m -> ImportedName' n m -> Bool

(<=) :: ImportedName' n m -> ImportedName' n m -> Bool

(>) :: ImportedName' n m -> ImportedName' n m -> Bool

(>=) :: ImportedName' n m -> ImportedName' n m -> Bool

max :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m

min :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m

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

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ImportedName' n m -> ShowS

show :: ImportedName' n m -> String

showList :: [ImportedName' n m] -> ShowS

(NFData a, NFData b) => NFData (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ImportedName' a b -> ()

(Pretty a, Pretty b) => Pretty (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

(KillRange a, KillRange b) => KillRange (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(HasRange a, HasRange b) => HasRange (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ImportedName' a b -> S Int32 Source #

icod_ :: ImportedName' a b -> S Int32 Source #

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

data Renaming' n m Source #

Constructors

Renaming 

Fields

Instances
(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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' n m -> r

gmapQ :: (forall d. Data d => d -> u) -> Renaming' n m -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Renaming' n m -> u

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m)

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m)

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m)

(Show a, Show b) => Show (Renaming' a b) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Renaming' a b -> ShowS

show :: Renaming' a b -> String

showList :: [Renaming' a b] -> ShowS

(NFData a, NFData b) => NFData (Renaming' a b) Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Renaming' a b -> ()

(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
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TerminationCheck m -> r

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

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

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

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

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

Show m => Show (TerminationCheck m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> TerminationCheck m -> ShowS

show :: TerminationCheck m -> String

showList :: [TerminationCheck m] -> ShowS

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

Defined in Agda.Syntax.Common

Methods

rnf :: TerminationCheck a -> ()

KillRange m => KillRange (TerminationCheck m) Source # 
Instance details

Defined in Agda.Syntax.Common

Positivity

type PositivityCheck = Bool Source #

Positivity check? (Default = True).

Universe checking

data UniverseCheck Source #

Universe check? (Default is yes).

Instances
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UniverseCheck -> r

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

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

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

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

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

Ord UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Show UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> UniverseCheck -> ShowS

show :: UniverseCheck -> String

showList :: [UniverseCheck] -> ShowS

KillRange UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common