Documentation

Methods

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

HasRange ConHead Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

getRange :: ConHead -> Range Source #

KillRange ConHead Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT ConHead Source #

SetRange ConHead Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

setRange :: Range -> ConHead -> ConHead Source #

PrettyTCM ConHead Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

InstantiateFull ConHead Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ConHead -> ReduceM ConHead Source #

EmbPrj ConHead Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ConHead -> S Int32 Source #

icod_ :: ConHead -> S Int32 Source #

value :: Int32 -> R ConHead Source #

Generic ConHead Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep ConHead

Instance details

Defined in Agda.Syntax.Internal

type Rep ConHead = D1 ('MetaData "ConHead" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "ConHead" 'PrefixI 'True) ((S1 ('MetaSel ('Just "conName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "conDataRecord") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataOrRecord)) :*: (S1 ('MetaSel ('Just "conInductive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Induction) :*: S1 ('MetaSel ('Just "conFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg QName]))))

Methods

from :: ConHead -> Rep ConHead x #

to :: Rep ConHead x -> ConHead #

Show ConHead Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> ConHead -> ShowS #

show :: ConHead -> String #

showList :: [ConHead] -> ShowS #

NFData ConHead Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: ConHead -> () #

Eq ConHead Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Ord ConHead Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

compare :: ConHead -> ConHead -> Ordering #

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

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

(>) :: ConHead -> ConHead -> Bool #

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

max :: ConHead -> ConHead -> ConHead #

min :: ConHead -> ConHead -> ConHead #

type Rep ConHead Source #

Instance details

Defined in Agda.Syntax.Internal

type Rep ConHead = D1 ('MetaData "ConHead" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "ConHead" 'PrefixI 'True) ((S1 ('MetaSel ('Just "conName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "conDataRecord") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataOrRecord)) :*: (S1 ('MetaSel ('Just "conInductive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Induction) :*: S1 ('MetaSel ('Just "conFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg QName]))))

data Term Source #

Raw values.

Def is used for both defined and undefined constants. Assume there is a type declaration and a definition for every constant, even if the definition is an empty list of clauses.

Constructors

Var !Int Elims	`x es` neutral
Lam ArgInfo (Abs Term)	Terms are beta normal. Relevance is ignored
Lit Literal
Def QName Elims	`f es`, possibly a delta/iota-redex
Con ConHead ConInfo Elims	`c es` or `record { fs = es }` `es` allows only Apply and IApply eliminations, and IApply only for data constructors.
Pi (Dom Type) (Abs Type)	dependent or non-dependent function space
Sort Sort
Level Level
MetaV !MetaId Elims
DontCare Term	Irrelevant stuff in relevant position, but created in an irrelevant context. Basically, an internal version of the irrelevance axiom `.irrAx : .A -> A`.
Dummy String Elims	A (part of a) term or type which is only used for internal purposes. Replaces the `Sort Prop` hack. The `String` typically describes the location where we create this dummy, but can contain other information as well. The second field accumulates eliminations in case we apply a dummy term to more of them. Dummy terms should never be used in places where they can affect type checking, so syntactic checks are free to ignore the eliminators, which are only there to ease debugging when a dummy term incorrectly leaks into a relevant position.

Instances

Instances details

Pretty Level Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Level -> Doc Source #

prettyPrec :: Int -> Level -> Doc Source #

prettyList :: [Level] -> Doc Source #

Pretty PlusLevel Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: PlusLevel -> Doc Source #

prettyPrec :: Int -> PlusLevel -> Doc Source #

prettyList :: [PlusLevel] -> Doc Source #

Pretty Sort Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Sort -> Doc Source #

prettyPrec :: Int -> Sort -> Doc Source #

prettyList :: [Sort] -> Doc Source #

Pretty Term Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Term -> Doc Source #

prettyPrec :: Int -> Term -> Doc Source #

prettyList :: [Term] -> Doc Source #

Pretty Type Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Type -> Doc Source #

prettyPrec :: Int -> Type -> Doc Source #

prettyList :: [Type] -> Doc Source #

Pretty CompiledClauses Source #

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: CompiledClauses -> Doc Source #

prettyPrec :: Int -> CompiledClauses -> Doc Source #

prettyList :: [CompiledClauses] -> Doc Source #

LensSort Sort Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort Sort Source #

getSort :: Sort -> Sort Source #

Suggest Term Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

suggestName :: Term -> Maybe String Source #

TelToArgs ListTel Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

telToArgs :: ListTel -> [Arg ArgName] Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

TermSize Level Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

termSize :: Level -> Int Source #

tsize :: Level -> Sum Int Source #

TermSize PlusLevel Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

termSize :: PlusLevel -> Int Source #

tsize :: PlusLevel -> Sum Int Source #

TermSize Sort Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

termSize :: Sort -> Int Source #

tsize :: Sort -> Sum Int Source #

TermSize Term Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

termSize :: Term -> Int Source #

tsize :: Term -> Sum Int Source #

GetDefs Level Source #

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs PlusLevel Source #

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Sort Source #

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Term Source #

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Type Source #

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike Level Source #

Instance details

Methods

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

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

TermLike PlusLevel Source #

Instance details

Methods

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

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

TermLike Sort Source #

Instance details

Methods

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

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

TermLike Term Source #

Instance details

Methods

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

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

TermLike Type Source #

Instance details

Methods

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

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

AllMetas Level Source #

Instance details

Methods

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

AllMetas PlusLevel Source #

Instance details

Methods

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

AllMetas Sort Source #

Instance details

Methods

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

AllMetas Term Source #

Instance details

Methods

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

AllMetas Type Source #

Instance details

Methods

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

NamesIn Level Source #

Instance details

Methods

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

NamesIn PlusLevel Source #

Instance details

Methods

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

NamesIn Sort Source #

Instance details

Methods

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

NamesIn Term Source #

Instance details

Methods

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

NamesIn CompiledClauses Source #

Instance details

Methods

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

KillRange Level Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Level Source #

KillRange PlusLevel Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PlusLevel Source #

KillRange Sort Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Sort Source #

KillRange Substitution Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Substitution Source #

KillRange Term Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Term Source #

KillRange CompiledClauses Source #

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

killRange :: KillRangeT CompiledClauses Source #

Reify Level Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Level
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Level = Expr

Methods

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

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

Reify Sort Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Sort
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Sort = Expr

Methods

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

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

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Telescope = Telescope

Methods

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

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

Reify Term Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Term
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Term = Expr

Methods

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

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

Reify Type Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Type
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Type = Type

Methods

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

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

TerSetSizeDepth ListTel Source #

Instance details

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: ListTel -> TerM a -> TerM a Source #

Instance details

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: Telescope -> TerM a -> TerM a Source #

AbsTerm Level Source #

Instance details

Methods

absTerm :: Term -> Level -> Level Source #

AbsTerm PlusLevel Source #

Instance details

Methods

absTerm :: Term -> PlusLevel -> PlusLevel Source #

AbsTerm Sort Source #

Instance details

Methods

absTerm :: Term -> Sort -> Sort Source #

AbsTerm Term Source #

Instance details

Methods

absTerm :: Term -> Term -> Term Source #

AbsTerm Type Source #

Instance details

Methods

absTerm :: Term -> Type -> Type Source #

EqualSy Level Source #

Instance details

Methods

equalSy :: Level -> Level -> Bool Source #

EqualSy PlusLevel Source #

Instance details

Methods

equalSy :: PlusLevel -> PlusLevel -> Bool Source #

EqualSy Sort Source #

Instance details

Methods

equalSy :: Sort -> Sort -> Bool Source #

EqualSy Term Source #

Instance details

Methods

equalSy :: Term -> Term -> Bool Source #

EqualSy Type Source #

Ignores sorts.

Instance details

Methods

equalSy :: Type -> Type -> Bool Source #

IsPrefixOf Args Source #

Instance details

Methods

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

IsPrefixOf Elims Source #

Instance details

Methods

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

IsPrefixOf Term Source #

Instance details

Methods

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

CheckInternal Elims Source #

Instance details

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Elims -> Comparison -> TypeOf Elims -> m Elims Source #

checkInternal :: MonadCheckInternal m => Elims -> Comparison -> TypeOf Elims -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Elims ~ ()) => Action m -> Elims -> m Elims Source #

inferInternal :: (MonadCheckInternal m, TypeOf Elims ~ ()) => Elims -> m () Source #

CheckInternal Level Source #

Instance details

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Level -> Comparison -> TypeOf Level -> m Level Source #

checkInternal :: MonadCheckInternal m => Level -> Comparison -> TypeOf Level -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Level ~ ()) => Action m -> Level -> m Level Source #

inferInternal :: (MonadCheckInternal m, TypeOf Level ~ ()) => Level -> m () Source #

CheckInternal PlusLevel Source #

Instance details

Methods

checkInternal' :: MonadCheckInternal m => Action m -> PlusLevel -> Comparison -> TypeOf PlusLevel -> m PlusLevel Source #

checkInternal :: MonadCheckInternal m => PlusLevel -> Comparison -> TypeOf PlusLevel -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => Action m -> PlusLevel -> m PlusLevel Source #

inferInternal :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => PlusLevel -> m () Source #

CheckInternal Sort Source #

Instance details

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Sort -> Comparison -> TypeOf Sort -> m Sort Source #

checkInternal :: MonadCheckInternal m => Sort -> Comparison -> TypeOf Sort -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Action m -> Sort -> m Sort Source #

inferInternal :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Sort -> m () Source #

CheckInternal Term Source #

Instance details

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Term -> Comparison -> TypeOf Term -> m Term Source #

checkInternal :: MonadCheckInternal m => Term -> Comparison -> TypeOf Term -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Term ~ ()) => Action m -> Term -> m Term Source #

inferInternal :: (MonadCheckInternal m, TypeOf Term ~ ()) => Term -> m () Source #

CheckInternal Type Source #

Instance details

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Type -> Comparison -> TypeOf Type -> m Type Source #

checkInternal :: MonadCheckInternal m => Type -> Comparison -> TypeOf Type -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Type ~ ()) => Action m -> Type -> m Type Source #

inferInternal :: (MonadCheckInternal m, TypeOf Type ~ ()) => Type -> m () Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Methods

DropArgs Term Source #

Use for dropping initial lambdas in clause bodies. NOTE: does not reduce term, need lambdas to be present.

Instance details

Methods

dropArgs :: Int -> Term -> Term Source #

DropArgs CompiledClauses Source #

To drop the first n arguments in a compiled clause, we reduce the split argument indices by n and drop n arguments from the bodies. NOTE: this only works for non-recursive functions, we are not dropping arguments to recursive calls in bodies.

Instance details

Methods

dropArgs :: Int -> CompiledClauses -> CompiledClauses Source #

Free Level Source #

Instance details

Methods

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

Free Sort Source #

Instance details

Methods

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

Free Term Source #

Instance details

Methods

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

PrecomputeFreeVars Level Source #

Instance details

Methods

precomputeFreeVars :: Level -> FV Level Source #

PrecomputeFreeVars PlusLevel Source #

Instance details

Methods

precomputeFreeVars :: PlusLevel -> FV PlusLevel Source #

PrecomputeFreeVars Sort Source #

Instance details

Methods

precomputeFreeVars :: Sort -> FV Sort Source #

PrecomputeFreeVars Term Source #

Instance details

Methods

precomputeFreeVars :: Term -> FV Term Source #

PrecomputeFreeVars Type Source #

Instance details

Methods

precomputeFreeVars :: Type -> FV Type Source #

ForceNotFree Level Source #

Instance details

Methods

forceNotFree' :: MonadFreeRed m => Level -> m Level

ForceNotFree PlusLevel Source #

Instance details

Methods

forceNotFree' :: MonadFreeRed m => PlusLevel -> m PlusLevel

ForceNotFree Sort Source #

Instance details

Methods

forceNotFree' :: MonadFreeRed m => Sort -> m Sort

ForceNotFree Term Source #

Instance details

Methods

forceNotFree' :: MonadFreeRed m => Term -> m Term

ForceNotFree Type Source #

Instance details

Methods

forceNotFree' :: MonadFreeRed m => Type -> m Type

UsableModality Level Source #

Instance details

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Level -> m Bool Source #

UsableModality Sort Source #

Instance details

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Sort -> m Bool Source #

UsableModality Term Source #

Instance details

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Term -> m Bool Source #

UsableRelevance Level Source #

Instance details

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Level -> m Bool Source #

UsableRelevance PlusLevel Source #

Instance details

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> PlusLevel -> m Bool Source #

UsableRelevance Sort Source #

Instance details

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Sort -> m Bool Source #

UsableRelevance Term Source #

Instance details

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Term -> m Bool Source #

NoProjectedVar Term Source #

Instance details

Defined in Agda.TypeChecking.MetaVars

Methods

noProjectedVar :: Term -> Either ProjectedVar () Source #

ReduceAndEtaContract Term Source #

Instance details

Defined in Agda.TypeChecking.MetaVars

Methods

reduceAndEtaContract :: Term -> TCM Term Source #

MentionsMeta Elim Source #

Instance details

Methods

mentionsMetas :: HashSet MetaId -> Elim -> Bool Source #

MentionsMeta Level Source #

Instance details

Methods

mentionsMetas :: HashSet MetaId -> Level -> Bool Source #

MentionsMeta PlusLevel Source #

Instance details

Methods

mentionsMetas :: HashSet MetaId -> PlusLevel -> Bool Source #

MentionsMeta Sort Source #

Instance details

Methods

mentionsMetas :: HashSet MetaId -> Sort -> Bool Source #

MentionsMeta Term Source #

Instance details

Methods

mentionsMetas :: HashSet MetaId -> Term -> Bool Source #

MentionsMeta Type Source #

Instance details

Methods

mentionsMetas :: HashSet MetaId -> Type -> Bool Source #

AnyRigid Level Source #

Instance details

Methods

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

AnyRigid PlusLevel Source #

Instance details

Methods

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

AnyRigid Sort Source #

Instance details

Methods

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

AnyRigid Term Source #

Instance details

Methods

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

AnyRigid Type Source #

Instance details

Methods

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

Occurs Elims Source #

Instance details

Methods

occurs :: Elims -> OccursM Elims Source #

metaOccurs :: MetaId -> Elims -> TCM () Source #

Occurs Level Source #

Instance details

Methods

occurs :: Level -> OccursM Level Source #

metaOccurs :: MetaId -> Level -> TCM () Source #

Occurs PlusLevel Source #

Instance details

Methods

occurs :: PlusLevel -> OccursM PlusLevel Source #

metaOccurs :: MetaId -> PlusLevel -> TCM () Source #

Occurs Sort Source #

Instance details

Methods

occurs :: Sort -> OccursM Sort Source #

metaOccurs :: MetaId -> Sort -> TCM () Source #

Occurs Term Source #

Instance details

Methods

occurs :: Term -> OccursM Term Source #

metaOccurs :: MetaId -> Term -> TCM () Source #

Occurs Type Source #

Instance details

Methods

occurs :: Type -> OccursM Type Source #

metaOccurs :: MetaId -> Type -> TCM () Source #

Instance details

Methods

addContext :: MonadAddContext m => Telescope -> m a -> m a Source #

IsInstantiatedMeta Level Source #

Instance details

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Level -> m Bool Source #

IsInstantiatedMeta PlusLevel Source #

Instance details

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => PlusLevel -> m Bool Source #

IsInstantiatedMeta Term Source #

Instance details

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Term -> m Bool Source #

UnFreezeMeta Level Source #

Instance details

Methods

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

UnFreezeMeta PlusLevel Source #

Instance details

Methods

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

UnFreezeMeta Sort Source #

Instance details

Methods

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

UnFreezeMeta Term Source #

Instance details

Methods

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

UnFreezeMeta Type Source #

Instance details

Methods

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

IsSizeType Term Source #

Instance details

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => Term -> m (Maybe BoundedSize) Source #

ComputeOccurrences Level Source #

Instance details

Methods

occurrences :: Level -> OccM OccurrencesBuilder Source #

ComputeOccurrences PlusLevel Source #

Instance details

Methods

occurrences :: PlusLevel -> OccM OccurrencesBuilder Source #

ComputeOccurrences Term Source #

Instance details

Methods

occurrences :: Term -> OccM OccurrencesBuilder Source #

ComputeOccurrences Type Source #

Instance details

Methods

occurrences :: Type -> OccM OccurrencesBuilder Source #

PrettyTCM Elim Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Level Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Sort Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Term Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Type Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ContextEntry Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrimTerm Type Source #

Instance details

Methods

primTerm :: Type -> TCM Term Source #

PrimType Type Source #

Instance details

Methods

primType :: Type -> TCM Type Source #

ToTerm Term Source #

Instance details

Methods

toTerm :: TCM (Term -> Term) Source #

toTermR :: TCM (Term -> ReduceM Term) Source #

ToTerm Type Source #

Instance details

InstantiateFull CompiledClauses Source #

Methods

toTerm :: TCM (Type -> Term) Source #

toTermR :: TCM (Type -> ReduceM Term) Source #

Instantiate Level Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Level -> ReduceM Level Source #

Instantiate Sort Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Sort -> ReduceM Sort Source #

Instantiate Term Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Term -> ReduceM Term Source #

InstantiateFull Level Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Level -> ReduceM Level Source #

InstantiateFull PlusLevel Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: PlusLevel -> ReduceM PlusLevel Source #

InstantiateFull Sort Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Sort -> ReduceM Sort Source #

InstantiateFull Substitution Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Substitution -> ReduceM Substitution Source #

InstantiateFull Term Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Term -> ReduceM Term Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses Source #

IsMeta Term Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Term -> Maybe MetaId Source #

Normalise Level Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Level -> ReduceM Level Source #

Normalise PlusLevel Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: PlusLevel -> ReduceM PlusLevel Source #

Normalise Sort Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Sort -> ReduceM Sort Source #

Normalise Term Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Term -> ReduceM Term Source #

Reduce Elim Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Elim -> ReduceM Elim Source #

reduceB' :: Elim -> ReduceM (Blocked Elim) Source #

Reduce Level Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Level -> ReduceM Level Source #

reduceB' :: Level -> ReduceM (Blocked Level) Source #

Reduce PlusLevel Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: PlusLevel -> ReduceM PlusLevel Source #

reduceB' :: PlusLevel -> ReduceM (Blocked PlusLevel) Source #

Reduce Sort Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Sort -> ReduceM Sort Source #

reduceB' :: Sort -> ReduceM (Blocked Sort) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Reduce Term Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Term -> ReduceM Term Source #

reduceB' :: Term -> ReduceM (Blocked Term) Source #

Reduce Type Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Type -> ReduceM Type Source #

reduceB' :: Type -> ReduceM (Blocked Type) Source #

Simplify Level Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Level -> ReduceM Level

Simplify PlusLevel Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: PlusLevel -> ReduceM PlusLevel

Simplify Sort Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Sort -> ReduceM Sort

Simplify Term Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Term -> ReduceM Term

GetMatchables Term Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Term -> [QName] Source #

EmbPrj Blocked_ Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Blocked_ -> S Int32 Source #

icod_ :: Blocked_ -> S Int32 Source #

value :: Int32 -> R Blocked_ Source #

EmbPrj Level Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Level -> S Int32 Source #

icod_ :: Level -> S Int32 Source #

value :: Int32 -> R Level Source #

EmbPrj NotBlocked Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NotBlocked -> S Int32 Source #

icod_ :: NotBlocked -> S Int32 Source #

value :: Int32 -> R NotBlocked Source #

EmbPrj PlusLevel Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PlusLevel -> S Int32 Source #

icod_ :: PlusLevel -> S Int32 Source #

value :: Int32 -> R PlusLevel Source #

EmbPrj Sort Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Sort -> S Int32 Source #

icod_ :: Sort -> S Int32 Source #

value :: Int32 -> R Sort Source #

EmbPrj Term Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Term -> S Int32 Source #

icod_ :: Term -> S Int32 Source #

value :: Int32 -> R Term Source #

EmbPrj CompiledClauses Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompiledClauses -> S Int32 Source #

icod_ :: CompiledClauses -> S Int32 Source #

value :: Int32 -> R CompiledClauses Source #

TeleNoAbs ListTel Source #

Instance details

Methods

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

Instance details

Methods

Abstract Sort Source #

Instance details

Methods

abstract :: Telescope -> Sort -> Sort Source #

Instance details

Methods

abstract :: Telescope -> Telescope -> Telescope Source #

Abstract Term Source #

Instance details

Methods

abstract :: Telescope -> Term -> Term Source #

Abstract Type Source #

Instance details

Methods

abstract :: Telescope -> Type -> Type Source #

Abstract CompiledClauses Source #

Instance details

Methods

abstract :: Telescope -> CompiledClauses -> CompiledClauses Source #

Apply Sort Source #

Instance details

Methods

apply :: Sort -> Args -> Sort Source #

applyE :: Sort -> Elims -> Sort Source #

Apply Term Source #

Instance details

Methods

apply :: Term -> Args -> Term Source #

applyE :: Term -> Elims -> Term Source #

Apply CompiledClauses Source #

Instance details

Methods

apply :: CompiledClauses -> Args -> CompiledClauses Source #

applyE :: CompiledClauses -> Elims -> CompiledClauses Source #

Subst Term Source #

Instance details

Associated Types

type SubstArg Term
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Term = Term

Methods

applySubst :: Substitution' (SubstArg Term) -> Term -> Term Source #

DeBruijn Level Source #

Instance details

Methods

deBruijnVar :: Int -> Level Source #

debruijnNamedVar :: String -> Int -> Level Source #

deBruijnView :: Level -> Maybe Int Source #

DeBruijn PlusLevel Source #

Instance details

Methods

deBruijnVar :: Int -> PlusLevel Source #

debruijnNamedVar :: String -> Int -> PlusLevel Source #

deBruijnView :: PlusLevel -> Maybe Int Source #

DeBruijn Term Source #

We can substitute Terms for variables.

Instance details

Methods

deBruijnVar :: Int -> Term Source #

debruijnNamedVar :: String -> Int -> Term Source #

deBruijnView :: Term -> Maybe Int Source #

SynEq Level Source #

Instance details

Methods

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

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

SynEq PlusLevel Source #

Instance details

Methods

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

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

SynEq Sort Source #

Instance details

Methods

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

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

SynEq Term Source #

Syntactic term equality ignores DontCare stuff.

Instance details

Methods

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

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

SynEq Type Source #

Syntactic equality ignores sorts.

Instance details

Methods

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

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

PiApplyM Term Source #

Instance details

Defined in Agda.TypeChecking.Telescope

Methods

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

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

Show Term Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Term -> ShowS #

show :: Term -> String #

showList :: [Term] -> ShowS #

NFData Level Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Level -> () #

NFData PlusLevel Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: PlusLevel -> () #

NFData Sort Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Sort -> () #

NFData Term Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Term -> () #

NFData Type Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Type -> () #

Eq Level Source #

Instance details

Methods

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

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

Eq NotBlocked Source #

Instance details

Methods

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

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

Eq PlusLevel Source #

Instance details

Methods

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

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

Eq Sort Source #

Instance details

Methods

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

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

Eq Substitution Source #

Instance details

Methods

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

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

Eq Term Source #

Syntactic Term equality, ignores stuff below DontCare and sharing.

Instance details

Methods

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

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

Eq SingleLevel Source #

Instance details

Defined in Agda.TypeChecking.Level

Methods

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

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

Ord Level Source #

Instance details

Methods

compare :: Level -> Level -> Ordering #

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

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

(>) :: Level -> Level -> Bool #

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

max :: Level -> Level -> Level #

min :: Level -> Level -> Level #

Ord PlusLevel Source #

Instance details

Methods

compare :: PlusLevel -> PlusLevel -> Ordering #

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

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

(>) :: PlusLevel -> PlusLevel -> Bool #

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

max :: PlusLevel -> PlusLevel -> PlusLevel #

min :: PlusLevel -> PlusLevel -> PlusLevel #

Ord Sort Source #

Instance details

Methods

compare :: Sort -> Sort -> Ordering #

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

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

(>) :: Sort -> Sort -> Bool #

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

max :: Sort -> Sort -> Sort #

min :: Sort -> Sort -> Sort #

Ord Substitution Source #

Instance details

Methods

compare :: Substitution -> Substitution -> Ordering #

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

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

(>) :: Substitution -> Substitution -> Bool #

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

max :: Substitution -> Substitution -> Substitution #

min :: Substitution -> Substitution -> Substitution #

Ord Term Source #

Instance details

Methods

compare :: Term -> Term -> Ordering #

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

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

(>) :: Term -> Term -> Bool #

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

max :: Term -> Term -> Term #

min :: Term -> Term -> Term #

Match NLPSort Sort Source #

Instance details

Methods

match :: Relevance -> Telescope -> Telescope -> TypeOf Sort -> NLPSort -> Sort -> NLM () Source #

Match NLPType Type Source #

Instance details

Methods

match :: Relevance -> Telescope -> Telescope -> TypeOf Type -> NLPType -> Type -> NLM () Source #

Match NLPat Level Source #

Instance details

Methods

match :: Relevance -> Telescope -> Telescope -> TypeOf Level -> NLPat -> Level -> NLM () Source #

Match NLPat Term Source #

Instance details

Methods

match :: Relevance -> Telescope -> Telescope -> TypeOf Term -> NLPat -> Term -> NLM () Source #

NLPatToTerm Nat Term Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatToTerm :: PureTCM m => Nat -> m Term Source #

NLPatToTerm NLPSort Sort Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatToTerm :: PureTCM m => NLPSort -> m Sort Source #

NLPatToTerm NLPType Type Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatToTerm :: PureTCM m => NLPType -> m Type Source #

NLPatToTerm NLPat Level Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatToTerm :: PureTCM m => NLPat -> m Level Source #

NLPatToTerm NLPat Term Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatToTerm :: PureTCM m => NLPat -> m Term Source #

PatternFrom Level NLPat Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> TypeOf Level -> Level -> TCM NLPat Source #

PatternFrom Sort NLPSort Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> TypeOf Sort -> Sort -> TCM NLPSort Source #

PatternFrom Term NLPat Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> TypeOf Term -> Term -> TCM NLPat Source #

PatternFrom Type NLPType Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> TypeOf Type -> Type -> TCM NLPType Source #

MonadError Blocked_ NLM Source #

Instance details

Methods

throwError :: Blocked_ -> NLM a #

catchError :: NLM a -> (Blocked_ -> NLM a) -> NLM a #

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 #

DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) Source #

Instance details

Defined in Agda.TypeChecking.Patterns.Internal

Methods

termToPattern :: Term -> TCM (Pattern' a) Source #

PatternFrom Elims [Elim' NLPat] Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> TypeOf Elims -> Elims -> TCM [Elim' NLPat] 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 #

Pretty a => Pretty (Blocked a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Blocked a -> Doc Source #

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

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

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

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

LensSort a => LensSort (Dom a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' (Dom a) Sort Source #

getSort :: Dom a -> Sort Source #

LensSort (Type' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' (Type' a) Sort Source #

getSort :: Type' a -> Sort Source #

SgTel (Dom Type) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom Type -> Telescope Source #

SgTel (Dom (ArgName, Type)) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

GetDefs a => GetDefs (Dom a) Source #

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike a => TermLike (Blocked a) Source #

Instance details

Methods

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

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

TermLike a => TermLike (Dom a) Source #

Instance details

Methods

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

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

NamesIn a => NamesIn (Type' a) Source #

Instance details

Methods

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

KillRange a => KillRange (Blocked a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Blocked a) Source #

KillRange a => KillRange (Type' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Type' a) Source #

Reify i => Reify (Dom i) Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Dom i)
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Dom i) = Arg (ReifiesTo i)

Methods

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

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

AbsTerm a => AbsTerm (Dom a) Source #

Instance details

Methods

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

EqualSy a => EqualSy (Dom a) Source #

Ignore the tactic.

Instance details

Methods

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

Free t => Free (Dom t) Source #

Instance details

Methods

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

Free t => Free (Type' t) Source #

Instance details

Methods

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

PrecomputeFreeVars a => PrecomputeFreeVars (Dom a) Source #

Instance details

Methods

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

(Reduce a, ForceNotFree a, TermSubst a) => ForceNotFree (Dom a) Source #

Instance details

Methods

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

UsableModality a => UsableModality (Dom a) Source #

Instance details

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Dom a -> m Bool Source #

UsableRelevance a => UsableModality (Type' a) Source #

Instance details

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Type' a -> m Bool Source #

UsableRelevance a => UsableRelevance (Dom a) Source #

Instance details

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Dom a -> m Bool Source #

UsableRelevance a => UsableRelevance (Type' a) Source #

Instance details

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Type' a -> m Bool Source #

MentionsMeta t => MentionsMeta (Dom t) Source #

Instance details

Methods

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

AnyRigid a => AnyRigid (Dom a) Source #

Instance details

Methods

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

Occurs (Abs Term) Source #

Instance details

Methods

occurs :: Abs Term -> OccursM (Abs Term) Source #

metaOccurs :: MetaId -> Abs Term -> TCM () Source #

Occurs (Abs Type) Source #

Instance details

Methods

occurs :: Abs Type -> OccursM (Abs Type) Source #

metaOccurs :: MetaId -> Abs Type -> TCM () Source #

Occurs a => Occurs (Dom a) Source #

Instance details

Methods

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

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

AddContext (Dom Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => Dom Type -> m a -> m a Source #

contextSize :: Dom Type -> Nat Source #

AddContext (Dom (Name, Type)) Source #

Instance details

Methods

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

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

AddContext (Dom (String, Type)) Source #

Instance details

Methods

addContext :: MonadAddContext m => Dom (String, Type) -> m a -> m a Source #

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

AddContext (KeepNames Telescope) Source #

Instance details

Methods

addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source #

IsSizeType a => IsSizeType (Dom a) Source #

Instance details

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => Dom a -> m (Maybe BoundedSize) Source #

IsSizeType a => IsSizeType (Type' a) Source #

Instance details

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => Type' a -> m (Maybe BoundedSize) Source #

ComputeOccurrences a => ComputeOccurrences (Dom a) Source #

Instance details

Methods

occurrences :: Dom a -> OccM OccurrencesBuilder 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 (NamedArg Term) Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Named_ Term) Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM a => PrettyTCM (Blocked a) Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Dom Type) Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Type' NLPat) Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Type' NLPat -> m Doc Source #

ToTerm (Dom Type) Source #

Instance details

Methods

toTerm :: TCM (Dom Type -> Term) Source #

toTermR :: TCM (Dom Type -> ReduceM Term) Source #

Instantiate a => Instantiate (Blocked a) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Blocked a -> ReduceM (Blocked a) Source #

Instantiate t => Instantiate (Type' t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull (Type' t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Dom t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Type' t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Reduce t => Reduce (Dom t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Simplify t => Simplify (Dom t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Type' t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

GetMatchables a => GetMatchables (Dom a) Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

EmbPrj a => EmbPrj (Dom a) Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Int32 Source #

icod_ :: Dom a -> S Int32 Source #

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

EmbPrj a => EmbPrj (Type' a) Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Type' a -> S Int32 Source #

icod_ :: Type' a -> S Int32 Source #

value :: Int32 -> R (Type' a) Source #

Apply t => Apply (Blocked t) Source #

Instance details

Methods

apply :: Blocked t -> Args -> Blocked t Source #

applyE :: Blocked t -> Elims -> Blocked t Source #

Subst a => Subst (Blocked a) Source #

Instance details

Associated Types

type SubstArg (Blocked a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Blocked a) = SubstArg a

Methods

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

SynEq a => SynEq (Dom a) Source #

Instance details

Methods

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

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

Unquote a => Unquote (Dom a) Source #

Instance details

Defined in Agda.TypeChecking.Unquote

Methods

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

NFData e => NFData (Dom e) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Dom e -> () #

Eq t => Eq (Blocked t) Source #

Instance details

Methods

(==) :: Blocked t -> Blocked t -> Bool #

(/=) :: Blocked t -> Blocked t -> Bool #

Eq a => Eq (Type' a) Source #

Syntactic Type equality, ignores sort annotations.

Instance details

Methods

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

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

Ord a => Ord (Dom a) Source #

Instance details

Methods

compare :: Dom a -> Dom a -> Ordering #

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

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

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

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

max :: Dom a -> Dom a -> Dom a #

min :: Dom a -> Dom a -> Dom a #

Ord a => Ord (Type' a) Source #

Instance details

Methods

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

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

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

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

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

max :: Type' a -> Type' a -> Type' a #

min :: Type' a -> Type' a -> Type' a #

Match [Elim' NLPat] Elims Source #

Instance details

Methods

match :: Relevance -> Telescope -> Telescope -> TypeOf Elims -> [Elim' NLPat] -> Elims -> NLM () Source #

ToNLPat a b => ToNLPat (Dom a) (Dom b) Source #

Instance details

Methods

toNLPat :: Dom a -> Dom b Source #

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

Instance details

Methods

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

NLPatToTerm p a => NLPatToTerm (Dom p) (Dom a) Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

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

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

SgTel (ArgName, Dom Type) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

(ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name) Source #

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Dom r, Name)
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Dom r, Name) = TypedBinding

Methods

toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m (AbsOfRef (Dom r, Name)) Source #

AddContext (Name, Dom Type) Source #

Instance details

Methods

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

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

AddContext (KeepNames String, Dom Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => (KeepNames String, Dom Type) -> m a -> m a Source #

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

AddContext (List1 Name, Dom Type) Source #

Instance details

Methods

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

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

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

Instance details

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

Methods

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

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

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

Instance details

Methods

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

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

AddContext (Text, Dom Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => (Text, Dom Type) -> m a -> m a Source #

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

AddContext (String, Dom Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => (String, Dom Type) -> m a -> m a Source #

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

AddContext ([Name], Dom Type) Source #

Instance details

Methods

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

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

AddContext ([Arg Name], Type) Source #

Instance details

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

Methods

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

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

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

Instance details

Methods

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

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

type TypeOf Elims Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf Elims = (Type, Elims -> Term)

type TypeOf Level Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf Level = ()

type TypeOf PlusLevel Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf PlusLevel = ()

type TypeOf Sort Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf Sort = ()

type TypeOf Term Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf Term = Type

type TypeOf Type Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf Type = ()

type ReifiesTo Level Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Level = Expr

type ReifiesTo Sort Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Sort = Expr

type ReifiesTo Telescope Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Term Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Term = Expr

type ReifiesTo Type Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Type = Type

type SubstArg Term Source #

Instance details

type SubstArg Term = Term

type TypeOf (Abs Term) Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Abs Term) = (Dom Type, Abs Type)

type TypeOf (Abs Type) Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Abs Type) = Dom Type

type TypeOf (Dom a) Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Dom a) = TypeOf a

type TypeOf [PlusLevel] Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf [PlusLevel] = ()

type ReifiesTo (Dom i) Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Dom i) = Arg (ReifiesTo i)

type SubstArg (Blocked a) Source #

Instance details

type SubstArg (Blocked a) = SubstArg a

type AbsOfRef (Dom r, Name) Source #

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Dom r, Name) = TypedBinding

litP :: Literal -> Pattern' a Source #

varP :: a -> Pattern' a Source #

data Substitution' a Source #

Substitutions.

Constructors

IdS	Identity substitution. `Γ ⊢ IdS : Γ`
EmptyS Impossible	Empty substitution, lifts from the empty context. First argument is `IMPOSSIBLE`. Apply this to closed terms you want to use in a non-empty context. `Γ ⊢ EmptyS : ()`
a :# (Substitution' a) infixr 4	Substitution extension, ``cons'`. `Γ ⊢ u : Aρ Γ ⊢ ρ : Δ ---------------------- Γ ⊢ u :# ρ : Δ, A`
Strengthen Impossible !Int (Substitution' a)	Strengthening substitution. First argument is `IMPOSSIBLE`. In `'Strengthen err n ρ` the number `n` must be non-negative. This substitution should only be applied to values `t` for which none of the variables `0` up to `n - 1` are free in `t[ρ]`, and in that case `n` is subtracted from all free de Bruijn indices in `t[ρ]`. Γ ⊢ ρ : Δ \|Θ\| = n --------------------------- Γ ⊢ Strengthen n ρ : Δ, Θ @
Wk !Int (Substitution' a)	Weakening substitution, lifts to an extended context. `Γ ⊢ ρ : Δ ------------------- Γ, Ψ ⊢ Wk \|Ψ\| ρ : Δ`
Lift !Int (Substitution' a)	Lifting substitution. Use this to go under a binder. `Lift 1 ρ == var 0 :# Wk 1 ρ`. `Γ ⊢ ρ : Δ ------------------------- Γ, Ψρ ⊢ Lift \|Ψ\| ρ : Δ, Ψ`

Instances

Instances details

KillRange Substitution Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Substitution Source #

InstantiateFull Substitution Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Substitution -> ReduceM Substitution Source #

Foldable Substitution' Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: Substitution' a -> Bool #

length :: Substitution' a -> Int #

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

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

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

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

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

Traversable Substitution' Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor Substitution' Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Eq Substitution Source #

Instance details

Methods

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

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

Ord Substitution Source #

Instance details

Methods

compare :: Substitution -> Substitution -> Ordering #

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

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

(>) :: Substitution -> Substitution -> Bool #

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

max :: Substitution -> Substitution -> Substitution #

min :: Substitution -> Substitution -> Substitution #

Pretty a => Pretty (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Substitution' a -> Doc Source #

prettyPrec :: Int -> Substitution' a -> Doc Source #

prettyList :: [Substitution' a] -> Doc Source #

TermSize a => TermSize (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

termSize :: Substitution' a -> Int Source #

tsize :: Substitution' a -> Sum Int Source #

NamesIn a => NamesIn (Substitution' a) Source #

Instance details

Methods

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

(Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a) Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Substitution' a -> m Doc Source #

EmbPrj a => EmbPrj (Substitution' a) Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Substitution' a -> S Int32 Source #

icod_ :: Substitution' a -> S Int32 Source #

value :: Int32 -> R (Substitution' a) Source #

EndoSubst a => Subst (Substitution' a) Source #

Instance details

Associated Types

type SubstArg (Substitution' a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Substitution' a) = a

Methods

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

Null (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

empty :: Substitution' a Source #

null :: Substitution' a -> Bool Source #

Generic (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Substitution' a)

Instance details

Defined in Agda.Syntax.Internal

type Rep (Substitution' a) = D1 ('MetaData "Substitution'" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) ((C1 ('MetaCons "IdS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible)) :+: C1 ('MetaCons ":#" ('InfixI 'RightAssociative 4) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))) :+: (C1 ('MetaCons "Strengthen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a)))) :+: (C1 ('MetaCons "Wk" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))) :+: C1 ('MetaCons "Lift" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))))

Methods

from :: Substitution' a -> Rep (Substitution' a) x #

to :: Rep (Substitution' a) x -> Substitution' a #

Show a => Show (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

show :: Substitution' a -> String #

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

NFData a => NFData (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Substitution' a -> () #

type SubstArg (Substitution' a) Source #

Instance details

type SubstArg (Substitution' a) = a

type Rep (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal

type Rep (Substitution' a) = D1 ('MetaData "Substitution'" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) ((C1 ('MetaCons "IdS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible)) :+: C1 ('MetaCons ":#" ('InfixI 'RightAssociative 4) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))) :+: (C1 ('MetaCons "Strengthen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a)))) :+: (C1 ('MetaCons "Wk" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))) :+: C1 ('MetaCons "Lift" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))))

data Clause Source #

A clause is a list of patterns and the clause body.

The telescope contains the types of the pattern variables and the de Bruijn indices say how to get from the order the variables occur in the patterns to the order they occur in the telescope. The body binds the variables in the order they appear in the telescope.

clauseTel ~ permute clausePerm (patternVars namedClausePats)

Terms in dot patterns are valid in the clause telescope.

For the purpose of the permutation and the body dot patterns count as variables. TODO: Change this!

Constructors

Clause

Fields

clauseLHSRange :: Range
clauseFullRange :: Range
clauseTel :: Telescope
Δ: The types of the pattern variables in dependency order.
namedClausePats :: NAPs
Δ ⊢ ps. The de Bruijn indices refer to Δ.
clauseBody :: Maybe Term
Just v with Δ ⊢ v for a regular clause, or Nothing for an absurd one.
clauseType :: Maybe (Arg Type)
Δ ⊢ t. The type of the rhs under clauseTel. Used, e.g., by TermCheck. Can be Irrelevant if we encountered an irrelevant projection pattern on the lhs.
clauseCatchall :: Bool
Clause has been labelled as CATCHALL.
clauseExact :: Maybe Bool
Pattern matching of this clause is exact, no catch-all case. Computed by the coverage checker. Nothing means coverage checker has not run yet (clause may be inexact). Just False means clause is not exact. Just True means clause is exact.
clauseRecursive :: Maybe Bool
clauseBody contains recursive calls; computed by termination checker. Nothing means that termination checker has not run yet, or that clauseBody contains meta-variables; these could be filled with recursive calls later! Just False means definitely no recursive call. Just True means definitely a recursive call.
clauseUnreachable :: Maybe Bool
Clause has been labelled as unreachable by the coverage checker. Nothing means coverage checker has not run yet (clause may be unreachable). Just False means clause is not unreachable. Just True means clause is unreachable.
clauseEllipsis :: ExpandedEllipsis
Was this clause created by expansion of an ellipsis?
clauseWhereModule :: Maybe ModuleName
Keeps track of the module name associate with the clause's where clause.

Instances

Instances details

Pretty Clause Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Clause -> Doc Source #

prettyPrec :: Int -> Clause -> Doc Source #

prettyList :: [Clause] -> Doc Source #

GetDefs Clause Source #

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

NamesIn Clause Source #

Instance details

Methods

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

FunArity Clause Source #

Get the number of initial Apply patterns in a clause.

Instance details

Methods

funArity :: Clause -> Int Source #

HasRange Clause Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

getRange :: Clause -> Range Source #

KillRange Clause Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Clause Source #

DropArgs Clause Source #

NOTE: does not work for recursive functions.

Instance details

Methods

dropArgs :: Int -> Clause -> Clause Source #

DropArgs FunctionInverse Source #

Instance details

Methods

dropArgs :: Int -> FunctionInverse -> FunctionInverse Source #

Free Clause Source #

Instance details

Methods

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

Occurs Clause Source #

Instance details

Methods

occurs :: Clause -> OccursM Clause Source #

metaOccurs :: MetaId -> Clause -> TCM () Source #

ComputeOccurrences Clause Source #

Instance details

InstantiateFull FunctionInverse Source #

Methods

occurrences :: Clause -> OccM OccurrencesBuilder Source #

PrettyTCM Clause Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

NormaliseProjP Clause Source #

Instance details

Defined in Agda.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => Clause -> m Clause Source #

InstantiateFull Clause Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Clause -> ReduceM Clause Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse Source #

EmbPrj Clause Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Clause -> S Int32 Source #

icod_ :: Clause -> S Int32 Source #

value :: Int32 -> R Clause Source #

Abstract Clause Source #

Instance details

Methods

abstract :: Telescope -> Clause -> Clause Source #

Abstract FunctionInverse Source #

Instance details

Methods

abstract :: Telescope -> FunctionInverse -> FunctionInverse Source #

Apply Clause Source #

Instance details

Methods

apply :: Clause -> Args -> Clause Source #

applyE :: Clause -> Elims -> Clause Source #

Apply FunctionInverse Source #

Instance details

Methods

apply :: FunctionInverse -> Args -> FunctionInverse Source #

applyE :: FunctionInverse -> Elims -> FunctionInverse Source #

Null Clause Source #

A null clause is one with no patterns and no rhs. Should not exist in practice.

Instance details

Defined in Agda.Syntax.Internal

Methods

empty :: Clause Source #

null :: Clause -> Bool Source #

Generic Clause Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep Clause

Instance details

Defined in Agda.Syntax.Internal

Methods

from :: Clause -> Rep Clause x #

to :: Rep Clause x -> Clause #

Show Clause Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Clause -> ShowS #

show :: Clause -> String #

showList :: [Clause] -> ShowS #

NFData Clause Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Clause -> () #

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 [Clause] [([Pat O], MExp O)] Source #

Instance details

Defined in Agda.Auto.Convert

Methods

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

FunArity [Clause] Source #

Get the number of common initial Apply patterns in a list of clauses.

Instance details

UsableSizeVars DeBruijnPattern Source #

Methods

funArity :: [Clause] -> Int Source #

Reify (QNamed Clause) Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (QNamed Clause)
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (QNamed Clause) = Clause

Methods

reify :: MonadReify m => QNamed Clause -> m (ReifiesTo (QNamed Clause)) Source #

reifyWhen :: MonadReify m => Bool -> QNamed Clause -> m (ReifiesTo (QNamed Clause)) Source #

PrettyTCM (QNamed Clause) Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => QNamed Clause -> m Doc Source #

type Rep Clause Source #

Instance details

Defined in Agda.Syntax.Internal

type ReifiesTo (QNamed Clause) Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (QNamed Clause) = Clause

data Pattern' x Source #

Patterns are variables, constructors, or wildcards. QName is used in ConP rather than Name since a constructor might come from a particular namespace. This also meshes well with the fact that values (i.e. the arguments we are matching with) use QName.

Constructors

VarP PatternInfo x	x
DotP PatternInfo Term	.t
ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]	`c ps` The subpatterns do not contain any projection copatterns.
LitP PatternInfo Literal	E.g. `5`, `"hello"`.
ProjP ProjOrigin QName	Projection copattern. Can only appear by itself.
IApplyP PatternInfo Term Term x	Path elimination pattern, like `VarP` but keeps track of endpoints.
DefP PatternInfo QName [NamedArg (Pattern' x)]	Used for HITs, the QName should be the one from primHComp.

Instances

Instances details

Instance details

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: DeBruijnPattern -> TerM VarSet Source #

UsableSizeVars MaskedDeBruijnPatterns Source #

Instance details

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet Source #

Reduce DeBruijnPattern Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: DeBruijnPattern -> ReduceM DeBruijnPattern Source #

reduceB' :: DeBruijnPattern -> ReduceM (Blocked DeBruijnPattern) Source #

Subst DeBruijnPattern Source #

Instance details

Associated Types

type SubstArg DeBruijnPattern
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg DeBruijnPattern = DeBruijnPattern

Methods

applySubst :: Substitution' (SubstArg DeBruijnPattern) -> DeBruijnPattern -> DeBruijnPattern Source #

Subst Pattern Source #

Instance details

Associated Types

type SubstArg Pattern
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Pattern = Term

Methods

applySubst :: Substitution' (SubstArg Pattern) -> Pattern -> Pattern Source #

Subst SplitPattern Source #

Instance details

Defined in Agda.TypeChecking.Coverage.Match

Associated Types

type SubstArg SplitPattern
Instance details Defined in Agda.TypeChecking.Coverage.Match type SubstArg SplitPattern = SplitPattern

Methods

applySubst :: Substitution' (SubstArg SplitPattern) -> SplitPattern -> SplitPattern Source #

Foldable Pattern' Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: Pattern' a -> Bool #

length :: Pattern' a -> Int #

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

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

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

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

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

Traversable Pattern' Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor Pattern' Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

LabelPatVars Pattern DeBruijnPattern Source #

Instance details

Associated Types

type PatVarLabel DeBruijnPattern
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel DeBruijnPattern = Int

Methods

labelPatVars :: Pattern -> State [PatVarLabel DeBruijnPattern] DeBruijnPattern Source #

unlabelPatVars :: DeBruijnPattern -> Pattern 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

Methods

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

PatternLike a (Pattern' a) Source #

Instance details

Methods

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

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

DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) Source #

Instance details

Defined in Agda.TypeChecking.Patterns.Internal

Methods

termToPattern :: Term -> TCM (Pattern' a) Source #

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

Instance details

Defined in Agda.Auto.Convert

Methods

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

IsProjP (Pattern' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

Pretty a => Pretty (Pattern' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Pattern' a -> Doc Source #

prettyPrec :: Int -> Pattern' a -> Doc Source #

prettyList :: [Pattern' a] -> Doc Source #

PatternVars (Arg (Pattern' a)) Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (Arg (Pattern' a))
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (Arg (Pattern' a)) = a

Methods

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

PatternVars (NamedArg (Pattern' a)) Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (NamedArg (Pattern' a))
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (NamedArg (Pattern' a)) = a

Methods

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

NamesIn (Pattern' a) Source #

Instance details

Methods

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

CountPatternVars (Pattern' x) Source #

Instance details

Methods

countPatternVars :: Pattern' x -> Int Source #

PatternVarModalities (Pattern' x) Source #

Instance details

Associated Types

type PatVar (Pattern' x)
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVar (Pattern' x) = x

Methods

patternVarModalities :: Pattern' x -> [(PatVar (Pattern' x), Modality)] Source #

KillRange a => KillRange (Pattern' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Pattern' a) Source #

UsableSizeVars (Masked DeBruijnPattern) Source #

Instance details

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet Source #

UsableSizeVars [DeBruijnPattern] Source #

Instance details

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: [DeBruijnPattern] -> TerM VarSet Source #

PrettyTCM a => PrettyTCM (Pattern' a) Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Pattern' a -> m Doc Source #

NormaliseProjP (Pattern' x) Source #

Instance details

Defined in Agda.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => Pattern' x -> m (Pattern' x) Source #

InstantiateFull a => InstantiateFull (Pattern' a) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Pattern' a -> ReduceM (Pattern' a) Source #

Normalise a => Normalise (Pattern' a) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Pattern' a -> ReduceM (Pattern' a) Source #

IsFlexiblePattern (Pattern' a) Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern' a -> MaybeT m FlexibleVarKind Source #

isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern' a -> m Bool Source #

EmbPrj a => EmbPrj (Pattern' a) Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Pattern' a -> S Int32 Source #

icod_ :: Pattern' a -> S Int32 Source #

value :: Int32 -> R (Pattern' a) Source #

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Methods

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

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

DeBruijn a => DeBruijn (Pattern' a) Source #

Instance details

Methods

deBruijnVar :: Int -> Pattern' a Source #

debruijnNamedVar :: String -> Int -> Pattern' a Source #

deBruijnView :: Pattern' a -> Maybe Int Source #

DeBruijn a => IApplyVars (Pattern' a) Source #

Instance details

Defined in Agda.TypeChecking.Telescope.Path

Methods

iApplyVars :: Pattern' a -> [Int] Source #

Generic (Pattern' x) Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Pattern' x)

Instance details

Defined in Agda.Syntax.Internal

Methods

from :: Pattern' x -> Rep (Pattern' x) x0 #

to :: Rep (Pattern' x) x0 -> Pattern' x #

Show x => Show (Pattern' x) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Pattern' x -> ShowS #

show :: Pattern' x -> String #

showList :: [Pattern' x] -> ShowS #

NFData x => NFData (Pattern' x) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Pattern' x -> () #

Eq a => Eq (Pattern' a) Source #

Instance details

Methods

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

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

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

Instance details

Methods

toNLPat :: Arg DeBruijnPattern -> Elim' NLPat Source #

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

Instance details

Methods

toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat Source #

type PatVarLabel DeBruijnPattern Source #

Instance details

type PatVarLabel DeBruijnPattern = Int

type SubstArg DeBruijnPattern Source #

Instance details

type SubstArg DeBruijnPattern = DeBruijnPattern

type SubstArg Pattern Source #

Instance details

type SubstArg Pattern = Term

type SubstArg SplitPattern Source #

Instance details

Defined in Agda.TypeChecking.Coverage.Match

type SubstArg SplitPattern = SplitPattern

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 PatternVarOut (NamedArg (Pattern' a)) = a

type PatVar (Pattern' x) Source #

Instance details

type PatVar (Pattern' x) = x

type Rep (Pattern' x) Source #

Instance details

Defined in Agda.Syntax.Internal

type Telescope = Tele (Dom Type) Source #

data Dom' t e Source #

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

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

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

Constructors

Dom
Fields domInfo :: ArgInfo domName :: Maybe NamedName e.g. `x` in `{x = y : A} -> B`. domIsFinite :: Bool Is this a Π-type (False), or a partial type (True)? domTactic :: Maybe t "@tactic e". unDom :: e

Instances

Instances details

TelToArgs ListTel Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

telToArgs :: ListTel -> [Arg ArgName] Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Telescope = Telescope

Methods

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

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

TerSetSizeDepth ListTel Source #

Instance details

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: ListTel -> TerM a -> TerM a Source #

Instance details

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: Telescope -> TerM a -> TerM a Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Methods

Instance details

Methods

addContext :: MonadAddContext m => Telescope -> m a -> m a Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ContextEntry Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

TeleNoAbs ListTel Source #

Instance details

Methods

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

Instance details

Methods

Instance details

Methods

abstract :: Telescope -> Telescope -> Telescope Source #

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

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

LensSort a => LensSort (Dom a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' (Dom a) Sort Source #

getSort :: Dom a -> Sort Source #

SgTel (Dom Type) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom Type -> Telescope Source #

SgTel (Dom (ArgName, Type)) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

GetDefs a => GetDefs (Dom a) Source #

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike a => TermLike (Dom a) Source #

Instance details

Methods

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

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

Reify i => Reify (Dom i) Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Dom i)
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Dom i) = Arg (ReifiesTo i)

Methods

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

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

AbsTerm a => AbsTerm (Dom a) Source #

Instance details

Methods

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

EqualSy a => EqualSy (Dom a) Source #

Ignore the tactic.

Instance details

Methods

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

Free t => Free (Dom t) Source #

Instance details

Methods

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

PrecomputeFreeVars a => PrecomputeFreeVars (Dom a) Source #

Instance details

Methods

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

(Reduce a, ForceNotFree a, TermSubst a) => ForceNotFree (Dom a) Source #

Instance details

Methods

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

UsableModality a => UsableModality (Dom a) Source #

Instance details

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Dom a -> m Bool Source #

UsableRelevance a => UsableRelevance (Dom a) Source #

Instance details

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Dom a -> m Bool Source #

MentionsMeta t => MentionsMeta (Dom t) Source #

Instance details

Methods

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

AnyRigid a => AnyRigid (Dom a) Source #

Instance details

Methods

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

Occurs a => Occurs (Dom a) Source #

Instance details

Methods

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

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

AddContext (Dom Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => Dom Type -> m a -> m a Source #

contextSize :: Dom Type -> Nat Source #

AddContext (Dom (Name, Type)) Source #

Instance details

Methods

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

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

AddContext (Dom (String, Type)) Source #

Instance details

Methods

addContext :: MonadAddContext m => Dom (String, Type) -> m a -> m a Source #

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

AddContext (KeepNames Telescope) Source #

Instance details

Methods

addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source #

IsSizeType a => IsSizeType (Dom a) Source #

Instance details

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => Dom a -> m (Maybe BoundedSize) Source #

ComputeOccurrences a => ComputeOccurrences (Dom a) Source #

Instance details

Methods

occurrences :: Dom a -> OccM OccurrencesBuilder Source #

PrettyTCM (Dom Type) Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

ToTerm (Dom Type) Source #

Instance details

Methods

toTerm :: TCM (Dom Type -> Term) Source #

toTermR :: TCM (Dom Type -> ReduceM Term) Source #

Normalise t => Normalise (Dom t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Reduce t => Reduce (Dom t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Simplify t => Simplify (Dom t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

GetMatchables a => GetMatchables (Dom a) Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

EmbPrj a => EmbPrj (Dom a) Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Int32 Source #

icod_ :: Dom a -> S Int32 Source #

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

SynEq a => SynEq (Dom a) Source #

Instance details

Methods

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

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

Unquote a => Unquote (Dom a) Source #

Instance details

Defined in Agda.TypeChecking.Unquote

Methods

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

Decoration (Dom' t) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable (Dom' t) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Dom' t m -> m #

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

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

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

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

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

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

foldr1 :: (a -> a -> a) -> Dom' t a -> a #

foldl1 :: (a -> a -> a) -> Dom' t a -> a #

toList :: Dom' t a -> [a] #

null :: Dom' t a -> Bool #

length :: Dom' t a -> Int #

elem :: Eq a => a -> Dom' t a -> Bool #

maximum :: Ord a => Dom' t a -> a #

minimum :: Ord a => Dom' t a -> a #

sum :: Num a => Dom' t a -> a #

product :: Num a => Dom' t a -> a #

Traversable (Dom' t) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor (Dom' t) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

fmap :: (a -> b) -> Dom' t a -> Dom' t b #

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

NFData e => NFData (Dom e) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Dom e -> () #

Ord a => Ord (Dom a) Source #

Instance details

Methods

compare :: Dom a -> Dom a -> Ordering #

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

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

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

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

max :: Dom a -> Dom a -> Dom a #

min :: Dom a -> Dom a -> Dom a #

ToNLPat a b => ToNLPat (Dom a) (Dom b) Source #

Instance details

Methods

toNLPat :: Dom a -> Dom b Source #

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

Instance details

Methods

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

NLPatToTerm p a => NLPatToTerm (Dom p) (Dom a) Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

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

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

LensAnnotation (Dom' t e) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

getAnnotation :: Dom' t e -> Annotation Source #

setAnnotation :: Annotation -> Dom' t e -> Dom' t e Source #

mapAnnotation :: (Annotation -> Annotation) -> Dom' t e -> Dom' t e Source #

LensArgInfo (Dom' t e) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

getArgInfo :: Dom' t e -> ArgInfo Source #

setArgInfo :: ArgInfo -> Dom' t e -> Dom' t e Source #

mapArgInfo :: (ArgInfo -> ArgInfo) -> Dom' t e -> Dom' t e Source #

LensCohesion (Dom' t e) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

getCohesion :: Dom' t e -> Cohesion Source #

setCohesion :: Cohesion -> Dom' t e -> Dom' t e Source #

mapCohesion :: (Cohesion -> Cohesion) -> Dom' t e -> Dom' t e Source #

LensFreeVariables (Dom' t e) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

getFreeVariables :: Dom' t e -> FreeVariables Source #

setFreeVariables :: FreeVariables -> Dom' t e -> Dom' t e Source #

mapFreeVariables :: (FreeVariables -> FreeVariables) -> Dom' t e -> Dom' t e 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 #

LensLock (Dom' t e) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

getLock :: Dom' t e -> Lock Source #

setLock :: Lock -> Dom' t e -> Dom' t e Source #

mapLock :: (Lock -> Lock) -> Dom' t e -> Dom' t e Source #

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 #

LensNamed (Dom' t e) Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type NameOf (Dom' t e)
Instance details Defined in Agda.Syntax.Internal type NameOf (Dom' t e) = NamedName

Methods

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

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 #

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 #

LensRelevance (Dom' t e) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

getRelevance :: Dom' t e -> Relevance Source #

setRelevance :: Relevance -> Dom' t e -> Dom' t e Source #

mapRelevance :: (Relevance -> Relevance) -> Dom' t e -> Dom' t e Source #

(Pretty t, Pretty e) => Pretty (Dom' t e) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Dom' t e -> Doc Source #

prettyPrec :: Int -> Dom' t e -> Doc Source #

prettyList :: [Dom' t e] -> Doc Source #

SgTel (ArgName, Dom Type) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

(AllMetas a, AllMetas b) => AllMetas (Dom' a b) Source #

Instance details

Methods

allMetas :: Monoid m => (MetaId -> m) -> Dom' a b -> m Source #

(NamesIn a, NamesIn b) => NamesIn (Dom' a b) Source #

Instance details

Methods

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

HasRange a => HasRange (Dom' t a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

getRange :: Dom' t a -> Range Source #

(KillRange t, KillRange a) => KillRange (Dom' t a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Dom' t a) Source #

(ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name) Source #

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Dom r, Name)
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Dom r, Name) = TypedBinding

Methods

toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m (AbsOfRef (Dom r, Name)) Source #

AddContext (Name, Dom Type) Source #

Instance details

Methods

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

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

AddContext (KeepNames String, Dom Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => (KeepNames String, Dom Type) -> m a -> m a Source #

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

AddContext (List1 Name, Dom Type) Source #

Instance details

Methods

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

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

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

Instance details

Methods

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

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

AddContext (Text, Dom Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => (Text, Dom Type) -> m a -> m a Source #

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

AddContext (String, Dom Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => (String, Dom Type) -> m a -> m a Source #

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

AddContext ([Name], Dom Type) Source #

Instance details

Methods

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

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

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

Instance details

Methods

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

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

(Instantiate t, Instantiate e) => Instantiate (Dom' t e) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

(InstantiateFull t, InstantiateFull e) => InstantiateFull (Dom' t e) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

(Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Dom' a b) Source #

Instance details

Associated Types

type SubstArg (Dom' a b)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Dom' a b) = SubstArg a

Methods

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

(Show t, Show e) => Show (Dom' t e) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Dom' t e -> ShowS #

show :: Dom' t e -> String #

showList :: [Dom' t e] -> ShowS #

Eq a => Eq (Dom' t a) Source #

Ignores Origin and FreeVariables and tactic.

Instance details

Defined in Agda.Syntax.Internal

Methods

(==) :: Dom' t a -> Dom' t a -> Bool #

(/=) :: Dom' t a -> Dom' t a -> Bool #

type ReifiesTo Telescope Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type TypeOf (Dom a) Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Dom a) = TypeOf a

type ReifiesTo (Dom i) Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Dom i) = Arg (ReifiesTo i)

type NameOf (Dom' t e) Source #

Instance details

Defined in Agda.Syntax.Internal

type NameOf (Dom' t e) = NamedName

type AbsOfRef (Dom r, Name) Source #

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Dom r, Name) = TypedBinding

type SubstArg (Dom' a b) Source #

Instance details

type SubstArg (Dom' a b) = SubstArg a

type Pattern Source #

Arguments

= Pattern' PatVarName

The PatVarName is a name suggestion.

type Level = Level' Term Source #

telToList :: Tele (Dom t) -> [Dom (ArgName, t)] Source #

Convert a telescope to its list form.

type Substitution = Substitution' Term Source #

type Dom = Dom' Term Source #

type Elim = Elim' Term Source #

data Sort' t Source #

Sorts.

Constructors

Univ Univ (Level' t)	`Prop ℓ`, `Set ℓ`, `SSet ℓ`.
Inf Univ !Integer	`Propωᵢ`, `(S)Setωᵢ`.
SizeUniv	`SizeUniv`, a sort inhabited by type `Size`.
LockUniv	`LockUniv`, a sort for locks.
LevelUniv	`LevelUniv`, a sort inhabited by type `Level`. When --level-universe isn't on, this universe reduces to `Set 0`
IntervalUniv	`IntervalUniv`, a sort inhabited by the cubical interval.
PiSort (Dom' t t) (Sort' t) (Abs (Sort' t))	Sort of the pi type.
FunSort (Sort' t) (Sort' t)	Sort of a (non-dependent) function type.
UnivSort (Sort' t)	Sort of another sort.
MetaS !MetaId [Elim' t]
DefS QName [Elim' t]	A postulated sort.
DummyS String	A (part of a) term or type which is only used for internal purposes. Replaces the abuse of `Prop` for a dummy sort. The `String` typically describes the location where we create this dummy, but can contain other information as well.

Instances

Instances details

Pretty Sort Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Sort -> Doc Source #

prettyPrec :: Int -> Sort -> Doc Source #

prettyList :: [Sort] -> Doc Source #

LensSort Sort Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort Sort Source #

getSort :: Sort -> Sort Source #

TermSize Sort Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

termSize :: Sort -> Int Source #

tsize :: Sort -> Sum Int Source #

GetDefs Sort Source #

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike Sort Source #

Instance details

Methods

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

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

AllMetas Sort Source #

Instance details

Methods

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

NamesIn Sort Source #

Instance details

Methods

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

KillRange Sort Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Sort Source #

Reify Sort Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Sort
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Sort = Expr

Methods

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

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

AbsTerm Sort Source #

Instance details

Methods

absTerm :: Term -> Sort -> Sort Source #

EqualSy Sort Source #

Instance details

Methods

equalSy :: Sort -> Sort -> Bool Source #

CheckInternal Sort Source #

Instance details

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Sort -> Comparison -> TypeOf Sort -> m Sort Source #

checkInternal :: MonadCheckInternal m => Sort -> Comparison -> TypeOf Sort -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Action m -> Sort -> m Sort Source #

inferInternal :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Sort -> m () Source #

Free Sort Source #

Instance details

Methods

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

PrecomputeFreeVars Sort Source #

Instance details

Methods

precomputeFreeVars :: Sort -> FV Sort Source #

ForceNotFree Sort Source #

Instance details

Methods

forceNotFree' :: MonadFreeRed m => Sort -> m Sort

UsableModality Sort Source #

Instance details

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Sort -> m Bool Source #

UsableRelevance Sort Source #

Instance details

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Sort -> m Bool Source #

MentionsMeta Sort Source #

Instance details

Methods

mentionsMetas :: HashSet MetaId -> Sort -> Bool Source #

AnyRigid Sort Source #

Instance details

Methods

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

Occurs Sort Source #

Instance details

Methods

occurs :: Sort -> OccursM Sort Source #

metaOccurs :: MetaId -> Sort -> TCM () Source #

UnFreezeMeta Sort Source #

Instance details

Methods

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

PrettyTCM Sort Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

Instantiate Sort Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Sort -> ReduceM Sort Source #

InstantiateFull Sort Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Sort -> ReduceM Sort Source #

Normalise Sort Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Sort -> ReduceM Sort Source #

Reduce Sort Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Sort -> ReduceM Sort Source #

reduceB' :: Sort -> ReduceM (Blocked Sort) Source #

Simplify Sort Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Sort -> ReduceM Sort

EmbPrj Sort Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Sort -> S Int32 Source #

icod_ :: Sort -> S Int32 Source #

value :: Int32 -> R Sort Source #

Abstract Sort Source #

Instance details

Methods

abstract :: Telescope -> Sort -> Sort Source #

Apply Sort Source #

Instance details

Methods

apply :: Sort -> Args -> Sort Source #

applyE :: Sort -> Elims -> Sort Source #

SynEq Sort Source #

Instance details

Methods

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

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

NFData Sort Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Sort -> () #

Eq Sort Source #

Instance details

Methods

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

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

Ord Sort Source #

Instance details

Methods

compare :: Sort -> Sort -> Ordering #

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

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

(>) :: Sort -> Sort -> Bool #

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

max :: Sort -> Sort -> Sort #

min :: Sort -> Sort -> Sort #

Match NLPSort Sort Source #

Instance details

Methods

match :: Relevance -> Telescope -> Telescope -> TypeOf Sort -> NLPSort -> Sort -> NLM () Source #

NLPatToTerm NLPSort Sort Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatToTerm :: PureTCM m => NLPSort -> m Sort Source #

PatternFrom Sort NLPSort Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> TypeOf Sort -> Sort -> TCM NLPSort Source #

IsMeta a => IsMeta (Sort' a) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Sort' a -> Maybe MetaId Source #

(Coercible a Term, Subst a) => Subst (Sort' a) Source #

Instance details

Associated Types

type SubstArg (Sort' a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Sort' a) = SubstArg a

Methods

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

Show t => Show (Sort' t) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Sort' t -> ShowS #

show :: Sort' t -> String #

showList :: [Sort' t] -> ShowS #

type TypeOf Sort Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf Sort = ()

type ReifiesTo Sort Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Sort = Expr

type SubstArg (Sort' a) Source #

Instance details

type SubstArg (Sort' a) = SubstArg a

class PatternVars a where Source #

Extract pattern variables in left-to-right order. A DotP is also treated as variable (see docu for Clause).

Associated Types

type PatternVarOut a Source #

Methods

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

Instances

Instances details

PatternVars (Arg (Pattern' a)) Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (Arg (Pattern' a))
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (Arg (Pattern' a)) = a

Methods

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

PatternVars (NamedArg (Pattern' a)) Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (NamedArg (Pattern' a))
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (NamedArg (Pattern' a)) = a

Methods

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

PatternVars a => PatternVars [a] Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut [a]
Instance details Defined in Agda.Syntax.Internal type PatternVarOut [a] = PatternVarOut a

Methods

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

type Sort = Sort' Term Source #

type DataOrRecord = DataOrRecord' PatternOrCopattern Source #

type Args = [Arg Term] Source #

Type of argument lists.

data Abs a Source #

Binder.

Abs: The bound variable might appear in the body. NoAbs is pseudo-binder, it does not introduce a fresh variable, similar to the const of Haskell.

Constructors

Abs	The body has (at least) one free variable. Danger: `unAbs` doesn't shift variables properly
Fields absName :: ArgName unAbs :: a
NoAbs
Fields absName :: ArgName unAbs :: a

Instances

Instances details

Decoration Abs Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Abs Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

toList :: Abs a -> [a] #

null :: Abs a -> Bool #

length :: Abs a -> Int #

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

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

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

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

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

Traversable Abs Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor Abs Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Conversion MOT a b => Conversion MOT (Abs a) (Abs b) Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Abs a -> MOT (Abs b) Source #

Pretty t => Pretty (Abs t) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Abs t -> Doc Source #

prettyPrec :: Int -> Abs t -> Doc Source #

prettyList :: [Abs t] -> Doc Source #

Suggest (Abs b) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

suggestName :: Abs b -> Maybe String Source #

GetDefs a => GetDefs (Abs a) Source #

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike a => TermLike (Abs a) Source #

Instance details

Methods

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

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

NamesIn a => NamesIn (Abs a) Source #

Instance details

Methods

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

KillRange a => KillRange (Abs a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Abs a) Source #

(Free i, Reify i) => Reify (Abs i) Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Abs i)
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Abs i) = (Name, ReifiesTo i)

Methods

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

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

(TermSubst a, AbsTerm a) => AbsTerm (Abs a) Source #

Instance details

Methods

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

(Subst a, EqualSy a) => EqualSy (Abs a) Source #

Ignores absName.

Instance details

Methods

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

Free t => Free (Abs t) Source #

Instance details

Methods

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

PrecomputeFreeVars a => PrecomputeFreeVars (Abs a) Source #

Instance details

Methods

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

(Reduce a, ForceNotFree a) => ForceNotFree (Abs a) Source #

Instance details

Methods

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

(Subst a, UsableRelevance a) => UsableRelevance (Abs a) Source #

Instance details

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Abs a -> m Bool Source #

MentionsMeta t => MentionsMeta (Abs t) Source #

Instance details

Methods

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

(Subst a, AnyRigid a) => AnyRigid (Abs a) Source #

Instance details

Methods

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

Occurs (Abs Term) Source #

Instance details

Methods

occurs :: Abs Term -> OccursM (Abs Term) Source #

metaOccurs :: MetaId -> Abs Term -> TCM () Source #

Occurs (Abs Type) Source #

Instance details

Methods

occurs :: Abs Type -> OccursM (Abs Type) Source #

metaOccurs :: MetaId -> Abs Type -> TCM () Source #

IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source #

Does not worry about raising.

Instance details

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Abs a -> m Bool Source #

UnFreezeMeta a => UnFreezeMeta (Abs a) Source #

Instance details

Methods

unfreezeMeta :: MonadMetaSolver m => Abs a -> m () Source #

ComputeOccurrences a => ComputeOccurrences (Abs a) Source #

Instance details

Methods

occurrences :: Abs a -> OccM OccurrencesBuilder Source #

Instantiate t => Instantiate (Abs t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

(Subst a, InstantiateFull a) => InstantiateFull (Abs a) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Abs a -> ReduceM (Abs a) Source #

(Subst a, Normalise a) => Normalise (Abs a) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Abs a -> ReduceM (Abs a) Source #

(Subst a, Reduce a) => Reduce (Abs a) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Abs a -> ReduceM (Abs a) Source #

reduceB' :: Abs a -> ReduceM (Blocked (Abs a)) Source #

(Subst a, Simplify a) => Simplify (Abs a) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Abs a -> ReduceM (Abs a)

GetMatchables a => GetMatchables (Abs a) Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

NLPatVars a => NLPatVars (Abs a) Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatVarsUnder :: Int -> Abs a -> IntSet Source #

nlPatVars :: Abs a -> IntSet Source #

EmbPrj a => EmbPrj (Abs a) Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Abs a -> S Int32 Source #

icod_ :: Abs a -> S Int32 Source #

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

Subst a => Subst (Abs a) Source #

Instance details

Associated Types

type SubstArg (Abs a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Abs a) = SubstArg a

Methods

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

(Subst a, SynEq a) => SynEq (Abs a) Source #

Instance details

Methods

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

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

Sized a => Sized (Abs a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

size :: Abs a -> Int Source #

natSize :: Abs a -> Peano Source #

Generic (Abs a) Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Abs a)

Instance details

Defined in Agda.Syntax.Internal

type Rep (Abs a) = D1 ('MetaData "Abs" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "Abs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "NoAbs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

Methods

from :: Abs a -> Rep (Abs a) x #

to :: Rep (Abs a) x -> Abs a #

Show a => Show (Abs a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Abs a -> ShowS #

show :: Abs a -> String #

showList :: [Abs a] -> ShowS #

NFData a => NFData (Abs a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Abs a -> () #

(Subst a, Eq a) => Eq (Abs a) Source #

Equality of binders relies on weakening which is a special case of renaming which is a special case of substitution.

Instance details

Methods

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

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

(Subst a, Ord a) => Ord (Abs a) Source #

Instance details

Methods

compare :: Abs a -> Abs a -> Ordering #

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

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

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

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

max :: Abs a -> Abs a -> Abs a #

min :: Abs a -> Abs a -> Abs a #

ToNLPat a b => ToNLPat (Abs a) (Abs b) Source #

Instance details

Methods

toNLPat :: Abs a -> Abs b Source #

NLPatToTerm p a => NLPatToTerm (Abs p) (Abs a) Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

type TypeOf (Abs Term) Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Abs Term) = (Dom Type, Abs Type)

type TypeOf (Abs Type) Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Abs Type) = Dom Type

type ReifiesTo (Abs i) Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Abs i) = (Name, ReifiesTo i)

type SubstArg (Abs a) Source #

Instance details

type SubstArg (Abs a) = SubstArg a

type Rep (Abs a) Source #

Instance details

Defined in Agda.Syntax.Internal

type Rep (Abs a) = D1 ('MetaData "Abs" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "Abs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "NoAbs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

class LensSort a where Source #

Minimal complete definition

lensSort

Methods

lensSort :: Lens' a Sort Source #

getSort :: a -> Sort Source #

Instances

Instances details

LensSort Sort Source #
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort Sort Source # getSort :: Sort -> Sort Source #
LensSort a => LensSort (Arg a) Source #
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' (Arg a) Sort Source # getSort :: Arg a -> Sort Source #
LensSort a => LensSort (Dom a) Source #
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' (Dom a) Sort Source # getSort :: Dom a -> Sort Source #
LensSort (Type' a) Source #
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' (Type' a) Sort Source # getSort :: Type' a -> Sort Source #

type Elims Source #

Arguments

= [Elim]

eliminations ordered left-to-right.

arity :: Type -> Nat Source #

Doesn't do any reduction.

pattern Prop :: Level' t -> Sort' t Source #

pattern SSet :: Level' t -> Sort' t Source #

var :: Nat -> Term Source #

An unapplied variable.

data PlusLevel' t Source #

Constructors

Plus !Integer t

Instances

Instances details

Pretty PlusLevel Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: PlusLevel -> Doc Source #

prettyPrec :: Int -> PlusLevel -> Doc Source #

prettyList :: [PlusLevel] -> Doc Source #

TermSize PlusLevel Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

termSize :: PlusLevel -> Int Source #

tsize :: PlusLevel -> Sum Int Source #

GetDefs PlusLevel Source #

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike PlusLevel Source #

Instance details

Methods

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

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

AllMetas PlusLevel Source #

Instance details

Methods

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

NamesIn PlusLevel Source #

Instance details

Methods

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

KillRange PlusLevel Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PlusLevel Source #

AbsTerm PlusLevel Source #

Instance details

Methods

absTerm :: Term -> PlusLevel -> PlusLevel Source #

EqualSy PlusLevel Source #

Instance details

Methods

equalSy :: PlusLevel -> PlusLevel -> Bool Source #

CheckInternal PlusLevel Source #

Instance details

Methods

checkInternal' :: MonadCheckInternal m => Action m -> PlusLevel -> Comparison -> TypeOf PlusLevel -> m PlusLevel Source #

checkInternal :: MonadCheckInternal m => PlusLevel -> Comparison -> TypeOf PlusLevel -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => Action m -> PlusLevel -> m PlusLevel Source #

inferInternal :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => PlusLevel -> m () Source #

PrecomputeFreeVars PlusLevel Source #

Instance details

Methods

precomputeFreeVars :: PlusLevel -> FV PlusLevel Source #

ForceNotFree PlusLevel Source #

Instance details

Methods

forceNotFree' :: MonadFreeRed m => PlusLevel -> m PlusLevel

UsableRelevance PlusLevel Source #

Instance details

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> PlusLevel -> m Bool Source #

MentionsMeta PlusLevel Source #

Instance details

Methods

mentionsMetas :: HashSet MetaId -> PlusLevel -> Bool Source #

AnyRigid PlusLevel Source #

Instance details

Methods

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

Occurs PlusLevel Source #

Instance details

Methods

occurs :: PlusLevel -> OccursM PlusLevel Source #

metaOccurs :: MetaId -> PlusLevel -> TCM () Source #

IsInstantiatedMeta PlusLevel Source #

Instance details

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => PlusLevel -> m Bool Source #

UnFreezeMeta PlusLevel Source #

Instance details

Methods

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

ComputeOccurrences PlusLevel Source #

Instance details

Methods

occurrences :: PlusLevel -> OccM OccurrencesBuilder Source #

InstantiateFull PlusLevel Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: PlusLevel -> ReduceM PlusLevel Source #

Normalise PlusLevel Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: PlusLevel -> ReduceM PlusLevel Source #

Reduce PlusLevel Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: PlusLevel -> ReduceM PlusLevel Source #

reduceB' :: PlusLevel -> ReduceM (Blocked PlusLevel) Source #

Simplify PlusLevel Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: PlusLevel -> ReduceM PlusLevel

EmbPrj PlusLevel Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PlusLevel -> S Int32 Source #

icod_ :: PlusLevel -> S Int32 Source #

value :: Int32 -> R PlusLevel Source #

DeBruijn PlusLevel Source #

Instance details

Methods

deBruijnVar :: Int -> PlusLevel Source #

debruijnNamedVar :: String -> Int -> PlusLevel Source #

deBruijnView :: PlusLevel -> Maybe Int Source #

SynEq PlusLevel Source #

Instance details

Methods

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

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

Foldable PlusLevel' Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: PlusLevel' a -> Bool #

length :: PlusLevel' a -> Int #

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

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

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

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

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

Traversable PlusLevel' Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor PlusLevel' Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

NFData PlusLevel Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: PlusLevel -> () #

Eq PlusLevel Source #

Instance details

Methods

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

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

Ord PlusLevel Source #

Instance details

Methods

compare :: PlusLevel -> PlusLevel -> Ordering #

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

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

(>) :: PlusLevel -> PlusLevel -> Bool #

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

max :: PlusLevel -> PlusLevel -> PlusLevel #

min :: PlusLevel -> PlusLevel -> PlusLevel #

Free t => Free (PlusLevel' t) Source #

Instance details

Methods

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

Instantiate t => Instantiate (PlusLevel' t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

IsMeta a => IsMeta (PlusLevel' a) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: PlusLevel' a -> Maybe MetaId Source #

Subst a => Subst (PlusLevel' a) Source #

Instance details

Associated Types

type SubstArg (PlusLevel' a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (PlusLevel' a) = SubstArg a

Methods

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

Show t => Show (PlusLevel' t) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> PlusLevel' t -> ShowS #

show :: PlusLevel' t -> String #

showList :: [PlusLevel' t] -> ShowS #

type TypeOf PlusLevel Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf PlusLevel = ()

type TypeOf [PlusLevel] Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf [PlusLevel] = ()

type SubstArg (PlusLevel' a) Source #

Instance details

CopatternMatchingAllowed DataOrRecord Source #

type SubstArg (PlusLevel' a) = SubstArg a

type Blocked = Blocked' Term Source #

class TermSize a where Source #

The size of a term is roughly the number of nodes in its syntax tree. This number need not be precise for logical correctness of Agda, it is only used for reporting (and maybe decisions regarding performance).

Not counting towards the term size are:

sort and color annotations,
projections.

Minimal complete definition

tsize

Methods

termSize :: a -> Int Source #

tsize :: a -> Sum Int Source #

Instances

Instances details

TermSize Level Source #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Level -> Int Source # tsize :: Level -> Sum Int Source #
TermSize PlusLevel Source #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: PlusLevel -> Int Source # tsize :: PlusLevel -> Sum Int Source #
TermSize Sort Source #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Sort -> Int Source # tsize :: Sort -> Sum Int Source #
TermSize Term Source #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Term -> Int Source # tsize :: Term -> Sum Int Source #
TermSize a => TermSize (Substitution' a) Source #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Substitution' a -> Int Source # tsize :: Substitution' a -> Sum Int Source #
(Foldable t, TermSize a) => TermSize (t a) Source #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: t a -> Int Source # tsize :: t a -> Sum Int Source #

dontCare :: Term -> Term Source #

Add DontCare is it is not already a DontCare.

type NotBlocked = NotBlocked' Term Source #

argFromDom :: Dom' t a -> Arg a Source #

namedArgFromDom :: Dom' t a -> NamedArg a Source #

domFromArg :: Arg a -> Dom a Source #

domFromNamedArg :: NamedArg a -> Dom a Source #

defaultDom :: a -> Dom a Source #

defaultArgDom :: ArgInfo -> a -> Dom a Source #

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

type NamedArgs = [NamedArg Term] Source #

data DataOrRecord' p Source #

Constructors

IsData
IsRecord p

Instances

Instances details

Instance details

Defined in Agda.Syntax.Internal

Methods

copatternMatchingAllowed :: DataOrRecord -> Bool Source #

PatternMatchingAllowed DataOrRecord Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

patternMatchingAllowed :: DataOrRecord -> Bool Source #

KillRange DataOrRecord Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT DataOrRecord Source #

EmbPrj DataOrRecord Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DataOrRecord -> S Int32 Source #

icod_ :: DataOrRecord -> S Int32 Source #

value :: Int32 -> R DataOrRecord Source #

NFData DataOrRecord Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: DataOrRecord -> () #

NFData DataOrRecordE Source #

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

rnf :: DataOrRecordE -> () #

Generic (DataOrRecord' p) Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep (DataOrRecord' p)
Instance details Defined in Agda.Syntax.Internal type Rep (DataOrRecord' p) = D1 ('MetaData "DataOrRecord'" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "IsData" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 p)))

Methods

from :: DataOrRecord' p -> Rep (DataOrRecord' p) x #

to :: Rep (DataOrRecord' p) x -> DataOrRecord' p #

Show p => Show (DataOrRecord' p) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> DataOrRecord' p -> ShowS #

show :: DataOrRecord' p -> String #

showList :: [DataOrRecord' p] -> ShowS #

Eq p => Eq (DataOrRecord' p) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

(==) :: DataOrRecord' p -> DataOrRecord' p -> Bool #

(/=) :: DataOrRecord' p -> DataOrRecord' p -> Bool #

type Rep (DataOrRecord' p) Source #

Instance details

Defined in Agda.Syntax.Internal

type Rep (DataOrRecord' p) = D1 ('MetaData "DataOrRecord'" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "IsData" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 p)))

class LensConName a where Source #

Minimal complete definition

getConName

Methods

getConName :: a -> QName Source #

setConName :: QName -> a -> a Source #

mapConName :: (QName -> QName) -> a -> a Source #

Instances

Instances details

LensConName ConHead Source #
Instance details Defined in Agda.Syntax.Internal Methods getConName :: ConHead -> QName Source # setConName :: QName -> ConHead -> ConHead Source # mapConName :: (QName -> QName) -> ConHead -> ConHead Source #

type ConInfo = ConOrigin Source #

data Type'' t a Source #

Types are terms with a sort annotation.

Constructors

El
Fields _getSort :: Sort' t unEl :: a

Instances

Instances details

Pretty Type Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Type -> Doc Source #

prettyPrec :: Int -> Type -> Doc Source #

prettyList :: [Type] -> Doc Source #

TelToArgs ListTel Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

telToArgs :: ListTel -> [Arg ArgName] Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Type Source #

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike Type Source #

Instance details

Methods

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

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

AllMetas Type Source #

Instance details

Methods

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

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Telescope = Telescope

Methods

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

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

Reify Type Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Type
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Type = Type

Methods

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

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

TerSetSizeDepth ListTel Source #

Instance details

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: ListTel -> TerM a -> TerM a Source #

Instance details

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: Telescope -> TerM a -> TerM a Source #

AbsTerm Type Source #

Instance details

Methods

absTerm :: Term -> Type -> Type Source #

EqualSy Type Source #

Ignores sorts.

Instance details

Methods

equalSy :: Type -> Type -> Bool Source #

CheckInternal Type Source #

Instance details

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Type -> Comparison -> TypeOf Type -> m Type Source #

checkInternal :: MonadCheckInternal m => Type -> Comparison -> TypeOf Type -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Type ~ ()) => Action m -> Type -> m Type Source #

inferInternal :: (MonadCheckInternal m, TypeOf Type ~ ()) => Type -> m () Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Methods

PrecomputeFreeVars Type Source #

Instance details

Methods

precomputeFreeVars :: Type -> FV Type Source #

ForceNotFree Type Source #

Instance details

Methods

forceNotFree' :: MonadFreeRed m => Type -> m Type

MentionsMeta Type Source #

Instance details

Methods

mentionsMetas :: HashSet MetaId -> Type -> Bool Source #

AnyRigid Type Source #

Instance details

Methods

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

Occurs Type Source #

Instance details

Methods

occurs :: Type -> OccursM Type Source #

metaOccurs :: MetaId -> Type -> TCM () Source #

Instance details

Methods

addContext :: MonadAddContext m => Telescope -> m a -> m a Source #

UnFreezeMeta Type Source #

Instance details

Methods

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

ComputeOccurrences Type Source #

Instance details

Methods

occurrences :: Type -> OccM OccurrencesBuilder Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Type Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ContextEntry Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrimTerm Type Source #

Instance details

Methods

primTerm :: Type -> TCM Term Source #

PrimType Type Source #

Instance details

Methods

primType :: Type -> TCM Type Source #

ToTerm Type Source #

Instance details

Methods

toTerm :: TCM (Type -> Term) Source #

toTermR :: TCM (Type -> ReduceM Term) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Reduce Type Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Type -> ReduceM Type Source #

reduceB' :: Type -> ReduceM (Blocked Type) Source #

TeleNoAbs ListTel Source #

Instance details

Methods

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

Instance details

Methods

Instance details

Methods

abstract :: Telescope -> Telescope -> Telescope Source #

Abstract Type Source #

Instance details

Methods

abstract :: Telescope -> Type -> Type Source #

SynEq Type Source #

Syntactic equality ignores sorts.

Instance details

Methods

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

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

NFData Type Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Type -> () #

Match NLPType Type Source #

Instance details

Methods

match :: Relevance -> Telescope -> Telescope -> TypeOf Type -> NLPType -> Type -> NLM () Source #

NLPatToTerm NLPType Type Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatToTerm :: PureTCM m => NLPType -> m Type Source #

PatternFrom Type NLPType Source #

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> TypeOf Type -> Type -> TCM NLPType Source #

Conversion TOM Type (MExp O) Source #

Instance details

Defined in Agda.Auto.Convert

Methods

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

Conversion MOT (Exp O) Type Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type Source #

LensSort (Type' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' (Type' a) Sort Source #

getSort :: Type' a -> Sort Source #

SgTel (Dom Type) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom Type -> Telescope Source #

SgTel (Dom (ArgName, Type)) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

NamesIn a => NamesIn (Type' a) Source #

Instance details

Methods

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

KillRange a => KillRange (Type' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Type' a) Source #

Free t => Free (Type' t) Source #

Instance details

Methods

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

UsableRelevance a => UsableModality (Type' a) Source #

Instance details

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Type' a -> m Bool Source #

UsableRelevance a => UsableRelevance (Type' a) Source #

Instance details

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Type' a -> m Bool Source #

Occurs (Abs Type) Source #

Instance details

Methods

occurs :: Abs Type -> OccursM (Abs Type) Source #

metaOccurs :: MetaId -> Abs Type -> TCM () Source #

AddContext (Dom Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => Dom Type -> m a -> m a Source #

contextSize :: Dom Type -> Nat Source #

AddContext (Dom (Name, Type)) Source #

Instance details

Methods

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

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

AddContext (Dom (String, Type)) Source #

Instance details

Methods

addContext :: MonadAddContext m => Dom (String, Type) -> m a -> m a Source #

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

AddContext (KeepNames Telescope) Source #

Instance details

Methods

addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source #

IsSizeType a => IsSizeType (Type' a) Source #

Instance details

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => Type' a -> m (Maybe BoundedSize) Source #

PrettyTCM (Arg Type) Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Dom Type) Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Type' NLPat) Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Type' NLPat -> m Doc Source #

ToTerm (Dom Type) Source #

Instance details

Methods

toTerm :: TCM (Dom Type -> Term) Source #

toTermR :: TCM (Dom Type -> ReduceM Term) Source #

Instantiate t => Instantiate (Type' t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull (Type' t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Type' t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Type' t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

EmbPrj a => EmbPrj (Type' a) Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Type' a -> S Int32 Source #

icod_ :: Type' a -> S Int32 Source #

value :: Int32 -> R (Type' a) Source #

Decoration (Type'' t) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

traverseF :: Functor m => (a -> m b) -> Type'' t a -> m (Type'' t b) Source #

distributeF :: Functor m => Type'' t (m a) -> m (Type'' t a) Source #

Foldable (Type'' t) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Type'' t m -> m #

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

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

foldr :: (a -> b -> b) -> b -> Type'' t a -> b #

foldr' :: (a -> b -> b) -> b -> Type'' t a -> b #

foldl :: (b -> a -> b) -> b -> Type'' t a -> b #

foldl' :: (b -> a -> b) -> b -> Type'' t a -> b #

foldr1 :: (a -> a -> a) -> Type'' t a -> a #

foldl1 :: (a -> a -> a) -> Type'' t a -> a #

toList :: Type'' t a -> [a] #

null :: Type'' t a -> Bool #

length :: Type'' t a -> Int #

elem :: Eq a => a -> Type'' t a -> Bool #

maximum :: Ord a => Type'' t a -> a #

minimum :: Ord a => Type'' t a -> a #

sum :: Num a => Type'' t a -> a #

product :: Num a => Type'' t a -> a #

Traversable (Type'' t) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor (Type'' t) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

fmap :: (a -> b) -> Type'' t a -> Type'' t b #

(<$) :: a -> Type'' t b -> Type'' t a #

Eq a => Eq (Type' a) Source #

Syntactic Type equality, ignores sort annotations.

Instance details

Methods

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

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

Ord a => Ord (Type' a) Source #

Instance details

Methods

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

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

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

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

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

max :: Type' a -> Type' a -> Type' a #

min :: Type' a -> Type' a -> Type' a #

SgTel (ArgName, Dom Type) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

AddContext (Name, Dom Type) Source #

Instance details

Methods

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

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

AddContext (KeepNames String, Dom Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => (KeepNames String, Dom Type) -> m a -> m a Source #

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

AddContext (List1 Name, Dom Type) Source #

Instance details

Methods

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

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

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

Instance details

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

Methods

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

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

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

Instance details

Methods

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

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

AddContext (Text, Dom Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => (Text, Dom Type) -> m a -> m a Source #

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

AddContext (String, Dom Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => (String, Dom Type) -> m a -> m a Source #

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

AddContext ([Name], Dom Type) Source #

Instance details

Methods

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

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

AddContext ([Arg Name], Type) Source #

Instance details

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

Methods

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

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

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

Instance details

Methods

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

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

IsMeta a => IsMeta (Type'' t a) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Type'' t a -> Maybe MetaId Source #

(Coercible a Term, Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Type'' a b) Source #

Instance details

Associated Types

type SubstArg (Type'' a b)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Type'' a b) = SubstArg a

Methods

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

(Show t, Show a) => Show (Type'' t a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Type'' t a -> ShowS #

show :: Type'' t a -> String #

showList :: [Type'' t a] -> ShowS #

type TypeOf Type Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf Type = ()

type ReifiesTo Telescope Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Type Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Type = Type

type TypeOf (Abs Type) Source #

Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Abs Type) = Dom Type

type SubstArg (Type'' a b) Source #

Instance details

type SubstArg (Type'' a b) = SubstArg a

type Type' a = Type'' Term a Source #

data Tele a Source #

Sequence of types. An argument of the first type is bound in later types and so on.

Constructors

EmptyTel
ExtendTel a (Abs (Tele a))	`Abs` is never `NoAbs`.

Instances

Instances details

Instance details

Defined in Agda.Syntax.Internal

Methods

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Telescope = Telescope

Methods

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

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

Instance details

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: Telescope -> TerM a -> TerM a Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Methods

Instance details

Methods

addContext :: MonadAddContext m => Telescope -> m a -> m a Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Instance details

Methods

Instance details

Methods

abstract :: Telescope -> Telescope -> Telescope Source #

Foldable Tele Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

toList :: Tele a -> [a] #

null :: Tele a -> Bool #

length :: Tele a -> Int #

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

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

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

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

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

Traversable Tele Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor Tele Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

TermLike a => TermLike (Tele a) Source #

Instance details

Methods

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

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

TermLike a => AllMetas (Tele a) Source #

Instance details

Methods

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

NamesIn a => NamesIn (Tele a) Source #

Instance details

Methods

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

KillRange a => KillRange (Tele a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Tele a) Source #

Free t => Free (Tele t) Source #

Instance details

Methods

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

MentionsMeta a => MentionsMeta (Tele a) Source #

Instance details

Methods

mentionsMetas :: HashSet MetaId -> Tele a -> Bool Source #

AddContext (KeepNames Telescope) Source #

Instance details

Methods

addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source #

ComputeOccurrences a => ComputeOccurrences (Tele a) Source #

Instance details

Methods

occurrences :: Tele a -> OccM OccurrencesBuilder Source #

Instantiate t => Instantiate (Tele t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

(Subst a, InstantiateFull a) => InstantiateFull (Tele a) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Tele a -> ReduceM (Tele a) Source #

(Subst a, Normalise a) => Normalise (Tele a) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Tele a -> ReduceM (Tele a) Source #

(Subst a, Simplify a) => Simplify (Tele a) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Tele a -> ReduceM (Tele a)

EmbPrj a => EmbPrj (Tele a) Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Tele a -> S Int32 Source #

icod_ :: Tele a -> S Int32 Source #

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

TermSubst a => Apply (Tele a) Source #

Instance details

Methods

apply :: Tele a -> Args -> Tele a Source #

applyE :: Tele a -> Elims -> Tele a Source #

Subst a => Subst (Tele a) Source #

Instance details

Associated Types

type SubstArg (Tele a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Tele a) = SubstArg a

Methods

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

Null (Tele a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

empty :: Tele a Source #

null :: Tele a -> Bool Source #

Sized (Tele a) Source #

The size of a telescope is its length (as a list).

Instance details

Defined in Agda.Syntax.Internal

Methods

size :: Tele a -> Int Source #

natSize :: Tele a -> Peano Source #

Generic (Tele a) Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Tele a)

Instance details

Defined in Agda.Syntax.Internal

type Rep (Tele a) = D1 ('MetaData "Tele" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "EmptyTel" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExtendTel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Abs (Tele a)))))

Methods

from :: Tele a -> Rep (Tele a) x #

to :: Rep (Tele a) x -> Tele a #

Show a => Show (Tele a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Tele a -> ShowS #

show :: Tele a -> String #

showList :: [Tele a] -> ShowS #

NFData a => NFData (Tele a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Tele a -> () #

(Subst a, Eq a) => Eq (Tele a) Source #

Instance details

Methods

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

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

(Subst a, Ord a) => Ord (Tele a) Source #

Instance details

Methods

compare :: Tele a -> Tele a -> Ordering #

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

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

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

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

max :: Tele a -> Tele a -> Tele a #

min :: Tele a -> Tele a -> Tele a #

type ReifiesTo Telescope Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type SubstArg (Tele a) Source #

Instance details

type SubstArg (Tele a) = SubstArg a

type Rep (Tele a) Source #

Instance details

Defined in Agda.Syntax.Internal

type Rep (Tele a) = D1 ('MetaData "Tele" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "EmptyTel" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExtendTel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Abs (Tele a)))))

data UnivSize Source #

Constructors

USmall	`PropSetSSet ℓ`.
ULarge	`(PropSetSSet)ωᵢ`.

Instances

Instances details

Show UnivSize Source #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> UnivSize -> ShowS # show :: UnivSize -> String # showList :: [UnivSize] -> ShowS #
Eq UnivSize Source #
Instance details Defined in Agda.Syntax.Internal Methods (==) :: UnivSize -> UnivSize -> Bool # (/=) :: UnivSize -> UnivSize -> Bool #

isStrictDataSort :: Sort' t -> Bool Source #

Is this a strict universe inhabitable by data types?

type PlusLevel = PlusLevel' Term Source #

type LevelAtom = Term Source #

newtype BraveTerm Source #

Newtypes for terms that produce a dummy, rather than crash, when applied to incompatible eliminations.

Constructors

BraveTerm
Fields unBrave :: Term

Instances

Instances details

Apply BraveTerm Source #

Instance details

Methods

apply :: BraveTerm -> Args -> BraveTerm Source #

applyE :: BraveTerm -> Elims -> BraveTerm Source #

Subst BraveTerm Source #

Instance details

Associated Types

type SubstArg BraveTerm
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg BraveTerm = BraveTerm

Methods

applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm Source #

DeBruijn BraveTerm Source #

Instance details

Methods

deBruijnVar :: Int -> BraveTerm Source #

debruijnNamedVar :: String -> Int -> BraveTerm Source #

deBruijnView :: BraveTerm -> Maybe Int Source #

Show BraveTerm Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> BraveTerm -> ShowS #

show :: BraveTerm -> String #

showList :: [BraveTerm] -> ShowS #

type SubstArg BraveTerm Source #

Instance details

InstantiateFull ConPatternInfo Source #

type SubstArg BraveTerm = BraveTerm

type Blocked_ = Blocked () Source #

'Blocked a without the a.

type NAPs = [NamedArg DeBruijnPattern] Source #

Named pattern arguments.

type DeBruijnPattern = Pattern' DBPatVar Source #

clausePats :: Clause -> [Arg DeBruijnPattern] Source #

type PatVarName = ArgName Source #

Pattern variables.

patVarNameToString :: PatVarName -> String Source #

nameToPatVarName :: Name -> PatVarName Source #

data PatternInfo Source #

Constructors

PatternInfo
Fields patOrigin :: PatOrigin patAsNames :: [Name]

Instances

Instances details

KillRange PatternInfo Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PatternInfo Source #

EmbPrj PatternInfo Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PatternInfo -> S Int32 Source #

icod_ :: PatternInfo -> S Int32 Source #

value :: Int32 -> R PatternInfo Source #

Generic PatternInfo Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep PatternInfo

Instance details

Defined in Agda.Syntax.Internal

type Rep PatternInfo = D1 ('MetaData "PatternInfo" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "PatternInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "patOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatOrigin) :*: S1 ('MetaSel ('Just "patAsNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])))

Methods

from :: PatternInfo -> Rep PatternInfo x #

to :: Rep PatternInfo x -> PatternInfo #

Show PatternInfo Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> PatternInfo -> ShowS #

show :: PatternInfo -> String #

showList :: [PatternInfo] -> ShowS #

NFData PatternInfo Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: PatternInfo -> () #

Eq PatternInfo Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

type Rep PatternInfo Source #

Instance details

Defined in Agda.Syntax.Internal

type Rep PatternInfo = D1 ('MetaData "PatternInfo" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "PatternInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "patOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatOrigin) :*: S1 ('MetaSel ('Just "patAsNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])))

data PatOrigin Source #

Origin of the pattern: what did the user write in this position?

Constructors

PatOSystem	Pattern inserted by the system
PatOSplit	Pattern generated by case split
PatOVar Name	User wrote a variable pattern
PatODot	User wrote a dot pattern
PatOWild	User wrote a wildcard pattern
PatOCon	User wrote a constructor pattern
PatORec	User wrote a record pattern
PatOLit	User wrote a literal pattern
PatOAbsurd	User wrote an absurd pattern

Instances

Instances details

KillRange PatOrigin Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PatOrigin Source #

EmbPrj PatOrigin Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PatOrigin -> S Int32 Source #

icod_ :: PatOrigin -> S Int32 Source #

value :: Int32 -> R PatOrigin Source #

Generic PatOrigin Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep PatOrigin

Instance details

Defined in Agda.Syntax.Internal

Methods

from :: PatOrigin -> Rep PatOrigin x #

to :: Rep PatOrigin x -> PatOrigin #

Show PatOrigin Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> PatOrigin -> ShowS #

show :: PatOrigin -> String #

showList :: [PatOrigin] -> ShowS #

NFData PatOrigin Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: PatOrigin -> () #

Eq PatOrigin Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

type Rep PatOrigin Source #

Instance details

Defined in Agda.Syntax.Internal

defaultPatternInfo :: PatternInfo Source #

data ConPatternInfo Source #

The ConPatternInfo states whether the constructor belongs to a record type (True) or data type (False). In the former case, the PatOrigin of the conPInfo says whether the record pattern orginates from the expansion of an implicit pattern. The Type is the type of the whole record pattern. The scope used for the type is given by any outer scope plus the clause's telescope (clauseTel).

Constructors

ConPatternInfo

Fields

conPInfo :: PatternInfo
Information on the origin of the pattern.
conPRecord :: Bool
False if data constructor. True if record constructor.
conPFallThrough :: Bool
Should the match block on non-canonical terms or can it proceed to the catch-all clause?
conPType :: Maybe (Arg Type)
The type of the whole constructor pattern. Should be present (Just) if constructor pattern is is generated ordinarily by type-checking. Could be absent (Nothing) if pattern comes from some plugin (like Agsy). Needed e.g. for with-clause stripping.
conPLazy :: Bool
Lazy patterns are generated by the forcing translation in the unifier (unifyStep) and are dropped by the clause compiler (TODO: not yet) (compileClauses) when the variables they bind are unused. The GHC backend compiles lazy matches to lazy patterns in Haskell (TODO: not yet).

Instances

Instances details

KillRange ConPatternInfo Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT ConPatternInfo Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ConPatternInfo -> ReduceM ConPatternInfo Source #

Normalise ConPatternInfo Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: ConPatternInfo -> ReduceM ConPatternInfo Source #

EmbPrj ConPatternInfo Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ConPatternInfo -> S Int32 Source #

icod_ :: ConPatternInfo -> S Int32 Source #

value :: Int32 -> R ConPatternInfo Source #

Subst ConPatternInfo Source #

Instance details

Associated Types

type SubstArg ConPatternInfo
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ConPatternInfo = Term

Methods

applySubst :: Substitution' (SubstArg ConPatternInfo) -> ConPatternInfo -> ConPatternInfo Source #

Generic ConPatternInfo Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep ConPatternInfo

Instance details

Defined in Agda.Syntax.Internal

type Rep ConPatternInfo = D1 ('MetaData "ConPatternInfo" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "ConPatternInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "conPInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Just "conPRecord") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "conPFallThrough") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "conPType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Arg Type))) :*: S1 ('MetaSel ('Just "conPLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

Methods

from :: ConPatternInfo -> Rep ConPatternInfo x #

to :: Rep ConPatternInfo x -> ConPatternInfo #

Show ConPatternInfo Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> ConPatternInfo -> ShowS #

show :: ConPatternInfo -> String #

showList :: [ConPatternInfo] -> ShowS #

NFData ConPatternInfo Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: ConPatternInfo -> () #

type SubstArg ConPatternInfo Source #

Instance details

UsableSizeVars DeBruijnPattern Source #

type SubstArg ConPatternInfo = Term

type Rep ConPatternInfo Source #

Instance details

Defined in Agda.Syntax.Internal

type Rep ConPatternInfo = D1 ('MetaData "ConPatternInfo" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "ConPatternInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "conPInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Just "conPRecord") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "conPFallThrough") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "conPType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Arg Type))) :*: S1 ('MetaSel ('Just "conPLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

dotP :: Term -> Pattern' a Source #

data DBPatVar Source #

Type used when numbering pattern variables.

Constructors

DBPatVar
Fields dbPatVarName :: PatVarName dbPatVarIndex :: !Int

Instances

Instances details

Pretty DBPatVar Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: DBPatVar -> Doc Source #

prettyPrec :: Int -> DBPatVar -> Doc Source #

prettyList :: [DBPatVar] -> Doc Source #

KillRange DBPatVar Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT DBPatVar Source #

Instance details

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: DeBruijnPattern -> TerM VarSet Source #

UsableSizeVars MaskedDeBruijnPatterns Source #

Instance details

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet Source #

PrettyTCM DBPatVar Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

InstantiateFull DBPatVar Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: DBPatVar -> ReduceM DBPatVar Source #

Normalise DBPatVar Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: DBPatVar -> ReduceM DBPatVar Source #

Reduce DeBruijnPattern Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: DeBruijnPattern -> ReduceM DeBruijnPattern Source #

reduceB' :: DeBruijnPattern -> ReduceM (Blocked DeBruijnPattern) Source #

EmbPrj DBPatVar Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DBPatVar -> S Int32 Source #

icod_ :: DBPatVar -> S Int32 Source #

value :: Int32 -> R DBPatVar Source #

Subst DeBruijnPattern Source #

Instance details

Associated Types

type SubstArg DeBruijnPattern
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg DeBruijnPattern = DeBruijnPattern

Methods

applySubst :: Substitution' (SubstArg DeBruijnPattern) -> DeBruijnPattern -> DeBruijnPattern Source #

DeBruijn DBPatVar Source #

Instance details

Methods

deBruijnVar :: Int -> DBPatVar Source #

debruijnNamedVar :: String -> Int -> DBPatVar Source #

deBruijnView :: DBPatVar -> Maybe Int Source #

Generic DBPatVar Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep DBPatVar

Instance details

Defined in Agda.Syntax.Internal

type Rep DBPatVar = D1 ('MetaData "DBPatVar" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "DBPatVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "dbPatVarName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatVarName) :*: S1 ('MetaSel ('Just "dbPatVarIndex") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

Methods

from :: DBPatVar -> Rep DBPatVar x #

to :: Rep DBPatVar x -> DBPatVar #

Show DBPatVar Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> DBPatVar -> ShowS #

show :: DBPatVar -> String #

showList :: [DBPatVar] -> ShowS #

NFData DBPatVar Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: DBPatVar -> () #

Eq DBPatVar Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

LabelPatVars Pattern DeBruijnPattern Source #

Instance details

Associated Types

type PatVarLabel DeBruijnPattern
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel DeBruijnPattern = Int

Methods

labelPatVars :: Pattern -> State [PatVarLabel DeBruijnPattern] DeBruijnPattern Source #

unlabelPatVars :: DeBruijnPattern -> Pattern Source #

UsableSizeVars (Masked DeBruijnPattern) Source #

Instance details

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet Source #

UsableSizeVars [DeBruijnPattern] Source #

Instance details

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: [DeBruijnPattern] -> TerM VarSet Source #

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

Instance details

Methods

toNLPat :: Arg DeBruijnPattern -> Elim' NLPat Source #

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

Instance details

Methods

toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat Source #

type PatVarLabel DeBruijnPattern Source #

Instance details

type PatVarLabel DeBruijnPattern = Int

type SubstArg DeBruijnPattern Source #

Instance details

properlyMatching' Source #

type SubstArg DeBruijnPattern = DeBruijnPattern

type Rep DBPatVar Source #

Instance details

Defined in Agda.Syntax.Internal

type Rep DBPatVar = D1 ('MetaData "DBPatVar" "Agda.Syntax.Internal" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "DBPatVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "dbPatVarName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatVarName) :*: S1 ('MetaSel ('Just "dbPatVarIndex") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

namedVarP :: PatVarName -> Named_ Pattern Source #

namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern Source #

absurdP :: Int -> DeBruijnPattern Source #

Make an absurd pattern with the given de Bruijn index.

absurdPatternName :: PatVarName Source #

noConPatternInfo :: ConPatternInfo Source #

toConPatternInfo :: ConInfo -> ConPatternInfo Source #

Build partial ConPatternInfo from ConInfo

fromConPatternInfo :: ConPatternInfo -> ConInfo Source #

Build ConInfo from ConPatternInfo.

type family PatternVarOut a Source #

Instances

Instances details

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 PatternVarOut (NamedArg (Pattern' a)) = a
type PatternVarOut [a] Source #
Instance details Defined in Agda.Syntax.Internal type PatternVarOut [a] = PatternVarOut a

patternInfo :: Pattern' x -> Maybe PatternInfo Source #

Retrieve the PatternInfo from a pattern

patternOrigin :: Pattern' x -> Maybe PatOrigin Source #

Retrieve the origin of a pattern

properlyMatching :: Pattern' a -> Bool Source #

Does the pattern perform a match that could fail?

Arguments

:: Bool	Should absurd patterns count as proper match?
-> Bool	Should projection patterns count as proper match?
-> Pattern' a	The pattern.
-> Bool

type PatternSubstitution = Substitution' DeBruijnPattern Source #

data EqualityView Source #

View type as equality type.

Constructors

EqualityViewType EqualityTypeData
OtherType Type	reduced
IdiomType Type	reduced

Instances

Instances details

TermLike EqualityView Source #

Instance details

Methods

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

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

Free EqualityView Source #

Instance details

Methods

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

EqualityUnview EqualityView Source #

Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

equalityUnview :: EqualityView -> Type Source #

PrettyTCM EqualityView Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

Instantiate EqualityView Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: EqualityView -> ReduceM EqualityView Source #

InstantiateFull EqualityView Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: EqualityView -> ReduceM EqualityView Source #

Normalise EqualityView Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: EqualityView -> ReduceM EqualityView Source #

Reduce EqualityView Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: EqualityView -> ReduceM EqualityView Source #

reduceB' :: EqualityView -> ReduceM (Blocked EqualityView) Source #

Simplify EqualityView Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: EqualityView -> ReduceM EqualityView

Subst EqualityView Source #

Instance details

Associated Types

type SubstArg EqualityView
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg EqualityView = Term

Methods

applySubst :: Substitution' (SubstArg EqualityView) -> EqualityView -> EqualityView Source #

type SubstArg EqualityView Source #

Instance details

EqualityUnview EqualityTypeData Source #

type SubstArg EqualityView = Term

data EqualityTypeData Source #

Constructors

EqualityTypeData
Fields _eqtSort :: Sort Sort of this type. _eqtName :: QName Builtin EQUALITY. _eqtParams :: Args Hidden. Empty or `Level`. _eqtType :: Arg Term Hidden. _eqtLhs :: Arg Term NotHidden. _eqtRhs :: Arg Term NotHidden.

Instances

Instances details

Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

equalityUnview :: EqualityTypeData -> Type Source #

Subst EqualityTypeData Source #

Instance details

Associated Types

type SubstArg EqualityTypeData
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg EqualityTypeData = Term

Methods

applySubst :: Substitution' (SubstArg EqualityTypeData) -> EqualityTypeData -> EqualityTypeData Source #

type SubstArg EqualityTypeData Source #

Instance details

type SubstArg EqualityTypeData = Term

pattern EqualityType :: Sort -> QName -> Args -> Arg Term -> Arg Term -> Arg Term -> EqualityView Source #

eqtSort :: EqualityView -> Sort Source #

eqtName :: EqualityView -> QName Source #

eqtParams :: EqualityView -> Args Source #

eqtType :: EqualityView -> Arg Term Source #

eqtLhs :: EqualityView -> Arg Term Source #

eqtRhs :: EqualityView -> Arg Term Source #

isEqualityType :: EqualityView -> Bool Source #

data PathView Source #

View type as path type.

Constructors

PathType
Fields pathSort :: Sort Sort of this type. pathName :: QName Builtin PATH. pathLevel :: Arg Term Hidden pathType :: Arg Term Hidden pathLhs :: Arg Term NotHidden pathRhs :: Arg Term NotHidden
OType Type	reduced

isPathType :: PathView -> Bool Source #

data IntervalView Source #

Constructors

IZero
IOne
IMin (Arg Term) (Arg Term)
IMax (Arg Term) (Arg Term)
INeg (Arg Term)
OTerm Term

Instances

Instances details

Show IntervalView Source #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> IntervalView -> ShowS # show :: IntervalView -> String # showList :: [IntervalView] -> ShowS #

isIOne :: IntervalView -> Bool Source #

absurdBody :: Abs Term Source #

Absurd lambdas are internally represented as identity with variable name "()".

isAbsurdBody :: Abs Term -> Bool Source #

isAbsurdPatternName :: PatVarName -> Bool Source #

type DummyTermKind = String Source #

dummyLocName :: CallStack -> String Source #

Construct a string representing the call-site that created the dummy thing.

dummyTermWith :: DummyTermKind -> CallStack -> Term Source #

Aux: A dummy term to constitute a dummy termlevelsort/type.

dummyLevel :: CallStack -> Level Source #

A dummy level to constitute a level/sort created at location. Note: use macro DUMMY_LEVEL !

atomicLevel :: t -> Level' t Source #

dummyTerm :: CallStack -> Term Source #

A dummy term created at location. Note: use macro DUMMY_TERM !

__DUMMY_TERM__ :: HasCallStack => Term Source #

__DUMMY_LEVEL__ :: HasCallStack => Level Source #

dummySort :: CallStack -> Sort Source #

A dummy sort created at location. Note: use macro DUMMY_SORT !

__DUMMY_SORT__ :: HasCallStack => Sort Source #

dummyType :: CallStack -> Type Source #

A dummy type created at location. Note: use macro DUMMY_TYPE !

__DUMMY_TYPE__ :: HasCallStack => Type Source #

dummyDom :: CallStack -> Dom Type Source #

Context entries without a type have this dummy type. Note: use macro DUMMY_DOM !

__DUMMY_DOM__ :: HasCallStack => Dom Type Source #

pattern ClosedLevel :: Integer -> Level Source #

Constant level n

varSort :: Int -> Sort Source #

tmSort :: Term -> Sort Source #

tmSSort :: Term -> Sort Source #

levelPlus :: Integer -> Level -> Level Source #

Given a constant m and level l, compute m + l

levelSuc :: Level -> Level Source #

mkType :: Integer -> Sort Source #

mkProp :: Integer -> Sort Source #

mkSSet :: Integer -> Sort Source #

isSort :: Term -> Maybe Sort Source #

impossibleTerm :: CallStack -> Term Source #

mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a) Source #

A traversal for the names in a telescope.

mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a Source #

replaceEmptyName :: ArgName -> Tele a -> Tele a Source #

type ListTel' a = [Dom (a, Type)] Source #

Telescope as list.

type ListTel = ListTel' ArgName Source #

telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope Source #

telFromList :: ListTel -> Telescope Source #

Convert a list telescope to a telescope.

listTel :: Lens' Telescope ListTel Source #

Lens to edit a Telescope as a list.

class TelToArgs a where Source #

Drop the types from a telescope.

Methods

telToArgs :: a -> [Arg ArgName] Source #

Instances

Instances details

TelToArgs ListTel Source #
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: ListTel -> [Arg ArgName] Source #
TelToArgs Telescope Source #
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: Telescope -> [Arg ArgName] Source #

class SgTel a where Source #

Constructing a singleton telescope.

Methods

sgTel :: a -> Telescope Source #

Instances

Instances details

SgTel (Dom Type) Source #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom Type -> Telescope Source #
SgTel (Dom (ArgName, Type)) Source #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom (ArgName, Type) -> Telescope Source #
SgTel (ArgName, Dom Type) Source #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: (ArgName, Dom Type) -> Telescope Source #

stripDontCare :: Term -> Term Source #

Removing a topmost DontCare constructor.

class Suggest a where Source #

Suggest a name if available (i.e. name is not "_")

Methods

suggestName :: a -> Maybe String Source #

Instances

Instances details

Suggest Name Source #
Instance details Defined in Agda.Syntax.Internal Methods suggestName :: Name -> Maybe String Source #
Suggest Term Source #
Instance details Defined in Agda.Syntax.Internal Methods suggestName :: Term -> Maybe String Source #
Suggest String Source #
Instance details Defined in Agda.Syntax.Internal Methods suggestName :: String -> Maybe String Source #
Suggest (Abs b) Source #
Instance details Defined in Agda.Syntax.Internal Methods suggestName :: Abs b -> Maybe String Source #

data Suggestion Source #

Constructors

Suggest a => Suggestion a

suggests :: [Suggestion] -> String Source #

unSpine :: Term -> Term Source #

Convert top-level postfix projections into prefix projections.

unSpine' :: (ProjOrigin -> Bool) -> Term -> Term Source #

Convert Proj projection eliminations according to their ProjOrigin into Def projection applications.

hasElims :: Term -> Maybe (Elims -> Term, Elims) Source #

A view distinguishing the neutrals Var, Def, and MetaV which can be projected.

type family TypeOf a Source #

Instances

Instances details

type TypeOf Elims Source #
Instance details Defined in Agda.Syntax.Internal type TypeOf Elims = (Type, Elims -> Term)
type TypeOf Level Source #
Instance details Defined in Agda.Syntax.Internal type TypeOf Level = ()
type TypeOf PlusLevel Source #
Instance details Defined in Agda.Syntax.Internal type TypeOf PlusLevel = ()
type TypeOf Sort Source #
Instance details Defined in Agda.Syntax.Internal type TypeOf Sort = ()
type TypeOf Term Source #
Instance details Defined in Agda.Syntax.Internal type TypeOf Term = Type
type TypeOf Type Source #
Instance details Defined in Agda.Syntax.Internal type TypeOf Type = ()
type TypeOf NLPat Source #
Instance details Defined in Agda.TypeChecking.Monad.Base type TypeOf NLPat = Type
type TypeOf (Arg a) Source #
Instance details Defined in Agda.Syntax.Internal type TypeOf (Arg a) = Dom (TypeOf a)
type TypeOf (Abs Term) Source #
Instance details Defined in Agda.Syntax.Internal type TypeOf (Abs Term) = (Dom Type, Abs Type)
type TypeOf (Abs Type) Source #
Instance details Defined in Agda.Syntax.Internal type TypeOf (Abs Type) = Dom Type
type TypeOf (Dom a) Source #
Instance details Defined in Agda.Syntax.Internal type TypeOf (Dom a) = TypeOf a
type TypeOf [PlusLevel] Source #
Instance details Defined in Agda.Syntax.Internal type TypeOf [PlusLevel] = ()
type TypeOf [Elim' NLPat] Source #
Instance details Defined in Agda.TypeChecking.Monad.Base type TypeOf [Elim' NLPat] = (Type, Elims -> Term)

pDom :: LensHiding a => a -> Doc -> Doc Source #

prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc Source #

module Agda.Syntax.Internal.Blockers

module Agda.Syntax.Internal.Elim

module Agda.Syntax.Internal.Univ

module Agda.Syntax.Abstract.Name

data MetaId Source #

Meta-variable identifiers use the same structure as NameIds.

Constructors

MetaId
Fields metaId :: !Word64 metaModule :: !ModuleNameHash

Instances

Instances details

EncodeTCM MetaId Source #

Instance details

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: MetaId -> TCM Value Source #

Pretty MetaId Source #

Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: MetaId -> Doc Source #

prettyPrec :: Int -> MetaId -> Doc Source #

prettyList :: [MetaId] -> Doc Source #

GetDefs MetaId Source #

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

NamesIn MetaId Source #

Instance details

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
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo MetaId = Expr

Methods

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

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

HasFresh MetaId Source #

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freshLens :: Lens' TCState MetaId Source #

nextFresh' :: MetaId -> MetaId Source #

IsInstantiatedMeta MetaId Source #

Instance details

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool Source #

UnFreezeMeta MetaId Source #

Instance details

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

Methods

fromTerm :: TCM (FromTermFunction MetaId) Source #

PrimTerm MetaId Source #

Instance details

Methods

primTerm :: MetaId -> TCM Term Source #

PrimType MetaId Source #

Instance details

Methods

primType :: MetaId -> TCM Type Source #

ToTerm MetaId Source #

Instance details

Methods

toTerm :: TCM (MetaId -> Term) Source #

toTermR :: TCM (MetaId -> ReduceM Term) Source #

EmbPrj MetaId Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: MetaId -> S Int32 Source #

icod_ :: MetaId -> S Int32 Source #

value :: Int32 -> R MetaId Source #

Unquote MetaId Source #

Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM MetaId Source #

Enum MetaId Source #

Instance details

Defined in Agda.Syntax.Common

Methods

succ :: MetaId -> MetaId #

pred :: MetaId -> MetaId #

toEnum :: Int -> MetaId #

fromEnum :: MetaId -> Int #

enumFrom :: MetaId -> [MetaId] #

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

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

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

Generic MetaId Source #

Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep MetaId
Instance details Defined in Agda.Syntax.Common type Rep MetaId = D1 ('MetaData "MetaId" "Agda.Syntax.Common" "Agda-2.6.4.3-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)))

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

Methods

showsPrec :: Int -> MetaId -> ShowS #

show :: MetaId -> String #

showList :: [MetaId] -> ShowS #

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

Methods

compare :: MetaId -> MetaId -> Ordering #

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

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

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

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

max :: MetaId -> MetaId -> MetaId #

min :: MetaId -> MetaId -> MetaId #

Hashable MetaId Source #

Instance details

Defined in Agda.Syntax.Common

Methods

hashWithSalt :: Int -> MetaId -> Int

hash :: MetaId -> Int

ToJSON MetaId Source #

Instance details

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: MetaId -> Value #

toEncoding :: MetaId -> Encoding #

toJSONList :: [MetaId] -> Value #

toEncodingList :: [MetaId] -> Encoding #

omitField :: MetaId -> Bool #

Singleton MetaId MetaSet Source #

Instance details

Methods

singleton :: MetaId -> MetaSet Source #

Singleton MetaId () Source #

Instance details