Agda-2.6.2.2.20221128: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Common

Description

Some common syntactic entities are defined in this module.

Synopsis

Documentation

type Nat = Int Source #

type Arity = Nat Source #

Delayed

data Delayed Source #

Used to specify whether something should be delayed.

Constructors

Delayed 
NotDelayed 

Instances

Instances details
KillRange Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Delayed Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Generic Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Delayed :: Type -> Type #

Methods

from :: Delayed -> Rep Delayed x #

to :: Rep Delayed x -> Delayed #

Show Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Delayed -> () #

Eq Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Ord Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Delayed Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Delayed = D1 ('MetaData "Delayed" "Agda.Syntax.Common" "Agda-2.6.2.2.20221128-inplace" 'False) (C1 ('MetaCons "Delayed" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotDelayed" 'PrefixI 'False) (U1 :: Type -> Type))

File

data FileType Source #

Instances

Instances details
EmbPrj FileType Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Pretty FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Generic FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep FileType :: Type -> Type #

Methods

from :: FileType -> Rep FileType x #

to :: Rep FileType x -> FileType #

Show FileType Source # 
Instance details

Defined in Agda.Syntax.Common

NFData FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: FileType -> () #

Eq FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Ord FileType Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep FileType Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep FileType = D1 ('MetaData "FileType" "Agda.Syntax.Common" "Agda-2.6.2.2.20221128-inplace" 'False) ((C1 ('MetaCons "AgdaFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MdFileType" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RstFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TexFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OrgFileType" 'PrefixI 'False) (U1 :: Type -> Type))))

Agda variants

data Cubical Source #

Variants of Cubical Agda.

Constructors

CErased 
CFull 

Instances

Instances details
EmbPrj Cubical Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Generic Cubical Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Cubical :: Type -> Type #

Methods

from :: Cubical -> Rep Cubical x #

to :: Rep Cubical x -> Cubical #

Show Cubical Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Cubical Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Cubical -> () #

Eq Cubical Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

type Rep Cubical Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Cubical = D1 ('MetaData "Cubical" "Agda.Syntax.Common" "Agda-2.6.2.2.20221128-inplace" 'False) (C1 ('MetaCons "CErased" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CFull" 'PrefixI 'False) (U1 :: Type -> Type))

data Language Source #

Agda variants.

Only some variants are tracked.

Constructors

WithoutK 
WithK 
Cubical Cubical 

Instances

Instances details
KillRange Language Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Language Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Generic Language Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Language :: Type -> Type #

Methods

from :: Language -> Rep Language x #

to :: Rep Language x -> Language #

Show Language Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Language Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Language -> () #

Eq Language Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Language Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Language = D1 ('MetaData "Language" "Agda.Syntax.Common" "Agda-2.6.2.2.20221128-inplace" 'False) (C1 ('MetaCons "WithoutK" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WithK" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Cubical" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cubical))))

Record Directives

data RecordDirectives' a Source #

Instances

Instances details
DeclaredNames RecordDirectives Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Functor RecordDirectives' Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange a => HasRange (RecordDirectives' a) Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange a => KillRange (RecordDirectives' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Show a => Show (RecordDirectives' a) Source # 
Instance details

Defined in Agda.Syntax.Common

NFData a => NFData (RecordDirectives' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: RecordDirectives' a -> () #

Eq a => Eq (RecordDirectives' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Eta-equality

data HasEta' a Source #

Does a record come with eta-equality?

Constructors

YesEta 
NoEta a 

Instances

Instances details
CopatternMatchingAllowed HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

PatternMatchingAllowed HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

Foldable HasEta' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => HasEta' m -> m #

foldMap :: Monoid m => (a -> m) -> HasEta' a -> m #

foldMap' :: Monoid m => (a -> m) -> HasEta' a -> m #

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

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

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

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

foldr1 :: (a -> a -> a) -> HasEta' a -> a #

foldl1 :: (a -> a -> a) -> HasEta' a -> a #

toList :: HasEta' a -> [a] #

null :: HasEta' a -> Bool #

length :: HasEta' a -> Int #

elem :: Eq a => a -> HasEta' a -> Bool #

maximum :: Ord a => HasEta' a -> a #

minimum :: Ord a => HasEta' a -> a #

sum :: Num a => HasEta' a -> a #

product :: Num a => HasEta' a -> a #

Traversable HasEta' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

sequenceA :: Applicative f => HasEta' (f a) -> f (HasEta' a) #

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

sequence :: Monad m => HasEta' (m a) -> m (HasEta' a) #

Functor HasEta' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> HasEta' a -> HasEta' b #

(<$) :: a -> HasEta' b -> HasEta' a #

HasRange a => HasRange (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: HasEta' a -> Range Source #

KillRange a => KillRange (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj a => EmbPrj (HasEta' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Show a => Show (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> HasEta' a -> ShowS #

show :: HasEta' a -> String #

showList :: [HasEta' a] -> ShowS #

NFData a => NFData (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: HasEta' a -> () #

Eq a => Eq (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Ord a => Ord (HasEta' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: HasEta' a -> HasEta' a -> Ordering #

(<) :: HasEta' a -> HasEta' a -> Bool #

(<=) :: HasEta' a -> HasEta' a -> Bool #

(>) :: HasEta' a -> HasEta' a -> Bool #

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

max :: HasEta' a -> HasEta' a -> HasEta' a #

min :: HasEta' a -> HasEta' a -> HasEta' a #

type HasEta = HasEta' PatternOrCopattern Source #

Pattern and copattern matching is allowed in the presence of eta.

In the absence of eta, we have to choose whether we want to allow matching on the constructor or copattern matching with the projections. Having both leads to breakage of subject reduction (issue #4560).

data PatternOrCopattern Source #

For a record without eta, which type of matching do we allow?

Constructors

PatternMatching

Can match on the record constructor.

CopatternMatching

Can copattern match using the projections. (Default.)

Instances

Instances details
CopatternMatchingAllowed HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

CopatternMatchingAllowed PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

PatternMatchingAllowed HasEta Source # 
Instance details

Defined in Agda.Syntax.Common

PatternMatchingAllowed PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj PatternOrCopattern Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Bounded PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

Enum PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

Show PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

NFData PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: PatternOrCopattern -> () #

Eq PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

Ord PatternOrCopattern Source # 
Instance details

Defined in Agda.Syntax.Common

Induction

data Induction Source #

Inductive < Coinductive

Constructors

Inductive 
CoInductive 

Instances

Instances details
PatternMatchingAllowed Induction Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Induction Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Eq Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Ord Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Hiding

data Overlappable Source #

Constructors

YesOverlap 
NoOverlap 

data Hiding Source #

Instances

Instances details
LensHiding Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Verbalize Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Errors

ChooseFlex Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

EmbPrj Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Unquote Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Pretty Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid 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

Show Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Hiding -> () #

Eq Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Ord Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

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

Defined in Agda.Auto.Convert

Methods

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

data WithHiding a Source #

Decorating something with Hiding information.

Constructors

WithHiding 

Fields

Instances

Instances details
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 #

Foldable WithHiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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

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

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

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

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

toList :: WithHiding a -> [a] #

null :: WithHiding a -> Bool #

length :: WithHiding a -> Int #

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

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

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

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

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

Traversable WithHiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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 #

Functor WithHiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

Defined in Agda.Syntax.Abstract.Views

LensHiding (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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 #

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

Defined in Agda.Syntax.Common

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

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (WithHiding a) Source #

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (WithHiding c) 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 #

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (WithHiding a) Source #

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

Defined in Agda.Syntax.Concrete.Pretty

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

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

Defined in Agda.Syntax.Common

Methods

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

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

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

Defined in Agda.Syntax.Common

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

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Monad.Context

type ConOfAbs (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfCon (WithHiding c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type SubstArg (WithHiding a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

class LensHiding a where Source #

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

Minimal complete definition

Nothing

Methods

getHiding :: a -> Hiding Source #

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

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

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

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

Instances

Instances details
LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

LensHiding ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensHiding (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getHiding :: Arg e -> Hiding Source #

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

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

LensHiding (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

LensHiding a => LensHiding (Named nm a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getHiding :: Named nm a -> Hiding Source #

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

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

LensHiding (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Monoidal composition of Hiding information in some data.

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

NotHidden arguments are visible.

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

Instance and Hidden arguments are notVisible.

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

Hidden arguments are hidden.

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

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

Ignores Overlappable.

Modalities

newtype UnderAddition t Source #

Type wrapper to indicate additive monoid/semigroup context.

Constructors

UnderAddition t 

Instances

Instances details
Applicative UnderAddition Source # 
Instance details

Defined in Agda.Syntax.Common

Functor UnderAddition Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

POMonoid (UnderAddition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

PartialOrd t => PartialOrd (UnderAddition t) Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Cohesion) Source #

Squash is the additive unit.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Modality) Source #

Pointwise additive unit.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Cohesion) Source #

Cohesion forms a semigroup under addition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Modality) Source #

Pointwise addition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

Show t => Show (UnderAddition t) Source # 
Instance details

Defined in Agda.Syntax.Common

Eq t => Eq (UnderAddition t) Source # 
Instance details

Defined in Agda.Syntax.Common

Ord t => Ord (UnderAddition t) Source # 
Instance details

Defined in Agda.Syntax.Common

newtype UnderComposition t Source #

Type wrapper to indicate composition or multiplicative monoid/semigroup context.

Constructors

UnderComposition t 

Instances

Instances details
Applicative UnderComposition Source # 
Instance details

Defined in Agda.Syntax.Common

Functor UnderComposition Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

LeftClosedPOMonoid (UnderComposition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid (UnderComposition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid (UnderComposition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid (UnderComposition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

PartialOrd t => PartialOrd (UnderComposition t) Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Cohesion) Source #

Continous is the multiplicative unit.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Modality) Source #

Pointwise composition unit.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Quantity) Source #

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

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Relevance) Source #

Relevant is the unit under composition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Cohesion) Source #

Cohesion forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Erased) Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Modality) Source #

Pointwise composition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Quantity) Source #

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Right-biased for origin.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Relevance) Source #

Relevance forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

Show t => Show (UnderComposition t) Source # 
Instance details

Defined in Agda.Syntax.Common

Eq t => Eq (UnderComposition t) Source # 
Instance details

Defined in Agda.Syntax.Common

Ord t => Ord (UnderComposition t) Source # 
Instance details

Defined in Agda.Syntax.Common

data Modality Source #

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

Constructors

Modality 

Fields

  • modRelevance :: Relevance

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

  • modQuantity :: Quantity

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

  • modCohesion :: Cohesion

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

Instances

Instances details
LensCohesion Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance Modality Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Modality Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Verbalize Modality Source # 
Instance details

Defined in Agda.TypeChecking.Errors

PrettyTCM Modality Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

EmbPrj Modality Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Unquote Modality Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

PartialOrd Modality Source #

Dominance ordering.

Instance details

Defined in Agda.Syntax.Common

Pretty Modality Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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 #

Show Modality Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Modality -> () #

Eq Modality Source # 
Instance details

Defined in Agda.Syntax.Common

Ord Modality Source # 
Instance details

Defined in Agda.Syntax.Common

IsVarSet () AllowedVar Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

LeftClosedPOMonoid (UnderComposition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Modality) Source #

Pointwise additive unit.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Modality) Source #

Pointwise composition unit.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Modality) Source #

Pointwise addition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Modality) Source #

Pointwise composition.

Instance details

Defined in Agda.Syntax.Common

type Rep Modality Source # 
Instance details

Defined in Agda.Syntax.Common

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

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

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

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

Multiplicative monoid (standard monoid).

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

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

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

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

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

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

Note that this function does not change quantities.

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

Modality forms a pointwise additive monoid.

zeroModality :: Modality Source #

Identity under addition

unitModality :: Modality Source #

Identity under composition

topModality :: Modality Source #

Absorptive element under addition.

defaultModality :: Modality Source #

The default Modality Beware that this is neither the additive unit nor the unit under composition, because the default quantity is ω.

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

Equality ignoring origin.

class LensModality a where Source #

Minimal complete definition

Nothing

Methods

getModality :: a -> Modality Source #

default getModality :: LensArgInfo a => a -> Modality Source #

setModality :: Modality -> a -> a Source #

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

default mapModality :: LensArgInfo a => (Modality -> Modality) -> a -> a Source #

Instances

Instances details
LensModality ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality MetaInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality MetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality RemoteMetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality (VarOcc' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

LensModality (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

LensModality (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Defined in Agda.TypeChecking.Free.Lazy

Quantities

Quantity origin.

data Q0Origin Source #

Origin of Quantity0.

Constructors

Q0Inferred

User wrote nothing.

Q0 Range

User wrote "@0".

Q0Erased Range

User wrote "@erased".

Instances

Instances details
HasRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Q0Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Null Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Monoid Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

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

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 #

Show Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Q0Origin -> () #

Eq Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Ord Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

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

data Q1Origin Source #

Origin of Quantity1.

Constructors

Q1Inferred

User wrote nothing.

Q1 Range

User wrote "@1".

Q1Linear Range

User wrote "@linear".

Instances

Instances details
HasRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Q1Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Null Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Monoid Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

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

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 #

Show Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Q1Origin -> () #

Eq Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Ord Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

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

data QωOrigin Source #

Origin of Quantityω.

Constructors

QωInferred

User wrote nothing.

Range

User wrote "@ω".

QωPlenty Range

User wrote "@plenty".

Instances

Instances details
HasRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj QωOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Null QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Monoid QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

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

Generic QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

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

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

Eq QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Ord QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

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

Instances for Q0Origin.

Instances for Q1Origin.

Instances for QωOrigin.

Quantity.

data Quantity Source #

Quantity for linearity.

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

Constructors

Quantity0 Q0Origin

Zero uses {0}, erased at runtime.

Quantity1 Q1Origin

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

Quantityω QωOrigin

Unrestricted use .

Instances

Instances details
LensQuantity Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Verbalize Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Errors

PrettyTCM Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

EmbPrj Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Unquote Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

PartialOrd Quantity Source #

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

Instance details

Defined in Agda.Syntax.Common

Pretty Quantity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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 #

Show Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Quantity -> () #

Eq Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

Ord Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid (UnderComposition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Quantity) Source #

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

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Quantity) Source #

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Right-biased for origin.

Instance details

Defined in Agda.Syntax.Common

type Rep Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

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

Equality ignoring origin.

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

Quantity forms an additive monoid with zero Quantity0.

zeroQuantity :: Quantity Source #

Identity element under addition

defaultQuantity :: Quantity Source #

Absorptive element! This differs from Relevance and Cohesion whose default is the multiplicative unit.

unitQuantity :: Quantity Source #

Identity element under composition

topQuantity :: Quantity Source #

Absorptive element is ω.

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

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

composeQuantity :: Quantity -> Quantity -> Quantity Source #

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Right-biased for origin.

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

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

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

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

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

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

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

Did the user supply a quantity annotation?

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

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

class LensQuantity a where Source #

Minimal complete definition

Nothing

Methods

getQuantity :: a -> Quantity Source #

setQuantity :: Quantity -> a -> a Source #

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

default mapQuantity :: LensModality a => (Quantity -> Quantity) -> a -> a Source #

Instances

Instances details
LensQuantity ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity Quantity Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity MetaInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity MetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity RemoteMetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity (VarOcc' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

LensQuantity (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Defined in Agda.TypeChecking.Free.Lazy

Erased.

data Erased Source #

A special case of Quantity: erased or not.

Instances

Instances details
HasRange Erased Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Erased Source # 
Instance details

Defined in Agda.Syntax.Common

Generic Erased Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Erased :: Type -> Type #

Methods

from :: Erased -> Rep Erased x #

to :: Rep Erased x -> Erased #

Show Erased Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Erased Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Erased -> () #

Eq Erased Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Semigroup (UnderComposition Erased) Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Erased Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Erased = D1 ('MetaData "Erased" "Agda.Syntax.Common" "Agda-2.6.2.2.20221128-inplace" 'False) (C1 ('MetaCons "Erased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Q0Origin)) :+: C1 ('MetaCons "NotErased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QωOrigin)))

defaultErased :: Erased Source #

The default value of type Erased: not erased.

asQuantity :: Erased -> Quantity Source #

Erased can be embedded into Quantity.

sameErased :: Erased -> Erased -> Bool Source #

Equality ignoring origin.

isErased :: Erased -> Bool Source #

Is the value "erased"?

composeErased :: Erased -> Erased -> Erased Source #

Composition of values of type Erased.

Erased is dominant. NotErased is neutral.

Right-biased for the origin.

Relevance

data Relevance Source #

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

Constructors

Relevant

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

NonStrict

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

Irrelevant

The argument is irrelevant at compile- and runtime.

Instances

Instances details
LensRelevance Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Verbalize Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Errors

PrettyTCM Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

EmbPrj Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Unquote Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

PartialOrd Relevance Source #

More relevant is smaller.

Instance details

Defined in Agda.Syntax.Common

Pretty Relevance Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Bounded Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

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

Show Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Relevance -> () #

Eq Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

Ord Relevance Source #

More relevant is smaller.

Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid (UnderComposition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Relevance) Source #

Relevant is the unit under composition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Relevance) Source #

Relevance forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

type Rep Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

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

class LensRelevance a where Source #

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

Minimal complete definition

Nothing

Instances

Instances details
LensRelevance ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance Modality Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance Relevance Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensRelevance Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensRelevance MetaInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensRelevance MetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensRelevance RemoteMetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensRelevance TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensRelevance (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance (VarOcc' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

LensRelevance (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Free.Lazy

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

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

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

Equality ignoring origin.

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

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

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

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

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

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

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

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

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

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

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

Combine inferred Relevance. The unit is Irrelevant.

zeroRelevance :: Relevance Source #

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

unitRelevance :: Relevance Source #

Identity element under composition

topRelevance :: Relevance Source #

Absorptive element under addition.

defaultRelevance :: Relevance Source #

Default Relevance is the identity element under composition

irrToNonStrict :: Relevance -> Relevance Source #

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

nonStrictToRel :: Relevance -> Relevance Source #

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

Annotations

data Annotation Source #

We have a tuple of annotations, which might not be fully orthogonal.

Constructors

Annotation 

Fields

  • annLock :: Lock

    Fitch-style dependent right adjoints. See Modal Dependent Type Theory and Dependent Right Adjoints, arXiv:1804.05236.

Instances

Instances details
LensAnnotation Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Annotation Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Generic Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Annotation :: Type -> Type #

Show Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Annotation -> () #

Eq Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

Ord Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Annotation Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Annotation = D1 ('MetaData "Annotation" "Agda.Syntax.Common" "Agda-2.6.2.2.20221128-inplace" 'False) (C1 ('MetaCons "Annotation" 'PrefixI 'True) (S1 ('MetaSel ('Just "annLock") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Lock)))

Locks

data Lock Source #

Constructors

IsNotLock 
IsLock

In the future there might be different kinds of them. For now we assume lock weakening.

Instances

Instances details
LensLock Lock Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Lock Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Bounded Lock Source # 
Instance details

Defined in Agda.Syntax.Common

Enum Lock Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

succ :: Lock -> Lock #

pred :: Lock -> Lock #

toEnum :: Int -> Lock #

fromEnum :: Lock -> Int #

enumFrom :: Lock -> [Lock] #

enumFromThen :: Lock -> Lock -> [Lock] #

enumFromTo :: Lock -> Lock -> [Lock] #

enumFromThenTo :: Lock -> Lock -> Lock -> [Lock] #

Generic Lock Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep Lock :: Type -> Type #

Methods

from :: Lock -> Rep Lock x #

to :: Rep Lock x -> Lock #

Show Lock Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> Lock -> ShowS #

show :: Lock -> String #

showList :: [Lock] -> ShowS #

NFData Lock Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Lock -> () #

Eq Lock Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Ord Lock Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Lock -> Lock -> Ordering #

(<) :: Lock -> Lock -> Bool #

(<=) :: Lock -> Lock -> Bool #

(>) :: Lock -> Lock -> Bool #

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

max :: Lock -> Lock -> Lock #

min :: Lock -> Lock -> Lock #

type Rep Lock Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep Lock = D1 ('MetaData "Lock" "Agda.Syntax.Common" "Agda-2.6.2.2.20221128-inplace" 'False) (C1 ('MetaCons "IsNotLock" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsLock" 'PrefixI 'False) (U1 :: Type -> Type))

class LensLock a where Source #

Minimal complete definition

getLock

Methods

getLock :: a -> Lock Source #

setLock :: Lock -> a -> a Source #

mapLock :: (Lock -> Lock) -> a -> a Source #

Instances

Instances details
LensLock ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensLock Lock Source # 
Instance details

Defined in Agda.Syntax.Common

LensLock (Arg t) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getLock :: Arg t -> Lock Source #

setLock :: Lock -> Arg t -> Arg t Source #

mapLock :: (Lock -> Lock) -> Arg t -> Arg t Source #

Cohesion

data Cohesion Source #

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

Constructors

Flat

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

Continuous

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

Squash

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

Instances

Instances details
LensCohesion Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Verbalize Cohesion Source # 
Instance details

Defined in Agda.TypeChecking.Errors

EmbPrj Cohesion Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

PartialOrd Cohesion Source #

Flatter is smaller.

Instance details

Defined in Agda.Syntax.Common

Pretty Cohesion Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Bounded Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

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

Show Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Cohesion -> () #

Eq Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Ord Cohesion Source #

Order is given by implication: flatter is smaller.

Instance details

Defined in Agda.Syntax.Common

LeftClosedPOMonoid (UnderComposition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid (UnderAddition Cohesion) Source #

Squash is the additive unit.

Instance details

Defined in Agda.Syntax.Common

Monoid (UnderComposition Cohesion) Source #

Continous is the multiplicative unit.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Cohesion) Source #

Cohesion forms a semigroup under addition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Cohesion) Source #

Cohesion forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

type Rep Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

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

class LensCohesion a where Source #

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

Minimal complete definition

Nothing

Methods

getCohesion :: a -> Cohesion Source #

setCohesion :: Cohesion -> a -> a Source #

mapCohesion :: (Cohesion -> Cohesion) -> a -> a Source #

default mapCohesion :: LensModality a => (Cohesion -> Cohesion) -> a -> a Source #

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

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

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

Equality ignoring origin.

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

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

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

Cohesion composition. Squash is dominant, Continuous is neutral.

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

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

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

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

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

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

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

Combine inferred Cohesion. The unit is Squash.

zeroCohesion :: Cohesion Source #

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

unitCohesion :: Cohesion Source #

Identity under composition

topCohesion :: Cohesion Source #

Absorptive element under addition.

defaultCohesion :: Cohesion Source #

Default Cohesion is the identity element under composition

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

data Origin Source #

Origin of arguments.

Constructors

UserWritten

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

Inserted

E.g. inserted hidden arguments.

Reflected

Produced by the reflection machinery.

CaseSplit

Produced by an interactive case split.

Substitution

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

Instances

Instances details
LensOrigin Origin Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Origin Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Origin Source # 
Instance details

Defined in Agda.Syntax.Common

ChooseFlex Origin Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

EmbPrj Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Show Origin Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Origin -> () #

Eq Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Ord Origin Source # 
Instance details

Defined in Agda.Syntax.Common

data WithOrigin a Source #

Decorating something with Origin information.

Constructors

WithOrigin 

Fields

Instances

Instances details
MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

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 #

Foldable WithOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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

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

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

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

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

toList :: WithOrigin a -> [a] #

null :: WithOrigin a -> Bool #

length :: WithOrigin a -> Int #

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

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

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

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

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

Traversable WithOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

Functor WithOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

LensOrigin (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Concrete.Name

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

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (NamedArg (Pattern' a)) Source #

HasRange a => HasRange (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

PrettyTCM (NamedArg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (NamedArg Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Named_ Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Records

Methods

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.TypeChecking.Substitute.DeBruijn

IApplyVars p => IApplyVars (NamedArg p) Source # 
Instance details

Defined in Agda.TypeChecking.Telescope.Path

Methods

iApplyVars :: NamedArg p -> [Int] Source #

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

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

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

Defined in Agda.Syntax.Common

Methods

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

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

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

Defined in Agda.Syntax.Common

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

Defined in Agda.TypeChecking.Rewriting.Clause

AddContext (List1 (NamedArg Name), Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

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 #

type PatternVarOut (NamedArg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

class LensOrigin a where Source #

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

Minimal complete definition

Nothing

Methods

getOrigin :: a -> Origin Source #

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

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

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

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

Instances

Instances details
LensOrigin ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin Origin Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

LensOrigin (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getOrigin :: Arg e -> Origin Source #

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

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

LensOrigin (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin (Elim' a) Source #

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

Instance details

Defined in Agda.Syntax.Internal.Elim

LensOrigin (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

LensOrigin (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

Free variable annotations

data FreeVariables Source #

Constructors

UnknownFVs 
KnownFVs IntSet 

Instances

Instances details
LensFreeVariables FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj FreeVariables Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Monoid FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Show FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

NFData FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: FreeVariables -> () #

Eq FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Ord FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

class LensFreeVariables a where Source #

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

Minimal complete definition

Nothing

Argument decoration

data ArgInfo Source #

A function argument can be hidden and/or irrelevant.

Constructors

ArgInfo 

Fields

Instances

Instances details
LensAnnotation ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensArgInfo ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensCohesion ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensFreeVariables ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensHiding ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensLock ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensModality ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensOrigin ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensQuantity ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

EqualSy ArgInfo Source #

Ignore origin and free variables.

Instance details

Defined in Agda.TypeChecking.Abstract

ToTerm ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ChooseFlex ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

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)

Unquote ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Show ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

NFData ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ArgInfo -> () #

Eq ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Ord ArgInfo Source # 
Instance details

Defined in Agda.Syntax.Common

class LensArgInfo a where Source #

Minimal complete definition

getArgInfo

Methods

getArgInfo :: a -> ArgInfo Source #

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

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

Arguments

data Arg e Source #

Constructors

Arg 

Fields

Instances

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

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 #

Foldable Arg Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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

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

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

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

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

toList :: Arg a -> [a] #

null :: Arg a -> Bool #

length :: Arg a -> Int #

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

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

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

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

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

Traversable Arg Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

Functor Arg Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (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 Args (MM (ArgList O) (RefInfo O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

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

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

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

Instance details

Defined in Agda.Syntax.Internal.Pattern

PatternLike a b => PatternLike a (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 #

Conversion MOT (Exp O) Term Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Term Source #

Conversion MOT (Exp O) Type Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type 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 [Clause] [([Pat O], MExp O)] Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp 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 #

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

Defined in Agda.Syntax.Abstract

Methods

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

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

Defined in Agda.Syntax.Abstract.Name

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

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Arg a) Source #

Methods

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

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

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

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => Arg a -> m Source #

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

Defined in Agda.Syntax.Abstract.Views

LensAnnotation (Arg t) Source # 
Instance details

Defined in Agda.Syntax.Common

LensArgInfo (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

LensCohesion (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

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

LensLock (Arg t) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getLock :: Arg t -> Lock Source #

setLock :: Lock -> Arg t -> Arg t Source #

mapLock :: (Lock -> Lock) -> Arg t -> Arg t Source #

LensModality (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

Associated Types

type NameOf (Arg a) Source #

Methods

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

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 #

LensQuantity (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

LensRelevance (Arg e) Source # 
Instance details

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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 #

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (Arg (Pattern' a)) Source #

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

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (NamedArg (Pattern' a)) Source #

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

Defined in Agda.Syntax.Internal.Defs

Methods

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

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

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

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

Defined in Agda.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> Arg a -> m Source #

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

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Arg a -> m Source #

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

Defined in Agda.Syntax.Internal.Pattern

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

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar (Arg a) Source #

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

Defined in Agda.Syntax.Common

Methods

getRange :: Arg a -> Range 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 #

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Arg a) Source #

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Arg c) Source #

Methods

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

Reify i => Reify (Arg i) Source #

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

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Arg i) Source #

Methods

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

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

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Arg r) Source #

ToAbstract r => ToAbstract [Arg r] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef [Arg r] Source #

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

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Arg a -> 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 #

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 #

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

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

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

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

Defined in Agda.TypeChecking.Irrelevance

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

Defined in Agda.TypeChecking.Irrelevance

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

Defined in Agda.TypeChecking.MetaVars

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

Defined in Agda.TypeChecking.MetaVars

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Arg t -> Bool Source #

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Arg a -> tcm Bool Source #

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

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

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

Defined in Agda.TypeChecking.Positivity

PrettyTCM (Arg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Arg Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Arg Type) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Arg Bool) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (NamedArg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (NamedArg Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Records

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Arg a -> Maybe MetaId Source #

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

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: 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 #

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

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

Defined in Agda.TypeChecking.Rules.LHS

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 #

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Arg a) Source #

Methods

applySubst :: Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a Source #

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)

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

Defined in Agda.TypeChecking.Telescope

Methods

piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> Arg a -> m Type Source #

piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> Arg a -> m Type Source #

IApplyVars p => IApplyVars (NamedArg p) Source # 
Instance details

Defined in Agda.TypeChecking.Telescope.Path

Methods

iApplyVars :: NamedArg p -> [Int] Source #

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

Defined in Agda.TypeChecking.Unquote

Methods

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

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 #

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

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

Defined in Agda.Syntax.Common

Methods

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

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

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 #

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

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel (Arg b) Source #

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

Defined in Agda.TypeChecking.Patterns.Internal

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.Clause

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

Defined in Agda.TypeChecking.Rewriting.Clause

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatToTerm :: PureTCM m => Arg p -> m (Arg a) Source #

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

AddContext (List1 (Arg Name), Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 (NamedArg Name), Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([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 #

type ADotT (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ADotT (Arg a) = ADotT a
type NameOf (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Common

type NameOf (Arg a) = NameOf a
type PatternVarOut (Arg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

type PatternVarOut (Arg (Pattern' a)) = a
type PatternVarOut (NamedArg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

type PatVar (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

type PatVar (Arg a) = PatVar a
type PatVarLabel (Arg b) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

type ConOfAbs (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Arg a) = Arg (ConOfAbs a)
type AbsOfCon (Arg c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Arg c) = Arg (AbsOfCon c)
type ReifiesTo (Arg i) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Arg i) = Arg (ReifiesTo i)
type AbsOfRef (Arg r) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Arg r) = NamedArg (AbsOfRef r)
type AbsOfRef [Arg r] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef [Arg r] = [NamedArg (AbsOfRef r)]
type SubstArg (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Arg a) = SubstArg a

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

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

Precondition: The two lists should have equal length.

Names

class Eq a => Underscore a where Source #

Minimal complete definition

underscore

Named arguments

data Named name a Source #

Something potentially carrying a name.

Constructors

Named 

Fields

Instances

Instances details
MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

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

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

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

Instance details

Defined in Agda.Syntax.Internal.Pattern

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

Defined in Agda.Syntax.Internal.Pattern

Methods

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

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

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

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (NamedArg (Pattern' a)) Source #

PrettyTCM (NamedArg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (NamedArg Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Named_ Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Records

Methods

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

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.TypeChecking.Substitute.DeBruijn

IApplyVars p => IApplyVars (NamedArg p) Source # 
Instance details

Defined in Agda.TypeChecking.Telescope.Path

Methods

iApplyVars :: NamedArg p -> [Int] Source #

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

Foldable (Named name) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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

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

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

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

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

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

null :: Named name a -> Bool #

length :: Named name a -> Int #

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

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

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

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

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

Traversable (Named name) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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 #

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

Defined in Agda.TypeChecking.Rewriting.Clause

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 #

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

Defined in Agda.Syntax.Abstract.Name

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

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Named n a) Source #

Methods

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

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

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

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => Named name a -> m Source #

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

Defined in Agda.Syntax.Abstract.Views

LensHiding a => LensHiding (Named nm a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getHiding :: Named nm a -> Hiding Source #

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

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

LensNamed (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type NameOf (Named name a) Source #

Methods

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

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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 #

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

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Named n a -> m Source #

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

Defined in Agda.Syntax.Internal.Pattern

Methods

countPatternVars :: Named x a -> Int Source #

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

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar (Named s a) Source #

Methods

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

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

Defined in Agda.Syntax.Common

Methods

getRange :: Named name a -> Range Source #

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

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Named name a) Source #

Methods

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

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

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Named name c) Source #

Methods

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

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Named n i) Source #

Methods

reify :: MonadReify m => Named n i -> m (ReifiesTo (Named n i)) Source #

reifyWhen :: MonadReify m => Bool -> Named n i -> m (ReifiesTo (Named n i)) Source #

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Named name r) Source #

Methods

toAbstract :: MonadReflectedToAbstract m => Named name r -> m (AbsOfRef (Named name r)) Source #

Free t => Free (Named nm t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

AddContext (List1 (NamedArg Name), Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

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 #

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)

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

Defined in Agda.TypeChecking.Rules.LHS

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

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Named name a) Source #

Methods

applySubst :: Substitution' (SubstArg (Named name a)) -> Named name a -> Named name a Source #

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

Defined in Agda.TypeChecking.Telescope

Methods

piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> Named n a -> m Type Source #

piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> Named n a -> m Type Source #

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

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

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

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

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel (Named x b) Source #

Methods

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

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

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

Defined in Agda.TypeChecking.Patterns.Internal

Methods

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

type PatternVarOut (NamedArg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

type ADotT (Named n a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ADotT (Named n a) = ADotT a
type NameOf (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

type NameOf (Named name a) = name
type PatVar (Named s a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

type PatVar (Named s a) = PatVar a
type PatVarLabel (Named x b) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

type ConOfAbs (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Named name a) = Named name (ConOfAbs a)
type AbsOfCon (Named name c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Named name c) = Named name (AbsOfCon c)
type ReifiesTo (Named n i) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Named n i) = Named n (ReifiesTo i)
type AbsOfRef (Named name r) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Named name r) = Named name (AbsOfRef r)
type SubstArg (Named name a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Named name a) = SubstArg a

type Named_ = Named NamedName Source #

Standard naming.

type NamedName = WithOrigin (Ranged ArgName) Source #

Standard argument names.

sameName :: NamedName -> NamedName -> Bool Source #

Equality of argument names of things modulo Range' and Origin.

unnamed :: a -> Named name a Source #

isUnnamed :: Named name a -> Maybe a Source #

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

class LensNamed a where Source #

Accessor/editor for the nameOf component.

Minimal complete definition

Nothing

Associated Types

type NameOf a Source #

The type of the name

Methods

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

default lensNamed :: (Decoration f, LensNamed b, NameOf b ~ NameOf a, f b ~ a) => Lens' (Maybe (NameOf a)) a Source #

Instances

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

Defined in Agda.Syntax.Common

Associated Types

type NameOf (Arg a) Source #

Methods

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

LensNamed (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type NameOf (Maybe a) Source #

Methods

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

LensNamed (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type NameOf (Named name a) Source #

Methods

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

LensNamed (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

type NameOf (Dom' t e) Source #

Methods

lensNamed :: Lens' (Maybe (NameOf (Dom' t e))) (Dom' t e) Source #

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

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

namedSame :: (LensNamed a, LensNamed b, NameOf a ~ NamedName, NameOf b ~ NamedName) => a -> b -> Bool Source #

Equality of argument names of things modulo Range' and Origin.

fittingNamedArg :: (LensNamed arg, NameOf arg ~ NamedName, LensHiding arg, LensNamed dom, NameOf dom ~ NamedName, LensHiding dom) => arg -> dom -> Maybe Bool Source #

Does an argument arg fit the shape dom of the next expected argument?

The hiding has to match, and if the argument has a name, it should match the name of the domain.

Nothing should be __IMPOSSIBLE__, so use as @ fromMaybe IMPOSSIBLE $ fittingNamedArg arg dom @

type NamedArg a = Arg (Named_ a) Source #

Only Hidden arguments can have names.

namedArg :: NamedArg a -> a Source #

Get the content of a NamedArg.

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

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

updateNamedArgA :: Applicative f => (a -> f b) -> NamedArg a -> f (NamedArg b) Source #

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

setNamedArg a b = updateNamedArg (const b) a

ArgName

type ArgName = String Source #

Names in binders and arguments.

Range decoration.

data Ranged a Source #

Thing with range info.

Constructors

Ranged 

Fields

Instances

Instances details
MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

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 #

Foldable Ranged Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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

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

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

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

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

toList :: Ranged a -> [a] #

null :: Ranged a -> Bool #

length :: Ranged a -> Int #

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

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

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

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

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

Traversable Ranged Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

Functor Ranged Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Ranged a -> Bool Source #

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

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (NamedArg (Pattern' a)) Source #

HasRange (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Ranged a -> Range Source #

KillRange (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

PrettyTCM (NamedArg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (NamedArg Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Named_ Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Records

Methods

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

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 #

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.TypeChecking.Substitute.DeBruijn

IApplyVars p => IApplyVars (NamedArg p) Source # 
Instance details

Defined in Agda.TypeChecking.Telescope.Path

Methods

iApplyVars :: NamedArg p -> [Int] Source #

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

Defined in Agda.Syntax.Concrete.Pretty

Pretty a => Pretty (Ranged a) Source #

Ignores range.

Instance details

Defined in Agda.Syntax.Common

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

Eq a => Eq (Ranged a) Source #

Ignores range.

Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Ord a => Ord (Ranged a) Source #

Ignores range.

Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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

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

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

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

Defined in Agda.TypeChecking.Rewriting.Clause

AddContext (List1 (NamedArg Name), Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

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 #

type PatternVarOut (NamedArg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

unranged :: a -> Ranged a Source #

Thing with no range info.

Raw names (before parsing into name parts).

type RawName = String Source #

A RawName is some sort of string.

type RString = Ranged RawName Source #

String with range info.

Further constructor and projection info

data ConOrigin Source #

Where does the ConP or Con come from?

Constructors

ConOSystem

Inserted by system or expanded from an implicit pattern.

ConOCon

User wrote a constructor (pattern).

ConORec

User wrote a record (pattern).

ConOSplit

Generated by interactive case splitting.

Instances

Instances details
KillRange ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj ConOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Bounded ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Enum ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Generic ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep ConOrigin :: Type -> Type #

Show ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

NFData ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ConOrigin -> () #

Eq ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Ord ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep ConOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep ConOrigin = D1 ('MetaData "ConOrigin" "Agda.Syntax.Common" "Agda-2.6.2.2.20221128-inplace" 'False) ((C1 ('MetaCons "ConOSystem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConOCon" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ConORec" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConOSplit" 'PrefixI 'False) (U1 :: Type -> Type)))

bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin Source #

Prefer user-written over system-inserted.

data ProjOrigin Source #

Where does a projection come from?

Constructors

ProjPrefix

User wrote a prefix projection.

ProjPostfix

User wrote a postfix projection.

ProjSystem

Projection was generated by the system.

Instances

Instances details
KillRange ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj ProjOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Bounded ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Enum ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Generic ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep ProjOrigin :: Type -> Type #

Show ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

NFData ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ProjOrigin -> () #

Eq ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Ord ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep ProjOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep ProjOrigin = D1 ('MetaData "ProjOrigin" "Agda.Syntax.Common" "Agda-2.6.2.2.20221128-inplace" 'False) (C1 ('MetaCons "ProjPrefix" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ProjPostfix" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ProjSystem" 'PrefixI 'False) (U1 :: Type -> Type)))

Infixity, access, abstract, etc.

data IsInfix Source #

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

Constructors

InfixDef 
PrefixDef 

Instances

Instances details
Show IsInfix Source # 
Instance details

Defined in Agda.Syntax.Common

Eq IsInfix Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Ord IsInfix Source # 
Instance details

Defined in Agda.Syntax.Common

private blocks, public imports

data Access Source #

Access modifier.

Constructors

PrivateAccess Origin

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

PublicAccess 

Instances

Instances details
HasRange Access Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Access Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Access Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

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

Eq Access Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Ord Access Source # 
Instance details

Defined in Agda.Syntax.Common

abstract blocks

data IsAbstract Source #

Abstract or concrete.

Constructors

AbstractDef 
ConcreteDef 

Instances

Instances details
AnyIsAbstract IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

LensIsAbstract IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj IsAbstract Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Monoid IsAbstract Source #

Default is ConcreteDef.

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

Generic IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep IsAbstract :: Type -> Type #

Show IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

NFData IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: IsAbstract -> () #

Eq IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

Ord IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep IsAbstract = D1 ('MetaData "IsAbstract" "Agda.Syntax.Common" "Agda-2.6.2.2.20221128-inplace" 'False) (C1 ('MetaCons "AbstractDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConcreteDef" 'PrefixI 'False) (U1 :: Type -> Type))

class AnyIsAbstract a where Source #

Is any element of a collection an AbstractDef.

Minimal complete definition

Nothing

Methods

anyIsAbstract :: a -> IsAbstract Source #

default anyIsAbstract :: (Foldable t, AnyIsAbstract b, t b ~ a) => a -> IsAbstract Source #

Instances

Instances details
AnyIsAbstract IsAbstract Source # 
Instance details

Defined in Agda.Syntax.Common

AnyIsAbstract (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

AnyIsAbstract a => AnyIsAbstract (Maybe a) 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 #

instance blocks

data IsInstance Source #

Is this definition eligible for instance search?

Constructors

InstanceDef Range

Range of the instance keyword.

NotInstanceDef 

Instances

Instances details
HasRange IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

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

Eq IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

Ord IsInstance Source # 
Instance details

Defined in Agda.Syntax.Common

macro blocks

data IsMacro Source #

Is this a macro definition?

Constructors

MacroDef 
NotMacroDef 

Instances

Instances details
HasRange IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Generic IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep IsMacro :: Type -> Type #

Methods

from :: IsMacro -> Rep IsMacro x #

to :: Rep IsMacro x -> IsMacro #

Show IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

NFData IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: IsMacro -> () #

Eq IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Ord IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep IsMacro Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep IsMacro = D1 ('MetaData "IsMacro" "Agda.Syntax.Common" "Agda-2.6.2.2.20221128-inplace" 'False) (C1 ('MetaCons "MacroDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotMacroDef" 'PrefixI 'False) (U1 :: Type -> Type))

NameId

newtype ModuleNameHash Source #

Constructors

ModuleNameHash 

Instances

Instances details
EmbPrj ModuleNameHash Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

HasTag ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Tag ModuleNameHash Source #

ToJSON ModuleNameHash Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Show ModuleNameHash Source #

The record selector is not included in the resulting strings.

Instance details

Defined in Agda.Syntax.Common

NFData ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ModuleNameHash -> () #

Eq ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.Common

Ord ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.Common

Hashable ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.Common

NFData (BiMap RawTopLevelModuleName ModuleNameHash) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type Tag ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.Common

data NameId Source #

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

Constructors

NameId !Word64 !ModuleNameHash 

Instances

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

Pretty NameId Source # 
Instance details

Defined in Agda.Syntax.Common

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

Show NameId Source # 
Instance details

Defined in Agda.Syntax.Common

NFData NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: NameId -> () #

Eq NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Ord NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Hashable NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

hashWithSalt :: Int -> NameId -> Int

hash :: NameId -> Int

MonadFresh NameId AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Monad m => MonadFresh NameId (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

type Rep NameId Source # 
Instance details

Defined in Agda.Syntax.Common

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

Meta variables

data MetaId Source #

Meta-variable identifiers use the same structure as NameIds.

Constructors

MetaId 

Instances

Instances details
EncodeTCM MetaId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

GetDefs MetaId Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

NamesIn MetaId Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> MetaId -> m Source #

Reify MetaId Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo MetaId Source #

HasFresh MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

IsInstantiatedMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

UnFreezeMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source #

PrettyTCM MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => MetaId -> m Doc Source #

FromTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimType MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

EmbPrj MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Unquote MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Pretty MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

ToJSON MetaId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Enum MetaId Source # 
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 #

Show MetaId Source #

The record selectors are not included in the resulting strings.

Instance details

Defined in Agda.Syntax.Common

NFData MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: MetaId -> () #

Eq MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Ord MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Hashable MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

hashWithSalt :: Int -> MetaId -> Int

hash :: MetaId -> Int

Singleton MetaId MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Singleton MetaId () Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

singleton :: MetaId -> () Source #

InstantiateFull (Judgement MetaId) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

type ReifiesTo MetaId 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.2.2.20221128-inplace" 'False) (C1 ('MetaCons "MetaId" 'PrefixI 'True) (S1 ('MetaSel ('Just "metaId") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Just "metaModule") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash)))

Problems

newtype ProblemId Source #

A "problem" consists of a set of constraints and the same constraint can be part of multiple problems.

Constructors

ProblemId Nat 

Instances

Instances details
EncodeTCM ProblemId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

HasFresh ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Pretty ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

ToJSON ProblemId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Enum ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Num ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Integral ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Real ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Show ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

NFData ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ProblemId -> () #

Eq ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Ord ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Monad m => MonadFresh ProblemId (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Placeholders (used to parse sections)

data PositionInName Source #

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

Constructors

Beginning

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

Middle

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

End

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

data MaybePlaceholder e Source #

Placeholders are used to represent the underscores in a section.

Constructors

Placeholder !PositionInName 
NoPlaceholder !(Maybe PositionInName) e

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

Instances

Instances details
Foldable MaybePlaceholder Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

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

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

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

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

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

toList :: MaybePlaceholder a -> [a] #

null :: MaybePlaceholder a -> Bool #

length :: MaybePlaceholder a -> Int #

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

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

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

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

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

Traversable MaybePlaceholder Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

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

Functor MaybePlaceholder Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

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

Defined in Agda.Syntax.Concrete.Generic

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Concrete.Pretty

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

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

noPlaceholder :: e -> MaybePlaceholder e Source #

An abbreviation: noPlaceholder = NoPlaceholder Nothing.

Interaction meta variables

newtype InteractionId Source #

Constructors

InteractionId 

Fields

Instances

Instances details
EncodeTCM InteractionId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

KillRange InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

ToConcrete InteractionId Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs InteractionId Source #

HasFresh InteractionId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

ToJSON InteractionId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Enum InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Num InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Read InteractionId Source # 
Instance details

Defined in Agda.Interaction.Base

Integral InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Real InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Show InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

NFData InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: InteractionId -> () #

NFData InteractionPoints Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

rnf :: InteractionPoints -> () #

Eq InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Ord InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

type ConOfAbs InteractionId Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Fixity

type PrecedenceLevel = Double Source #

Precedence levels for operators.

data FixityLevel Source #

Constructors

Unrelated

No fixity declared.

Related !PrecedenceLevel

Fixity level declared as the number.

Instances

Instances details
ToTerm FixityLevel Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

EmbPrj FixityLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Null FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Show FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

NFData FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: FixityLevel -> () #

Eq FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

Ord FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

data Associativity Source #

Associativity.

Constructors

NonAssoc 
LeftAssoc 
RightAssoc 

data Fixity Source #

Fixity of operators.

Constructors

Fixity 

Fields

Instances

Instances details
LensFixity Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

ToTerm Fixity Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

EmbPrj Fixity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Null Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Fixity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Show Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Fixity -> () #

Eq Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Ord Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Notation coupled with Fixity

data Fixity' Source #

The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.

Constructors

Fixity' 

Fields

Instances

Instances details
LensFixity Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

LensFixity' Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

PrimTerm Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimType Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

EmbPrj Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Null Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Fixity' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Show Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

NFData Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Fixity' -> () #

Eq Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: Fixity' -> Fixity' -> Bool #

(/=) :: Fixity' -> Fixity' -> Bool #

class LensFixity' a where Source #

Instances

Instances details
LensFixity' Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

LensFixity' QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

LensFixity' Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

LensFixity' (ThingWithFixity a) Source # 
Instance details

Defined in Agda.Syntax.Fixity

Import directive

data ImportDirective' n m Source #

The things you are allowed to say when you shuffle names between name spaces (i.e. in import, namespace, or open declarations).

Constructors

ImportDirective 

Fields

Instances

Instances details
(HasRange a, HasRange b) => HasRange (ImportDirective' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(KillRange a, KillRange b) => KillRange (ImportDirective' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

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

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Common

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

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

Defined in Agda.Syntax.Common

defaultImportDir :: ImportDirective' n m Source #

Default is directive is private (use everything, but do not export).

isDefaultImportDir :: ImportDirective' n m -> Bool Source #

isDefaultImportDir implies null, but not the other way round.

data Using' n m Source #

The using clause of import directive.

Constructors

UseEverything

No using clause given.

Using [ImportedName' n m]

using the specified names.

Instances

Instances details
(HasRange a, HasRange b) => HasRange (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Using' a b -> Range Source #

(KillRange a, KillRange b) => KillRange (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

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 #

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 #

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 #

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

(NFData a, NFData b) => NFData (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: Using' a b -> () #

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

mapUsing :: ([ImportedName' n1 m1] -> [ImportedName' n2 m2]) -> Using' n1 m1 -> Using' n2 m2 Source #

data ImportedName' n m Source #

An imported name can be a module or a defined name.

Constructors

ImportedModule m

Imported module name of type m.

ImportedName n

Imported name of type n.

Instances

Instances details
(HasRange a, HasRange b) => HasRange (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(KillRange a, KillRange b) => KillRange (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

(Pretty a, Pretty b) => Pretty (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

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

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

Defined in Agda.Syntax.Common

partitionImportedNames :: [ImportedName' n m] -> ([n], [m]) Source #

Like partitionEithers.

data Renaming' n m Source #

Constructors

Renaming 

Fields

Instances

Instances details
(HasRange a, HasRange b) => HasRange (Renaming' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Renaming' a b -> Range Source #

(KillRange a, KillRange b) => KillRange (Renaming' a b) Source # 
Instance details

Defined in Agda.Syntax.Common

(Pretty a, Pretty b) => Pretty (Renaming' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

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

HasRange instances

KillRange instances

NFData instances

Termination

data TerminationCheck m Source #

Termination check? (Default = TerminationCheck).

Constructors

TerminationCheck

Run the termination checker.

NoTerminationCheck

Skip termination checking (unsafe).

NonTerminating

Treat as non-terminating.

Terminating

Treat as terminating (unsafe). Same effect as NoTerminationCheck.

TerminationMeasure Range m

Skip termination checking but use measure instead.

Instances

Instances details
Functor TerminationCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

KillRange m => KillRange (TerminationCheck m) Source # 
Instance details

Defined in Agda.Syntax.Common

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

Eq m => Eq (TerminationCheck m) Source # 
Instance details

Defined in Agda.Syntax.Common

Positivity

data PositivityCheck Source #

Positivity check? (Default = True).

Instances

Instances details
KillRange PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Bounded PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Enum PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Generic PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep PositivityCheck :: Type -> Type #

Show PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

NFData PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: PositivityCheck -> () #

Eq PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Ord PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep PositivityCheck = D1 ('MetaData "PositivityCheck" "Agda.Syntax.Common" "Agda-2.6.2.2.20221128-inplace" 'False) (C1 ('MetaCons "YesPositivityCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoPositivityCheck" 'PrefixI 'False) (U1 :: Type -> Type))

Universe checking

data UniverseCheck Source #

Universe check? (Default is yes).

Instances

Instances details
KillRange UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Bounded UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Enum UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Generic UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep UniverseCheck :: Type -> Type #

Show UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

NFData UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: UniverseCheck -> () #

Eq UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Ord UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep UniverseCheck Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep UniverseCheck = D1 ('MetaData "UniverseCheck" "Agda.Syntax.Common" "Agda-2.6.2.2.20221128-inplace" 'False) (C1 ('MetaCons "YesUniverseCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoUniverseCheck" 'PrefixI 'False) (U1 :: Type -> Type))

Universe checking

data CoverageCheck Source #

Coverage check? (Default is yes).

Instances

Instances details
KillRange CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Bounded CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Enum CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Generic CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep CoverageCheck :: Type -> Type #

Show CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

NFData CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: CoverageCheck -> () #

Eq CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Ord CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep CoverageCheck = D1 ('MetaData "CoverageCheck" "Agda.Syntax.Common" "Agda-2.6.2.2.20221128-inplace" 'False) (C1 ('MetaCons "YesCoverageCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoCoverageCheck" 'PrefixI 'False) (U1 :: Type -> Type))

Rewrite Directives on the LHS

data RewriteEqn' qn nm p e Source #

RewriteEqn' qn p e represents the rewrite and irrefutable with clauses of the LHS. qn stands for the QName of the auxiliary function generated to implement the feature nm is the type of names for pattern variables p is the type of patterns e is the type of expressions

Constructors

Rewrite (List1 (qn, e))
rewrite e
Invert qn (List1 (Named nm (p, e)))
with p <- e in eq

Instances

Instances details
ToAbstract RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RewriteEqn Source #

Foldable (RewriteEqn' qn nm p) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => RewriteEqn' qn nm p m -> m #

foldMap :: Monoid m => (a -> m) -> RewriteEqn' qn nm p a -> m #

foldMap' :: Monoid m => (a -> m) -> RewriteEqn' qn nm p a -> m #

foldr :: (a -> b -> b) -> b -> RewriteEqn' qn nm p a -> b #

foldr' :: (a -> b -> b) -> b -> RewriteEqn' qn nm p a -> b #

foldl :: (b -> a -> b) -> b -> RewriteEqn' qn nm p a -> b #

foldl' :: (b -> a -> b) -> b -> RewriteEqn' qn nm p a -> b #

foldr1 :: (a -> a -> a) -> RewriteEqn' qn nm p a -> a #

foldl1 :: (a -> a -> a) -> RewriteEqn' qn nm p a -> a #

toList :: RewriteEqn' qn nm p a -> [a] #

null :: RewriteEqn' qn nm p a -> Bool #

length :: RewriteEqn' qn nm p a -> Int #

elem :: Eq a => a -> RewriteEqn' qn nm p a -> Bool #

maximum :: Ord a => RewriteEqn' qn nm p a -> a #

minimum :: Ord a => RewriteEqn' qn nm p a -> a #

sum :: Num a => RewriteEqn' qn nm p a -> a #

product :: Num a => RewriteEqn' qn nm p a -> a #

Traversable (RewriteEqn' qn nm p) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

traverse :: Applicative f => (a -> f b) -> RewriteEqn' qn nm p a -> f (RewriteEqn' qn nm p b) #

sequenceA :: Applicative f => RewriteEqn' qn nm p (f a) -> f (RewriteEqn' qn nm p a) #

mapM :: Monad m => (a -> m b) -> RewriteEqn' qn nm p a -> m (RewriteEqn' qn nm p b) #

sequence :: Monad m => RewriteEqn' qn nm p (m a) -> m (RewriteEqn' qn nm p a) #

Functor (RewriteEqn' qn nm p) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

fmap :: (a -> b) -> RewriteEqn' qn nm p a -> RewriteEqn' qn nm p b #

(<$) :: a -> RewriteEqn' qn nm p b -> RewriteEqn' qn nm p a #

(ExprLike qn, ExprLike nm, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

(ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e Source #

foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn nm p e -> m Source #

traverseExpr :: Monad m => (Expr -> m Expr) -> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e) Source #

(HasRange qn, HasRange nm, HasRange p, HasRange e) => HasRange (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: RewriteEqn' qn nm p e -> Range Source #

(KillRange qn, KillRange nm, KillRange e, KillRange p) => KillRange (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (RewriteEqn' qn nm p e) Source #

(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (RewriteEqn' qn BindName p a) Source #

ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source #

(Pretty nm, Pretty p, Pretty e) => Pretty (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: RewriteEqn' qn nm p e -> Doc Source #

prettyPrec :: Int -> RewriteEqn' qn nm p e -> Doc Source #

prettyList :: [RewriteEqn' qn nm p e] -> Doc Source #

(Show e, Show qn, Show nm, Show p) => Show (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> RewriteEqn' qn nm p e -> ShowS #

show :: RewriteEqn' qn nm p e -> String #

showList :: [RewriteEqn' qn nm p e] -> ShowS #

(NFData qn, NFData nm, NFData p, NFData e) => NFData (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: RewriteEqn' qn nm p e -> () #

(Eq e, Eq qn, Eq nm, Eq p) => Eq (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e -> Bool #

(/=) :: RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e -> Bool #

type AbsOfCon RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type ConOfAbs (RewriteEqn' qn BindName p a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Information on expanded ellipsis (...)

data ExpandedEllipsis Source #

Instances

Instances details
KillRange ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj ExpandedEllipsis Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Null ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

Monoid ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

Show ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

NFData ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ExpandedEllipsis -> () #

Eq ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

type Notation = [NotationPart] Source #

Notation as provided by the syntax declaration.

data BoundVariablePosition Source #

Positions of variables in syntax declarations.

Constructors

BoundVariablePosition 

Fields

  • holeNumber :: !Int

    The position (in the left-hand side of the syntax declaration) of the hole in which the variable is bound, counting from zero (and excluding parts that are not holes). For instance, for syntax Σ A (λ x → B) = B , A , x the number for x is 1, corresponding to B (0 would correspond to A).

  • varNumber :: !Int

    The position in the list of variables for this particular variable, counting from zero, and including wildcards. For instance, for syntax F (λ x _ y → A) = y ! A ! x the number for x is 0, the number for _ is 1, and the number for y is 2.

data NotationPart Source #

Notation parts.

Constructors

IdPart RString

An identifier part. For instance, for _+_ the only identifier part is +.

HolePart Range (NamedArg (Ranged Int))

A hole: a place where argument expressions can be written. For instance, for _+_ the two underscores are holes, and for syntax Σ A (λ x → B) = B , A , x the variables A and B are holes. The number is the position of the hole, counting from zero. For instance, the number for A is 0, and the number for B is 1.

VarPart Range (Ranged BoundVariablePosition)

A bound variable.

The first range is the range of the variable in the right-hand side of the syntax declaration, and the second range is the range of the variable in the left-hand side.

WildPart (Ranged BoundVariablePosition)

A wildcard (an underscore in binding position).

Instances

Instances details
HasRange NotationPart Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange NotationPart Source # 
Instance details

Defined in Agda.Syntax.Common

SetRange NotationPart Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj NotationPart Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Pretty NotationPart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Show NotationPart Source # 
Instance details

Defined in Agda.Syntax.Common

NFData NotationPart Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: NotationPart -> () #

Eq NotationPart Source # 
Instance details

Defined in Agda.Syntax.Common

Ord NotationPart Source # 
Instance details

Defined in Agda.Syntax.Common