Agda.Syntax.Common

Some common syntactic entities are defined in this module.

Delayed

data Delayed

Used to specify whether something should be delayed.

Constructors

Delayed

NotDelayed

Instances

Eq Delayed

Defined in Agda.Syntax.Common

Methods

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

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

Data Delayed

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

Defined in Agda.Syntax.Common

Methods

compare :: Delayed -> Delayed -> Ordering

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

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

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

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

max :: Delayed -> Delayed -> Delayed

min :: Delayed -> Delayed -> Delayed

Show Delayed

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Delayed -> ShowS

show :: Delayed -> String

showList :: [Delayed] -> ShowS

KillRange Delayed

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Delayed

EmbPrj Delayed

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Delayed -> S Int32

icod_ :: Delayed -> S Int32

value :: Int32 -> R Delayed

Eta-equality

data HasEta

Constructors

NoEta

YesEta

Instances

Eq HasEta

Defined in Agda.Syntax.Common

Methods

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

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

Data HasEta

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

Defined in Agda.Syntax.Common

Methods

compare :: HasEta -> HasEta -> Ordering

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

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

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

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

max :: HasEta -> HasEta -> HasEta

min :: HasEta -> HasEta -> HasEta

Show HasEta

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> HasEta -> ShowS

show :: HasEta -> String

showList :: [HasEta] -> ShowS

NFData HasEta

Defined in Agda.Syntax.Common

Methods

rnf :: HasEta -> ()

KillRange HasEta

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT HasEta

HasRange HasEta

Defined in Agda.Syntax.Common

Methods

getRange :: HasEta -> Range

EmbPrj HasEta

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: HasEta -> S Int32

icod_ :: HasEta -> S Int32

value :: Int32 -> R HasEta

Induction

data Induction

Constructors

Inductive

CoInductive

Instances

Eq Induction

Defined in Agda.Syntax.Common

Methods

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

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

Data Induction

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

Defined in Agda.Syntax.Common

Methods

compare :: Induction -> Induction -> Ordering

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

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

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

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

max :: Induction -> Induction -> Induction

min :: Induction -> Induction -> Induction

Show Induction

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Induction -> ShowS

show :: Induction -> String

showList :: [Induction] -> ShowS

NFData Induction

Defined in Agda.Syntax.Common

Methods

rnf :: Induction -> ()

Pretty Induction

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Induction -> Doc

prettyPrec :: Int -> Induction -> Doc

prettyList :: [Induction] -> Doc

KillRange Induction

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Induction

HasRange Induction

Defined in Agda.Syntax.Common

Methods

getRange :: Induction -> Range

EmbPrj Induction

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Induction -> S Int32

icod_ :: Induction -> S Int32

value :: Int32 -> R Induction

Hiding

data Overlappable

Constructors

YesOverlap

NoOverlap

Instances

Eq Overlappable

Defined in Agda.Syntax.Common

Methods

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

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

Data Overlappable

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

Defined in Agda.Syntax.Common

Methods

compare :: Overlappable -> Overlappable -> Ordering

(<) :: Overlappable -> Overlappable -> Bool

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

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

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

max :: Overlappable -> Overlappable -> Overlappable

min :: Overlappable -> Overlappable -> Overlappable

Show Overlappable

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Overlappable -> ShowS

show :: Overlappable -> String

showList :: [Overlappable] -> ShowS

Semigroup Overlappable

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

Defined in Agda.Syntax.Common

Methods

(<>) :: Overlappable -> Overlappable -> Overlappable

sconcat :: NonEmpty Overlappable -> Overlappable

stimes :: Integral b => b -> Overlappable -> Overlappable

Monoid Overlappable

Defined in Agda.Syntax.Common

Methods

mempty :: Overlappable

mappend :: Overlappable -> Overlappable -> Overlappable

mconcat :: [Overlappable] -> Overlappable

NFData Overlappable

Defined in Agda.Syntax.Common

Methods

rnf :: Overlappable -> ()

data Hiding

Constructors

Hidden

Instance Overlappable

NotHidden

Instances

Eq Hiding

Defined in Agda.Syntax.Common

Methods

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

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

Data Hiding

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

Defined in Agda.Syntax.Common

Methods

compare :: Hiding -> Hiding -> Ordering

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

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

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

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

max :: Hiding -> Hiding -> Hiding

min :: Hiding -> Hiding -> Hiding

Show Hiding

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Hiding -> ShowS

show :: Hiding -> String

showList :: [Hiding] -> ShowS

Semigroup Hiding

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

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Hiding -> Hiding

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

Monoid Hiding

Defined in Agda.Syntax.Common

Methods

mempty :: Hiding

mappend :: Hiding -> Hiding -> Hiding

mconcat :: [Hiding] -> Hiding

NFData Hiding

Defined in Agda.Syntax.Common

Methods

rnf :: Hiding -> ()

KillRange Hiding

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Hiding

LensHiding Hiding

Defined in Agda.Syntax.Common

Methods

getHiding :: Hiding -> Hiding

setHiding :: Hiding -> Hiding -> Hiding

mapHiding :: (Hiding -> Hiding) -> Hiding -> Hiding

EmbPrj Hiding

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Hiding -> S Int32

icod_ :: Hiding -> S Int32

value :: Int32 -> R Hiding

ChooseFlex Hiding

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

chooseFlex :: Hiding -> Hiding -> FlexChoice

Unquote Hiding

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Hiding

Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b)

Defined in Agda.Auto.Convert

Methods

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

data WithHiding a

Decorating something with Hiding information.

Constructors

WithHiding

Fields

• whHiding :: !Hiding
• whThing :: a

Instances

Functor WithHiding

Defined in Agda.Syntax.Common

Methods

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

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

Applicative WithHiding

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

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

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

Defined in Agda.Syntax.Common

Methods

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

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

Eq a => Eq (WithHiding a)

Defined in Agda.Syntax.Common

Methods

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

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

Data a => Data (WithHiding a)

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)

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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

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

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

Show a => Show (WithHiding a)

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> WithHiding a -> ShowS

show :: WithHiding a -> String

showList :: [WithHiding a] -> ShowS

NFData a => NFData (WithHiding a)

Defined in Agda.Syntax.Common

Methods

rnf :: WithHiding a -> ()

Pretty a => Pretty (WithHiding a)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: WithHiding a -> Doc

prettyPrec :: Int -> WithHiding a -> Doc

prettyList :: [WithHiding a] -> Doc

KillRange a => KillRange (WithHiding a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (WithHiding a)

SetRange a => SetRange (WithHiding a)

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> WithHiding a -> WithHiding a

HasRange a => HasRange (WithHiding a)

Defined in Agda.Syntax.Common

Methods

getRange :: WithHiding a -> Range

LensHiding (WithHiding a)

Defined in Agda.Syntax.Common

Methods

getHiding :: WithHiding a -> Hiding

setHiding :: Hiding -> WithHiding a -> WithHiding a

mapHiding :: (Hiding -> Hiding) -> WithHiding a -> WithHiding a

EmbPrj a => EmbPrj (WithHiding a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: WithHiding a -> S Int32

icod_ :: WithHiding a -> S Int32

value :: Int32 -> R (WithHiding a)

PrettyTCM a => PrettyTCM (WithHiding a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: WithHiding a -> TCM Doc

ToConcrete a c => ToConcrete (WithHiding a) (WithHiding c)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: WithHiding a -> AbsToCon (WithHiding c)

bindToConcrete :: WithHiding a -> (WithHiding c -> AbsToCon b) -> AbsToCon b

ToAbstract c a => ToAbstract (WithHiding c) (WithHiding a)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: WithHiding c -> ScopeM (WithHiding a)

AddContext ([WithHiding Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

class LensHiding a where

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

setHiding :: Hiding -> a -> a

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

Instances

LensHiding ArgInfo

Defined in Agda.Syntax.Common

Methods

getHiding :: ArgInfo -> Hiding

setHiding :: Hiding -> ArgInfo -> ArgInfo

mapHiding :: (Hiding -> Hiding) -> ArgInfo -> ArgInfo

LensHiding Hiding

Defined in Agda.Syntax.Common

Methods

getHiding :: Hiding -> Hiding

setHiding :: Hiding -> Hiding -> Hiding

mapHiding :: (Hiding -> Hiding) -> Hiding -> Hiding

LensHiding TypedBindings

Defined in Agda.Syntax.Concrete

Methods

getHiding :: TypedBindings -> Hiding

setHiding :: Hiding -> TypedBindings -> TypedBindings

mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings

LensHiding LamBinding

Defined in Agda.Syntax.Concrete

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding

LensHiding TypedBindings

Defined in Agda.Syntax.Abstract

Methods

getHiding :: TypedBindings -> Hiding

setHiding :: Hiding -> TypedBindings -> TypedBindings

mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings

LensHiding LamBinding

Defined in Agda.Syntax.Abstract

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding

LensHiding (Dom e)

Defined in Agda.Syntax.Common

Methods

getHiding :: Dom e -> Hiding

setHiding :: Hiding -> Dom e -> Dom e

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

LensHiding (Arg e)

Defined in Agda.Syntax.Common

Methods

getHiding :: Arg e -> Hiding

setHiding :: Hiding -> Arg e -> Arg e

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

LensHiding (WithHiding a)

Defined in Agda.Syntax.Common

Methods

getHiding :: WithHiding a -> Hiding

setHiding :: Hiding -> WithHiding a -> WithHiding a

mapHiding :: (Hiding -> Hiding) -> WithHiding a -> WithHiding a

LensHiding (FlexibleVar a)

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

getHiding :: FlexibleVar a -> Hiding

setHiding :: Hiding -> FlexibleVar a -> FlexibleVar a

mapHiding :: (Hiding -> Hiding) -> FlexibleVar a -> FlexibleVar a

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

Monoidal composition of Hiding information in some data.

visible :: LensHiding a => a -> Bool

NotHidden arguments are visible.

notVisible :: LensHiding a => a -> Bool

Instance and Hidden arguments are notVisible.

hidden :: LensHiding a => a -> Bool

Hidden arguments are hidden.

hide :: LensHiding a => a -> a

hideOrKeepInstance :: LensHiding a => a -> a

makeInstance :: LensHiding a => a -> a

makeInstance' :: LensHiding a => Overlappable -> a -> a

isOverlappable :: LensHiding a => a -> Bool

isInstance :: LensHiding a => a -> Bool

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

Ignores Overlappable.

Modalities

data Modality

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.

Instances

Eq Modality

Defined in Agda.Syntax.Common

Methods

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

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

Data Modality

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

Defined in Agda.Syntax.Common

Methods

compare :: Modality -> Modality -> Ordering

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

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

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

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

max :: Modality -> Modality -> Modality

min :: Modality -> Modality -> Modality

Show Modality

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Modality -> ShowS

show :: Modality -> String

showList :: [Modality] -> ShowS

Generic Modality

Defined in Agda.Syntax.Common

Associated Types

type Rep Modality :: * -> *

Methods

from :: Modality -> Rep Modality x

to :: Rep Modality x -> Modality

Semigroup Modality

Pointwise composition.

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Modality -> Modality

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

Monoid Modality

Pointwise unit.

Defined in Agda.Syntax.Common

Methods

mempty :: Modality

mappend :: Modality -> Modality -> Modality

mconcat :: [Modality] -> Modality

NFData Modality

Defined in Agda.Syntax.Common

Methods

rnf :: Modality -> ()

PartialOrd Modality

Dominance ordering.

Defined in Agda.Syntax.Common

Methods

comparable :: Comparable Modality

POMonoid Modality

Defined in Agda.Syntax.Common

POSemigroup Modality

Defined in Agda.Syntax.Common

KillRange Modality

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Modality

LensRelevance Modality

Defined in Agda.Syntax.Common

Methods

getRelevance :: Modality -> Relevance

setRelevance :: Relevance -> Modality -> Modality

mapRelevance :: (Relevance -> Relevance) -> Modality -> Modality

LensQuantity Modality

Defined in Agda.Syntax.Common

Methods

getQuantity :: Modality -> Quantity

setQuantity :: Quantity -> Modality -> Modality

mapQuantity :: (Quantity -> Quantity) -> Modality -> Modality

LensModality Modality

Defined in Agda.Syntax.Common

Methods

getModality :: Modality -> Modality

setModality :: Modality -> Modality -> Modality

mapModality :: (Modality -> Modality) -> Modality -> Modality

EmbPrj Modality

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Modality -> S Int32

icod_ :: Modality -> S Int32

value :: Int32 -> R Modality

Unquote Modality

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Modality

type Rep Modality

Defined in Agda.Syntax.Common

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

defaultModality :: Modality

class LensModality a where

Minimal complete definition

getModality

Methods

getModality :: a -> Modality

setModality :: Modality -> a -> a

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

Instances

LensModality ArgInfo

Defined in Agda.Syntax.Common

Methods

getModality :: ArgInfo -> Modality

setModality :: Modality -> ArgInfo -> ArgInfo

mapModality :: (Modality -> Modality) -> ArgInfo -> ArgInfo

LensModality Modality

Defined in Agda.Syntax.Common

Methods

getModality :: Modality -> Modality

setModality :: Modality -> Modality -> Modality

mapModality :: (Modality -> Modality) -> Modality -> Modality

LensModality (Dom e)

Defined in Agda.Syntax.Common

Methods

getModality :: Dom e -> Modality

setModality :: Modality -> Dom e -> Dom e

mapModality :: (Modality -> Modality) -> Dom e -> Dom e

LensModality (Arg e)

Defined in Agda.Syntax.Common

Methods

getModality :: Arg e -> Modality

setModality :: Modality -> Arg e -> Arg e

mapModality :: (Modality -> Modality) -> Arg e -> Arg e

getRelevanceMod :: LensModality a => LensGet Relevance a

setRelevanceMod :: LensModality a => LensSet Relevance a

mapRelevanceMod :: LensModality a => LensMap Relevance a

getQuantityMod :: LensModality a => LensGet Quantity a

setQuantityMod :: LensModality a => LensSet Quantity a

mapQuantityMod :: LensModality a => LensMap Quantity a

Quantities

data Quantity

Quantity for linearity.

Constructors

Quantity0

Zero uses, erased at runtime. TODO: | Quantity1 -- ^ Linear use (could be updated destructively). (needs postponable constraints between quantities to compute uses).

Quantityω

Unrestricted use.

Instances

Bounded Quantity

Defined in Agda.Syntax.Common

Methods

minBound :: Quantity

maxBound :: Quantity

Enum Quantity

Defined in Agda.Syntax.Common

Methods

succ :: Quantity -> Quantity

pred :: Quantity -> Quantity

toEnum :: Int -> Quantity

fromEnum :: Quantity -> Int

enumFrom :: Quantity -> [Quantity]

enumFromThen :: Quantity -> Quantity -> [Quantity]

enumFromTo :: Quantity -> Quantity -> [Quantity]

enumFromThenTo :: Quantity -> Quantity -> Quantity -> [Quantity]

Eq Quantity

Defined in Agda.Syntax.Common

Methods

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

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

Data Quantity

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

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

Defined in Agda.Syntax.Common

Methods

compare :: Quantity -> Quantity -> Ordering

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

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

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

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

max :: Quantity -> Quantity -> Quantity

min :: Quantity -> Quantity -> Quantity

Show Quantity

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Quantity -> ShowS

show :: Quantity -> String

showList :: [Quantity] -> ShowS

Generic Quantity

Defined in Agda.Syntax.Common

Associated Types

type Rep Quantity :: * -> *

Methods

from :: Quantity -> Rep Quantity x

to :: Rep Quantity x -> Quantity

Semigroup Quantity

Composition of quantities (multiplication).

Quantity0 is dominant.

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Quantity -> Quantity

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

Monoid Quantity

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

Defined in Agda.Syntax.Common

Methods

mempty :: Quantity

mappend :: Quantity -> Quantity -> Quantity

mconcat :: [Quantity] -> Quantity

NFData Quantity

Defined in Agda.Syntax.Common

Methods

rnf :: Quantity -> ()

PartialOrd Quantity

Defined in Agda.Syntax.Common

Methods

comparable :: Comparable Quantity

POMonoid Quantity

Defined in Agda.Syntax.Common

POSemigroup Quantity

Defined in Agda.Syntax.Common

KillRange Quantity

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Quantity

LensQuantity Quantity

Defined in Agda.Syntax.Common

Methods

getQuantity :: Quantity -> Quantity

setQuantity :: Quantity -> Quantity -> Quantity

mapQuantity :: (Quantity -> Quantity) -> Quantity -> Quantity

EmbPrj Quantity

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Quantity -> S Int32

icod_ :: Quantity -> S Int32

value :: Int32 -> R Quantity

type Rep Quantity

Defined in Agda.Syntax.Common

type Rep Quantity = D1 (MetaData "Quantity" "Agda.Syntax.Common" "Agda-2.5.4-KW6aUUUGirkK5xqjcQ2M8W" False) (C1 (MetaCons "Quantity0" PrefixI False) (U1 :: * -> *) :+: C1 (MetaCons "Quantity\969" PrefixI False) (U1 :: * -> *))

defaultQuantity :: Quantity

class LensQuantity a where

Minimal complete definition

getQuantity

Methods

getQuantity :: a -> Quantity

setQuantity :: Quantity -> a -> a

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

Instances

LensQuantity ArgInfo

Defined in Agda.Syntax.Common

Methods

getQuantity :: ArgInfo -> Quantity

setQuantity :: Quantity -> ArgInfo -> ArgInfo

mapQuantity :: (Quantity -> Quantity) -> ArgInfo -> ArgInfo

LensQuantity Quantity

Defined in Agda.Syntax.Common

Methods

getQuantity :: Quantity -> Quantity

setQuantity :: Quantity -> Quantity -> Quantity

mapQuantity :: (Quantity -> Quantity) -> Quantity -> Quantity

LensQuantity Modality

Defined in Agda.Syntax.Common

Methods

getQuantity :: Modality -> Quantity

setQuantity :: Quantity -> Modality -> Modality

mapQuantity :: (Quantity -> Quantity) -> Modality -> Modality

LensQuantity (Dom e)

Defined in Agda.Syntax.Common

Methods

getQuantity :: Dom e -> Quantity

setQuantity :: Quantity -> Dom e -> Dom e

mapQuantity :: (Quantity -> Quantity) -> Dom e -> Dom e

LensQuantity (Arg e)

Defined in Agda.Syntax.Common

Methods

getQuantity :: Arg e -> Quantity

setQuantity :: Quantity -> Arg e -> Arg e

mapQuantity :: (Quantity -> Quantity) -> Arg e -> Arg e

Relevance

data Relevance

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

Defined in Agda.Syntax.Common

Methods

minBound :: Relevance

maxBound :: Relevance

Enum Relevance

Defined in Agda.Syntax.Common

Methods

succ :: Relevance -> Relevance

pred :: Relevance -> Relevance

toEnum :: Int -> Relevance

fromEnum :: Relevance -> Int

enumFrom :: Relevance -> [Relevance]

enumFromThen :: Relevance -> Relevance -> [Relevance]

enumFromTo :: Relevance -> Relevance -> [Relevance]

enumFromThenTo :: Relevance -> Relevance -> Relevance -> [Relevance]

Eq Relevance

Defined in Agda.Syntax.Common

Methods

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

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

Data Relevance

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

More relevant is smaller.

Defined in Agda.Syntax.Common

Methods

compare :: Relevance -> Relevance -> Ordering

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

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

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

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

max :: Relevance -> Relevance -> Relevance

min :: Relevance -> Relevance -> Relevance

Show Relevance

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Relevance -> ShowS

show :: Relevance -> String

showList :: [Relevance] -> ShowS

Generic Relevance

Defined in Agda.Syntax.Common

Associated Types

type Rep Relevance :: * -> *

Methods

from :: Relevance -> Rep Relevance x

to :: Rep Relevance x -> Relevance

Semigroup Relevance

Relevance forms a semigroup under composition.

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Relevance -> Relevance

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

Monoid Relevance

Relevant is the unit.

Defined in Agda.Syntax.Common

Methods

mempty :: Relevance

mappend :: Relevance -> Relevance -> Relevance

mconcat :: [Relevance] -> Relevance

NFData Relevance

Defined in Agda.Syntax.Common

Methods

rnf :: Relevance -> ()

PartialOrd Relevance

More relevant is smaller.

Defined in Agda.Syntax.Common

Methods

comparable :: Comparable Relevance

LeftClosedPOMonoid Relevance

Defined in Agda.Syntax.Common

Methods

inverseCompose :: Relevance -> Relevance -> Relevance

POMonoid Relevance

Defined in Agda.Syntax.Common

POSemigroup Relevance

Defined in Agda.Syntax.Common

Pretty Relevance

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Relevance -> Doc

prettyPrec :: Int -> Relevance -> Doc

prettyList :: [Relevance] -> Doc

KillRange Relevance

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Relevance

LensRelevance Relevance

Defined in Agda.Syntax.Common

Methods

getRelevance :: Relevance -> Relevance

setRelevance :: Relevance -> Relevance -> Relevance

mapRelevance :: (Relevance -> Relevance) -> Relevance -> Relevance

EmbPrj Relevance

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Relevance -> S Int32

icod_ :: Relevance -> S Int32

value :: Int32 -> R Relevance

PrettyTCM Relevance

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Relevance -> TCM Doc

Unquote Relevance

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Relevance

type Rep Relevance

Defined in Agda.Syntax.Common

type Rep Relevance = D1 (MetaData "Relevance" "Agda.Syntax.Common" "Agda-2.5.4-KW6aUUUGirkK5xqjcQ2M8W" False) (C1 (MetaCons "Relevant" PrefixI False) (U1 :: * -> *) :+: (C1 (MetaCons "NonStrict" PrefixI False) (U1 :: * -> *) :+: C1 (MetaCons "Irrelevant" PrefixI False) (U1 :: * -> *)))

allRelevances :: [Relevance]

defaultRelevance :: Relevance

class LensRelevance a where

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

Minimal complete definition

getRelevance

Methods

getRelevance :: a -> Relevance

setRelevance :: Relevance -> a -> a

mapRelevance :: (Relevance -> Relevance) -> a -> a

Instances

LensRelevance ArgInfo

Defined in Agda.Syntax.Common

Methods

getRelevance :: ArgInfo -> Relevance

setRelevance :: Relevance -> ArgInfo -> ArgInfo

mapRelevance :: (Relevance -> Relevance) -> ArgInfo -> ArgInfo

LensRelevance Relevance

Defined in Agda.Syntax.Common

Methods

getRelevance :: Relevance -> Relevance

setRelevance :: Relevance -> Relevance -> Relevance

mapRelevance :: (Relevance -> Relevance) -> Relevance -> Relevance

LensRelevance Modality

Defined in Agda.Syntax.Common

Methods

getRelevance :: Modality -> Relevance

setRelevance :: Relevance -> Modality -> Modality

mapRelevance :: (Relevance -> Relevance) -> Modality -> Modality

LensRelevance TypedBindings

Defined in Agda.Syntax.Concrete

Methods

getRelevance :: TypedBindings -> Relevance

setRelevance :: Relevance -> TypedBindings -> TypedBindings

mapRelevance :: (Relevance -> Relevance) -> TypedBindings -> TypedBindings

LensRelevance VarOcc

Defined in Agda.TypeChecking.Free.Lazy

Methods

getRelevance :: VarOcc -> Relevance

setRelevance :: Relevance -> VarOcc -> VarOcc

mapRelevance :: (Relevance -> Relevance) -> VarOcc -> VarOcc

LensRelevance (Dom e)

Defined in Agda.Syntax.Common

Methods

getRelevance :: Dom e -> Relevance

setRelevance :: Relevance -> Dom e -> Dom e

mapRelevance :: (Relevance -> Relevance) -> Dom e -> Dom e

LensRelevance (Arg e)

Defined in Agda.Syntax.Common

Methods

getRelevance :: Arg e -> Relevance

setRelevance :: Relevance -> Arg e -> Arg e

mapRelevance :: (Relevance -> Relevance) -> Arg e -> Arg e

isRelevant :: LensRelevance a => a -> Bool

isIrrelevant :: LensRelevance a => a -> Bool

isNonStrict :: LensRelevance a => a -> Bool

moreRelevant :: Relevance -> Relevance -> Bool

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

unusableRelevance :: LensRelevance a => a -> Bool

unusableRelevance rel == True iff we cannot use a variable of rel.

composeRelevance :: Relevance -> Relevance -> Relevance

Relevance composition. Irrelevant is dominant, Relevant is neutral.

inverseComposeRelevance :: Relevance -> Relevance -> Relevance

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

irrToNonStrict :: Relevance -> Relevance

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

nonStrictToRel :: Relevance -> Relevance

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

nonStrictToIrr :: Relevance -> Relevance

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

data Origin

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.

Instances

Eq Origin

Defined in Agda.Syntax.Common

Methods

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

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

Data Origin

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

Defined in Agda.Syntax.Common

Methods

compare :: Origin -> Origin -> Ordering

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

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

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

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

max :: Origin -> Origin -> Origin

min :: Origin -> Origin -> Origin

Show Origin

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Origin -> ShowS

show :: Origin -> String

showList :: [Origin] -> ShowS

NFData Origin

Defined in Agda.Syntax.Common

Methods

rnf :: Origin -> ()

KillRange Origin

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Origin

LensOrigin Origin

Defined in Agda.Syntax.Common

Methods

getOrigin :: Origin -> Origin

setOrigin :: Origin -> Origin -> Origin

mapOrigin :: (Origin -> Origin) -> Origin -> Origin

EmbPrj Origin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Origin -> S Int32

icod_ :: Origin -> S Int32

value :: Int32 -> R Origin

ChooseFlex Origin

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

chooseFlex :: Origin -> Origin -> FlexChoice

data WithOrigin a

Decorating something with Origin information.

Constructors

WithOrigin

Fields

• woOrigin :: !Origin
• woThing :: a

Instances

Functor WithOrigin

Defined in Agda.Syntax.Common

Methods

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

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

Foldable WithOrigin

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

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

Defined in Agda.Syntax.Common

Methods

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

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

Eq a => Eq (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

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

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

Data a => Data (WithOrigin a)

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)

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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

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

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

Show a => Show (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> WithOrigin a -> ShowS

show :: WithOrigin a -> String

showList :: [WithOrigin a] -> ShowS

NFData a => NFData (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

rnf :: WithOrigin a -> ()

KillRange a => KillRange (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (WithOrigin a)

SetRange a => SetRange (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> WithOrigin a -> WithOrigin a

HasRange a => HasRange (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

getRange :: WithOrigin a -> Range

LensOrigin (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

getOrigin :: WithOrigin a -> Origin

setOrigin :: Origin -> WithOrigin a -> WithOrigin a

mapOrigin :: (Origin -> Origin) -> WithOrigin a -> WithOrigin a

class LensOrigin a where

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

setOrigin :: Origin -> a -> a

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

Instances

LensOrigin ArgInfo

Defined in Agda.Syntax.Common

Methods

getOrigin :: ArgInfo -> Origin

setOrigin :: Origin -> ArgInfo -> ArgInfo

mapOrigin :: (Origin -> Origin) -> ArgInfo -> ArgInfo

LensOrigin Origin

Defined in Agda.Syntax.Common

Methods

getOrigin :: Origin -> Origin

setOrigin :: Origin -> Origin -> Origin

mapOrigin :: (Origin -> Origin) -> Origin -> Origin

LensOrigin AppInfo

Defined in Agda.Syntax.Info

Methods

getOrigin :: AppInfo -> Origin

setOrigin :: Origin -> AppInfo -> AppInfo

mapOrigin :: (Origin -> Origin) -> AppInfo -> AppInfo

LensOrigin (Dom e)

Defined in Agda.Syntax.Common

Methods

getOrigin :: Dom e -> Origin

setOrigin :: Origin -> Dom e -> Dom e

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

LensOrigin (Arg e)

Defined in Agda.Syntax.Common

Methods

getOrigin :: Arg e -> Origin

setOrigin :: Origin -> Arg e -> Arg e

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

LensOrigin (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

getOrigin :: WithOrigin a -> Origin

setOrigin :: Origin -> WithOrigin a -> WithOrigin a

mapOrigin :: (Origin -> Origin) -> WithOrigin a -> WithOrigin a

LensOrigin (Elim' a)

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

Defined in Agda.Syntax.Internal

Methods

getOrigin :: Elim' a -> Origin

setOrigin :: Origin -> Elim' a -> Elim' a

mapOrigin :: (Origin -> Origin) -> Elim' a -> Elim' a

LensOrigin (FlexibleVar a)

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

getOrigin :: FlexibleVar a -> Origin

setOrigin :: Origin -> FlexibleVar a -> FlexibleVar a

mapOrigin :: (Origin -> Origin) -> FlexibleVar a -> FlexibleVar a

Free variable annotations

data FreeVariables

Constructors

UnknownFVs

KnownFVs IntSet

Instances

Eq FreeVariables

Defined in Agda.Syntax.Common

Methods

(==) :: FreeVariables -> FreeVariables -> Bool

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

Data FreeVariables

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

Defined in Agda.Syntax.Common

Methods

compare :: FreeVariables -> FreeVariables -> Ordering

(<) :: FreeVariables -> FreeVariables -> Bool

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

(>) :: FreeVariables -> FreeVariables -> Bool

(>=) :: FreeVariables -> FreeVariables -> Bool

max :: FreeVariables -> FreeVariables -> FreeVariables

min :: FreeVariables -> FreeVariables -> FreeVariables

Show FreeVariables

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> FreeVariables -> ShowS

show :: FreeVariables -> String

showList :: [FreeVariables] -> ShowS

Semigroup FreeVariables

Defined in Agda.Syntax.Common

Methods

(<>) :: FreeVariables -> FreeVariables -> FreeVariables

sconcat :: NonEmpty FreeVariables -> FreeVariables

stimes :: Integral b => b -> FreeVariables -> FreeVariables

Monoid FreeVariables

Defined in Agda.Syntax.Common

Methods

mempty :: FreeVariables

mappend :: FreeVariables -> FreeVariables -> FreeVariables

mconcat :: [FreeVariables] -> FreeVariables

NFData FreeVariables

Defined in Agda.Syntax.Common

Methods

rnf :: FreeVariables -> ()

LensFreeVariables FreeVariables

Defined in Agda.Syntax.Common

Methods

getFreeVariables :: FreeVariables -> FreeVariables

setFreeVariables :: FreeVariables -> FreeVariables -> FreeVariables

mapFreeVariables :: (FreeVariables -> FreeVariables) -> FreeVariables -> FreeVariables

EmbPrj FreeVariables

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FreeVariables -> S Int32

icod_ :: FreeVariables -> S Int32

value :: Int32 -> R FreeVariables

unknownFreeVariables :: FreeVariables

noFreeVariables :: FreeVariables

oneFreeVariable :: Int -> FreeVariables

freeVariablesFromList :: [Int] -> FreeVariables

class LensFreeVariables a where

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

Minimal complete definition

getFreeVariables

Methods

getFreeVariables :: a -> FreeVariables

setFreeVariables :: FreeVariables -> a -> a

mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a

Instances

LensFreeVariables ArgInfo

Defined in Agda.Syntax.Common

Methods

getFreeVariables :: ArgInfo -> FreeVariables

setFreeVariables :: FreeVariables -> ArgInfo -> ArgInfo

mapFreeVariables :: (FreeVariables -> FreeVariables) -> ArgInfo -> ArgInfo

LensFreeVariables FreeVariables

Defined in Agda.Syntax.Common

Methods

getFreeVariables :: FreeVariables -> FreeVariables

setFreeVariables :: FreeVariables -> FreeVariables -> FreeVariables

mapFreeVariables :: (FreeVariables -> FreeVariables) -> FreeVariables -> FreeVariables

LensFreeVariables (Dom e)

Defined in Agda.Syntax.Common

Methods

getFreeVariables :: Dom e -> FreeVariables

setFreeVariables :: FreeVariables -> Dom e -> Dom e

mapFreeVariables :: (FreeVariables -> FreeVariables) -> Dom e -> Dom e

LensFreeVariables (Arg e)

Defined in Agda.Syntax.Common

Methods

getFreeVariables :: Arg e -> FreeVariables

setFreeVariables :: FreeVariables -> Arg e -> Arg e

mapFreeVariables :: (FreeVariables -> FreeVariables) -> Arg e -> Arg e

hasNoFreeVariables :: LensFreeVariables a => a -> Bool

Argument decoration

data ArgInfo

A function argument can be hidden and/or irrelevant.

Constructors

ArgInfo

Fields

• argInfoHiding :: Hiding
• argInfoModality :: Modality
• argInfoOrigin :: Origin
• argInfoFreeVariables :: FreeVariables

Instances

Eq ArgInfo

Defined in Agda.Syntax.Common

Methods

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

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

Data ArgInfo

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

Defined in Agda.Syntax.Common

Methods

compare :: ArgInfo -> ArgInfo -> Ordering

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

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

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

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

max :: ArgInfo -> ArgInfo -> ArgInfo

min :: ArgInfo -> ArgInfo -> ArgInfo

Show ArgInfo

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ArgInfo -> ShowS

show :: ArgInfo -> String

showList :: [ArgInfo] -> ShowS

NFData ArgInfo

Defined in Agda.Syntax.Common

Methods

rnf :: ArgInfo -> ()

KillRange ArgInfo

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT ArgInfo

LensArgInfo ArgInfo

Defined in Agda.Syntax.Common

Methods

getArgInfo :: ArgInfo -> ArgInfo

setArgInfo :: ArgInfo -> ArgInfo -> ArgInfo

mapArgInfo :: (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo

LensFreeVariables ArgInfo

Defined in Agda.Syntax.Common

Methods

getFreeVariables :: ArgInfo -> FreeVariables

setFreeVariables :: FreeVariables -> ArgInfo -> ArgInfo

mapFreeVariables :: (FreeVariables -> FreeVariables) -> ArgInfo -> ArgInfo

LensOrigin ArgInfo

Defined in Agda.Syntax.Common

Methods

getOrigin :: ArgInfo -> Origin

setOrigin :: Origin -> ArgInfo -> ArgInfo

mapOrigin :: (Origin -> Origin) -> ArgInfo -> ArgInfo

LensRelevance ArgInfo

Defined in Agda.Syntax.Common

Methods

getRelevance :: ArgInfo -> Relevance

setRelevance :: Relevance -> ArgInfo -> ArgInfo

mapRelevance :: (Relevance -> Relevance) -> ArgInfo -> ArgInfo

LensQuantity ArgInfo

Defined in Agda.Syntax.Common

Methods

getQuantity :: ArgInfo -> Quantity

setQuantity :: Quantity -> ArgInfo -> ArgInfo

mapQuantity :: (Quantity -> Quantity) -> ArgInfo -> ArgInfo

LensModality ArgInfo

Defined in Agda.Syntax.Common

Methods

getModality :: ArgInfo -> Modality

setModality :: Modality -> ArgInfo -> ArgInfo

mapModality :: (Modality -> Modality) -> ArgInfo -> ArgInfo

LensHiding ArgInfo

Defined in Agda.Syntax.Common

Methods

getHiding :: ArgInfo -> Hiding

setHiding :: Hiding -> ArgInfo -> ArgInfo

mapHiding :: (Hiding -> Hiding) -> ArgInfo -> ArgInfo

EmbPrj ArgInfo

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ArgInfo -> S Int32

icod_ :: ArgInfo -> S Int32

value :: Int32 -> R ArgInfo

SynEq ArgInfo

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

ToTerm ArgInfo

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (ArgInfo -> Term)

toTermR :: TCM (ArgInfo -> ReduceM Term)

Unquote ArgInfo

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM ArgInfo

class LensArgInfo a where

Minimal complete definition

getArgInfo

Methods

getArgInfo :: a -> ArgInfo

setArgInfo :: ArgInfo -> a -> a

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

Instances

LensArgInfo ArgInfo

Defined in Agda.Syntax.Common

Methods

getArgInfo :: ArgInfo -> ArgInfo

setArgInfo :: ArgInfo -> ArgInfo -> ArgInfo

mapArgInfo :: (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo

LensArgInfo (Dom e)

Defined in Agda.Syntax.Common

Methods

getArgInfo :: Dom e -> ArgInfo

setArgInfo :: ArgInfo -> Dom e -> Dom e

mapArgInfo :: (ArgInfo -> ArgInfo) -> Dom e -> Dom e

LensArgInfo (Arg a)

Defined in Agda.Syntax.Common

Methods

getArgInfo :: Arg a -> ArgInfo

setArgInfo :: ArgInfo -> Arg a -> Arg a

mapArgInfo :: (ArgInfo -> ArgInfo) -> Arg a -> Arg a

defaultArgInfo :: ArgInfo

getHidingArgInfo :: LensArgInfo a => LensGet Hiding a

setHidingArgInfo :: LensArgInfo a => LensSet Hiding a

mapHidingArgInfo :: LensArgInfo a => LensMap Hiding a

getModalityArgInfo :: LensArgInfo a => LensGet Modality a

setModalityArgInfo :: LensArgInfo a => LensSet Modality a

mapModalityArgInfo :: LensArgInfo a => LensMap Modality a

getOriginArgInfo :: LensArgInfo a => LensGet Origin a

setOriginArgInfo :: LensArgInfo a => LensSet Origin a

mapOriginArgInfo :: LensArgInfo a => LensMap Origin a

getFreeVariablesArgInfo :: LensArgInfo a => LensGet FreeVariables a

setFreeVariablesArgInfo :: LensArgInfo a => LensSet FreeVariables a

mapFreeVariablesArgInfo :: LensArgInfo a => LensMap FreeVariables a

Arguments

data Arg e

Constructors

Arg

Fields

• argInfo :: ArgInfo
• unArg :: e

Instances

Functor Arg

Defined in Agda.Syntax.Common

Methods

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

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

Foldable Arg

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

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

Defined in Agda.Syntax.Common

Methods

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

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

MapNamedArgPattern NAP

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP

IsPrefixOf Args

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Args -> Args -> Maybe Elims

UniverseBi Args Pattern

Defined in Agda.Syntax.Internal

Methods

universeBi :: Args -> [Pattern]

UniverseBi Args Term

Defined in Agda.Syntax.Internal

Methods

universeBi :: Args -> [Term]

Conversion TOM Args (MM (ArgList O) (RefInfo O))

Defined in Agda.Auto.Convert

Methods

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

PatternVars a (NamedArg (Pattern' a))

Defined in Agda.Syntax.Internal

Methods

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

PatternVars a (Arg (Pattern' a))

Defined in Agda.Syntax.Internal

Methods

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

Subst t a => Subst t (Arg a)

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> Arg a -> Arg a

PatternLike a b => PatternLike a (Arg b)

Defined in Agda.Syntax.Internal.Pattern

Methods

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

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

MapNamedArgPattern a (NamedArg (Pattern' a))

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.

Defined in Agda.Syntax.Internal.Pattern

Methods

mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)

APatternLike a b => APatternLike a (Arg b)

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Arg b -> m (Arg b)

Conversion TOM (Arg Pattern) (Pat O)

Defined in Agda.Auto.Convert

Methods

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

Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b)

Defined in Agda.Auto.Convert

Methods

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

Eq a => Eq (Arg a)

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

Defined in Agda.Syntax.Common

Methods

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

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

Data e => Data (Arg e)

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)

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 a => Show (Arg a)

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Arg a -> ShowS

show :: Arg a -> String

showList :: [Arg a] -> ShowS

NFData e => NFData (Arg e)

Defined in Agda.Syntax.Common

Methods

rnf :: Arg e -> ()

Pretty a => Pretty (Arg a)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Arg a -> Doc

prettyPrec :: Int -> Arg a -> Doc

prettyList :: [Arg a] -> Doc

KillRange a => KillRange (Arg a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Arg a)

SetRange a => SetRange (Arg a)

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Arg a -> Arg a

HasRange a => HasRange (Arg a)

Defined in Agda.Syntax.Common

Methods

getRange :: Arg a -> Range

LensArgInfo (Arg a)

Defined in Agda.Syntax.Common

Methods

getArgInfo :: Arg a -> ArgInfo

setArgInfo :: ArgInfo -> Arg a -> Arg a

mapArgInfo :: (ArgInfo -> ArgInfo) -> Arg a -> Arg a

LensFreeVariables (Arg e)

Defined in Agda.Syntax.Common

Methods

getFreeVariables :: Arg e -> FreeVariables

setFreeVariables :: FreeVariables -> Arg e -> Arg e

mapFreeVariables :: (FreeVariables -> FreeVariables) -> Arg e -> Arg e

LensOrigin (Arg e)

Defined in Agda.Syntax.Common

Methods

getOrigin :: Arg e -> Origin

setOrigin :: Origin -> Arg e -> Arg e

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

LensRelevance (Arg e)

Defined in Agda.Syntax.Common

Methods

getRelevance :: Arg e -> Relevance

setRelevance :: Relevance -> Arg e -> Arg e

mapRelevance :: (Relevance -> Relevance) -> Arg e -> Arg e

LensQuantity (Arg e)

Defined in Agda.Syntax.Common

Methods

getQuantity :: Arg e -> Quantity

setQuantity :: Quantity -> Arg e -> Arg e

mapQuantity :: (Quantity -> Quantity) -> Arg e -> Arg e

LensModality (Arg e)

Defined in Agda.Syntax.Common

Methods

getModality :: Arg e -> Modality

setModality :: Modality -> Arg e -> Arg e

mapModality :: (Modality -> Modality) -> Arg e -> Arg e

LensHiding (Arg e)

Defined in Agda.Syntax.Common

Methods

getHiding :: Arg e -> Hiding

setHiding :: Hiding -> Arg e -> Arg e

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

IsProjP a => IsProjP (Arg a)

Defined in Agda.Syntax.Abstract.Name

Methods

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

CPatternLike p => CPatternLike (Arg p)

Defined in Agda.Syntax.Concrete.Pattern

Methods

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

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

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

IsWithP p => IsWithP (Arg p)

Defined in Agda.Syntax.Concrete.Pattern

Methods

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

ExprLike a => ExprLike (Arg a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

PrecomputeFreeVars a => PrecomputeFreeVars (Arg a)

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Arg a -> FV (Arg a)

Free a => Free (Arg a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Apply [NamedArg (Pattern' a)]

Make sure we only drop variable patterns.

Defined in Agda.TypeChecking.Substitute

Methods

apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)]

applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)]

TermLike a => TermLike (Arg a)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Arg a -> m (Arg a)

foldTerm :: Monoid m => (Term -> m) -> Arg a -> m

GetDefs a => GetDefs (Arg a)

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => Arg a -> m ()

MaybePostfixProjP a => MaybePostfixProjP (Arg a)

Defined in Agda.Syntax.Abstract

Methods

maybePostfixProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName)

SubstExpr a => SubstExpr (Arg a)

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> Arg a -> Arg a

AllNames a => AllNames (Arg a)

Defined in Agda.Syntax.Abstract

Methods

allNames :: Arg a -> Seq QName

CountPatternVars a => CountPatternVars (Arg a)

Defined in Agda.Syntax.Internal.Pattern

Methods

countPatternVars :: Arg a -> Int

ExprLike a => ExprLike (Arg a)

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

Free a => Free (Arg a)

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Arg a -> FreeT

EmbPrj a => EmbPrj (Arg a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Arg a -> S Int32

icod_ :: Arg a -> S Int32

value :: Int32 -> R (Arg a)

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Arg a -> TCM Doc

NamesIn a => NamesIn (Arg a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Arg a -> Set QName

IsInstantiatedMeta a => IsInstantiatedMeta (Arg a)

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: Arg a -> TCM Bool

ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a)

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

expandPatternSynonyms :: Arg a -> TCM (Arg a)

MentionsMeta t => MentionsMeta (Arg t)

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Arg t -> Bool

InstantiateFull t => InstantiateFull (Arg t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Arg t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Arg t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Reduce t => Reduce (Arg t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Instantiate t => Instantiate (Arg t)

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Arg t -> ReduceM (Arg t)

SynEq a => SynEq (Arg a)

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)

SubstWithOrigin (Arg Term)

Defined in Agda.TypeChecking.DisplayForm

Methods

substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg Term -> Arg Term

SubstWithOrigin (Arg DisplayTerm)

Defined in Agda.TypeChecking.DisplayForm

Methods

substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg DisplayTerm -> Arg DisplayTerm

Match a => Match (Arg a)

Defined in Agda.TypeChecking.DisplayForm

Methods

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

NormaliseProjP a => NormaliseProjP (Arg a)

Defined in Agda.TypeChecking.Records

Methods

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

HasPolarity a => HasPolarity (Arg a)

Defined in Agda.TypeChecking.Polarity

Methods

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

UsableRelevance a => UsableRelevance (Arg a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

ForcedVariables a => ForcedVariables (Arg a)

Defined in Agda.TypeChecking.Forcing

Methods

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

ComputeOccurrences a => ComputeOccurrences (Arg a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Arg a -> OccM OccurrencesBuilder

FoldRigid a => FoldRigid (Arg a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs a => Occurs (Arg a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

ReduceAndEtaContract a => ReduceAndEtaContract (Arg a)

Defined in Agda.TypeChecking.MetaVars

Methods

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

NoProjectedVar a => NoProjectedVar (Arg a)

Defined in Agda.TypeChecking.MetaVars

Methods

noProjectedVar :: Arg a -> Either ProjVarExc ()

Unquote a => Unquote (Arg a)

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Arg a)

IsFlexiblePattern a => IsFlexiblePattern (Arg a)

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: Arg a -> MaybeT TCM FlexibleVarKind

isFlexiblePattern :: Arg a -> TCM Bool

AbsTerm a => AbsTerm (Arg a)

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Arg a -> Arg a

PatternVarModalities a x => PatternVarModalities (Arg a) x

Defined in Agda.Syntax.Internal.Pattern

Methods

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

ToConcrete a c => ToConcrete (Arg a) (Arg c)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

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

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

TermToPattern a b => TermToPattern (Arg a) (Arg b)

Defined in Agda.TypeChecking.Patterns.Internal

Methods

termToPattern :: Arg a -> TCM (Arg b)

Reify i a => Reify (Dom i) (Arg a)

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

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

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

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

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

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

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

ToAbstract [Arg Term] [NamedArg Expr]

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: [Arg Term] -> WithNames [NamedArg Expr]

ToAbstract r a => ToAbstract (Arg r) (NamedArg a)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: Arg r -> WithNames (NamedArg a)

Match a b => Match (Arg a) (Arg b)

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Arg a -> Arg b -> NLM ()

PatternFrom a b => PatternFrom (Arg a) (Arg b)

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> Arg a -> TCM (Arg b)

ToAbstract c a => ToAbstract (Arg c) (Arg a)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

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

LabelPatVars a b i => LabelPatVars (Arg a) (Arg b) i

Defined in Agda.Syntax.Internal.Pattern

Methods

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

unlabelPatVars :: Arg b -> Arg a

defaultArg :: a -> Arg a

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

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.

withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a]

Names

class Eq a => Underscore a where

Minimal complete definition

underscore

Methods

underscore :: a

isUnderscore :: a -> Bool

Instances

Underscore String

Defined in Agda.Syntax.Common

Methods

underscore :: String

isUnderscore :: String -> Bool

Underscore ByteString

Defined in Agda.Syntax.Common

Methods

underscore :: ByteString

isUnderscore :: ByteString -> Bool

Underscore Doc

Defined in Agda.Syntax.Common

Methods

underscore :: Doc

isUnderscore :: Doc -> Bool

Underscore QName

Defined in Agda.Syntax.Concrete.Name

Methods

underscore :: QName

isUnderscore :: QName -> Bool

Underscore Name

Defined in Agda.Syntax.Concrete.Name

Methods

underscore :: Name

isUnderscore :: Name -> Bool

Underscore Expr

Defined in Agda.Syntax.Abstract

Methods

underscore :: Expr

isUnderscore :: Expr -> Bool

Function type domain

data Dom e

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.

Constructors

Dom

Fields

• domInfo :: ArgInfo
• unDom :: e

Instances

Functor Dom

Defined in Agda.Syntax.Common

Methods

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

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

Foldable Dom

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

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

Defined in Agda.Syntax.Common

Methods

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

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

TelToArgs ListTel

Defined in Agda.Syntax.Internal

Methods

telToArgs :: ListTel -> [Arg ArgName]

TelToArgs Telescope

Defined in Agda.Syntax.Internal

Methods

telToArgs :: Telescope -> [Arg ArgName]

Abstract Telescope

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Telescope -> Telescope

TeleNoAbs ListTel

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: ListTel -> Term -> Term

TeleNoAbs Telescope

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: Telescope -> Term -> Term

PrettyTCM Telescope

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Telescope -> TCM Doc

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Telescope -> Telescope

AddContext Telescope

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Telescope -> Nat

Reduce Telescope

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Telescope -> ReduceM Telescope

reduceB' :: Telescope -> ReduceM (Blocked Telescope)

Instantiate Telescope

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Telescope -> ReduceM Telescope

Reify Telescope Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Telescope0 -> TCM Telescope

reifyWhen :: Bool -> Telescope0 -> TCM Telescope

Subst t a => Subst t (Dom a)

Defined in Agda.TypeChecking.Substitute

Methods

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

Eq a => Eq (Dom a)

Ignores Origin and FreeVariables.

Defined in Agda.Syntax.Common

Methods

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

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

Data e => Data (Dom e)

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)

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 a => Show (Dom a)

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Dom a -> ShowS

show :: Dom a -> String

showList :: [Dom a] -> ShowS

Pretty a => Pretty (Tele (Dom a))

Defined in Agda.Syntax.Internal

Methods

pretty :: Tele (Dom a) -> Doc

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

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

KillRange a => KillRange (Dom a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Dom a)

HasRange a => HasRange (Dom a)

Defined in Agda.Syntax.Common

Methods

getRange :: Dom a -> Range

LensArgInfo (Dom e)

Defined in Agda.Syntax.Common

Methods

getArgInfo :: Dom e -> ArgInfo

setArgInfo :: ArgInfo -> Dom e -> Dom e

mapArgInfo :: (ArgInfo -> ArgInfo) -> Dom e -> Dom e

LensFreeVariables (Dom e)

Defined in Agda.Syntax.Common

Methods

getFreeVariables :: Dom e -> FreeVariables

setFreeVariables :: FreeVariables -> Dom e -> Dom e

mapFreeVariables :: (FreeVariables -> FreeVariables) -> Dom e -> Dom e

LensOrigin (Dom e)

Defined in Agda.Syntax.Common

Methods

getOrigin :: Dom e -> Origin

setOrigin :: Origin -> Dom e -> Dom e

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

LensRelevance (Dom e)

Defined in Agda.Syntax.Common

Methods

getRelevance :: Dom e -> Relevance

setRelevance :: Relevance -> Dom e -> Dom e

mapRelevance :: (Relevance -> Relevance) -> Dom e -> Dom e

LensQuantity (Dom e)

Defined in Agda.Syntax.Common

Methods

getQuantity :: Dom e -> Quantity

setQuantity :: Quantity -> Dom e -> Dom e

mapQuantity :: (Quantity -> Quantity) -> Dom e -> Dom e

LensModality (Dom e)

Defined in Agda.Syntax.Common

Methods

getModality :: Dom e -> Modality

setModality :: Modality -> Dom e -> Dom e

mapModality :: (Modality -> Modality) -> Dom e -> Dom e

LensHiding (Dom e)

Defined in Agda.Syntax.Common

Methods

getHiding :: Dom e -> Hiding

setHiding :: Hiding -> Dom e -> Dom e

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

SgTel (Dom (ArgName, Type))

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom (ArgName, Type) -> Telescope

SgTel (Dom Type)

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom Type -> Telescope

LensSort a => LensSort (Dom a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort (Dom a)

getSort :: Dom a -> Sort

PrecomputeFreeVars a => PrecomputeFreeVars (Dom a)

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

Free a => Free (Dom a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

TermLike a => TermLike (Dom a)

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

GetDefs a => GetDefs (Dom a)

Defined in Agda.Syntax.Internal.Defs

Methods

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

Free a => Free (Dom a)

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Dom a -> FreeT

EmbPrj a => EmbPrj (Dom a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Dom a -> S Int32

icod_ :: Dom a -> S Int32

value :: Int32 -> R (Dom a)

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Dom a -> TCM Doc

NamesIn a => NamesIn (Dom a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Dom a -> Set QName

IsSizeType a => IsSizeType (Dom a)

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

AddContext (Dom (String, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Dom (Name, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Dom Type -> Nat

AddContext (KeepNames Telescope)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: KeepNames Telescope -> Nat

MentionsMeta t => MentionsMeta (Dom t)

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Dom t -> Bool

InstantiateFull t => InstantiateFull (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Reduce t => Reduce (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Instantiate t => Instantiate (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

SynEq a => SynEq (Dom a)

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)

HasPolarity a => HasPolarity (Dom a)

Defined in Agda.TypeChecking.Polarity

Methods

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

UsableRelevance a => UsableRelevance (Dom a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

ComputeOccurrences a => ComputeOccurrences (Dom a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Dom a -> OccM OccurrencesBuilder

FoldRigid a => FoldRigid (Dom a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs a => Occurs (Dom a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

Unquote a => Unquote (Dom a)

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Dom a)

AbsTerm a => AbsTerm (Dom a)

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Dom a -> Dom a

Reify i a => Reify (Dom i) (Arg a)

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

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

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

Match a b => Match (Dom a) (Dom b)

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

PatternFrom a b => PatternFrom (Dom a) (Dom b)

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

SgTel (ArgName, Dom Type)

Defined in Agda.Syntax.Internal

Methods

sgTel :: (ArgName, Dom Type) -> Telescope

AddContext ([WithHiding Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBindings

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: (Dom r, Name) -> WithNames TypedBindings

argFromDom :: Dom a -> Arg a

domFromArg :: Arg a -> Dom a

defaultDom :: a -> Dom a

Named arguments

data Named name a

Something potentially carrying a name.

Constructors

Named

Fields

• nameOf :: Maybe name
• namedThing :: a

Instances

MapNamedArgPattern NAP

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP

PatternVars a (NamedArg (Pattern' a))

Defined in Agda.Syntax.Internal

Methods

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

MapNamedArgPattern a (NamedArg (Pattern' a))

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.

Defined in Agda.Syntax.Internal.Pattern

Methods

mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)

Subst t a => Subst t (Named name a)

Defined in Agda.TypeChecking.Substitute

Methods

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

PatternLike a b => PatternLike a (Named x b)

Defined in Agda.Syntax.Internal.Pattern

Methods

foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Named x b -> m

traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Named x b -> m (Named x b)

APatternLike a b => APatternLike a (Named n b)

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Named n b -> m (Named n b)

Functor (Named name)

Defined in Agda.Syntax.Common

Methods

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

(<$) :: a -> Named name b -> Named name a

Show a => Show (Named_ a)

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Named_ a -> ShowS

show :: Named_ a -> String

showList :: [Named_ a] -> ShowS

Foldable (Named name)

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)

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)

Defined in Agda.Syntax.Common

Methods

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

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

Pretty e => Pretty (Named_ e)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Named_ e -> Doc

prettyPrec :: Int -> Named_ e -> Doc

prettyList :: [Named_ e] -> Doc

Apply [NamedArg (Pattern' a)]

Make sure we only drop variable patterns.

Defined in Agda.TypeChecking.Substitute

Methods

apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)]

applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)]

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Named_ a -> TCM Doc

NormaliseProjP a => NormaliseProjP (Named_ a)

Defined in Agda.TypeChecking.Records

Methods

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

ToAbstract [Arg Term] [NamedArg Expr]

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: [Arg Term] -> WithNames [NamedArg Expr]

ToAbstract r a => ToAbstract (Arg r) (NamedArg a)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: Arg r -> WithNames (NamedArg a)

(Eq name, Eq a) => Eq (Named name a)

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)

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)

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

(NFData name, NFData a) => NFData (Named name a)

Defined in Agda.Syntax.Common

Methods

rnf :: Named name a -> ()

(KillRange name, KillRange a) => KillRange (Named name a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Named name a)

SetRange a => SetRange (Named name a)

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Named name a -> Named name a

HasRange a => HasRange (Named name a)

Defined in Agda.Syntax.Common

Methods

getRange :: Named name a -> Range

IsProjP a => IsProjP (Named n a)

Defined in Agda.Syntax.Abstract.Name

Methods

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

CPatternLike p => CPatternLike (Named n p)

Defined in Agda.Syntax.Concrete.Pattern

Methods

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

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

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

IsWithP p => IsWithP (Named n p)

Defined in Agda.Syntax.Concrete.Pattern

Methods

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

ExprLike a => ExprLike (Named name a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

foldExpr :: Monoid m => (Expr -> m) -> Named name a -> m

MaybePostfixProjP a => MaybePostfixProjP (Named n a)

Defined in Agda.Syntax.Abstract

Methods

maybePostfixProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName)

SubstExpr a => SubstExpr (Named name a)

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> Named name a -> Named name a

AllNames a => AllNames (Named name a)

Defined in Agda.Syntax.Abstract

Methods

allNames :: Named name a -> Seq QName

CountPatternVars a => CountPatternVars (Named x a)

Defined in Agda.Syntax.Internal.Pattern

Methods

countPatternVars :: Named x a -> Int

ExprLike a => ExprLike (Named x a)

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

mapExpr :: (Expr -> Expr) -> Named x a -> Named x a

(EmbPrj s, EmbPrj t) => EmbPrj (Named s t)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Named s t -> S Int32

icod_ :: Named s t -> S Int32

value :: Int32 -> R (Named s t)

NamesIn a => NamesIn (Named n a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Named n a -> Set QName

ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a)

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

expandPatternSynonyms :: Named n a -> TCM (Named n a)

InstantiateFull t => InstantiateFull (Named name t)

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Named name t -> ReduceM (Named name t)

Normalise t => Normalise (Named name t)

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Named name t -> ReduceM (Named name t)

Simplify t => Simplify (Named name t)

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Named name t -> ReduceM (Named name t)

IsFlexiblePattern a => IsFlexiblePattern (Named name a)

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: Named name a -> MaybeT TCM FlexibleVarKind

isFlexiblePattern :: Named name a -> TCM Bool

PatternVarModalities a x => PatternVarModalities (Named s a) x

Defined in Agda.Syntax.Internal.Pattern

Methods

patternVarModalities :: Named s a -> [(x, Modality)]

ToConcrete a c => ToConcrete (Named name a) (Named name c)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

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

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

TermToPattern a b => TermToPattern (Named c a) (Named c b)

Defined in Agda.TypeChecking.Patterns.Internal

Methods

termToPattern :: Named c a -> TCM (Named c b)

Reify i a => Reify (Named n i) (Named n a)

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

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

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

ToAbstract r a => ToAbstract (Named name r) (Named name a)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

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

ToAbstract c a => ToAbstract (Named name c) (Named name a)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

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

LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i

Defined in Agda.Syntax.Internal.Pattern

Methods

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

unlabelPatVars :: Named x b -> Named x a

type Named_ = Named RString

Standard naming.

unnamed :: a -> Named name a

named :: name -> a -> Named name a

type NamedArg a = Arg (Named_ a)

Only Hidden arguments can have names.

namedArg :: NamedArg a -> a

Get the content of a NamedArg.

defaultNamedArg :: a -> NamedArg a

updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b

The functor instance for NamedArg would be ambiguous, so we give it another name here.

setNamedArg :: NamedArg a -> b -> NamedArg b

setNamedArg a b = updateNamedArg (const b) a

Range decoration.

data Ranged a

Thing with range info.

Constructors

Ranged

Fields

• rangeOf :: Range
• rangedThing :: a

Instances

Functor Ranged

Defined in Agda.Syntax.Common

Methods

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

(<$) :: a -> Ranged b -> Ranged a

Foldable Ranged

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => Ranged m -> m

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

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

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

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

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

foldr1 :: (a -> a -> a) -> Ranged a -> a

foldl1 :: (a -> a -> a) -> Ranged a -> a

toList :: Ranged a -> [a]

null :: Ranged a -> Bool

length :: Ranged a -> Int

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

maximum :: Ord a => Ranged a -> a

minimum :: Ord a => Ranged a -> a

sum :: Num a => Ranged a -> a

product :: Num a => Ranged a -> a

Traversable Ranged

Defined in Agda.Syntax.Common

Methods

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

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

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

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

Decoration Ranged

Defined in Agda.Syntax.Common

Methods

traverseF :: Functor m => (a -> m b) -> Ranged a -> m (Ranged b)

distributeF :: Functor m => Ranged (m a) -> m (Ranged a)

MapNamedArgPattern NAP

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP

UniverseBi Declaration RString

Defined in Agda.Syntax.Abstract

Methods

universeBi :: Declaration -> [RString]

PatternVars a (NamedArg (Pattern' a))

Defined in Agda.Syntax.Internal

Methods

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

MapNamedArgPattern a (NamedArg (Pattern' a))

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.

Defined in Agda.Syntax.Internal.Pattern

Methods

mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)

Eq a => Eq (Ranged a)

Defined in Agda.Syntax.Common

Methods

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

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

Data a => Data (Ranged a)

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Ranged a -> Constr

dataTypeOf :: Ranged a -> DataType

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

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

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

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

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

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

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

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

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

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

Ord a => Ord (Ranged a)

Defined in Agda.Syntax.Common

Methods

compare :: Ranged a -> Ranged a -> Ordering

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

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

(>) :: Ranged a -> Ranged a -> Bool

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

max :: Ranged a -> Ranged a -> Ranged a

min :: Ranged a -> Ranged a -> Ranged a

Show a => Show (Ranged a)

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Ranged a -> ShowS

show :: Ranged a -> String

showList :: [Ranged a] -> ShowS

Show a => Show (Named_ a)

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Named_ a -> ShowS

show :: Named_ a -> String

showList :: [Named_ a] -> ShowS

NFData a => NFData (Ranged a)

Ranges are not forced.

Defined in Agda.Syntax.Common

Methods

rnf :: Ranged a -> ()

Pretty e => Pretty (Named_ e)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Named_ e -> Doc

prettyPrec :: Int -> Named_ e -> Doc

prettyList :: [Named_ e] -> Doc

KillRange (Ranged a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Ranged a)

HasRange (Ranged a)

Defined in Agda.Syntax.Common

Methods

getRange :: Ranged a -> Range

Apply [NamedArg (Pattern' a)]

Make sure we only drop variable patterns.

Defined in Agda.TypeChecking.Substitute

Methods

apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)]

applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)]

EmbPrj a => EmbPrj (Ranged a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Ranged a -> S Int32

icod_ :: Ranged a -> S Int32

value :: Int32 -> R (Ranged a)

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Named_ a -> TCM Doc

NormaliseProjP a => NormaliseProjP (Named_ a)

Defined in Agda.TypeChecking.Records

Methods

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

ToAbstract [Arg Term] [NamedArg Expr]

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: [Arg Term] -> WithNames [NamedArg Expr]

ToAbstract r a => ToAbstract (Arg r) (NamedArg a)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: Arg r -> WithNames (NamedArg a)

unranged :: a -> Ranged a

Thing with no range info.

Raw names (before parsing into name parts).

type RawName = String

A RawName is some sort of string.

rawNameToString :: RawName -> String

stringToRawName :: String -> RawName

type RString = Ranged RawName

String with range info.

Further constructor and projection info

data ConOrigin

Where does the ConP or Con come from?

Constructors

ConOSystem

Inserted by system or expanded from an implicit pattern.

ConOCon

User wrote a constructor (pattern).

ConORec

User wrote a record (pattern).

ConOSplit

Generated by interactive case splitting.

Instances

Bounded ConOrigin

Defined in Agda.Syntax.Common

Methods

minBound :: ConOrigin

maxBound :: ConOrigin

Enum ConOrigin

Defined in Agda.Syntax.Common

Methods

succ :: ConOrigin -> ConOrigin

pred :: ConOrigin -> ConOrigin

toEnum :: Int -> ConOrigin

fromEnum :: ConOrigin -> Int

enumFrom :: ConOrigin -> [ConOrigin]

enumFromThen :: ConOrigin -> ConOrigin -> [ConOrigin]

enumFromTo :: ConOrigin -> ConOrigin -> [ConOrigin]

enumFromThenTo :: ConOrigin -> ConOrigin -> ConOrigin -> [ConOrigin]

Eq ConOrigin

Defined in Agda.Syntax.Common

Methods

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

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

Data ConOrigin

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: ConOrigin -> Constr

dataTypeOf :: ConOrigin -> DataType

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

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

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

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

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

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

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

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

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

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

Ord ConOrigin

Defined in Agda.Syntax.Common

Methods

compare :: ConOrigin -> ConOrigin -> Ordering

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

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

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

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

max :: ConOrigin -> ConOrigin -> ConOrigin

min :: ConOrigin -> ConOrigin -> ConOrigin

Show ConOrigin

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ConOrigin -> ShowS

show :: ConOrigin -> String

showList :: [ConOrigin] -> ShowS

KillRange ConOrigin

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT ConOrigin

EmbPrj ConOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ConOrigin -> S Int32

icod_ :: ConOrigin -> S Int32

value :: Int32 -> R ConOrigin

bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin

Prefer user-written over system-inserted.

data ProjOrigin

Where does a projection come from?

Constructors

ProjPrefix

User wrote a prefix projection.

ProjPostfix

User wrote a postfix projection.

ProjSystem

Projection was generated by the system.

Instances

Bounded ProjOrigin

Defined in Agda.Syntax.Common

Methods

minBound :: ProjOrigin

maxBound :: ProjOrigin

Enum ProjOrigin

Defined in Agda.Syntax.Common

Methods

succ :: ProjOrigin -> ProjOrigin

pred :: ProjOrigin -> ProjOrigin

toEnum :: Int -> ProjOrigin

fromEnum :: ProjOrigin -> Int

enumFrom :: ProjOrigin -> [ProjOrigin]

enumFromThen :: ProjOrigin -> ProjOrigin -> [ProjOrigin]

enumFromTo :: ProjOrigin -> ProjOrigin -> [ProjOrigin]

enumFromThenTo :: ProjOrigin -> ProjOrigin -> ProjOrigin -> [ProjOrigin]

Eq ProjOrigin

Defined in Agda.Syntax.Common

Methods

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

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

Data ProjOrigin

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: ProjOrigin -> Constr

dataTypeOf :: ProjOrigin -> DataType

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

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

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

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

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

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

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

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

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

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

Ord ProjOrigin

Defined in Agda.Syntax.Common

Methods

compare :: ProjOrigin -> ProjOrigin -> Ordering

(<) :: ProjOrigin -> ProjOrigin -> Bool

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

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

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

max :: ProjOrigin -> ProjOrigin -> ProjOrigin

min :: ProjOrigin -> ProjOrigin -> ProjOrigin

Show ProjOrigin

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ProjOrigin -> ShowS

show :: ProjOrigin -> String

showList :: [ProjOrigin] -> ShowS

KillRange ProjOrigin

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT ProjOrigin

EmbPrj ProjOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ProjOrigin -> S Int32

icod_ :: ProjOrigin -> S Int32

value :: Int32 -> R ProjOrigin

data DataOrRecord

Constructors

IsData

IsRecord

Instances

Eq DataOrRecord

Defined in Agda.Syntax.Common

Methods

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

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

Data DataOrRecord

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: DataOrRecord -> Constr

dataTypeOf :: DataOrRecord -> DataType

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

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

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

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

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

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

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

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

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

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

Ord DataOrRecord

Defined in Agda.Syntax.Common

Methods

compare :: DataOrRecord -> DataOrRecord -> Ordering

(<) :: DataOrRecord -> DataOrRecord -> Bool

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

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

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

max :: DataOrRecord -> DataOrRecord -> DataOrRecord

min :: DataOrRecord -> DataOrRecord -> DataOrRecord

Show DataOrRecord

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> DataOrRecord -> ShowS

show :: DataOrRecord -> String

showList :: [DataOrRecord] -> ShowS

EmbPrj DataOrRecord

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: DataOrRecord -> S Int32

icod_ :: DataOrRecord -> S Int32

value :: Int32 -> R DataOrRecord

Infixity, access, abstract, etc.

data IsInfix

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

Constructors

InfixDef

PrefixDef

Instances

Eq IsInfix

Defined in Agda.Syntax.Common

Methods

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

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

Data IsInfix

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: IsInfix -> Constr

dataTypeOf :: IsInfix -> DataType

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

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

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

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

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

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

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

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

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

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

Ord IsInfix

Defined in Agda.Syntax.Common

Methods

compare :: IsInfix -> IsInfix -> Ordering

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

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

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

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

max :: IsInfix -> IsInfix -> IsInfix

min :: IsInfix -> IsInfix -> IsInfix

Show IsInfix

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> IsInfix -> ShowS

show :: IsInfix -> String

showList :: [IsInfix] -> ShowS

data Access

Access modifier.

Constructors

PrivateAccess Origin

Store the Origin of the private block that lead to this qualifier. This is needed for more faithful printing of declarations.

PublicAccess

OnlyQualified

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

Instances

Eq Access

Defined in Agda.Syntax.Common

Methods

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

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

Data Access

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Access -> Constr

dataTypeOf :: Access -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Access

Defined in Agda.Syntax.Common

Methods

compare :: Access -> Access -> Ordering

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

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

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

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

max :: Access -> Access -> Access

min :: Access -> Access -> Access

Show Access

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Access -> ShowS

show :: Access -> String

showList :: [Access] -> ShowS

NFData Access

Defined in Agda.Syntax.Common

Methods

rnf :: Access -> ()

Pretty Access

Defined in Agda.Syntax.Common

Methods

pretty :: Access -> Doc

prettyPrec :: Int -> Access -> Doc

prettyList :: [Access] -> Doc

KillRange Access

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Access

HasRange Access

Defined in Agda.Syntax.Common

Methods

getRange :: Access -> Range

EmbPrj Access

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Access -> S Int32

icod_ :: Access -> S Int32

value :: Int32 -> R Access

data IsAbstract

Abstract or concrete

Constructors

AbstractDef

ConcreteDef

Instances

Eq IsAbstract

Defined in Agda.Syntax.Common

Methods

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

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

Data IsAbstract

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: IsAbstract -> Constr

dataTypeOf :: IsAbstract -> DataType

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

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

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

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

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

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

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

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

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

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

Ord IsAbstract

Defined in Agda.Syntax.Common

Methods

compare :: IsAbstract -> IsAbstract -> Ordering

(<) :: IsAbstract -> IsAbstract -> Bool

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

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

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

max :: IsAbstract -> IsAbstract -> IsAbstract

min :: IsAbstract -> IsAbstract -> IsAbstract

Show IsAbstract

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> IsAbstract -> ShowS

show :: IsAbstract -> String

showList :: [IsAbstract] -> ShowS

KillRange IsAbstract

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT IsAbstract

EmbPrj IsAbstract

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: IsAbstract -> S Int32

icod_ :: IsAbstract -> S Int32

value :: Int32 -> R IsAbstract

data IsInstance

Is this definition eligible for instance search?

Constructors

InstanceDef

NotInstanceDef

Instances

Eq IsInstance

Defined in Agda.Syntax.Common

Methods

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

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

Data IsInstance

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: IsInstance -> Constr

dataTypeOf :: IsInstance -> DataType

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

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

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

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

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

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

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

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

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

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

Ord IsInstance

Defined in Agda.Syntax.Common

Methods

compare :: IsInstance -> IsInstance -> Ordering

(<) :: IsInstance -> IsInstance -> Bool

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

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

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

max :: IsInstance -> IsInstance -> IsInstance

min :: IsInstance -> IsInstance -> IsInstance

Show IsInstance

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> IsInstance -> ShowS

show :: IsInstance -> String

showList :: [IsInstance] -> ShowS

NFData IsInstance

Defined in Agda.Syntax.Common

Methods

rnf :: IsInstance -> ()

KillRange IsInstance

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT IsInstance

HasRange IsInstance

Defined in Agda.Syntax.Common

Methods

getRange :: IsInstance -> Range

data IsMacro

Is this a macro definition?

Constructors

MacroDef

NotMacroDef

Instances

Eq IsMacro

Defined in Agda.Syntax.Common

Methods

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

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

Data IsMacro

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: IsMacro -> Constr

dataTypeOf :: IsMacro -> DataType

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

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

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

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

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

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

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

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

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

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

Ord IsMacro

Defined in Agda.Syntax.Common

Methods

compare :: IsMacro -> IsMacro -> Ordering

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

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

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

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

max :: IsMacro -> IsMacro -> IsMacro

min :: IsMacro -> IsMacro -> IsMacro

Show IsMacro

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> IsMacro -> ShowS

show :: IsMacro -> String

showList :: [IsMacro] -> ShowS

KillRange IsMacro

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT IsMacro

HasRange IsMacro

Defined in Agda.Syntax.Common

Methods

getRange :: IsMacro -> Range

type Nat = Int

type Arity = Nat

NameId

data NameId

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

Constructors

NameId !Word64 !Word64

Instances

Enum NameId

Defined in Agda.Syntax.Common

Methods

succ :: NameId -> NameId

pred :: NameId -> NameId

toEnum :: Int -> NameId

fromEnum :: NameId -> Int

enumFrom :: NameId -> [NameId]

enumFromThen :: NameId -> NameId -> [NameId]

enumFromTo :: NameId -> NameId -> [NameId]

enumFromThenTo :: NameId -> NameId -> NameId -> [NameId]

Eq NameId

Defined in Agda.Syntax.Common

Methods

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

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

Data NameId

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: NameId -> Constr

dataTypeOf :: NameId -> DataType

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

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

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

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

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

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

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

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

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

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

Ord NameId

Defined in Agda.Syntax.Common

Methods

compare :: NameId -> NameId -> Ordering

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

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

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

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

max :: NameId -> NameId -> NameId

min :: NameId -> NameId -> NameId

Show NameId

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> NameId -> ShowS

show :: NameId -> String

showList :: [NameId] -> ShowS

Generic NameId

Defined in Agda.Syntax.Common

Associated Types

type Rep NameId :: * -> *

Methods

from :: NameId -> Rep NameId x

to :: Rep NameId x -> NameId

NFData NameId

Defined in Agda.Syntax.Common

Methods

rnf :: NameId -> ()

Hashable NameId

Defined in Agda.Syntax.Common

Methods

hashWithSalt :: Int -> NameId -> Int

hash :: NameId -> Int

Pretty NameId

Defined in Agda.TypeChecking.Reduce.Fast

Methods

pretty :: NameId -> Doc

prettyPrec :: Int -> NameId -> Doc

prettyList :: [NameId] -> Doc

KillRange NameId

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT NameId

HasFresh NameId

Defined in Agda.TypeChecking.Monad.Base

Methods

freshLens :: Lens' NameId TCState

nextFresh' :: NameId -> NameId

EmbPrj NameId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NameId -> S Int32

icod_ :: NameId -> S Int32

value :: Int32 -> R NameId

type Rep NameId

Defined in Agda.Syntax.Common

type Rep NameId = D1 (MetaData "NameId" "Agda.Syntax.Common" "Agda-2.5.4-KW6aUUUGirkK5xqjcQ2M8W" False) (C1 (MetaCons "NameId" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) SourceUnpack SourceStrict DecidedStrict) (Rec0 Word64) :*: S1 (MetaSel (Nothing :: Maybe Symbol) SourceUnpack SourceStrict DecidedStrict) (Rec0 Word64)))

Meta variables

newtype MetaId

A meta variable identifier is just a natural number.

Constructors

MetaId

Fields

• metaId :: Nat

Instances

Enum MetaId

Defined in Agda.Syntax.Common

Methods

succ :: MetaId -> MetaId

pred :: MetaId -> MetaId

toEnum :: Int -> MetaId

fromEnum :: MetaId -> Int

enumFrom :: MetaId -> [MetaId]

enumFromThen :: MetaId -> MetaId -> [MetaId]

enumFromTo :: MetaId -> MetaId -> [MetaId]

enumFromThenTo :: MetaId -> MetaId -> MetaId -> [MetaId]

Eq MetaId

Defined in Agda.Syntax.Common

Methods

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

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

Integral MetaId

Defined in Agda.Syntax.Common

Methods

quot :: MetaId -> MetaId -> MetaId

rem :: MetaId -> MetaId -> MetaId

div :: MetaId -> MetaId -> MetaId

mod :: MetaId -> MetaId -> MetaId

quotRem :: MetaId -> MetaId -> (MetaId, MetaId)

divMod :: MetaId -> MetaId -> (MetaId, MetaId)

toInteger :: MetaId -> Integer

Data MetaId

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: MetaId -> Constr

dataTypeOf :: MetaId -> DataType

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

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

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

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

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

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

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

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

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

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

Num MetaId

Defined in Agda.Syntax.Common

Methods

(+) :: MetaId -> MetaId -> MetaId

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

(*) :: MetaId -> MetaId -> MetaId

negate :: MetaId -> MetaId

abs :: MetaId -> MetaId

signum :: MetaId -> MetaId

fromInteger :: Integer -> MetaId

Ord MetaId

Defined in Agda.Syntax.Common

Methods

compare :: MetaId -> MetaId -> Ordering

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

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

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

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

max :: MetaId -> MetaId -> MetaId

min :: MetaId -> MetaId -> MetaId

Real MetaId

Defined in Agda.Syntax.Common

Methods

toRational :: MetaId -> Rational

Show MetaId

Show non-record version of this newtype.

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> MetaId -> ShowS

show :: MetaId -> String

showList :: [MetaId] -> ShowS

NFData MetaId

Defined in Agda.Syntax.Common

Methods

rnf :: MetaId -> ()

Pretty MetaId

Defined in Agda.Syntax.Common

Methods

pretty :: MetaId -> Doc

prettyPrec :: Int -> MetaId -> Doc

prettyList :: [MetaId] -> Doc

GetDefs MetaId

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => MetaId -> m ()

HasFresh MetaId

Defined in Agda.TypeChecking.Monad.Base

Methods

freshLens :: Lens' MetaId TCState

nextFresh' :: MetaId -> MetaId

EmbPrj MetaId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: MetaId -> S Int32

icod_ :: MetaId -> S Int32

value :: Int32 -> R MetaId

PrettyTCM MetaId

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MetaId -> TCM Doc

UnFreezeMeta MetaId

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MetaId -> TCM ()

IsInstantiatedMeta MetaId

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: MetaId -> TCM Bool

FromTerm MetaId

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction MetaId)

ToTerm MetaId

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (MetaId -> Term)

toTermR :: TCM (MetaId -> ReduceM Term)

PrimTerm MetaId

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: MetaId -> TCM Term

Unquote MetaId

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM MetaId

Reify MetaId Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MetaId -> TCM Expr

reifyWhen :: Bool -> MetaId -> TCM Expr

newtype Constr a

Constructors

Constr a

Instances

ToConcrete (Constr Constructor) Declaration

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Constr Constructor -> AbsToCon Declaration

bindToConcrete :: Constr Constructor -> (Declaration -> AbsToCon b) -> AbsToCon b

Placeholders (used to parse sections)

data PositionInName

The position of a name part or underscore in a name.

Constructors

Beginning

The following underscore is at the beginning of the name: _foo.

Middle

The following underscore is in the middle of the name: foo_bar.

End

The following underscore is at the end of the name: foo_.

Instances

Eq PositionInName

Defined in Agda.Syntax.Common

Methods

(==) :: PositionInName -> PositionInName -> Bool

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

Data PositionInName

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: PositionInName -> Constr

dataTypeOf :: PositionInName -> DataType

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

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

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

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

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

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

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

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

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

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

Ord PositionInName

Defined in Agda.Syntax.Common

Methods

compare :: PositionInName -> PositionInName -> Ordering

(<) :: PositionInName -> PositionInName -> Bool

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

(>) :: PositionInName -> PositionInName -> Bool

(>=) :: PositionInName -> PositionInName -> Bool

max :: PositionInName -> PositionInName -> PositionInName

min :: PositionInName -> PositionInName -> PositionInName

Show PositionInName

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> PositionInName -> ShowS

show :: PositionInName -> String

showList :: [PositionInName] -> ShowS

data MaybePlaceholder e

Placeholders are used to represent the underscores in a section.

Constructors

Placeholder !PositionInName

NoPlaceholder !(Maybe PositionInName) e

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

Instances

Functor MaybePlaceholder

Defined in Agda.Syntax.Common

Methods

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

(<$) :: a -> MaybePlaceholder b -> MaybePlaceholder a

Foldable MaybePlaceholder

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => MaybePlaceholder m -> m

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

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

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

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

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

foldr1 :: (a -> a -> a) -> MaybePlaceholder a -> a

foldl1 :: (a -> a -> a) -> MaybePlaceholder a -> a

toList :: MaybePlaceholder a -> [a]

null :: MaybePlaceholder a -> Bool

length :: MaybePlaceholder a -> Int

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

maximum :: Ord a => MaybePlaceholder a -> a

minimum :: Ord a => MaybePlaceholder a -> a

sum :: Num a => MaybePlaceholder a -> a

product :: Num a => MaybePlaceholder a -> a

Traversable MaybePlaceholder

Defined in Agda.Syntax.Common

Methods

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

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

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

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

Eq e => Eq (MaybePlaceholder e)

Defined in Agda.Syntax.Common

Methods

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

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

Data e => Data (MaybePlaceholder e)

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: MaybePlaceholder e -> Constr

dataTypeOf :: MaybePlaceholder e -> DataType

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

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

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

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

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

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

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

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

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

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

Ord e => Ord (MaybePlaceholder e)

Defined in Agda.Syntax.Common

Methods

compare :: MaybePlaceholder e -> MaybePlaceholder e -> Ordering

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

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

(>) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool

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

max :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e

min :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e

Show e => Show (MaybePlaceholder e)

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> MaybePlaceholder e -> ShowS

show :: MaybePlaceholder e -> String

showList :: [MaybePlaceholder e] -> ShowS

NFData a => NFData (MaybePlaceholder a)

Defined in Agda.Syntax.Common

Methods

rnf :: MaybePlaceholder a -> ()

Pretty a => Pretty (MaybePlaceholder a)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: MaybePlaceholder a -> Doc

prettyPrec :: Int -> MaybePlaceholder a -> Doc

prettyList :: [MaybePlaceholder a] -> Doc

KillRange a => KillRange (MaybePlaceholder a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (MaybePlaceholder a)

HasRange a => HasRange (MaybePlaceholder a)

Defined in Agda.Syntax.Common

Methods

getRange :: MaybePlaceholder a -> Range

ExprLike a => ExprLike (MaybePlaceholder a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

noPlaceholder :: e -> MaybePlaceholder e

An abbreviation: noPlaceholder = NoPlaceholder Nothing.

Interaction meta variables

newtype InteractionId

Constructors

InteractionId

Fields

• interactionId :: Nat

Instances

Enum InteractionId

Defined in Agda.Syntax.Common

Methods

succ :: InteractionId -> InteractionId

pred :: InteractionId -> InteractionId

toEnum :: Int -> InteractionId

fromEnum :: InteractionId -> Int

enumFrom :: InteractionId -> [InteractionId]

enumFromThen :: InteractionId -> InteractionId -> [InteractionId]

enumFromTo :: InteractionId -> InteractionId -> [InteractionId]

enumFromThenTo :: InteractionId -> InteractionId -> InteractionId -> [InteractionId]

Eq InteractionId

Defined in Agda.Syntax.Common

Methods

(==) :: InteractionId -> InteractionId -> Bool

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

Integral InteractionId

Defined in Agda.Syntax.Common

Methods

quot :: InteractionId -> InteractionId -> InteractionId

rem :: InteractionId -> InteractionId -> InteractionId

div :: InteractionId -> InteractionId -> InteractionId

mod :: InteractionId -> InteractionId -> InteractionId

quotRem :: InteractionId -> InteractionId -> (InteractionId, InteractionId)

divMod :: InteractionId -> InteractionId -> (InteractionId, InteractionId)

toInteger :: InteractionId -> Integer

Data InteractionId

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: InteractionId -> Constr

dataTypeOf :: InteractionId -> DataType

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

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

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

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

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

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

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

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

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

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

Num InteractionId

Defined in Agda.Syntax.Common

Methods

(+) :: InteractionId -> InteractionId -> InteractionId

(-) :: InteractionId -> InteractionId -> InteractionId

(*) :: InteractionId -> InteractionId -> InteractionId

negate :: InteractionId -> InteractionId

abs :: InteractionId -> InteractionId

signum :: InteractionId -> InteractionId

fromInteger :: Integer -> InteractionId

Ord InteractionId

Defined in Agda.Syntax.Common

Methods

compare :: InteractionId -> InteractionId -> Ordering

(<) :: InteractionId -> InteractionId -> Bool

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

(>) :: InteractionId -> InteractionId -> Bool

(>=) :: InteractionId -> InteractionId -> Bool

max :: InteractionId -> InteractionId -> InteractionId

min :: InteractionId -> InteractionId -> InteractionId

Read InteractionId

Defined in Agda.Interaction.InteractionTop

Methods

readsPrec :: Int -> ReadS InteractionId

readList :: ReadS [InteractionId]

readPrec :: ReadPrec InteractionId

readListPrec :: ReadPrec [InteractionId]

Real InteractionId

Defined in Agda.Syntax.Common

Methods

toRational :: InteractionId -> Rational

Show InteractionId

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> InteractionId -> ShowS

show :: InteractionId -> String

showList :: [InteractionId] -> ShowS

KillRange InteractionId

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT InteractionId

HasFresh InteractionId

Defined in Agda.TypeChecking.Monad.Base

Methods

freshLens :: Lens' InteractionId TCState

nextFresh' :: InteractionId -> InteractionId

ToConcrete InteractionId Expr

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: InteractionId -> AbsToCon Expr

bindToConcrete :: InteractionId -> (Expr -> AbsToCon b) -> AbsToCon b

Import directive

data ImportDirective' a b

The things you are allowed to say when you shuffle names between name spaces (i.e. in import, namespace, or open declarations).

Constructors

ImportDirective

Fields

• importDirRange :: Range
• using :: Using' a b
• hiding :: [ImportedName' a b]
• impRenaming :: [Renaming' a b]
• publicOpen :: Bool

  Only for open. Exports the opened names from the current module.

Instances

(Eq b, Eq a) => Eq (ImportDirective' a b)

Defined in Agda.Syntax.Common

Methods

(==) :: ImportDirective' a b -> ImportDirective' a b -> Bool

(/=) :: ImportDirective' a b -> ImportDirective' a b -> Bool

(Data a, Data b) => Data (ImportDirective' a b)

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: ImportDirective' a b -> Constr

dataTypeOf :: ImportDirective' a b -> DataType

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

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

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

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

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

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

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

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

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

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

(Pretty a, Pretty b) => Show (ImportDirective' a b)

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> ImportDirective' a b -> ShowS

show :: ImportDirective' a b -> String

showList :: [ImportDirective' a b] -> ShowS

(NFData a, NFData b) => NFData (ImportDirective' a b)

Ranges are not forced.

Defined in Agda.Syntax.Common

Methods

rnf :: ImportDirective' a b -> ()

(Pretty a, Pretty b) => Pretty (ImportDirective' a b)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ImportDirective' a b -> Doc

prettyPrec :: Int -> ImportDirective' a b -> Doc

prettyList :: [ImportDirective' a b] -> Doc

(KillRange a, KillRange b) => KillRange (ImportDirective' a b)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (ImportDirective' a b)

(HasRange a, HasRange b) => HasRange (ImportDirective' a b)

Defined in Agda.Syntax.Common

Methods

getRange :: ImportDirective' a b -> Range

data Using' a b

Constructors

UseEverything

Using [ImportedName' a b]

Instances

(Eq b, Eq a) => Eq (Using' a b)

Defined in Agda.Syntax.Common

Methods

(==) :: Using' a b -> Using' a b -> Bool

(/=) :: Using' a b -> Using' a b -> Bool

(Data a, Data b) => Data (Using' a b)

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Using' a b -> Constr

dataTypeOf :: Using' a b -> DataType

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

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

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

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

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

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

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

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

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

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

Semigroup (Using' a b)

Defined in Agda.Syntax.Common

Methods

(<>) :: Using' a b -> Using' a b -> Using' a b

sconcat :: NonEmpty (Using' a b) -> Using' a b

stimes :: Integral b0 => b0 -> Using' a b -> Using' a b

Monoid (Using' a b)

Defined in Agda.Syntax.Common

Methods

mempty :: Using' a b

mappend :: Using' a b -> Using' a b -> Using' a b

mconcat :: [Using' a b] -> Using' a b

(NFData a, NFData b) => NFData (Using' a b)

Defined in Agda.Syntax.Common

Methods

rnf :: Using' a b -> ()

(Pretty a, Pretty b) => Pretty (Using' a b)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Using' a b -> Doc

prettyPrec :: Int -> Using' a b -> Doc

prettyList :: [Using' a b] -> Doc

(KillRange a, KillRange b) => KillRange (Using' a b)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Using' a b)

(HasRange a, HasRange b) => HasRange (Using' a b)

Defined in Agda.Syntax.Common

Methods

getRange :: Using' a b -> Range

defaultImportDir :: ImportDirective' a b

Default is directive is private (use everything, but do not export).

isDefaultImportDir :: ImportDirective' a b -> Bool

data ImportedName' a b

An imported name can be a module or a defined name

Constructors

ImportedModule b

ImportedName a

Instances

(Eq b, Eq a) => Eq (ImportedName' a b)

Defined in Agda.Syntax.Common

Methods

(==) :: ImportedName' a b -> ImportedName' a b -> Bool

(/=) :: ImportedName' a b -> ImportedName' a b -> Bool

(Data a, Data b) => Data (ImportedName' a b)

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: ImportedName' a b -> Constr

dataTypeOf :: ImportedName' a b -> DataType

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

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

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

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

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

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

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

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

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

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

(Ord b, Ord a) => Ord (ImportedName' a b)

Defined in Agda.Syntax.Common

Methods

compare :: ImportedName' a b -> ImportedName' a b -> Ordering

(<) :: ImportedName' a b -> ImportedName' a b -> Bool

(<=) :: ImportedName' a b -> ImportedName' a b -> Bool

(>) :: ImportedName' a b -> ImportedName' a b -> Bool

(>=) :: ImportedName' a b -> ImportedName' a b -> Bool

max :: ImportedName' a b -> ImportedName' a b -> ImportedName' a b

min :: ImportedName' a b -> ImportedName' a b -> ImportedName' a b

(Show a, Show b) => Show (ImportedName' a b)

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ImportedName' a b -> ShowS

show :: ImportedName' a b -> String

showList :: [ImportedName' a b] -> ShowS

(NFData a, NFData b) => NFData (ImportedName' a b)

Defined in Agda.Syntax.Common

Methods

rnf :: ImportedName' a b -> ()

(Pretty a, Pretty b) => Pretty (ImportedName' a b)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ImportedName' a b -> Doc

prettyPrec :: Int -> ImportedName' a b -> Doc

prettyList :: [ImportedName' a b] -> Doc

(KillRange a, KillRange b) => KillRange (ImportedName' a b)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (ImportedName' a b)

(HasRange a, HasRange b) => HasRange (ImportedName' a b)

Defined in Agda.Syntax.Common

Methods

getRange :: ImportedName' a b -> Range

setImportedName :: ImportedName' a a -> a -> ImportedName' a a

data Renaming' a b

Constructors

Renaming

Fields

• renFrom :: ImportedName' a b

  Rename from this name.

• renTo :: ImportedName' a b

  To this one. Must be same kind as renFrom.

• renToRange :: Range

  The range of the "to" keyword. Retained for highlighting purposes.

Instances

(Eq b, Eq a) => Eq (Renaming' a b)

Defined in Agda.Syntax.Common

Methods

(==) :: Renaming' a b -> Renaming' a b -> Bool

(/=) :: Renaming' a b -> Renaming' a b -> Bool

(Data a, Data b) => Data (Renaming' a b)

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Renaming' a b -> Constr

dataTypeOf :: Renaming' a b -> DataType

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

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

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

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

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

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

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

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

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

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

(NFData a, NFData b) => NFData (Renaming' a b)

Ranges are not forced.

Defined in Agda.Syntax.Common

Methods

rnf :: Renaming' a b -> ()

(KillRange a, KillRange b) => KillRange (Renaming' a b)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Renaming' a b)

(HasRange a, HasRange b) => HasRange (Renaming' a b)

Defined in Agda.Syntax.Common

Methods

getRange :: Renaming' a b -> Range

HasRange instances

KillRange instances

NFData instances

Termination

data TerminationCheck m

Termination check? (Default = TerminationCheck).

Constructors

TerminationCheck

Run the termination checker.

NoTerminationCheck

Skip termination checking (unsafe).

NonTerminating

Treat as non-terminating.

Terminating

Treat as terminating (unsafe). Same effect as NoTerminationCheck.

TerminationMeasure Range m

Skip termination checking but use measure instead.

Instances

Functor TerminationCheck

Defined in Agda.Syntax.Common

Methods

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

(<$) :: a -> TerminationCheck b -> TerminationCheck a

Eq m => Eq (TerminationCheck m)

Defined in Agda.Syntax.Common

Methods

(==) :: TerminationCheck m -> TerminationCheck m -> Bool

(/=) :: TerminationCheck m -> TerminationCheck m -> Bool

Data m => Data (TerminationCheck m)

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: TerminationCheck m -> Constr

dataTypeOf :: TerminationCheck m -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> TerminationCheck m -> TerminationCheck m

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

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

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

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

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

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

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

Show m => Show (TerminationCheck m)

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> TerminationCheck m -> ShowS

show :: TerminationCheck m -> String

showList :: [TerminationCheck m] -> ShowS

NFData a => NFData (TerminationCheck a)

Defined in Agda.Syntax.Common

Methods

rnf :: TerminationCheck a -> ()

KillRange m => KillRange (TerminationCheck m)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (TerminationCheck m)

Positivity

type PositivityCheck = Bool

Positivity check? (Default = True).