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

Show Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Delayed Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

File

data FileType Source #

Instances
Eq FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Data FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: FileType -> Constr #

dataTypeOf :: FileType -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Show FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty FileType Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj FileType Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Show HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

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

Induction

data Induction Source #

Constructors

Inductive 
CoInductive 
Instances
Eq Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Data Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Induction -> Constr #

dataTypeOf :: Induction -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Show Induction Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Induction -> () #

Pretty Induction Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Induction Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Hiding

data Overlappable Source #

Constructors

YesOverlap 
NoOverlap 
Instances
Eq Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Data Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Overlappable -> Constr #

dataTypeOf :: Overlappable -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Show Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup Overlappable Source #

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

Instance details

Defined in Agda.Syntax.Common

Monoid Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Overlappable -> () #

data Hiding Source #

Instances
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

Show Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup Hiding Source #

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

Instance details

Defined in Agda.Syntax.Common

Monoid Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Hiding -> () #

Pretty Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

ChooseFlex Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Unquote Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

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

Defined in Agda.Auto.Convert

Methods

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

data WithHiding a Source #

Decorating something with Hiding information.

Constructors

WithHiding 

Fields

Instances
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

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

Methods

rnf :: WithHiding a -> () #

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

Defined in Agda.Syntax.Concrete.Pretty

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

LensHiding (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Defined in Agda.TypeChecking.Pretty

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 #

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

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

Show Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Generic Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Modality :: Type -> Type #

Methods

from :: Modality -> Rep Modality x #

to :: Rep Modality x -> Modality #

Semigroup Modality Source #

Pointwise composition.

Instance details

Defined in Agda.Syntax.Common

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

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-2SkZ65HA0oW2dV5p2oTsQP" 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

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

Show Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Generic Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Quantity :: Type -> Type #

Methods

from :: Quantity -> Rep Quantity x #

to :: Rep Quantity x -> Quantity #

Semigroup Quantity Source #

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Instance details

Defined in Agda.Syntax.Common

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

type Rep Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Quantity = D1 (MetaData "Quantity" "Agda.Syntax.Common" "Agda-2.6.0-2SkZ65HA0oW2dV5p2oTsQP" 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

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

Show Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Generic Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Relevance :: Type -> Type #

Semigroup Relevance Source #

Relevance forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

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

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-2SkZ65HA0oW2dV5p2oTsQP" 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

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

Show Origin Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Origin -> () #

KillRange Origin Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin Origin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

ChooseFlex Origin Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

data WithOrigin a Source #

Decorating something with Origin information.

Constructors

WithOrigin 

Fields

Instances
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

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

Methods

rnf :: WithOrigin a -> () #

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

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

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

Show ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

NFData ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ArgInfo -> () #

KillRange ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

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

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

UniverseBi Args Pattern Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

universeBi :: Args -> [Pattern] #

UniverseBi Args Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

universeBi :: Args -> [Term] #

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

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

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

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

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

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

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

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

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

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

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

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

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