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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Common

Contents

Description

Some common syntactic entities are defined in this module.

Synopsis

Documentation

type Nat = Int Source #

type Arity = Nat Source #

Delayed

data Delayed Source #

Used to specify whether something should be delayed.

Constructors

Delayed 
NotDelayed 
Instances
Eq Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Data Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Delayed -> Constr #

dataTypeOf :: Delayed -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

Show Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Delayed Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

File

data FileType Source #

Instances
Eq FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Data FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: FileType -> Constr #

dataTypeOf :: FileType -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Show FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty FileType Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj FileType Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Eta-equality

data HasEta Source #

Constructors

NoEta 
YesEta 
Instances
Eq HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Data HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: HasEta -> Constr #

dataTypeOf :: HasEta -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

Show HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

NFData HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: HasEta -> () #

KillRange HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj HasEta Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Induction

data Induction Source #

Constructors

Inductive 
CoInductive 
Instances
Eq Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Data Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Induction -> Constr #

dataTypeOf :: Induction -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Show Induction Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Induction -> () #

Pretty Induction Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Induction Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Hiding

data Overlappable Source #

Constructors

YesOverlap 
NoOverlap 
Instances
Eq Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Data Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Overlappable -> Constr #

dataTypeOf :: Overlappable -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Show Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup Overlappable Source #

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

Instance details

Defined in Agda.Syntax.Common

Monoid Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Overlappable Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Overlappable -> () #

data Hiding Source #

Instances
Eq Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Data Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Hiding -> Constr #

dataTypeOf :: Hiding -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Show Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup Hiding Source #

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

Instance details

Defined in Agda.Syntax.Common

Monoid Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Hiding -> () #

Pretty Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

ChooseFlex Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Unquote Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

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

Defined in Agda.Auto.Convert

Methods

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

data WithHiding a Source #

Decorating something with Hiding information.

Constructors

WithHiding 

Fields

Instances
Functor WithHiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Applicative WithHiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pure :: a -> WithHiding a #

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

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

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

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

Foldable WithHiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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

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

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

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

toList :: WithHiding a -> [a] #

null :: WithHiding a -> Bool #

length :: WithHiding a -> Int #

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

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

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

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

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

Traversable WithHiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

Decoration WithHiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

Defined in Agda.TypeChecking.Substitute

ToConcrete RHS (RHS, [RewriteEqn], [WithHiding Expr], [Declaration]) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Defined in Agda.Syntax.Common

Methods

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

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

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

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: WithHiding a -> Constr #

dataTypeOf :: WithHiding a -> DataType #

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

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

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

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

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

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

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

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

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

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

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

Methods

rnf :: WithHiding a -> () #

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

Defined in Agda.Syntax.Concrete.Pretty

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

LensHiding (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

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

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Defined in Agda.TypeChecking.Pretty

Methods

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

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

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.TypeChecking.Monad.Context

class LensHiding a where Source #

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

Minimal complete definition

Nothing

Methods

getHiding :: a -> Hiding Source #

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

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

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

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

Instances
LensHiding ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

LensHiding (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getHiding :: Arg e -> Hiding Source #

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

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

LensHiding (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

LensHiding (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Monoidal composition of Hiding information in some data.

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

NotHidden arguments are visible.

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

Instance and Hidden arguments are notVisible.

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

Hidden arguments are hidden.

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

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

Ignores Overlappable.

Modalities

data Modality Source #

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

Constructors

Modality 

Fields

  • modRelevance :: Relevance

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

  • modQuantity :: Quantity

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

  • modCohesion :: Cohesion

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

Instances
Eq Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Data Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Modality -> Constr #

dataTypeOf :: Modality -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Show Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Generic Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Modality :: Type -> Type #

Methods

from :: Modality -> Rep Modality x #

to :: Rep Modality x -> Modality #

Semigroup Modality Source #

Pointwise composition.

Instance details

Defined in Agda.Syntax.Common

Monoid Modality Source #

Pointwise unit.

Instance details

Defined in Agda.Syntax.Common

NFData Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Modality -> () #

PartialOrd Modality Source #

Dominance ordering.

Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid Modality Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid Modality Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup Modality Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensCohesion Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality Modality Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Modality Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

PrettyTCM Modality Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Unquote Modality Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

IsVarSet () AllowedVar Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

type Rep Modality Source # 
Instance details

Defined in Agda.Syntax.Common

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

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

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

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

Multiplicative monoid (standard monoid).

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

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

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

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

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

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

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

Modality forms a pointwise additive monoid.

topModality :: Modality Source #

Absorptive element under addition.

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

Equality ignoring origin.

class LensModality a where Source #

Minimal complete definition

Nothing

Instances
LensModality ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality (VarOcc' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

LensModality (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

LensModality (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Defined in Agda.TypeChecking.Free.Lazy

Quantities

Quantity origin.

data Q0Origin Source #

Origin of Quantity0.

Constructors

Q0Inferred

User wrote nothing.

Q0 Range

User wrote "@0".

Q0Erased Range

User wrote "@erased".

Instances
Eq Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Data Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Q0Origin -> Constr #

dataTypeOf :: Q0Origin -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Show Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Generic Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Q0Origin :: Type -> Type #

Methods

from :: Q0Origin -> Rep Q0Origin x #

to :: Rep Q0Origin x -> Q0Origin #

Semigroup Q0Origin Source #

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

Instance details

Defined in Agda.Syntax.Common

Monoid Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Q0Origin -> () #

Null Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Q0Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

type Rep Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

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

data Q1Origin Source #

Origin of Quantity1.

Constructors

Q1Inferred

User wrote nothing.

Q1 Range

User wrote "@1".

Q1Linear Range

User wrote "@linear".

Instances
Eq Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Data Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Q1Origin -> Constr #

dataTypeOf :: Q1Origin -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Show Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Generic Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Q1Origin :: Type -> Type #

Methods

from :: Q1Origin -> Rep Q1Origin x #

to :: Rep Q1Origin x -> Q1Origin #

Semigroup Q1Origin Source #

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

Instance details

Defined in Agda.Syntax.Common

Monoid Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Q1Origin -> () #

Null Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Q1Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

type Rep Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

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

data QωOrigin Source #

Origin of Quantityω.

Constructors

QωInferred

User wrote nothing.

Range

User wrote "@ω".

QωPlenty Range

User wrote "@plenty".

Instances
Eq QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Data QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: QωOrigin -> Constr #

dataTypeOf :: QωOrigin -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Show QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Generic QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

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

Semigroup QωOrigin Source #

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

Instance details

Defined in Agda.Syntax.Common

Monoid QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

NFData QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: QωOrigin -> () #

Null QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj QωOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

type Rep QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

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

Instances for Q0Origin.

Instances for Q1Origin.

Instances for QωOrigin.

Quantity.

data Quantity Source #

Quantity for linearity.

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

Constructors

Quantity0 Q0Origin

Zero uses {0}, erased at runtime.

Quantity1 Q1Origin

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

Quantityω QωOrigin

Unrestricted use .

Instances
Eq Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Data Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Quantity -> Constr #

dataTypeOf :: Quantity -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Show Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Generic Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Quantity :: Type -> Type #

Methods

from :: Quantity -> Rep Quantity x #

to :: Rep Quantity x -> Quantity #

Semigroup Quantity Source #

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Right-biased for origin.

Instance details

Defined in Agda.Syntax.Common

Monoid Quantity Source #

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

Instance details

Defined in Agda.Syntax.Common

NFData Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Quantity -> () #

PartialOrd Quantity Source #

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

Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Quantity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

PrettyTCM Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

UniverseBi Declaration Quantity Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

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

Equality ignoring origin.

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

Quantity forms an additive monoid with zero Quantity0.

topQuantity :: Quantity Source #

Absorptive element is ω.

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

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

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

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

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

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

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

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

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

Did the user supply a quantity annotation?

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

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

class LensQuantity a where Source #

Minimal complete definition

Nothing

Instances
LensQuantity ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity (VarOcc' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

LensQuantity (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Defined in Agda.TypeChecking.Free.Lazy

Relevance

data Relevance Source #

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

Constructors

Relevant

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

NonStrict

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

Irrelevant

The argument is irrelevant at compile- and runtime.

Instances
Bounded Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Enum Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Eq Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Data Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Relevance -> Constr #

dataTypeOf :: Relevance -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Relevance Source #

More relevant is smaller.

Instance details

Defined in Agda.Syntax.Common

Show Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Generic Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Relevance :: Type -> Type #

Semigroup Relevance Source #

Relevance forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

Monoid Relevance Source #

Relevant is the unit.

Instance details

Defined in Agda.Syntax.Common

NFData Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Relevance -> () #

PartialOrd Relevance Source #

More relevant is smaller.

Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Relevance Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

PrettyTCM Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Unquote Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

type Rep Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

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

class LensRelevance a where Source #

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

Minimal complete definition

Nothing

Instances
LensRelevance ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensRelevance TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensRelevance Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensRelevance (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance (VarOcc' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

LensRelevance (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Free.Lazy

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

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

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

Equality ignoring origin.

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

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

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

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

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

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

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

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

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

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

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

Combine inferred Relevance. The unit is Irrelevant.

zeroRelevance :: Relevance Source #

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

topRelevance :: Relevance Source #

Absorptive element under addition.

irrToNonStrict :: Relevance -> Relevance Source #

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

nonStrictToRel :: Relevance -> Relevance Source #

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

Cohesion

data Cohesion Source #

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

Constructors

Flat

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

Continuous

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

Squash

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

Instances
Bounded Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Enum Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Eq Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Data Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Cohesion -> Constr #

dataTypeOf :: Cohesion -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Cohesion Source #

Order is given by implication: flatter is smaller.

Instance details

Defined in Agda.Syntax.Common

Show Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Generic Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Cohesion :: Type -> Type #

Methods

from :: Cohesion -> Rep Cohesion x #

to :: Rep Cohesion x -> Cohesion #

Semigroup Cohesion Source #

Cohesion forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

Monoid Cohesion Source #

Continous is the unit.

Instance details

Defined in Agda.Syntax.Common

NFData Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Cohesion -> () #

PartialOrd Cohesion Source #

Flatter is smaller.

Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Cohesion Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

LensCohesion Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Cohesion Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

type Rep Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

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

class LensCohesion a where Source #

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

Minimal complete definition

Nothing

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

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

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

Equality ignoring origin.

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

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

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

Cohesion composition. Squash is dominant, Continuous is neutral.

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

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

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

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

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

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

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

Combine inferred Cohesion. The unit is Squash.

zeroCohesion :: Cohesion Source #

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

topCohesion :: Cohesion Source #

Absorptive element under addition.

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

data Origin Source #

Origin of arguments.

Constructors

UserWritten

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

Inserted

E.g. inserted hidden arguments.

Reflected

Produced by the reflection machinery.

CaseSplit

Produced by an interactive case split.

Substitution

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

Instances
Eq Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Data Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Origin -> Constr #

dataTypeOf :: Origin -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Show Origin Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Origin -> () #

KillRange Origin Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin Origin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

ChooseFlex Origin Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

data WithOrigin a Source #

Decorating something with Origin information.

Constructors

WithOrigin 

Fields

Instances
Functor WithOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Foldable WithOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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

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

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

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

toList :: WithOrigin a -> [a] #

null :: WithOrigin a -> Bool #

length :: WithOrigin a -> Int #

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

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

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

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

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

Traversable WithOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

Decoration WithOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

UniverseBi Declaration (NamedArg Pattern) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg LHSCore) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg Expr) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg BindName) Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Internal

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

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

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

Instance details

Defined in Agda.Syntax.Internal.Pattern

LensNamed NamedName (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Common

Methods

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

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

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

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: WithOrigin a -> Constr #

dataTypeOf :: WithOrigin a -> DataType #

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

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

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

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

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

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

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

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

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

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

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

Methods

rnf :: WithOrigin a -> () #

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

Defined in Agda.Syntax.Concrete.Pretty

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

LensOrigin (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Concrete.Name

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Defined in Agda.TypeChecking.Pretty

Methods

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

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

Defined in Agda.TypeChecking.Records

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.Clause

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

class LensOrigin a where Source #

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

Minimal complete definition

Nothing

Methods

getOrigin :: a -> Origin Source #

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

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

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

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

Instances
LensOrigin ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin Origin Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

LensOrigin (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getOrigin :: Arg e -> Origin Source #

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

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

LensOrigin (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin (Elim' a) Source #

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

Instance details

Defined in Agda.Syntax.Internal

LensOrigin (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

LensOrigin (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

Free variable annotations

data FreeVariables Source #

Constructors

UnknownFVs 
KnownFVs IntSet 
Instances
Eq FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Data FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: FreeVariables -> Constr #

dataTypeOf :: FreeVariables -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Show FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

NFData FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: FreeVariables -> () #

LensFreeVariables FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj FreeVariables Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

class LensFreeVariables a where Source #

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

Minimal complete definition

Nothing

Argument decoration

data ArgInfo Source #

A function argument can be hidden and/or irrelevant.

Instances
Eq ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Data ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: ArgInfo -> Constr #

dataTypeOf :: ArgInfo -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Show ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

NFData ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ArgInfo -> () #

KillRange ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensArgInfo ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensFreeVariables ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensCohesion ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

SynEq ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

ToTerm ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ChooseFlex ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Unquote ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

EqualSy ArgInfo Source #

Ignore origin and free variables.

Instance details

Defined in Agda.TypeChecking.Abstract

class LensArgInfo a where Source #

Minimal complete definition

getArgInfo

Methods

getArgInfo :: a -> ArgInfo Source #

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

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

Arguments

data Arg e Source #

Constructors

Arg 

Fields

Instances
Functor Arg Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Foldable Arg Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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

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

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

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

toList :: Arg a -> [a] #

null :: Arg a -> Bool #

length :: Arg a -> Int #

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

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

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

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

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

Traversable Arg Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

Decoration Arg Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

IsPrefixOf Args Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

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

Defined in Agda.Auto.Convert

Methods

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

Conversion TOM Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

Conversion TOM Term (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.Auto.Convert

Methods

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

UniverseBi Declaration (NamedArg Pattern) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg LHSCore) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg Expr) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg BindName) Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Common

Methods

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

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Defined in Agda.Syntax.Internal.Pattern

Methods

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

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

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

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

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

Instance details

Defined in Agda.Syntax.Internal.Pattern

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

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

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

Conversion MOT (Exp O) Type Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type Source #

Conversion MOT (Exp O) Term Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Term Source #

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

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.Syntax.Common

Methods

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

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

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

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Arg e -> Constr #

dataTypeOf :: Arg e -> DataType #

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

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

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

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

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

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

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

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

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

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

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

Defined in Agda.Syntax.Common

Methods

compare :: Arg e -> Arg e -> Ordering #

(<) :: Arg e -> Arg e -> Bool #

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

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

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

max :: Arg e -> Arg e -> Arg e #

min :: Arg e -> Arg e -> Arg e #

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

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Arg e -> ShowS #

show :: Arg e -> String #

showList :: [Arg e] -> ShowS #

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

Defined in Agda.Syntax.Common

Methods

rnf :: Arg e -> () #

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

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Arg a -> Doc Source #

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

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

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Arg a -> Arg a Source #

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

Defined in Agda.Syntax.Common

Methods

getRange :: Arg a -> Range Source #

LensArgInfo (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

LensFreeVariables (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getOrigin :: Arg e -> Origin Source #

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

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

LensCohesion (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getHiding :: Arg e -> Hiding Source #

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

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

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

Defined in Agda.Syntax.Abstract.Name

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

Defined in Agda.Syntax.Concrete.Pattern

Methods

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

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

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

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

Defined in Agda.Syntax.Concrete.Pattern

Methods

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

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

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

Defined in Agda.Syntax.Internal.Defs

Methods

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

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

Defined in Agda.Syntax.Abstract

Methods

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

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

Defined in Agda.Syntax.Abstract

Methods

allNames :: Arg a -> Seq QName Source #

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

Defined in Agda.Syntax.Internal.Pattern

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

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Arg a -> S Int32 Source #

icod_ :: Arg a -> S Int32 Source #

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

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

Defined in Agda.TypeChecking.Pretty

Methods

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

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

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Arg a -> Set QName Source #

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

Defined in Agda.TypeChecking.Telescope

Methods

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

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

Defined in Agda.TypeChecking.Monad.MetaVars

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

Defined in Agda.TypeChecking.Patterns.Abstract

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

Defined in Agda.TypeChecking.MetaVars.Mention

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

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

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

SubstWithOrigin (Arg Term) Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

SubstWithOrigin (Arg DisplayTerm) Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

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

Defined in Agda.TypeChecking.DisplayForm

Methods

match :: MonadDisplayForm m => Arg a -> Arg a -> MaybeT m [WithOrigin Term] Source #

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

Defined in Agda.TypeChecking.Irrelevance

Methods

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

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

Defined in Agda.TypeChecking.Irrelevance

Methods

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

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

Defined in Agda.TypeChecking.Records

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Arg a -> [QName] Source #

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

Defined in Agda.TypeChecking.Positivity

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

Defined in Agda.TypeChecking.Polarity

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Arg a -> tcm Bool Source #

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Arg a -> OccursM (Arg a) Source #

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

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

Defined in Agda.TypeChecking.MetaVars

Methods

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

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

Defined in Agda.TypeChecking.MetaVars

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

Defined in Agda.TypeChecking.Unquote

Methods

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

EqualSy a => EqualSy (Arg a) Source #

Ignores irrelevant arguments and modality. (And, of course, origin and free variables).

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Arg a -> Arg a -> Bool Source #

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

Defined in Agda.TypeChecking.Abstract

Methods

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

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

Defined in Agda.TypeChecking.Rules.LHS

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

Defined in Agda.Syntax.Internal.Pattern

Methods

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

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

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

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

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

Defined in Agda.TypeChecking.Rewriting.Clause

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

Defined in Agda.TypeChecking.Rewriting.Clause

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

Defined in Agda.TypeChecking.Patterns.Internal

Methods

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

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

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

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Arg i -> m (Arg a) Source #

reifyWhen :: MonadReify m => Bool -> Arg i -> m (Arg a) Source #

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Dom i -> m (Arg a) Source #

reifyWhen :: MonadReify m => Bool -> Dom i -> m (Arg a) Source #

NLPatToTerm p a => NLPatToTerm (Arg p) (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

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

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

Defined in Agda.Syntax.Internal.Pattern

Methods

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

unlabelPatVars :: Arg b -> Arg a Source #

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

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

Precondition: The two lists should have equal length.

Names

class Eq a => Underscore a where Source #

Minimal complete definition

underscore

Named arguments

data Named name a Source #

Something potentially carrying a name.

Constructors

Named 

Fields

Instances
MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

UniverseBi Declaration (NamedArg Pattern) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg LHSCore) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg Expr) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg BindName) Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Internal

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

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

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

Instance details

Defined in Agda.Syntax.Internal.Pattern

LensNamed name (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Defined in Agda.Syntax.Internal.Pattern

Methods

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

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

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

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

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

Functor (Named name) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Foldable (Named name) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => Named name m -> m #

foldMap :: Monoid m => (a -> m) -> Named name a -> m #

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

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

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

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

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

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

toList :: Named name a -> [a] #

null :: Named name a -> Bool #

length :: Named name a -> Int #

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

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

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

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

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

Traversable (Named name) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

Decoration (Named name) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

Defined in Agda.Syntax.Concrete.Pretty

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.TypeChecking.Pretty

Methods

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

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

Defined in Agda.TypeChecking.Records

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.Clause

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

(Eq name, Eq a) => Eq (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Named name a -> Named name a -> Bool #

(/=) :: Named name a -> Named name a -> Bool #

(Data name, Data a) => Data (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Named name a -> c (Named name a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Named name a) #

toConstr :: Named name a -> Constr #

dataTypeOf :: Named name a -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> Named name a -> Named name a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Named name a -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Named name a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Named name a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Named name a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a) #

(Ord name, Ord a) => Ord (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Named name a -> Named name a -> Ordering #

(<) :: Named name a -> Named name a -> Bool #

(<=) :: Named name a -> Named name a -> Bool #

(>) :: Named name a -> Named name a -> Bool #

(>=) :: Named name a -> Named name a -> Bool #

max :: Named name a -> Named name a -> Named name a #

min :: Named name a -> Named name a -> Named name a #

(Show name, Show a) => Show (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Named name a -> ShowS #

show :: Named name a -> String #

showList :: [Named name a] -> ShowS #

(NFData name, NFData a) => NFData (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Named name a -> () #

(KillRange name, KillRange a) => KillRange (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Named name a) Source #

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

Defined in Agda.Syntax.Common

Methods

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

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

Defined in Agda.Syntax.Common

Methods

getRange :: Named name a -> Range Source #

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

Defined in Agda.Syntax.Abstract.Name

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

Defined in Agda.Syntax.Concrete.Pattern

Methods

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

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

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

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

Defined in Agda.Syntax.Concrete.Pattern

Methods

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

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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

Defined in Agda.Syntax.Abstract

Methods

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

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

Defined in Agda.Syntax.Abstract

Methods

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

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

Defined in Agda.Syntax.Internal.Pattern

Methods

countPatternVars :: Named x a -> Int Source #

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

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

(EmbPrj s, EmbPrj t) => EmbPrj (Named s t) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Named s t -> S Int32 Source #

icod_ :: Named s t -> S Int32 Source #

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

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

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Named n a -> Set QName Source #

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Telescope

Methods

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

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

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

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

InstantiateFull t => InstantiateFull (Named name t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Named name t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Named name t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Rules.LHS

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

Defined in Agda.Syntax.Internal.Pattern

Methods

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

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

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

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

TermToPattern a b => TermToPattern (Named c a) (Named c b) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Internal

Methods

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

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: MonadReflectedToAbstract m => Named name r -> m (Named name a) Source #

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Named n i -> m (Named n a) Source #

reifyWhen :: MonadReify m => Bool -> Named n i -> m (Named n a) Source #

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

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

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

Defined in Agda.Syntax.Internal.Pattern

Methods

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

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

type Named_ = Named NamedName Source #

Standard naming.

type NamedName = WithOrigin (Ranged ArgName) Source #

Standard argument names.

sameName :: NamedName -> NamedName -> Bool Source #

Equality of argument names of things modulo Range' and Origin.

unnamed :: a -> Named name a Source #

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

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

Accessor/editor for the nameOf component.

Minimal complete definition

Nothing

Methods

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

lensNamed :: (Decoration f, LensNamed name b, f b ~ a) => Lens' (Maybe name) a Source #

Instances
LensNamed name (Maybe name) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Defined in Agda.Syntax.Common

Methods

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

LensNamed name (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

LensNamed NamedName (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

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

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

namedSame :: (LensNamed NamedName a, LensNamed NamedName b) => a -> b -> Bool Source #

Equality of argument names of things modulo Range' and Origin.

fittingNamedArg :: (LensNamed NamedName arg, LensHiding arg, LensNamed NamedName dom, LensHiding dom) => arg -> dom -> Maybe Bool Source #

Does an argument arg fit the shape dom of the next expected argument?

The hiding has to match, and if the argument has a name, it should match the name of the domain.

Nothing should be __IMPOSSIBLE__, so use as @ fromMaybe IMPOSSIBLE $ fittingNamedArg arg dom @

type NamedArg a = Arg (Named_ a) Source #

Only Hidden arguments can have names.

namedArg :: NamedArg a -> a Source #

Get the content of a NamedArg.

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

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

updateNamedArgA :: Applicative f => (a -> f b) -> NamedArg a -> f (NamedArg b) Source #

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

setNamedArg a b = updateNamedArg (const b) a

ArgName

type ArgName = String Source #

Names in binders and arguments.

Range decoration.

data Ranged a Source #

Thing with range info.

Constructors

Ranged 

Fields

Instances
Functor Ranged Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Foldable Ranged Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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

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

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

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

toList :: Ranged a -> [a] #

null :: Ranged a -> Bool #

length :: Ranged a -> Int #

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

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

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

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

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

Traversable Ranged Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

Decoration Ranged Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

UniverseBi Declaration (NamedArg Pattern) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg LHSCore) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg Expr) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg BindName) Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Internal

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

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

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

Instance details

Defined in Agda.Syntax.Internal.Pattern

LensNamed NamedName (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Common

Methods

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

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

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

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: Ranged a -> Constr #

dataTypeOf :: Ranged a -> DataType #

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

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

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

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

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

gmapQ :: (forall d. Data d => d -> u) -> Ranged a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Ranged a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) #

Ord a => Ord (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Ranged a -> Ranged a -> Ordering #

(<) :: Ranged a -> Ranged a -> Bool #

(<=) :: Ranged a -> Ranged a -> Bool #

(>) :: Ranged a -> Ranged a -> Bool #

(>=) :: Ranged a -> Ranged a -> Bool #

max :: Ranged a -> Ranged a -> Ranged a #

min :: Ranged a -> Ranged a -> Ranged a #

Show a => Show (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Ranged a -> ShowS #

show :: Ranged a -> String #

showList :: [Ranged a] -> ShowS #

NFData a => NFData (Ranged a) Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Ranged a -> () #

Pretty a => Pretty (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty e => Pretty (Named_ e) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Ranged a -> Range Source #

IsNoName a => IsNoName (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Ranged a -> Bool Source #

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj a => EmbPrj (Ranged a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Ranged a -> S Int32 Source #

icod_ :: Ranged a -> S Int32 Source #

value :: Int32 -> R (Ranged a) Source #

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Named_ a -> m Doc Source #

NormaliseProjP a => NormaliseProjP (Named_ a) Source # 
Instance details

Defined in Agda.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source #

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

ToAbstract [Arg Term] [NamedArg Expr] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

AddContext ([NamedArg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source #

contextSize :: ([NamedArg Name], Type) -> Nat Source #

unranged :: a -> Ranged a Source #

Thing with no range info.

Raw names (before parsing into name parts).

type RawName = String Source #

A RawName is some sort of string.

type RString = Ranged RawName Source #

String with range info.

Further constructor and projection info

data ConOrigin Source #

Where does the ConP or Con come from?

Constructors

ConOSystem

Inserted by system or expanded from an implicit pattern.

ConOCon

User wrote a constructor (pattern).

ConORec

User wrote a record (pattern).

ConOSplit

Generated by interactive case splitting.

Instances
Bounded ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Enum ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Eq ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Data ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConOrigin -> c ConOrigin #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConOrigin #

toConstr :: ConOrigin -> Constr #

dataTypeOf :: ConOrigin -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConOrigin) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConOrigin) #

gmapT :: (forall b. Data b => b -> b) -> ConOrigin -> ConOrigin #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConOrigin -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConOrigin -> r #

gmapQ :: (forall d. Data d => d -> u) -> ConOrigin -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ConOrigin -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin #

Ord ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Show ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj ConOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin Source #

Prefer user-written over system-inserted.

data ProjOrigin Source #

Where does a projection come from?

Constructors

ProjPrefix

User wrote a prefix projection.

ProjPostfix

User wrote a postfix projection.

ProjSystem

Projection was generated by the system.

Instances
Bounded ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Enum ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Eq ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Data ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProjOrigin -> c ProjOrigin #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProjOrigin #

toConstr :: ProjOrigin -> Constr #

dataTypeOf :: ProjOrigin -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProjOrigin) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProjOrigin) #

gmapT :: (forall b. Data b => b -> b) -> ProjOrigin -> ProjOrigin #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProjOrigin -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProjOrigin -> r #

gmapQ :: (forall d. Data d => d -> u) -> ProjOrigin -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProjOrigin -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProjOrigin -> m ProjOrigin #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjOrigin -> m ProjOrigin #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjOrigin -> m ProjOrigin #

Ord ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Show ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj ProjOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

data DataOrRecord Source #

Constructors

IsData 
IsRecord 
Instances
Eq DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Common

Data DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataOrRecord -> c DataOrRecord #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataOrRecord #

toConstr :: DataOrRecord -> Constr #

dataTypeOf :: DataOrRecord -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataOrRecord) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataOrRecord) #

gmapT :: (forall b. Data b => b -> b) -> DataOrRecord -> DataOrRecord #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r #

gmapQ :: (forall d. Data d => d -> u) -> DataOrRecord -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DataOrRecord -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord #

Ord DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Common

Show DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj DataOrRecord Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Infixity, access, abstract, etc.

data IsInfix Source #

Functions can be defined in both infix and prefix style. See LHS.

Constructors

InfixDef 
PrefixDef 
Instances
Eq IsInfix Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: IsInfix -> IsInfix -> Bool #

(/=) :: IsInfix -> IsInfix -> Bool #

Data IsInfix Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsInfix -> c IsInfix #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsInfix #

toConstr :: IsInfix -> Constr #

dataTypeOf :: IsInfix -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsInfix) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsInfix) #

gmapT :: (forall b. Data b => b -> b) -> IsInfix -> IsInfix #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsInfix -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsInfix -> r #

gmapQ :: (forall d. Data d => d -> u) -> IsInfix -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsInfix -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix #

Ord IsInfix Source # 
Instance details

Defined in Agda.Syntax.Common

Show IsInfix Source # 
Instance details

Defined in Agda.Syntax.Common

private blocks, public imports

data Access Source #

Access modifier.

Constructors

PrivateAccess Origin

Store the Origin of the private block that lead to this qualifier. This is needed for more faithful printing of declarations.

PublicAccess 
Instances
Eq Access Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Access -> Access -> Bool #

(/=) :: Access -> Access -> Bool #

Data Access Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Access -> c Access #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Access #

toConstr :: Access -> Constr #

dataTypeOf :: Access -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Access) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Access) #

gmapT :: (forall b. Data b => b -> b) -> Access -> Access #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Access -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Access -> r #

gmapQ :: (forall d. Data d => d -> u) -> Access -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Access -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Access -> m Access #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Access -> m Access #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Access -> m Access #

Ord Access Source # 
Instance details

Defined in Agda.Syntax.Common

Show Access Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Access Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Access -> () #

Pretty Access Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Access Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Access Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Access Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

abstract blocks

data IsAbstract Source #

Abstract or concrete.

Constructors

AbstractDef 
ConcreteDef 
Instances
Eq IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Data IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsAbstract -> c IsAbstract #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsAbstract #

toConstr :: IsAbstract -> Constr #

dataTypeOf :: IsAbstract -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsAbstract) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsAbstract) #

gmapT :: (forall b. Data b => b -> b) -> IsAbstract -> IsAbstract #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsAbstract -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsAbstract -> r #

gmapQ :: (forall d. Data d => d -> u) -> IsAbstract -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsAbstract -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsAbstract -> m IsAbstract #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsAbstract -> m IsAbstract #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsAbstract -> m IsAbstract #

Ord IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Show IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup IsAbstract Source #

Semigroup computes if any of several is an AbstractDef.

Instance details

Defined in Agda.Syntax.Common

Monoid IsAbstract Source #

Default is ConcreteDef.

Instance details

Defined in Agda.Syntax.Common

KillRange IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

AnyIsAbstract IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

LensIsAbstract IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj IsAbstract Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

class AnyIsAbstract a where Source #

Is any element of a collection an AbstractDef.

Minimal complete definition

Nothing

Instances
AnyIsAbstract IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

AnyIsAbstract a => AnyIsAbstract [a] Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

anyIsAbstract :: [a] -> IsAbstract Source #

AnyIsAbstract a => AnyIsAbstract (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Common

AnyIsAbstract (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

instance blocks

data IsInstance Source #

Is this definition eligible for instance search?

Constructors

InstanceDef Range

Range of the instance keyword.

NotInstanceDef 
Instances
Eq IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Data IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsInstance -> c IsInstance #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsInstance #

toConstr :: IsInstance -> Constr #

dataTypeOf :: IsInstance -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsInstance) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsInstance) #

gmapT :: (forall b. Data b => b -> b) -> IsInstance -> IsInstance #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsInstance -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsInstance -> r #

gmapQ :: (forall d. Data d => d -> u) -> IsInstance -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsInstance -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsInstance -> m IsInstance #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInstance -> m IsInstance #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInstance -> m IsInstance #

Ord IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Show IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

NFData IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: IsInstance -> () #

KillRange IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

macro blocks

data IsMacro Source #

Is this a macro definition?

Constructors

MacroDef 
NotMacroDef 
Instances
Eq IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: IsMacro -> IsMacro -> Bool #

(/=) :: IsMacro -> IsMacro -> Bool #

Data IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsMacro -> c IsMacro #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsMacro #

toConstr :: IsMacro -> Constr #

dataTypeOf :: IsMacro -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsMacro) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsMacro) #

gmapT :: (forall b. Data b => b -> b) -> IsMacro -> IsMacro #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsMacro -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsMacro -> r #

gmapQ :: (forall d. Data d => d -> u) -> IsMacro -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsMacro -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro #

Ord IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Show IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

NameId

data NameId Source #

The unique identifier of a name. Second argument is the top-level module identifier.

Constructors

NameId !Word64 !Word64 
Instances
Enum NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Eq NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: NameId -> NameId -> Bool #

(/=) :: NameId -> NameId -> Bool #

Data NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameId -> c NameId #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameId #

toConstr :: NameId -> Constr #

dataTypeOf :: NameId -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameId) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameId) #

gmapT :: (forall b. Data b => b -> b) -> NameId -> NameId #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r #

gmapQ :: (forall d. Data d => d -> u) -> NameId -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NameId -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameId -> m NameId #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId #

Ord NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Show NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Generic NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep NameId :: Type -> Type #

Methods

from :: NameId -> Rep NameId x #

to :: Rep NameId x -> NameId #

Hashable NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

hashWithSalt :: Int -> NameId -> Int #

hash :: NameId -> Int #

NFData NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: NameId -> () #

Pretty NameId Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange NameId Source # 
Instance details

Defined in Agda.Syntax.Common

HasFresh NameId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj NameId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Monad m => MonadFresh NameId (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

type Rep NameId Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep NameId = D1 (MetaData "NameId" "Agda.Syntax.Common" "Agda-2.6.1-HTVbJ7KJ8pbJE1PvbUqEEQ" False) (C1 (MetaCons "NameId" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) SourceUnpack SourceStrict DecidedStrict) (Rec0 Word64) :*: S1 (MetaSel (Nothing :: Maybe Symbol) SourceUnpack SourceStrict DecidedStrict) (Rec0 Word64)))

Meta variables

newtype MetaId Source #

A meta variable identifier is just a natural number.

Constructors

MetaId 

Fields

Instances
Enum MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Eq MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: MetaId -> MetaId -> Bool #

(/=) :: MetaId -> MetaId -> Bool #

Integral MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Data MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MetaId -> c MetaId #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MetaId #

toConstr :: MetaId -> Constr #

dataTypeOf :: MetaId -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MetaId) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MetaId) #

gmapT :: (forall b. Data b => b -> b) -> MetaId -> MetaId #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r #

gmapQ :: (forall d. Data d => d -> u) -> MetaId -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> MetaId -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId #

Num MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Ord MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Real MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Show MetaId Source #

Show non-record version of this newtype.

Instance details

Defined in Agda.Syntax.Common

Generic MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep MetaId :: Type -> Type #

Methods

from :: MetaId -> Rep MetaId x #

to :: Rep MetaId x -> MetaId #

Hashable MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

hashWithSalt :: Int -> MetaId -> Int #

hash :: MetaId -> Int #

NFData MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: MetaId -> () #

Pretty MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

GetDefs MetaId Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => MetaId -> m () Source #

HasFresh MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

PrettyTCM MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => MetaId -> m Doc Source #

UnFreezeMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source #

IsInstantiatedMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

FromTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Unquote MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Singleton MetaId () Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

singleton :: MetaId -> () Source #

Singleton MetaId MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Reify MetaId Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type Rep MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep MetaId = D1 (MetaData "MetaId" "Agda.Syntax.Common" "Agda-2.6.1-HTVbJ7KJ8pbJE1PvbUqEEQ" True) (C1 (MetaCons "MetaId" PrefixI True) (S1 (MetaSel (Just "metaId") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Nat)))

Placeholders (used to parse sections)

data PositionInName Source #

The position of a name part or underscore in a name.

Constructors

Beginning

The following underscore is at the beginning of the name: _foo.

Middle

The following underscore is in the middle of the name: foo_bar.

End

The following underscore is at the end of the name: foo_.

Instances
Eq PositionInName Source # 
Instance details

Defined in Agda.Syntax.Common

Data PositionInName Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PositionInName -> c PositionInName #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PositionInName #

toConstr :: PositionInName -> Constr #

dataTypeOf :: PositionInName -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PositionInName) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PositionInName) #

gmapT :: (forall b. Data b => b -> b) -> PositionInName -> PositionInName #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PositionInName -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PositionInName -> r #

gmapQ :: (forall d. Data d => d -> u) -> PositionInName -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PositionInName -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PositionInName -> m PositionInName #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PositionInName -> m PositionInName #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PositionInName -> m PositionInName #

Ord PositionInName Source # 
Instance details

Defined in Agda.Syntax.Common

Show PositionInName Source # 
Instance details

Defined in Agda.Syntax.Common

data MaybePlaceholder e Source #

Placeholders are used to represent the underscores in a section.

Constructors

Placeholder !PositionInName 
NoPlaceholder !(Maybe PositionInName) e

The second argument is used only (but not always) for name parts other than underscores.

Instances
Functor MaybePlaceholder Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> MaybePlaceholder a -> MaybePlaceholder b #

(<$) :: a -> MaybePlaceholder b -> MaybePlaceholder a #

Foldable MaybePlaceholder Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => MaybePlaceholder m -> m #

foldMap :: Monoid m => (a -> m) -> MaybePlaceholder a -> m #

foldr :: (a -> b -> b) -> b -> MaybePlaceholder a -> b #

foldr' :: (a -> b -> b) -> b -> MaybePlaceholder a -> b #

foldl :: (b -> a -> b) -> b -> MaybePlaceholder a -> b #

foldl' :: (b -> a -> b) -> b -> MaybePlaceholder a -> b #

foldr1 :: (a -> a -> a) -> MaybePlaceholder a -> a #

foldl1 :: (a -> a -> a) -> MaybePlaceholder a -> a #

toList :: MaybePlaceholder a -> [a] #

null :: MaybePlaceholder a -> Bool #

length :: MaybePlaceholder a -> Int #

elem :: Eq a => a -> MaybePlaceholder a -> Bool #

maximum :: Ord a => MaybePlaceholder a -> a #

minimum :: Ord a => MaybePlaceholder a -> a #

sum :: Num a => MaybePlaceholder a -> a #

product :: Num a => MaybePlaceholder a -> a #

Traversable MaybePlaceholder Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverse :: Applicative f => (a -> f b) -> MaybePlaceholder a -> f (MaybePlaceholder b) #

sequenceA :: Applicative f => MaybePlaceholder (f a) -> f (MaybePlaceholder a) #

mapM :: Monad m => (a -> m b) -> MaybePlaceholder a -> m (MaybePlaceholder b) #

sequence :: Monad m => MaybePlaceholder (m a) -> m (MaybePlaceholder a) #

Eq e => Eq (MaybePlaceholder e) Source # 
Instance details

Defined in Agda.Syntax.Common

Data e => Data (MaybePlaceholder e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MaybePlaceholder e -> c (MaybePlaceholder e) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (MaybePlaceholder e) #

toConstr :: MaybePlaceholder e -> Constr #

dataTypeOf :: MaybePlaceholder e -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (MaybePlaceholder e)) #

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (MaybePlaceholder e)) #

gmapT :: (forall b. Data b => b -> b) -> MaybePlaceholder e -> MaybePlaceholder e #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MaybePlaceholder e -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MaybePlaceholder e -> r #

gmapQ :: (forall d. Data d => d -> u) -> MaybePlaceholder e -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> MaybePlaceholder e -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MaybePlaceholder e -> m (MaybePlaceholder e) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MaybePlaceholder e -> m (MaybePlaceholder e) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MaybePlaceholder e -> m (MaybePlaceholder e) #

Ord e => Ord (MaybePlaceholder e) Source # 
Instance details

Defined in Agda.Syntax.Common

Show e => Show (MaybePlaceholder e) Source # 
Instance details

Defined in Agda.Syntax.Common

NFData a => NFData (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: MaybePlaceholder a -> () #

Pretty a => Pretty (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange a => KillRange (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange a => HasRange (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Common

ExprLike a => ExprLike (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

noPlaceholder :: e -> MaybePlaceholder e Source #

An abbreviation: noPlaceholder = NoPlaceholder Nothing.

Interaction meta variables

newtype InteractionId Source #

Constructors

InteractionId 

Fields

Instances
Enum InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Eq InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Integral InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Data InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> InteractionId -> c InteractionId #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c InteractionId #

toConstr :: InteractionId -> Constr #

dataTypeOf :: InteractionId -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c InteractionId) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InteractionId) #

gmapT :: (forall b. Data b => b -> b) -> InteractionId -> InteractionId #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> InteractionId -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InteractionId -> r #

gmapQ :: (forall d. Data d => d -> u) -> InteractionId -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> InteractionId -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> InteractionId -> m InteractionId #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InteractionId -> m InteractionId #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InteractionId -> m InteractionId #

Num InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Ord InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Read InteractionId Source # 
Instance details

Defined in Agda.Interaction.Base

Real InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Show InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

ToJSON InteractionId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Pretty InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

HasFresh InteractionId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EncodeTCM InteractionId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

ToConcrete InteractionId Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Fixity

type PrecedenceLevel = Double Source #

Precedence levels for operators.

data FixityLevel Source #

Constructors

Unrelated

No fixity declared.

Related !PrecedenceLevel

Fixity level declared as the number.

Instances
Eq FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

Data FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FixityLevel -> c FixityLevel #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FixityLevel #

toConstr :: FixityLevel -> Constr #

dataTypeOf :: FixityLevel -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FixityLevel) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FixityLevel) #

gmapT :: (forall b. Data b => b -> b) -> FixityLevel -> FixityLevel #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FixityLevel -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FixityLevel -> r #

gmapQ :: (forall d. Data d => d -> u) -> FixityLevel -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> FixityLevel -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FixityLevel -> m FixityLevel #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FixityLevel -> m FixityLevel #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FixityLevel -> m FixityLevel #

Ord FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

Show FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

Null FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj FixityLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

ToTerm FixityLevel Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

data Associativity Source #

Associativity.

Constructors

NonAssoc 
LeftAssoc 
RightAssoc 
Instances
Eq Associativity Source # 
Instance details

Defined in Agda.Syntax.Common

Data Associativity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Associativity -> c Associativity #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Associativity #

toConstr :: Associativity -> Constr #

dataTypeOf :: Associativity -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Associativity) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Associativity) #

gmapT :: (forall b. Data b => b -> b) -> Associativity -> Associativity #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r #

gmapQ :: (forall d. Data d => d -> u) -> Associativity -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Associativity -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity #

Ord Associativity Source # 
Instance details

Defined in Agda.Syntax.Common

Show Associativity Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Associativity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

ToTerm Associativity Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

data Fixity Source #

Fixity of operators.

Constructors

Fixity 

Fields

Instances
Eq Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Fixity -> Fixity -> Bool #

(/=) :: Fixity -> Fixity -> Bool #

Data Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Fixity -> c Fixity #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity #

toConstr :: Fixity -> Constr #

dataTypeOf :: Fixity -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Fixity) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity) #

gmapT :: (forall b. Data b => b -> b) -> Fixity -> Fixity #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r #

gmapQ :: (forall d. Data d => d -> u) -> Fixity -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity #

Ord Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Show Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Fixity -> () #

Null Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Fixity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

LensFixity Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Fixity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

ToTerm Fixity Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Notation coupled with Fixity

data Fixity' Source #

The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.

Constructors

Fixity' 

Fields

Instances
Eq Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Fixity' -> Fixity' -> Bool #

(/=) :: Fixity' -> Fixity' -> Bool #

Data Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Fixity' -> c Fixity' #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity' #

toConstr :: Fixity' -> Constr #

dataTypeOf :: Fixity' -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Fixity') #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity') #

gmapT :: (forall b. Data b => b -> b) -> Fixity' -> Fixity' #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r #

gmapQ :: (forall d. Data d => d -> u) -> Fixity' -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity' -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' #

Show Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Fixity' -> () #

Null Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Fixity' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

LensFixity' Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

LensFixity Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

ToTerm Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Import directive

data ImportDirective' n m Source #

The things you are allowed to say when you shuffle names between name spaces (i.e. in import, namespace, or open declarations).

Constructors

ImportDirective 

Fields

Instances
(Eq m, Eq n) => Eq (ImportDirective' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

(Data n, Data m) => Data (ImportDirective' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ImportDirective' n m -> c (ImportDirective' n m) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ImportDirective' n m) #

toConstr :: ImportDirective' n m -> Constr #

dataTypeOf :: ImportDirective' n m -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ImportDirective' n m)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ImportDirective' n m)) #

gmapT :: (forall b. Data b => b -> b) -> ImportDirective' n m -> ImportDirective' n m #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportDirective' n m -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportDirective' n m -> r #

gmapQ :: (forall d. Data d => d -> u) -> ImportDirective' n m -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportDirective' n m -> u #

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m) #

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m) #

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m) #

(Show a, Show b) => Show (ImportDirective' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

(NFData a, NFData b) => NFData (ImportDirective' a b) Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ImportDirective' a b -> () #

Null (ImportDirective' n m) Source #

null for import directives holds when everything is imported unchanged (no names are hidden or renamed).

Instance details

Defined in Agda.Syntax.Common

(Pretty a, Pretty b) => Pretty (ImportDirective' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

(KillRange a, KillRange b) => KillRange (ImportDirective' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(HasRange a, HasRange b) => HasRange (ImportDirective' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

defaultImportDir :: ImportDirective' n m Source #

Default is directive is private (use everything, but do not export).

isDefaultImportDir :: ImportDirective' n m -> Bool Source #

isDefaultImportDir implies null, but not the other way round.

data Using' n m Source #

The using clause of import directive.

Constructors

UseEverything

No using clause given.

Using [ImportedName' n m]

using the specified names.

Instances
(Eq m, Eq n) => Eq (Using' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Using' n m -> Using' n m -> Bool #

(/=) :: Using' n m -> Using' n m -> Bool #

(Data n, Data m) => Data (Using' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Using' n m -> c (Using' n m) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Using' n m) #

toConstr :: Using' n m -> Constr #

dataTypeOf :: Using' n m -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Using' n m)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Using' n m)) #

gmapT :: (forall b. Data b => b -> b) -> Using' n m -> Using' n m #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Using' n m -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Using' n m -> r #

gmapQ :: (forall d. Data d => d -> u) -> Using' n m -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Using' n m -> u #

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m) #

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m) #

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m) #

(Show a, Show b) => Show (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Using' a b -> ShowS #

show :: Using' a b -> String #

showList :: [Using' a b] -> ShowS #

Semigroup (Using' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(<>) :: Using' n m -> Using' n m -> Using' n m #

sconcat :: NonEmpty (Using' n m) -> Using' n m #

stimes :: Integral b => b -> Using' n m -> Using' n m #

Monoid (Using' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

mempty :: Using' n m #

mappend :: Using' n m -> Using' n m -> Using' n m #

mconcat :: [Using' n m] -> Using' n m #

(NFData a, NFData b) => NFData (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Using' a b -> () #

Null (Using' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

empty :: Using' n m Source #

null :: Using' n m -> Bool Source #

(Pretty a, Pretty b) => Pretty (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Using' a b -> Doc Source #

prettyPrec :: Int -> Using' a b -> Doc Source #

prettyList :: [Using' a b] -> Doc Source #

(KillRange a, KillRange b) => KillRange (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(HasRange a, HasRange b) => HasRange (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Using' a b -> Range Source #

mapUsing :: ([ImportedName' n1 m1] -> [ImportedName' n2 m2]) -> Using' n1 m1 -> Using' n2 m2 Source #

data ImportedName' n m Source #

An imported name can be a module or a defined name.

Constructors

ImportedModule m

Imported module name of type m.

ImportedName n

Imported name of type n.

Instances
(Eq m, Eq n) => Eq (ImportedName' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: ImportedName' n m -> ImportedName' n m -> Bool #

(/=) :: ImportedName' n m -> ImportedName' n m -> Bool #

(Data n, Data m) => Data (ImportedName' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ImportedName' n m -> c (ImportedName' n m) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ImportedName' n m) #

toConstr :: ImportedName' n m -> Constr #

dataTypeOf :: ImportedName' n m -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ImportedName' n m)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ImportedName' n m)) #

gmapT :: (forall b. Data b => b -> b) -> ImportedName' n m -> ImportedName' n m #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportedName' n m -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportedName' n m -> r #

gmapQ :: (forall d. Data d => d -> u) -> ImportedName' n m -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportedName' n m -> u #

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m) #

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m) #

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m) #

(Ord m, Ord n) => Ord (ImportedName' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

(Show m, Show n) => Show (ImportedName' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

(NFData a, NFData b) => NFData (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ImportedName' a b -> () #

(Pretty a, Pretty b) => Pretty (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

(KillRange a, KillRange b) => KillRange (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(HasRange a, HasRange b) => HasRange (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

data Renaming' n m Source #

Constructors

Renaming 

Fields

Instances
(Eq m, Eq n) => Eq (Renaming' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Renaming' n m -> Renaming' n m -> Bool #

(/=) :: Renaming' n m -> Renaming' n m -> Bool #

(Data n, Data m) => Data (Renaming' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Renaming' n m -> c (Renaming' n m) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Renaming' n m) #

toConstr :: Renaming' n m -> Constr #

dataTypeOf :: Renaming' n m -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Renaming' n m)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Renaming' n m)) #

gmapT :: (forall b. Data b => b -> b) -> Renaming' n m -> Renaming' n m #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' n m -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' n m -> r #

gmapQ :: (forall d. Data d => d -> u) -> Renaming' n m -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Renaming' n m -> u #

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m) #

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m) #

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m) #

(Show a, Show b) => Show (Renaming' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Renaming' a b -> ShowS #

show :: Renaming' a b -> String #

showList :: [Renaming' a b] -> ShowS #

(NFData a, NFData b) => NFData (Renaming' a b) Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Renaming' a b -> () #

(Pretty a, Pretty b) => Pretty (Renaming' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

(KillRange a, KillRange b) => KillRange (Renaming' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(HasRange a, HasRange b) => HasRange (Renaming' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Renaming' a b -> Range Source #

HasRange instances

KillRange instances

NFData instances

Termination

data TerminationCheck m Source #

Termination check? (Default = TerminationCheck).

Constructors

TerminationCheck

Run the termination checker.

NoTerminationCheck

Skip termination checking (unsafe).

NonTerminating

Treat as non-terminating.

Terminating

Treat as terminating (unsafe). Same effect as NoTerminationCheck.

TerminationMeasure Range m

Skip termination checking but use measure instead.

Instances
Functor TerminationCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> TerminationCheck a -> TerminationCheck b #

(<$) :: a -> TerminationCheck b -> TerminationCheck a #

Eq m => Eq (TerminationCheck m) Source # 
Instance details

Defined in Agda.Syntax.Common

Data m => Data (TerminationCheck m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TerminationCheck m -> c (TerminationCheck m) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TerminationCheck m) #

toConstr :: TerminationCheck m -> Constr #

dataTypeOf :: TerminationCheck m -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TerminationCheck m)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TerminationCheck m)) #

gmapT :: (forall b. Data b => b -> b) -> TerminationCheck m -> TerminationCheck m #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TerminationCheck m -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TerminationCheck m -> r #

gmapQ :: (forall d. Data d => d -> u) -> TerminationCheck m -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TerminationCheck m -> u #

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> TerminationCheck m -> m0 (TerminationCheck m) #

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> TerminationCheck m -> m0 (TerminationCheck m) #

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> TerminationCheck m -> m0 (TerminationCheck m) #

Show m => Show (TerminationCheck m) Source # 
Instance details

Defined in Agda.Syntax.Common

NFData a => NFData (TerminationCheck a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: TerminationCheck a -> () #

KillRange m => KillRange (TerminationCheck m) Source # 
Instance details

Defined in Agda.Syntax.Common

Positivity

data PositivityCheck Source #

Positivity check? (Default = True).

Instances
Bounded PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Enum PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Eq PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Data PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PositivityCheck -> c PositivityCheck #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PositivityCheck #

toConstr :: PositivityCheck -> Constr #

dataTypeOf :: PositivityCheck -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PositivityCheck) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PositivityCheck) #

gmapT :: (forall b. Data b => b -> b) -> PositivityCheck -> PositivityCheck #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PositivityCheck -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PositivityCheck -> r #

gmapQ :: (forall d. Data d => d -> u) -> PositivityCheck -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PositivityCheck -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PositivityCheck -> m PositivityCheck #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PositivityCheck -> m PositivityCheck #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PositivityCheck -> m PositivityCheck #

Ord PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Show PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Universe checking

data UniverseCheck Source #

Universe check? (Default is yes).

Instances
Bounded UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Enum UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Eq UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Data UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UniverseCheck -> c UniverseCheck #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UniverseCheck #

toConstr :: UniverseCheck -> Constr #

dataTypeOf :: UniverseCheck -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UniverseCheck) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UniverseCheck) #

gmapT :: (forall b. Data b => b -> b) -> UniverseCheck -> UniverseCheck #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UniverseCheck -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UniverseCheck -> r #

gmapQ :: (forall d. Data d => d -> u) -> UniverseCheck -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> UniverseCheck -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UniverseCheck -> m UniverseCheck #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UniverseCheck -> m UniverseCheck #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UniverseCheck -> m UniverseCheck #

Ord UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Show UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Universe checking

data CoverageCheck Source #

Coverage check? (Default is yes).

Instances
Bounded CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Enum CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Eq CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Data CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoverageCheck -> c CoverageCheck #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoverageCheck #

toConstr :: CoverageCheck -> Constr #

dataTypeOf :: CoverageCheck -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CoverageCheck) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoverageCheck) #

gmapT :: (forall b. Data b => b -> b) -> CoverageCheck -> CoverageCheck #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoverageCheck -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoverageCheck -> r #

gmapQ :: (forall d. Data d => d -> u) -> CoverageCheck -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> CoverageCheck -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoverageCheck -> m CoverageCheck #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoverageCheck -> m CoverageCheck #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoverageCheck -> m CoverageCheck #

Ord CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Show CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Rewrite Directives on the LHS

data RewriteEqn' qn p e Source #

RewriteEqn' qn p e represents the rewrite and irrefutable with clauses of the LHS. qn stands for the QName of the auxiliary function generated to implement the feature p is the type of patterns e is the type of expressions

Constructors

Rewrite [(qn, e)]
rewrite e
Invert qn [(p, e)]
with p <- e
Instances
ToAbstract RewriteEqn (RewriteEqn' () Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToConcrete RHS (RHS, [RewriteEqn], [WithHiding Expr], [Declaration]) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Functor (RewriteEqn' qn p) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> RewriteEqn' qn p a -> RewriteEqn' qn p b #

(<$) :: a -> RewriteEqn' qn p b -> RewriteEqn' qn p a #

Foldable (RewriteEqn' qn p) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => RewriteEqn' qn p m -> m #

foldMap :: Monoid m => (a -> m) -> RewriteEqn' qn p a -> m #

foldr :: (a -> b -> b) -> b -> RewriteEqn' qn p a -> b #

foldr' :: (a -> b -> b) -> b -> RewriteEqn' qn p a -> b #

foldl :: (b -> a -> b) -> b -> RewriteEqn' qn p a -> b #

foldl' :: (b -> a -> b) -> b -> RewriteEqn' qn p a -> b #

foldr1 :: (a -> a -> a) -> RewriteEqn' qn p a -> a #

foldl1 :: (a -> a -> a) -> RewriteEqn' qn p a -> a #

toList :: RewriteEqn' qn p a -> [a] #

null :: RewriteEqn' qn p a -> Bool #

length :: RewriteEqn' qn p a -> Int #

elem :: Eq a => a -> RewriteEqn' qn p a -> Bool #

maximum :: Ord a => RewriteEqn' qn p a -> a #

minimum :: Ord a => RewriteEqn' qn p a -> a #

sum :: Num a => RewriteEqn' qn p a -> a #

product :: Num a => RewriteEqn' qn p a -> a #

Traversable (RewriteEqn' qn p) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverse :: Applicative f => (a -> f b) -> RewriteEqn' qn p a -> f (RewriteEqn' qn p b) #

sequenceA :: Applicative f => RewriteEqn' qn p (f a) -> f (RewriteEqn' qn p a) #

mapM :: Monad m => (a -> m b) -> RewriteEqn' qn p a -> m (RewriteEqn' qn p b) #

sequence :: Monad m => RewriteEqn' qn p (m a) -> m (RewriteEqn' qn p a) #

(Eq qn, Eq e, Eq p) => Eq (RewriteEqn' qn p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: RewriteEqn' qn p e -> RewriteEqn' qn p e -> Bool #

(/=) :: RewriteEqn' qn p e -> RewriteEqn' qn p e -> Bool #

(Data qn, Data p, Data e) => Data (RewriteEqn' qn p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RewriteEqn' qn p e -> c (RewriteEqn' qn p e) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RewriteEqn' qn p e) #

toConstr :: RewriteEqn' qn p e -> Constr #

dataTypeOf :: RewriteEqn' qn p e -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RewriteEqn' qn p e)) #

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (RewriteEqn' qn p e)) #

gmapT :: (forall b. Data b => b -> b) -> RewriteEqn' qn p e -> RewriteEqn' qn p e #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RewriteEqn' qn p e -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RewriteEqn' qn p e -> r #

gmapQ :: (forall d. Data d => d -> u) -> RewriteEqn' qn p e -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RewriteEqn' qn p e -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) #

(Show qn, Show e, Show p) => Show (RewriteEqn' qn p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> RewriteEqn' qn p e -> ShowS #

show :: RewriteEqn' qn p e -> String #

showList :: [RewriteEqn' qn p e] -> ShowS #

(NFData qn, NFData p, NFData e) => NFData (RewriteEqn' qn p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: RewriteEqn' qn p e -> () #

(Pretty p, Pretty e) => Pretty (RewriteEqn' qn p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: RewriteEqn' qn p e -> Doc Source #

prettyPrec :: Int -> RewriteEqn' qn p e -> Doc Source #

prettyList :: [RewriteEqn' qn p e] -> Doc Source #

(KillRange qn, KillRange e, KillRange p) => KillRange (RewriteEqn' qn p e) Source # 
Instance details

Defined in Agda.Syntax.Common

(HasRange qn, HasRange p, HasRange e) => HasRange (RewriteEqn' qn p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: RewriteEqn' qn p e -> Range Source #

(ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn p e) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> RewriteEqn' qn p e -> RewriteEqn' qn p e Source #

traverseExpr :: Monad m => (Expr -> m Expr) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) Source #

foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn p e -> m Source #

(AllNames qn, AllNames e) => AllNames (RewriteEqn' qn p e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

allNames :: RewriteEqn' qn p e -> Seq QName Source #

(ExprLike qn, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn p e) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) Source #

foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn p e -> m Source #

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) Source #

mapExpr :: (Expr -> Expr) -> RewriteEqn' qn p e -> RewriteEqn' qn p e Source #

ToAbstract (RewriteEqn' () Pattern Expr) RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

(ToConcrete p q, ToConcrete a b) => ToConcrete (RewriteEqn' qn p a) (RewriteEqn' () q b) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: RewriteEqn' qn p a -> AbsToCon (RewriteEqn' () q b) Source #

bindToConcrete :: RewriteEqn' qn p a -> (RewriteEqn' () q b -> AbsToCon b0) -> AbsToCon b0 Source #

Information on expanded ellipsis (...)

data ExpandedEllipsis Source #

Instances
Eq ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

Data ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExpandedEllipsis -> c ExpandedEllipsis #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExpandedEllipsis #

toConstr :: ExpandedEllipsis -> Constr #

dataTypeOf :: ExpandedEllipsis -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExpandedEllipsis) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExpandedEllipsis) #

gmapT :: (forall b. Data b => b -> b) -> ExpandedEllipsis -> ExpandedEllipsis #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExpandedEllipsis -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExpandedEllipsis -> r #

gmapQ :: (forall d. Data d => d -> u) -> ExpandedEllipsis -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ExpandedEllipsis -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExpandedEllipsis -> m ExpandedEllipsis #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandedEllipsis -> m ExpandedEllipsis #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandedEllipsis -> m ExpandedEllipsis #

Show ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

NFData ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ExpandedEllipsis -> () #

Null ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj ExpandedEllipsis Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

type Notation = [GenPart] Source #

Notation as provided by the syntax declaration.

data GenPart Source #

Part of a Notation

Constructors

BindHole Range (Ranged Int)

Argument is the position of the hole (with binding) where the binding should occur. First range is the rhs range and second is the binder.

NormalHole Range (NamedArg (Ranged Int))

Argument is where the expression should go.

WildHole (Ranged Int)

An underscore in binding position.

IdPart RString 
Instances
Eq GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: GenPart -> GenPart -> Bool #

(/=) :: GenPart -> GenPart -> Bool #

Data GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GenPart -> c GenPart #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GenPart #

toConstr :: GenPart -> Constr #

dataTypeOf :: GenPart -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GenPart) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GenPart) #

gmapT :: (forall b. Data b => b -> b) -> GenPart -> GenPart #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GenPart -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GenPart -> r #

gmapQ :: (forall d. Data d => d -> u) -> GenPart -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> GenPart -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart #

Ord GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

Show GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

NFData GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: GenPart -> () #

Pretty GenPart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange GenPart Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj GenPart Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common