Agda.Syntax.Internal

Documentation

type Type = Type' Term

data Term

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

LensSort Sort

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort Sort

getSort :: Sort -> Sort

Suggest Term

Defined in Agda.Syntax.Internal

Methods

suggestName :: Term -> Maybe String

TelToArgs ListTel

Defined in Agda.Syntax.Internal

Methods

telToArgs :: ListTel -> [Arg ArgName]

TelToArgs Telescope

Defined in Agda.Syntax.Internal

Methods

telToArgs :: Telescope -> [Arg ArgName]

TermSize Level

Defined in Agda.Syntax.Internal

Methods

termSize :: Level -> Int

tsize :: Level -> Sum Int

TermSize PlusLevel

Defined in Agda.Syntax.Internal

Methods

termSize :: PlusLevel -> Int

tsize :: PlusLevel -> Sum Int

TermSize Sort

Defined in Agda.Syntax.Internal

Methods

termSize :: Sort -> Int

tsize :: Sort -> Sum Int

TermSize Term

Defined in Agda.Syntax.Internal

Methods

termSize :: Term -> Int

tsize :: Term -> Sum Int

GetDefs Level

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs PlusLevel

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Sort

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Telescope

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Term

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Type

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike Level

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike PlusLevel

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike Sort

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike Term

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike Type

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

AllMetas Level

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas PlusLevel

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Sort

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Term

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Type

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

NamesIn Level

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn PlusLevel

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn Sort

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn Term

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn CompiledClauses

Defined in Agda.Syntax.Internal.Names

Methods

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

KillRange Level

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Level

KillRange PlusLevel

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PlusLevel

KillRange Sort

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Sort

KillRange Substitution

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Substitution

KillRange Term

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Term

KillRange CompiledClauses

Defined in Agda.TypeChecking.CompiledClause

Methods

killRange :: KillRangeT CompiledClauses

Reify Level

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Level

Methods

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

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

Reify Sort

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Sort

Methods

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

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

Reify Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope

Methods

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

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

Reify Term

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Term

Methods

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

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

Reify Type

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Type

Methods

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

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

TerSetSizeDepth ListTel

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: ListTel -> TerM a -> TerM a

TerSetSizeDepth Telescope

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: Telescope -> TerM a -> TerM a

AbsTerm Level

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Level -> Level

AbsTerm PlusLevel

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> PlusLevel -> PlusLevel

AbsTerm Sort

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Sort -> Sort

AbsTerm Term

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Term -> Term

AbsTerm Type

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Type -> Type

EqualSy Level

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Level -> Level -> Bool

EqualSy PlusLevel

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: PlusLevel -> PlusLevel -> Bool

EqualSy Sort

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Sort -> Sort -> Bool

EqualSy Term

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Term -> Term -> Bool

EqualSy Type

Ignores sorts.

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Type -> Type -> Bool

IsPrefixOf Args

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Args -> Args -> Maybe Elims

IsPrefixOf Elims

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Elims -> Elims -> Maybe Elims

IsPrefixOf Term

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Term -> Term -> Maybe Elims

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Telescope -> Telescope

DropArgs Term

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

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Term -> Term

DropArgs CompiledClauses

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.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> CompiledClauses -> CompiledClauses

Free Level

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Sort

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Term

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

PrecomputeFreeVars Level

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Level -> FV Level

PrecomputeFreeVars PlusLevel

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: PlusLevel -> FV PlusLevel

PrecomputeFreeVars Sort

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Sort -> FV Sort

PrecomputeFreeVars Term

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Term -> FV Term

PrecomputeFreeVars Type

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Type -> FV Type

ForceNotFree Level

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree PlusLevel

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree Sort

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree Term

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree Type

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

UsableModality Level

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableModality Sort

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableModality Term

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance Level

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance PlusLevel

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance Sort

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance Term

Defined in Agda.TypeChecking.Irrelevance

Methods

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

NoProjectedVar Term

Defined in Agda.TypeChecking.MetaVars

Methods

noProjectedVar :: Term -> Either ProjectedVar ()

ReduceAndEtaContract Term

Defined in Agda.TypeChecking.MetaVars

Methods

reduceAndEtaContract :: Term -> TCM Term

MentionsMeta Elim

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Elim -> Bool

MentionsMeta Level

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Level -> Bool

MentionsMeta PlusLevel

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> PlusLevel -> Bool

MentionsMeta Sort

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Sort -> Bool

MentionsMeta Term

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Term -> Bool

MentionsMeta Type

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Type -> Bool

AnyRigid Level

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

AnyRigid PlusLevel

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

AnyRigid Sort

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

AnyRigid Term

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

AnyRigid Type

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs Level

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Level -> OccursM Level

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

Occurs PlusLevel

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: PlusLevel -> OccursM PlusLevel

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

Occurs Sort

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Sort -> OccursM Sort

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

Occurs Term

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Term -> OccursM Term

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

Occurs Type

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Type -> OccursM Type

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

AddContext Telescope

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Telescope -> Nat

IsInstantiatedMeta Level

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

IsInstantiatedMeta PlusLevel

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

IsInstantiatedMeta Term

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta Level

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta PlusLevel

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta Sort

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta Term

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta Type

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

IsSizeType Term

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

ComputeOccurrences Level

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Level -> OccM OccurrencesBuilder

ComputeOccurrences PlusLevel

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: PlusLevel -> OccM OccurrencesBuilder

ComputeOccurrences Term

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Term -> OccM OccurrencesBuilder

ComputeOccurrences Type

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Type -> OccM OccurrencesBuilder

PrettyTCM Elim

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Level

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Sort

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Telescope

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Term

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Type

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ContextEntry

Defined in Agda.TypeChecking.Pretty

Methods

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

PrimTerm Type

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Type -> TCM Term

PrimType Type

Defined in Agda.TypeChecking.Primitive

Methods

primType :: Type -> TCM Type

ToTerm Term

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Term -> Term)

toTermR :: TCM (Term -> ReduceM Term)

ToTerm Type

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Type -> Term)

toTermR :: TCM (Type -> ReduceM Term)

Instantiate Level

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Level -> ReduceM Level

Instantiate Sort

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Sort -> ReduceM Sort

Instantiate Term

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Term -> ReduceM Term

InstantiateFull Level

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Level -> ReduceM Level

InstantiateFull PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: PlusLevel -> ReduceM PlusLevel

InstantiateFull Sort

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Sort -> ReduceM Sort

InstantiateFull Substitution

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Substitution -> ReduceM Substitution

InstantiateFull Term

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Term -> ReduceM Term

InstantiateFull CompiledClauses

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses

IsMeta Term

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Term -> Maybe MetaId

Normalise Level

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Level -> ReduceM Level

Normalise PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: PlusLevel -> ReduceM PlusLevel

Normalise Sort

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Sort -> ReduceM Sort

Normalise Term

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Term -> ReduceM Term

Reduce Elim

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Elim -> ReduceM Elim

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

Reduce Level

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Level -> ReduceM Level

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

Reduce PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: PlusLevel -> ReduceM PlusLevel

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

Reduce Sort

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Sort -> ReduceM Sort

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

Reduce Telescope

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Telescope -> ReduceM Telescope

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

Reduce Term

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Term -> ReduceM Term

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

Reduce Type

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Type -> ReduceM Type

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

Simplify Level

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Level -> ReduceM Level

Simplify PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: PlusLevel -> ReduceM PlusLevel

Simplify Sort

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Sort -> ReduceM Sort

Simplify Term

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Term -> ReduceM Term

GetMatchables Term

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Term -> [QName]

EmbPrj Blocked_

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Blocked_ -> S Int32

icod_ :: Blocked_ -> S Int32

value :: Int32 -> R Blocked_

EmbPrj Level

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Level -> S Int32

icod_ :: Level -> S Int32

value :: Int32 -> R Level

EmbPrj NotBlocked

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NotBlocked -> S Int32

icod_ :: NotBlocked -> S Int32

value :: Int32 -> R NotBlocked

EmbPrj PlusLevel

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PlusLevel -> S Int32

icod_ :: PlusLevel -> S Int32

value :: Int32 -> R PlusLevel

EmbPrj Sort

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Sort -> S Int32

icod_ :: Sort -> S Int32

value :: Int32 -> R Sort

EmbPrj Term

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Term -> S Int32

icod_ :: Term -> S Int32

value :: Int32 -> R Term

EmbPrj CompiledClauses

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompiledClauses -> S Int32

icod_ :: CompiledClauses -> S Int32

value :: Int32 -> R CompiledClauses

TeleNoAbs ListTel

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: ListTel -> Term -> Term

TeleNoAbs Telescope

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: Telescope -> Term -> Term

Abstract Sort

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Sort -> Sort

Abstract Telescope

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Telescope -> Telescope

Abstract Term

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Term -> Term

Abstract Type

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Type -> Type

Abstract CompiledClauses

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> CompiledClauses -> CompiledClauses

Apply Sort

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Sort -> Args -> Sort

applyE :: Sort -> Elims -> Sort

Apply Term

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Term -> Args -> Term

applyE :: Term -> Elims -> Term

Apply CompiledClauses

Defined in Agda.TypeChecking.Substitute

Methods

apply :: CompiledClauses -> Args -> CompiledClauses

applyE :: CompiledClauses -> Elims -> CompiledClauses

Subst Term

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Term

Methods

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

DeBruijn Level

Defined in Agda.TypeChecking.Substitute.DeBruijn

Methods

deBruijnVar :: Int -> Level

debruijnNamedVar :: String -> Int -> Level

deBruijnView :: Level -> Maybe Int

DeBruijn PlusLevel

Defined in Agda.TypeChecking.Substitute.DeBruijn

Methods

deBruijnVar :: Int -> PlusLevel

debruijnNamedVar :: String -> Int -> PlusLevel

deBruijnView :: PlusLevel -> Maybe Int

DeBruijn Term

We can substitute Terms for variables.

Defined in Agda.TypeChecking.Substitute.DeBruijn

Methods

deBruijnVar :: Int -> Term

debruijnNamedVar :: String -> Int -> Term

deBruijnView :: Term -> Maybe Int

SynEq Level

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq PlusLevel

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Sort

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Term

Syntactic term equality ignores DontCare stuff.

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Type

Syntactic equality ignores sorts.

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

PiApplyM Term

Defined in Agda.TypeChecking.Telescope

Methods

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

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

Pretty Level

Defined in Agda.Syntax.Internal

Methods

pretty :: Level -> Doc

prettyPrec :: Int -> Level -> Doc

prettyList :: [Level] -> Doc

Pretty PlusLevel

Defined in Agda.Syntax.Internal

Methods

pretty :: PlusLevel -> Doc

prettyPrec :: Int -> PlusLevel -> Doc

prettyList :: [PlusLevel] -> Doc

Pretty Sort

Defined in Agda.Syntax.Internal

Methods

pretty :: Sort -> Doc

prettyPrec :: Int -> Sort -> Doc

prettyList :: [Sort] -> Doc

Pretty Term

Defined in Agda.Syntax.Internal

Methods

pretty :: Term -> Doc

prettyPrec :: Int -> Term -> Doc

prettyList :: [Term] -> Doc

Pretty Type

Defined in Agda.Syntax.Internal

Methods

pretty :: Type -> Doc

prettyPrec :: Int -> Type -> Doc

prettyList :: [Type] -> Doc

Pretty CompiledClauses

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: CompiledClauses -> Doc

prettyPrec :: Int -> CompiledClauses -> Doc

prettyList :: [CompiledClauses] -> Doc

Show Term

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

NFData Level

Defined in Agda.Syntax.Internal

Methods

rnf :: Level -> ()

NFData PlusLevel

Defined in Agda.Syntax.Internal

Methods

rnf :: PlusLevel -> ()

NFData Sort

Defined in Agda.Syntax.Internal

Methods

rnf :: Sort -> ()

NFData Term

Defined in Agda.Syntax.Internal

Methods

rnf :: Term -> ()

NFData Type

Defined in Agda.Syntax.Internal

Methods

rnf :: Type -> ()

Eq Level

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq NotBlocked

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq PlusLevel

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq Sort

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq Substitution

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq Term

Syntactic Term equality, ignores stuff below DontCare and sharing.

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq SingleLevel

Defined in Agda.TypeChecking.Level

Methods

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

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

Ord Level

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.TypeChecking.Substitute

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

NLPatToTerm Nat Term

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

NLPatToTerm NLPSort Sort

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

NLPatToTerm NLPType Type

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

NLPatToTerm NLPat Level

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

NLPatToTerm NLPat Term

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

MonadError Blocked_ NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

throwError :: Blocked_ -> NLM a

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

Match Type NLPat Term

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()

Match () NLPSort Sort

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPSort -> Sort -> NLM ()

Match () NLPType Type

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPType -> Type -> NLM ()

Match () NLPat Level

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPat -> Level -> NLM ()

PatternFrom Type Term NLPat

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> Type -> Term -> TCM NLPat

PatternFrom () Level NLPat

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> () -> Level -> TCM NLPat

PatternFrom () Sort NLPSort

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> () -> Sort -> TCM NLPSort

PatternFrom () Type NLPType

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> () -> Type -> TCM NLPType

Conversion TOM Term (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O)

Conversion TOM Type (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O)

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

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.TypeChecking.Patterns.Internal

Methods

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

Conversion MOT (Exp O) Term

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Term

Conversion MOT (Exp O) Type

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

LensSort a => LensSort (Dom a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort (Dom a)

getSort :: Dom a -> Sort

LensSort (Type' a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort (Type' a)

getSort :: Type' a -> Sort

SgTel (Dom Type)

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom Type -> Telescope

SgTel (Dom (ArgName, Type))

Defined in Agda.Syntax.Internal

Methods

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

GetDefs a => GetDefs (Dom a)

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike a => TermLike (Blocked a)

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike a => TermLike (Dom a)

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

NamesIn a => NamesIn (Type' a)

Defined in Agda.Syntax.Internal.Names

Methods

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

KillRange a => KillRange (Blocked a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Blocked a)

KillRange a => KillRange (Type' a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Type' a)

Reify i => Reify (Dom i)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Dom i)

Methods

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

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

AbsTerm a => AbsTerm (Dom a)

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy a => EqualSy (Dom a)

Ignore the tactic.

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Dom a -> Dom a -> Bool

Free t => Free (Dom t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free t => Free (Type' t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

PrecomputeFreeVars a => PrecomputeFreeVars (Dom a)

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

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

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

UsableModality a => UsableModality (Dom a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance a => UsableModality (Type' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance a => UsableRelevance (Dom a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance a => UsableRelevance (Type' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

MentionsMeta t => MentionsMeta (Dom t)

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

AnyRigid a => AnyRigid (Dom a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs a => Occurs (Dom a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

AddContext (Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Dom Type -> Nat

AddContext (Dom (Name, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Dom (String, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames Telescope)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: KeepNames Telescope -> Nat

IsSizeType a => IsSizeType (Dom a)

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

IsSizeType a => IsSizeType (Type' a)

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

ComputeOccurrences a => ComputeOccurrences (Dom a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Dom a -> OccM OccurrencesBuilder

PrettyTCM (Arg Term)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Arg Type)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (NamedArg Term)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Named_ Term)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM a => PrettyTCM (Blocked a)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Dom Type)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Type' NLPat)

Defined in Agda.TypeChecking.Pretty

Methods

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

ToTerm (Dom Type)

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Dom Type -> Term)

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

Instantiate a => Instantiate (Blocked a)

Defined in Agda.TypeChecking.Reduce

Methods

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

Instantiate t => Instantiate (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Reduce t => Reduce (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Simplify t => Simplify (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

GetMatchables a => GetMatchables (Dom a)

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Dom a -> [QName]

EmbPrj a => EmbPrj (Dom a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Int32

icod_ :: Dom a -> S Int32

value :: Int32 -> R (Dom a)

EmbPrj a => EmbPrj (Type' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Type' a -> S Int32

icod_ :: Type' a -> S Int32

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

Apply t => Apply (Blocked t)

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Blocked t -> Args -> Blocked t

applyE :: Blocked t -> Elims -> Blocked t

Subst a => Subst (Blocked a)

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Blocked a)

Methods

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

SynEq a => SynEq (Dom a)

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

Unquote a => Unquote (Dom a)

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Dom a)

Pretty a => Pretty (Blocked a)

Defined in Agda.Syntax.Internal

Methods

pretty :: Blocked a -> Doc

prettyPrec :: Int -> Blocked a -> Doc

prettyList :: [Blocked a] -> Doc

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

Defined in Agda.Syntax.Internal

Methods

pretty :: Tele (Dom a) -> Doc

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

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

NFData e => NFData (Dom e)

Defined in Agda.Syntax.Internal

Methods

rnf :: Dom e -> ()

Eq t => Eq (Blocked t)

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq a => Eq (Type' a)

Syntactic Type equality, ignores sort annotations.

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Ord a => Ord (Dom a)

Defined in Agda.TypeChecking.Substitute

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)

Defined in Agda.TypeChecking.Substitute

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

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

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Dom a -> Dom b

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

SgTel (ArgName, Dom Type)

Defined in Agda.Syntax.Internal

Methods

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

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Dom r, Name)

Methods

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

AddContext (Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 (Arg Name), Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 (NamedArg Name), Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 (WithHiding Name), Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Text, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([Arg Name], Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([NamedArg Name], Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([WithHiding Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

PatternFrom (Type, Term) Elims [Elim' NLPat]

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]

Match (Type, Elims -> Term) [Elim' NLPat] Elims

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> (Type, Elims -> Term) -> [Elim' NLPat] -> Elims -> NLM ()

type ReifiesTo Level

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Level = Expr

type ReifiesTo Sort

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Sort = Expr

type ReifiesTo Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Telescope = Telescope

type ReifiesTo Term

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Term = Expr

type ReifiesTo Type

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Type = Type

type SubstArg Term

Defined in Agda.TypeChecking.Substitute

type SubstArg Term = Term

type ReifiesTo (Dom i)

Defined in Agda.Syntax.Translation.InternalToAbstract

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

type SubstArg (Blocked a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Blocked a) = SubstArg a

type AbsOfRef (Dom r, Name)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Dom r, Name) = TypedBinding

data Clause

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

GetDefs Clause

Defined in Agda.Syntax.Internal.Defs

Methods

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

NamesIn Clause

Defined in Agda.Syntax.Internal.Names

Methods

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

FunArity Clause

Get the number of initial Apply patterns in a clause.

Defined in Agda.Syntax.Internal.Pattern

Methods

funArity :: Clause -> Int

HasRange Clause

Defined in Agda.Syntax.Internal

Methods

getRange :: Clause -> Range

KillRange Clause

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Clause

DropArgs Clause

NOTE: does not work for recursive functions.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Clause -> Clause

DropArgs FunctionInverse

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> FunctionInverse -> FunctionInverse

Free Clause

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Occurs Clause

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Clause -> OccursM Clause

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

ComputeOccurrences Clause

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Clause -> OccM OccurrencesBuilder

PrettyTCM Clause

Defined in Agda.TypeChecking.Pretty

Methods

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

NormaliseProjP Clause

Defined in Agda.TypeChecking.Records

Methods

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

InstantiateFull Clause

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Clause -> ReduceM Clause

InstantiateFull FunctionInverse

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse

EmbPrj Clause

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Clause -> S Int32

icod_ :: Clause -> S Int32

value :: Int32 -> R Clause

Abstract Clause

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Clause -> Clause

Abstract FunctionInverse

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> FunctionInverse -> FunctionInverse

Apply Clause

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Clause -> Args -> Clause

applyE :: Clause -> Elims -> Clause

Apply FunctionInverse

Defined in Agda.TypeChecking.Substitute

Methods

apply :: FunctionInverse -> Args -> FunctionInverse

applyE :: FunctionInverse -> Elims -> FunctionInverse

Null Clause

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

Defined in Agda.Syntax.Internal

Methods

empty :: Clause

null :: Clause -> Bool

Pretty Clause

Defined in Agda.Syntax.Internal

Methods

pretty :: Clause -> Doc

prettyPrec :: Int -> Clause -> Doc

prettyList :: [Clause] -> Doc

Generic Clause

Defined in Agda.Syntax.Internal

Associated Types

type Rep Clause :: Type -> Type

Methods

from :: Clause -> Rep Clause x

to :: Rep Clause x -> Clause

Show Clause

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Clause -> ShowS

show :: Clause -> String

showList :: [Clause] -> ShowS

NFData Clause

Defined in Agda.Syntax.Internal

Methods

rnf :: Clause -> ()

Conversion TOM Clause (Maybe ([Pat O], MExp O))

Defined in Agda.Auto.Convert

Methods

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

Conversion TOM [Clause] [([Pat O], MExp O)]

Defined in Agda.Auto.Convert

Methods

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

FunArity [Clause]

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

Defined in Agda.Syntax.Internal.Pattern

Methods

funArity :: [Clause] -> Int

Reify (QNamed Clause)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (QNamed Clause)

Methods

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

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

PrettyTCM (QNamed Clause)

Defined in Agda.TypeChecking.Pretty

Methods

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

type Rep Clause

Defined in Agda.Syntax.Internal

type Rep Clause = D1 ('MetaData "Clause" "Agda.Syntax.Internal" "Agda-2.6.2.2.20230105-inplace" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'True) (((S1 ('MetaSel ('Just "clauseLHSRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Just "clauseFullRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "clauseTel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope))) :*: (S1 ('MetaSel ('Just "namedClausePats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NAPs) :*: (S1 ('MetaSel ('Just "clauseBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Term)) :*: S1 ('MetaSel ('Just "clauseType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Arg Type)))))) :*: ((S1 ('MetaSel ('Just "clauseCatchall") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "clauseExact") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)) :*: S1 ('MetaSel ('Just "clauseRecursive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)))) :*: (S1 ('MetaSel ('Just "clauseUnreachable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)) :*: (S1 ('MetaSel ('Just "clauseEllipsis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExpandedEllipsis) :*: S1 ('MetaSel ('Just "clauseWhereModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModuleName)))))))

type ReifiesTo (QNamed Clause)

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (QNamed Clause) = Clause

type Telescope = Tele (Dom Type)

data Dom' t e

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

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

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

TelToArgs ListTel

Defined in Agda.Syntax.Internal

Methods

telToArgs :: ListTel -> [Arg ArgName]

TelToArgs Telescope

Defined in Agda.Syntax.Internal

Methods

telToArgs :: Telescope -> [Arg ArgName]

GetDefs Telescope

Defined in Agda.Syntax.Internal.Defs

Methods

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

Reify Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope

Methods

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

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

TerSetSizeDepth ListTel

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: ListTel -> TerM a -> TerM a

TerSetSizeDepth Telescope

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: Telescope -> TerM a -> TerM a

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Telescope -> Telescope

AddContext Telescope

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Telescope -> Nat

PrettyTCM Telescope

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ContextEntry

Defined in Agda.TypeChecking.Pretty

Methods

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

Reduce Telescope

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Telescope -> ReduceM Telescope

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

TeleNoAbs ListTel

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: ListTel -> Term -> Term

TeleNoAbs Telescope

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: Telescope -> Term -> Term

Abstract Telescope

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Telescope -> Telescope

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

LensSort a => LensSort (Dom a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort (Dom a)

getSort :: Dom a -> Sort

SgTel (Dom Type)

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom Type -> Telescope

SgTel (Dom (ArgName, Type))

Defined in Agda.Syntax.Internal

Methods

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

GetDefs a => GetDefs (Dom a)

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike a => TermLike (Dom a)

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

Reify i => Reify (Dom i)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Dom i)

Methods

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

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

AbsTerm a => AbsTerm (Dom a)

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy a => EqualSy (Dom a)

Ignore the tactic.

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Dom a -> Dom a -> Bool

Free t => Free (Dom t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

PrecomputeFreeVars a => PrecomputeFreeVars (Dom a)

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

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

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

UsableModality a => UsableModality (Dom a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance a => UsableRelevance (Dom a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

MentionsMeta t => MentionsMeta (Dom t)

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

AnyRigid a => AnyRigid (Dom a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs a => Occurs (Dom a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

AddContext (Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Dom Type -> Nat

AddContext (Dom (Name, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Dom (String, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames Telescope)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: KeepNames Telescope -> Nat

IsSizeType a => IsSizeType (Dom a)

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

ComputeOccurrences a => ComputeOccurrences (Dom a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Dom a -> OccM OccurrencesBuilder

PrettyTCM (Dom Type)

Defined in Agda.TypeChecking.Pretty

Methods

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

ToTerm (Dom Type)

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Dom Type -> Term)

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

Normalise t => Normalise (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Reduce t => Reduce (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Simplify t => Simplify (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

GetMatchables a => GetMatchables (Dom a)

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Dom a -> [QName]

EmbPrj a => EmbPrj (Dom a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Int32

icod_ :: Dom a -> S Int32

value :: Int32 -> R (Dom a)

SynEq a => SynEq (Dom a)

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

Unquote a => Unquote (Dom a)

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Dom a)

Decoration (Dom' t)

Defined in Agda.Syntax.Internal

Methods

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

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

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

Defined in Agda.Syntax.Internal

Methods

pretty :: Tele (Dom a) -> Doc

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

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

Foldable (Dom' t)

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)

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)

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)

Defined in Agda.Syntax.Internal

Methods

rnf :: Dom e -> ()

Ord a => Ord (Dom a)

Defined in Agda.TypeChecking.Substitute

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)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Dom a -> Dom b

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

LensAnnotation (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getAnnotation :: Dom' t e -> Annotation

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

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

LensArgInfo (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getArgInfo :: Dom' t e -> ArgInfo

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

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

LensCohesion (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getCohesion :: Dom' t e -> Cohesion

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

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

LensFreeVariables (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getFreeVariables :: Dom' t e -> FreeVariables

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

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

LensHiding (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getHiding :: Dom' t e -> Hiding

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

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

LensModality (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getModality :: Dom' t e -> Modality

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

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

LensNamed (Dom' t e)

Defined in Agda.Syntax.Internal

Associated Types

type NameOf (Dom' t e)

Methods

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

LensOrigin (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getOrigin :: Dom' t e -> Origin

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

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

LensQuantity (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getQuantity :: Dom' t e -> Quantity

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

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

LensRelevance (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getRelevance :: Dom' t e -> Relevance

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

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

SgTel (ArgName, Dom Type)

Defined in Agda.Syntax.Internal

Methods

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

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

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

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

Defined in Agda.Syntax.Internal.Names

Methods

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

HasRange a => HasRange (Dom' t a)

Defined in Agda.Syntax.Internal

Methods

getRange :: Dom' t a -> Range

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

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Dom' t a)

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Dom r, Name)

Methods

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

AddContext (Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 (WithHiding Name), Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Text, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([WithHiding Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Dom' a b)

Methods

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

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

Defined in Agda.Syntax.Internal

Methods

pretty :: Dom' t e -> Doc

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

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

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

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)

Ignores Origin and FreeVariables and tactic.

Defined in Agda.Syntax.Internal

Methods

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

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

type ReifiesTo Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Telescope = Telescope

type ReifiesTo (Dom i)

Defined in Agda.Syntax.Translation.InternalToAbstract

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

type NameOf (Dom' t e)

Defined in Agda.Syntax.Internal

type NameOf (Dom' t e) = NamedName

type AbsOfRef (Dom r, Name)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Dom r, Name) = TypedBinding

type SubstArg (Dom' a b)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Dom' a b) = SubstArg a

type Pattern

Arguments

 = Pattern' PatVarName

The PatVarName is a name suggestion.

type Level = Level' Term

type Substitution = Substitution' Term

type Dom = Dom' Term

type Elim = Elim' Term

type Sort = Sort' Term

data DataOrRecord

Constructors

IsData

IsRecord PatternOrCopattern

Instances

KillRange DataOrRecord

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT DataOrRecord

EmbPrj DataOrRecord

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DataOrRecord -> S Int32

icod_ :: DataOrRecord -> S Int32

value :: Int32 -> R DataOrRecord

Generic DataOrRecord

Defined in Agda.Syntax.Internal

Associated Types

type Rep DataOrRecord :: Type -> Type

Methods

from :: DataOrRecord -> Rep DataOrRecord x

to :: Rep DataOrRecord x -> DataOrRecord

Show DataOrRecord

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> DataOrRecord -> ShowS

show :: DataOrRecord -> String

showList :: [DataOrRecord] -> ShowS

NFData DataOrRecord

Defined in Agda.Syntax.Internal

Methods

rnf :: DataOrRecord -> ()

Eq DataOrRecord

Defined in Agda.Syntax.Internal

Methods

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

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

type Rep DataOrRecord

Defined in Agda.Syntax.Internal

type Rep DataOrRecord = D1 ('MetaData "DataOrRecord" "Agda.Syntax.Internal" "Agda-2.6.2.2.20230105-inplace" 'False) (C1 ('MetaCons "IsData" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternOrCopattern)))

type Args = [Arg Term]

Type of argument lists.

data Substitution' a

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

KillRange Substitution

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Substitution

InstantiateFull Substitution

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Substitution -> ReduceM Substitution

Foldable Substitution'

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'

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'

Defined in Agda.Syntax.Internal

Methods

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

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

Eq Substitution

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Ord Substitution

Defined in Agda.TypeChecking.Substitute

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

TermSize a => TermSize (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

termSize :: Substitution' a -> Int

tsize :: Substitution' a -> Sum Int

NamesIn a => NamesIn (Substitution' a)

Defined in Agda.Syntax.Internal.Names

Methods

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

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

Defined in Agda.TypeChecking.Pretty

Methods

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

EmbPrj a => EmbPrj (Substitution' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Substitution' a -> S Int32

icod_ :: Substitution' a -> S Int32

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

EndoSubst a => Subst (Substitution' a)

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Substitution' a)

Methods

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

Null (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

empty :: Substitution' a

null :: Substitution' a -> Bool

Pretty a => Pretty (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

pretty :: Substitution' a -> Doc

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

prettyList :: [Substitution' a] -> Doc

Generic (Substitution' a)

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Substitution' a) :: Type -> Type

Methods

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

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

Show a => Show (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

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

show :: Substitution' a -> String

showList :: [Substitution' a] -> ShowS

NFData a => NFData (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

rnf :: Substitution' a -> ()

type SubstArg (Substitution' a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Substitution' a) = a

type Rep (Substitution' a)

Defined in Agda.Syntax.Internal

type Rep (Substitution' a) = D1 ('MetaData "Substitution'" "Agda.Syntax.Internal" "Agda-2.6.2.2.20230105-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 Abs a

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

Decoration Abs

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Abs

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

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

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)

Defined in Agda.Auto.Convert

Methods

convert :: Abs0 a -> MOT (Abs b)

Suggest (Abs b)

Defined in Agda.Syntax.Internal

Methods

suggestName :: Abs b -> Maybe String

GetDefs a => GetDefs (Abs a)

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike a => TermLike (Abs a)

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

NamesIn a => NamesIn (Abs a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Abs a -> m

KillRange a => KillRange (Abs a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Abs a)

(Free i, Reify i) => Reify (Abs i)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Abs i)

Methods

reify :: MonadReify m => Abs i -> m (ReifiesTo (Abs i))

reifyWhen :: MonadReify m => Bool -> Abs i -> m (ReifiesTo (Abs i))

(TermSubst a, AbsTerm a) => AbsTerm (Abs a)

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Abs a -> Abs a

(Subst a, EqualSy a) => EqualSy (Abs a)

Ignores absName.

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Abs a -> Abs a -> Bool

Free t => Free (Abs t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Abs t -> FreeM a c

PrecomputeFreeVars a => PrecomputeFreeVars (Abs a)

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

(Reduce a, ForceNotFree a) => ForceNotFree (Abs a)

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

(Subst a, UsableRelevance a) => UsableRelevance (Abs a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

MentionsMeta t => MentionsMeta (Abs t)

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Abs t -> Bool

(Subst a, AnyRigid a) => AnyRigid (Abs a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Abs a -> tcm Bool

(Occurs a, Subst a) => Occurs (Abs a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Abs a -> OccursM (Abs a)

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

IsInstantiatedMeta a => IsInstantiatedMeta (Abs a)

Does not worry about raising.

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Abs a -> m Bool

UnFreezeMeta a => UnFreezeMeta (Abs a)

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Abs a -> m ()

ComputeOccurrences a => ComputeOccurrences (Abs a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Abs a -> OccM OccurrencesBuilder

Instantiate t => Instantiate (Abs t)

Defined in Agda.TypeChecking.Reduce

Methods

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

(Subst a, InstantiateFull a) => InstantiateFull (Abs a)

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Abs a -> ReduceM (Abs a)

(Subst a, Normalise a) => Normalise (Abs a)

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Abs a -> ReduceM (Abs a)

(Subst a, Reduce a) => Reduce (Abs a)

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Abs a -> ReduceM (Abs a)

reduceB' :: Abs a -> ReduceM (Blocked (Abs a))

(Subst a, Simplify a) => Simplify (Abs a)

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Abs a -> ReduceM (Abs a)

GetMatchables a => GetMatchables (Abs a)

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Abs a -> [QName]

NLPatVars a => NLPatVars (Abs a)

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatVarsUnder :: Int -> Abs a -> IntSet

nlPatVars :: Abs a -> IntSet

EmbPrj a => EmbPrj (Abs a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Abs a -> S Int32

icod_ :: Abs a -> S Int32

value :: Int32 -> R (Abs a)

Subst a => Subst (Abs a)

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Abs a)

Methods

applySubst :: Substitution' (SubstArg (Abs a)) -> Abs a -> Abs a

(Subst a, SynEq a) => SynEq (Abs a)

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

Pretty t => Pretty (Abs t)

Defined in Agda.Syntax.Internal

Methods

pretty :: Abs t -> Doc

prettyPrec :: Int -> Abs t -> Doc

prettyList :: [Abs t] -> Doc

Sized a => Sized (Abs a)

Defined in Agda.Syntax.Internal

Methods

size :: Abs a -> Int

Generic (Abs a)

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Abs a) :: Type -> Type

Methods

from :: Abs a -> Rep (Abs a) x

to :: Rep (Abs a) x -> Abs a

Show a => Show (Abs a)

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Abs a -> ShowS

show :: Abs a -> String

showList :: [Abs a] -> ShowS

NFData a => NFData (Abs a)

Defined in Agda.Syntax.Internal

Methods

rnf :: Abs a -> ()

(Subst a, Eq a) => Eq (Abs a)

Equality of binders relies on weakening which is a special case of renaming which is a special case of substitution.

Defined in Agda.TypeChecking.Substitute

Methods

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

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

(Subst a, Ord a) => Ord (Abs a)

Defined in Agda.TypeChecking.Substitute

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)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Abs a -> Abs b

NLPatToTerm p a => NLPatToTerm (Abs p) (Abs a)

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatToTerm :: PureTCM m => Abs p -> m (Abs a)

type ReifiesTo (Abs i)

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Abs i) = (Name, ReifiesTo i)

type SubstArg (Abs a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Abs a) = SubstArg a

type Rep (Abs a)

Defined in Agda.Syntax.Internal

type Rep (Abs a) = D1 ('MetaData "Abs" "Agda.Syntax.Internal" "Agda-2.6.2.2.20230105-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

Minimal complete definition

lensSort

Methods

lensSort :: Lens' Sort a

getSort :: a -> Sort

Instances

LensSort Sort

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort Sort

getSort :: Sort -> Sort

LensSort a => LensSort (Arg a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort (Arg a)

getSort :: Arg a -> Sort

LensSort a => LensSort (Dom a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort (Dom a)

getSort :: Dom a -> Sort

LensSort (Type' a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort (Type' a)

getSort :: Type' a -> Sort

type Elims

Arguments

 = [Elim]

eliminations ordered left-to-right.

type Blocked = Blocked' Term

class TermSize a where

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

tsize :: a -> Sum Int

Instances

TermSize Level

Defined in Agda.Syntax.Internal

Methods

termSize :: Level -> Int

tsize :: Level -> Sum Int

TermSize PlusLevel

Defined in Agda.Syntax.Internal

Methods

termSize :: PlusLevel -> Int

tsize :: PlusLevel -> Sum Int

TermSize Sort

Defined in Agda.Syntax.Internal

Methods

termSize :: Sort -> Int

tsize :: Sort -> Sum Int

TermSize Term

Defined in Agda.Syntax.Internal

Methods

termSize :: Term -> Int

tsize :: Term -> Sum Int

TermSize a => TermSize (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

termSize :: Substitution' a -> Int

tsize :: Substitution' a -> Sum Int

(Foldable t, TermSize a) => TermSize (t a)

Defined in Agda.Syntax.Internal

Methods

termSize :: t a -> Int

tsize :: t a -> Sum Int

data Pattern' x

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

UsableSizeVars DeBruijnPattern

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: DeBruijnPattern -> TerM VarSet

UsableSizeVars MaskedDeBruijnPatterns

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet

Reduce DeBruijnPattern

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: DeBruijnPattern -> ReduceM DeBruijnPattern

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

Subst DeBruijnPattern

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg DeBruijnPattern

Methods

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

Subst Pattern

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Pattern

Methods

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

Subst SplitPattern

Defined in Agda.TypeChecking.Coverage.Match

Associated Types

type SubstArg SplitPattern

Methods

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

Foldable Pattern'

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'

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'

Defined in Agda.Syntax.Internal

Methods

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

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

LabelPatVars Pattern DeBruijnPattern

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel DeBruijnPattern

Methods

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

unlabelPatVars :: DeBruijnPattern -> Pattern

MapNamedArgPattern a (NamedArg (Pattern' a))

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

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

Defined in Agda.Syntax.Internal.Pattern

Methods

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

PatternLike a (Pattern' a)

Defined in Agda.Syntax.Internal.Pattern

Methods

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

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

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

Defined in Agda.TypeChecking.Patterns.Internal

Methods

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

Conversion TOM (Arg Pattern) (Pat O)

Defined in Agda.Auto.Convert

Methods

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

IsProjP (Pattern' a)

Defined in Agda.Syntax.Internal

Methods

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

PatternVars (Arg (Pattern' a))

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (Arg (Pattern' a))

Methods

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

PatternVars (NamedArg (Pattern' a))

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (NamedArg (Pattern' a))

Methods

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

NamesIn (Pattern' a)

Defined in Agda.Syntax.Internal.Names

Methods

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

CountPatternVars (Pattern' x)

Defined in Agda.Syntax.Internal.Pattern

Methods

countPatternVars :: Pattern' x -> Int

PatternVarModalities (Pattern' x)

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar (Pattern' x)

Methods

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

KillRange a => KillRange (Pattern' a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Pattern' a)

UsableSizeVars (Masked DeBruijnPattern)

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet

UsableSizeVars [DeBruijnPattern]

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: [DeBruijnPattern] -> TerM VarSet

PrettyTCM a => PrettyTCM (Pattern' a)

Defined in Agda.TypeChecking.Pretty

Methods

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

NormaliseProjP (Pattern' x)

Defined in Agda.TypeChecking.Records

Methods

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

InstantiateFull a => InstantiateFull (Pattern' a)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise a => Normalise (Pattern' a)

Defined in Agda.TypeChecking.Reduce

Methods

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

IsFlexiblePattern (Pattern' a)

Defined in Agda.TypeChecking.Rules.LHS

Methods

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

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

EmbPrj a => EmbPrj (Pattern' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Pattern' a -> S Int32

icod_ :: Pattern' a -> S Int32

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

Apply [NamedArg (Pattern' a)]

Make sure we only drop variable patterns.

Defined in Agda.TypeChecking.Substitute

Methods

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

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

DeBruijn a => DeBruijn (Pattern' a)

Defined in Agda.TypeChecking.Substitute

Methods

deBruijnVar :: Int -> Pattern' a

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

deBruijnView :: Pattern' a -> Maybe Int

DeBruijn a => IApplyVars (Pattern' a)

Defined in Agda.TypeChecking.Telescope.Path

Methods

iApplyVars :: Pattern' a -> [Int]

Pretty a => Pretty (Pattern' a)

Defined in Agda.Syntax.Internal

Methods

pretty :: Pattern' a -> Doc

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

prettyList :: [Pattern' a] -> Doc

Generic (Pattern' x)

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Pattern' x) :: Type -> Type

Methods

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

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

Show x => Show (Pattern' x)

Defined in Agda.Syntax.Internal

Methods

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

show :: Pattern' x -> String

showList :: [Pattern' x] -> ShowS

NFData x => NFData (Pattern' x)

Defined in Agda.Syntax.Internal

Methods

rnf :: Pattern' x -> ()

Eq a => Eq (Pattern' a)

Defined in Agda.TypeChecking.Substitute

Methods

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

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

ToNLPat (Arg DeBruijnPattern) (Elim' NLPat)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Arg DeBruijnPattern -> Elim' NLPat

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat

type PatVarLabel DeBruijnPattern

Defined in Agda.Syntax.Internal.Pattern

type PatVarLabel DeBruijnPattern = Int

type SubstArg DeBruijnPattern

Defined in Agda.TypeChecking.Substitute

type SubstArg DeBruijnPattern = DeBruijnPattern

type SubstArg Pattern

Defined in Agda.TypeChecking.Substitute

type SubstArg Pattern = Term

type SubstArg SplitPattern

Defined in Agda.TypeChecking.Coverage.Match

type SubstArg SplitPattern = SplitPattern

type PatternVarOut (Arg (Pattern' a))

Defined in Agda.Syntax.Internal

type PatternVarOut (Arg (Pattern' a)) = a

type PatternVarOut (NamedArg (Pattern' a))

Defined in Agda.Syntax.Internal

type PatternVarOut (NamedArg (Pattern' a)) = a

type PatVar (Pattern' x)

Defined in Agda.Syntax.Internal.Pattern

type PatVar (Pattern' x) = x

type Rep (Pattern' x)

Defined in Agda.Syntax.Internal

type Rep (Pattern' x) = D1 ('MetaData "Pattern'" "Agda.Syntax.Internal" "Agda-2.6.2.2.20230105-inplace" 'False) ((C1 ('MetaCons "VarP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 x)) :+: (C1 ('MetaCons "DotP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "ConP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConHead) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' x)]))))) :+: ((C1 ('MetaCons "LitP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "ProjP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "IApplyP" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 x))) :+: C1 ('MetaCons "DefP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' x)]))))))

type NotBlocked = NotBlocked' Term

type NamedArgs = [NamedArg Term]

data ConHead

Store the names of the record fields in the constructor. This allows reduction of projection redexes outside of TCM. For instance, during substitution and application.

Constructors

ConHead

Fields

• conName :: QName

  The name of the constructor.

• conDataRecord :: DataOrRecord

  Data or record constructor?

• conInductive :: Induction

  Record constructors can be coinductive.

• conFields :: [Arg QName]

  The name of the record fields. Arg is stored since the info in the constructor args might not be accurate because of subtyping (issue #2170).

Instances

LensConName ConHead

Defined in Agda.Syntax.Internal

Methods

getConName :: ConHead -> QName

setConName :: QName -> ConHead -> ConHead

mapConName :: (QName -> QName) -> ConHead -> ConHead

NamesIn ConHead

Defined in Agda.Syntax.Internal.Names

Methods

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

HasRange ConHead

Defined in Agda.Syntax.Internal

Methods

getRange :: ConHead -> Range

KillRange ConHead

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT ConHead

SetRange ConHead

Defined in Agda.Syntax.Internal

Methods

setRange :: Range -> ConHead -> ConHead

PrettyTCM ConHead

Defined in Agda.TypeChecking.Pretty

Methods

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

InstantiateFull ConHead

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ConHead -> ReduceM ConHead

EmbPrj ConHead

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ConHead -> S Int32

icod_ :: ConHead -> S Int32

value :: Int32 -> R ConHead

Pretty ConHead

Defined in Agda.Syntax.Internal

Methods

pretty :: ConHead -> Doc

prettyPrec :: Int -> ConHead -> Doc

prettyList :: [ConHead] -> Doc

Generic ConHead

Defined in Agda.Syntax.Internal

Associated Types

type Rep ConHead :: Type -> Type

Methods

from :: ConHead -> Rep ConHead x

to :: Rep ConHead x -> ConHead

Show ConHead

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> ConHead -> ShowS

show :: ConHead -> String

showList :: [ConHead] -> ShowS

NFData ConHead

Defined in Agda.Syntax.Internal

Methods

rnf :: ConHead -> ()

Eq ConHead

Defined in Agda.Syntax.Internal

Methods

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

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

Ord ConHead

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

Defined in Agda.Syntax.Internal

type Rep ConHead = D1 ('MetaData "ConHead" "Agda.Syntax.Internal" "Agda-2.6.2.2.20230105-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]))))

class LensConName a where

Minimal complete definition

getConName

Methods

getConName :: a -> QName

setConName :: QName -> a -> a

mapConName :: (QName -> QName) -> a -> a

Instances

LensConName ConHead

Defined in Agda.Syntax.Internal

Methods

getConName :: ConHead -> QName

setConName :: QName -> ConHead -> ConHead

mapConName :: (QName -> QName) -> ConHead -> ConHead

type ConInfo = ConOrigin

data Type'' t a

Types are terms with a sort annotation.

Constructors

El

Fields

• _getSort :: Sort' t
• unEl :: a

Instances

TelToArgs ListTel

Defined in Agda.Syntax.Internal

Methods

telToArgs :: ListTel -> [Arg ArgName]

TelToArgs Telescope

Defined in Agda.Syntax.Internal

Methods

telToArgs :: Telescope -> [Arg ArgName]

GetDefs Telescope

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Type

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike Type

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

AllMetas Type

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

Reify Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope

Methods

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

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

Reify Type

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Type

Methods

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

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

TerSetSizeDepth ListTel

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: ListTel -> TerM a -> TerM a

TerSetSizeDepth Telescope

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: Telescope -> TerM a -> TerM a

AbsTerm Type

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Type -> Type

EqualSy Type

Ignores sorts.

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Type -> Type -> Bool

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Telescope -> Telescope

PrecomputeFreeVars Type

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Type -> FV Type

ForceNotFree Type

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

MentionsMeta Type

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Type -> Bool

AnyRigid Type

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs Type

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Type -> OccursM Type

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

AddContext Telescope

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Telescope -> Nat

UnFreezeMeta Type

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

ComputeOccurrences Type

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Type -> OccM OccurrencesBuilder

PrettyTCM Telescope

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Type

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ContextEntry

Defined in Agda.TypeChecking.Pretty

Methods

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

PrimTerm Type

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Type -> TCM Term

PrimType Type

Defined in Agda.TypeChecking.Primitive

Methods

primType :: Type -> TCM Type

ToTerm Type

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Type -> Term)

toTermR :: TCM (Type -> ReduceM Term)

Reduce Telescope

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Telescope -> ReduceM Telescope

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

Reduce Type

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Type -> ReduceM Type

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

TeleNoAbs ListTel

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: ListTel -> Term -> Term

TeleNoAbs Telescope

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: Telescope -> Term -> Term

Abstract Telescope

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Telescope -> Telescope

Abstract Type

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Type -> Type

SynEq Type

Syntactic equality ignores sorts.

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

Pretty Type

Defined in Agda.Syntax.Internal

Methods

pretty :: Type -> Doc

prettyPrec :: Int -> Type -> Doc

prettyList :: [Type] -> Doc

NFData Type

Defined in Agda.Syntax.Internal

Methods

rnf :: Type -> ()

NLPatToTerm NLPType Type

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

Match Type NLPat Term

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()

Match () NLPType Type

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPType -> Type -> NLM ()

PatternFrom Type Term NLPat

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> Type -> Term -> TCM NLPat

PatternFrom () Type NLPType

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> () -> Type -> TCM NLPType

Conversion TOM Type (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O)

Conversion MOT (Exp O) Type

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type

LensSort (Type' a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort (Type' a)

getSort :: Type' a -> Sort

SgTel (Dom Type)

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom Type -> Telescope

SgTel (Dom (ArgName, Type))

Defined in Agda.Syntax.Internal

Methods

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

NamesIn a => NamesIn (Type' a)

Defined in Agda.Syntax.Internal.Names

Methods

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

KillRange a => KillRange (Type' a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Type' a)

Free t => Free (Type' t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

UsableRelevance a => UsableModality (Type' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance a => UsableRelevance (Type' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

AddContext (Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Dom Type -> Nat

AddContext (Dom (Name, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Dom (String, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames Telescope)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: KeepNames Telescope -> Nat

IsSizeType a => IsSizeType (Type' a)

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

PrettyTCM (Arg Type)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Dom Type)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Type' NLPat)

Defined in Agda.TypeChecking.Pretty

Methods

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

ToTerm (Dom Type)

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Dom Type -> Term)

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

Instantiate t => Instantiate (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

EmbPrj a => EmbPrj (Type' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Type' a -> S Int32

icod_ :: Type' a -> S Int32

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

Decoration (Type'' t)

Defined in Agda.Syntax.Internal

Methods

traverseF :: Functor m => (a -> m b) -> Type'' t a -> m (Type'' t b)

distributeF :: Functor m => Type'' t (m a) -> m (Type'' t a)

Foldable (Type'' t)

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)

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)

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)

Syntactic Type equality, ignores sort annotations.

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Ord a => Ord (Type' a)

Defined in Agda.TypeChecking.Substitute

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)

Defined in Agda.Syntax.Internal

Methods

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

AddContext (Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 (Arg Name), Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 (NamedArg Name), Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 (WithHiding Name), Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Text, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([Arg Name], Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([NamedArg Name], Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([WithHiding Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

IsMeta a => IsMeta (Type'' t a)

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Type'' t a -> Maybe MetaId

(Coercible a Term, Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Type'' a b)

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Type'' a b)

Methods

applySubst :: Substitution' (SubstArg (Type'' a b)) -> Type'' a b -> Type'' a b

(Show t, Show a) => Show (Type'' t a)

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Type'' t a -> ShowS

show :: Type'' t a -> String

showList :: [Type'' t a] -> ShowS

PatternFrom (Type, Term) Elims [Elim' NLPat]

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]

Match (Type, Elims -> Term) [Elim' NLPat] Elims

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> (Type, Elims -> Term) -> [Elim' NLPat] -> Elims -> NLM ()

type ReifiesTo Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Telescope = Telescope

type ReifiesTo Type

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Type = Type

type SubstArg (Type'' a b)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Type'' a b) = SubstArg a

data Sort' t

Sorts.

Constructors

Type (Level' t)

Set ℓ.

Prop (Level' t)

Prop ℓ.

Inf IsFibrant !Integer

Setωᵢ.

SSet (Level' t)

SSet ℓ.

SizeUniv

SizeUniv, a sort inhabited by type Size.

LockUniv

LockUniv, a sort for locks.

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

LensSort Sort

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort Sort

getSort :: Sort -> Sort

TermSize Sort

Defined in Agda.Syntax.Internal

Methods

termSize :: Sort -> Int

tsize :: Sort -> Sum Int

GetDefs Sort

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike Sort

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

AllMetas Sort

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

NamesIn Sort

Defined in Agda.Syntax.Internal.Names

Methods

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

KillRange Sort

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Sort

Reify Sort

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Sort

Methods

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

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

AbsTerm Sort

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Sort -> Sort

EqualSy Sort

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Sort -> Sort -> Bool

Free Sort

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

PrecomputeFreeVars Sort

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Sort -> FV Sort

ForceNotFree Sort

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

UsableModality Sort

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance Sort

Defined in Agda.TypeChecking.Irrelevance

Methods

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

MentionsMeta Sort

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Sort -> Bool

AnyRigid Sort

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs Sort

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Sort -> OccursM Sort

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

UnFreezeMeta Sort

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

PrettyTCM Sort

Defined in Agda.TypeChecking.Pretty

Methods

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

Instantiate Sort

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Sort -> ReduceM Sort

InstantiateFull Sort

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Sort -> ReduceM Sort

Normalise Sort

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Sort -> ReduceM Sort

Reduce Sort

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Sort -> ReduceM Sort

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

Simplify Sort

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Sort -> ReduceM Sort

EmbPrj Sort

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Sort -> S Int32

icod_ :: Sort -> S Int32

value :: Int32 -> R Sort

Abstract Sort

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Sort -> Sort

Apply Sort

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Sort -> Args -> Sort

applyE :: Sort -> Elims -> Sort

SynEq Sort

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

Pretty Sort

Defined in Agda.Syntax.Internal

Methods

pretty :: Sort -> Doc

prettyPrec :: Int -> Sort -> Doc

prettyList :: [Sort] -> Doc

NFData Sort

Defined in Agda.Syntax.Internal

Methods

rnf :: Sort -> ()

Eq Sort

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Ord Sort

Defined in Agda.TypeChecking.Substitute

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

NLPatToTerm NLPSort Sort

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

Match () NLPSort Sort

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPSort -> Sort -> NLM ()

PatternFrom () Sort NLPSort

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> () -> Sort -> TCM NLPSort

IsMeta a => IsMeta (Sort' a)

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Sort' a -> Maybe MetaId

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Sort' a)

Methods

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

Show t => Show (Sort' t)

Defined in Agda.Syntax.Internal

Methods

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

show :: Sort' t -> String

showList :: [Sort' t] -> ShowS

type ReifiesTo Sort

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Sort = Expr

type SubstArg (Sort' a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Sort' a) = SubstArg a

type Type' a = Type'' Term a

data Tele a

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

TelToArgs Telescope

Defined in Agda.Syntax.Internal

Methods

telToArgs :: Telescope -> [Arg ArgName]

GetDefs Telescope

Defined in Agda.Syntax.Internal.Defs

Methods

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

Reify Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope

Methods

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

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

TerSetSizeDepth Telescope

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: Telescope -> TerM a -> TerM a

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Telescope -> Telescope

AddContext Telescope

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Telescope -> Nat

PrettyTCM Telescope

Defined in Agda.TypeChecking.Pretty

Methods

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

Reduce Telescope

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Telescope -> ReduceM Telescope

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

TeleNoAbs Telescope

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: Telescope -> Term -> Term

Abstract Telescope

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Telescope -> Telescope

Foldable Tele

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

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

Defined in Agda.Syntax.Internal

Methods

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

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

TermLike a => TermLike (Tele a)

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike a => AllMetas (Tele a)

Defined in Agda.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> Tele a -> m

NamesIn a => NamesIn (Tele a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Tele a -> m

KillRange a => KillRange (Tele a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Tele a)

Free t => Free (Tele t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Tele t -> FreeM a c

MentionsMeta a => MentionsMeta (Tele a)

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Tele a -> Bool

AddContext (KeepNames Telescope)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: KeepNames Telescope -> Nat

ComputeOccurrences a => ComputeOccurrences (Tele a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Tele a -> OccM OccurrencesBuilder

Instantiate t => Instantiate (Tele t)

Defined in Agda.TypeChecking.Reduce

Methods

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

(Subst a, InstantiateFull a) => InstantiateFull (Tele a)

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Tele a -> ReduceM (Tele a)

(Subst a, Normalise a) => Normalise (Tele a)

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Tele a -> ReduceM (Tele a)

(Subst a, Simplify a) => Simplify (Tele a)

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Tele a -> ReduceM (Tele a)

EmbPrj a => EmbPrj (Tele a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Tele a -> S Int32

icod_ :: Tele a -> S Int32

value :: Int32 -> R (Tele a)

TermSubst a => Apply (Tele a)

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Tele a -> Args -> Tele a

applyE :: Tele a -> Elims -> Tele a

Subst a => Subst (Tele a)

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Tele a)

Methods

applySubst :: Substitution' (SubstArg (Tele a)) -> Tele a -> Tele a

Null (Tele a)

Defined in Agda.Syntax.Internal

Methods

empty :: Tele a

null :: Tele a -> Bool

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

Defined in Agda.Syntax.Internal

Methods

pretty :: Tele (Dom a) -> Doc

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

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

Sized (Tele a)

The size of a telescope is its length (as a list).

Defined in Agda.Syntax.Internal

Methods

size :: Tele a -> Int

Generic (Tele a)

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Tele a) :: Type -> Type

Methods

from :: Tele a -> Rep (Tele a) x

to :: Rep (Tele a) x -> Tele a

Show a => Show (Tele a)

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Tele a -> ShowS

show :: Tele a -> String

showList :: [Tele a] -> ShowS

NFData a => NFData (Tele a)

Defined in Agda.Syntax.Internal

Methods

rnf :: Tele a -> ()

(Subst a, Eq a) => Eq (Tele a)

Defined in Agda.TypeChecking.Substitute

Methods

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

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

(Subst a, Ord a) => Ord (Tele a)

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Telescope = Telescope

type SubstArg (Tele a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Tele a) = SubstArg a

type Rep (Tele a)

Defined in Agda.Syntax.Internal

type Rep (Tele a) = D1 ('MetaData "Tele" "Agda.Syntax.Internal" "Agda-2.6.2.2.20230105-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 IsFibrant

Constructors

IsFibrant

IsStrict

Instances

EmbPrj IsFibrant

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: IsFibrant -> S Int32

icod_ :: IsFibrant -> S Int32

value :: Int32 -> R IsFibrant

Generic IsFibrant

Defined in Agda.Syntax.Internal

Associated Types

type Rep IsFibrant :: Type -> Type

Methods

from :: IsFibrant -> Rep IsFibrant x

to :: Rep IsFibrant x -> IsFibrant

Show IsFibrant

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> IsFibrant -> ShowS

show :: IsFibrant -> String

showList :: [IsFibrant] -> ShowS

NFData IsFibrant

Defined in Agda.Syntax.Internal

Methods

rnf :: IsFibrant -> ()

Eq IsFibrant

Defined in Agda.Syntax.Internal

Methods

(==) :: IsFibrant -> IsFibrant -> Bool

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

Ord IsFibrant

Defined in Agda.Syntax.Internal

Methods

compare :: IsFibrant -> IsFibrant -> Ordering

(<) :: IsFibrant -> IsFibrant -> Bool

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

(>) :: IsFibrant -> IsFibrant -> Bool

(>=) :: IsFibrant -> IsFibrant -> Bool

max :: IsFibrant -> IsFibrant -> IsFibrant

min :: IsFibrant -> IsFibrant -> IsFibrant

type Rep IsFibrant

Defined in Agda.Syntax.Internal

type Rep IsFibrant = D1 ('MetaData "IsFibrant" "Agda.Syntax.Internal" "Agda-2.6.2.2.20230105-inplace" 'False) (C1 ('MetaCons "IsFibrant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsStrict" 'PrefixI 'False) (U1 :: Type -> Type))

data Level' t

A level is a maximum expression of a closed level and 0..n PlusLevel expressions each of which is an atom plus a number.

Constructors

Max !Integer [PlusLevel' t]

Instances

TermSize Level

Defined in Agda.Syntax.Internal

Methods

termSize :: Level -> Int

tsize :: Level -> Sum Int

GetDefs Level

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike Level

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

AllMetas Level

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

NamesIn Level

Defined in Agda.Syntax.Internal.Names

Methods

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

KillRange Level

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Level

Reify Level

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Level

Methods

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

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

AbsTerm Level

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Level -> Level

EqualSy Level

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Level -> Level -> Bool

Free Level

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

PrecomputeFreeVars Level

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Level -> FV Level

ForceNotFree Level

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

UsableModality Level

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance Level

Defined in Agda.TypeChecking.Irrelevance

Methods

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

MentionsMeta Level

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Level -> Bool

AnyRigid Level

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs Level

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Level -> OccursM Level

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

IsInstantiatedMeta Level

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta Level

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

ComputeOccurrences Level

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Level -> OccM OccurrencesBuilder

PrettyTCM Level

Defined in Agda.TypeChecking.Pretty

Methods

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

Instantiate Level

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Level -> ReduceM Level

InstantiateFull Level

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Level -> ReduceM Level

Normalise Level

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Level -> ReduceM Level

Reduce Level

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Level -> ReduceM Level

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

Simplify Level

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Level -> ReduceM Level

EmbPrj Level

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Level -> S Int32

icod_ :: Level -> S Int32

value :: Int32 -> R Level

DeBruijn Level

Defined in Agda.TypeChecking.Substitute.DeBruijn

Methods

deBruijnVar :: Int -> Level

debruijnNamedVar :: String -> Int -> Level

deBruijnView :: Level -> Maybe Int

SynEq Level

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

Pretty Level

Defined in Agda.Syntax.Internal

Methods

pretty :: Level -> Doc

prettyPrec :: Int -> Level -> Doc

prettyList :: [Level] -> Doc

Foldable Level'

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Level' m -> m

foldMap :: Monoid m => (a -> m) -> Level' a -> m

foldMap' :: Monoid m => (a -> m) -> Level' a -> m

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

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

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

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

foldr1 :: (a -> a -> a) -> Level' a -> a

foldl1 :: (a -> a -> a) -> Level' a -> a

toList :: Level' a -> [a]

null :: Level' a -> Bool

length :: Level' a -> Int

elem :: Eq a => a -> Level' a -> Bool

maximum :: Ord a => Level' a -> a

minimum :: Ord a => Level' a -> a

sum :: Num a => Level' a -> a

product :: Num a => Level' a -> a

Traversable Level'

Defined in Agda.Syntax.Internal

Methods

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

sequenceA :: Applicative f => Level' (f a) -> f (Level' a)

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

sequence :: Monad m => Level' (m a) -> m (Level' a)

Functor Level'

Defined in Agda.Syntax.Internal

Methods

fmap :: (a -> b) -> Level' a -> Level' b

(<$) :: a -> Level' b -> Level' a

NFData Level

Defined in Agda.Syntax.Internal

Methods

rnf :: Level -> ()

Eq Level

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Ord Level

Defined in Agda.TypeChecking.Substitute

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

NLPatToTerm NLPat Level

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

Match () NLPat Level

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPat -> Level -> NLM ()

PatternFrom () Level NLPat

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> () -> Level -> TCM NLPat

IsMeta a => IsMeta (Level' a)

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Level' a -> Maybe MetaId

Subst a => Subst (Level' a)

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Level' a)

Methods

applySubst :: Substitution' (SubstArg (Level' a)) -> Level' a -> Level' a

Show t => Show (Level' t)

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Level' t -> ShowS

show :: Level' t -> String

showList :: [Level' t] -> ShowS

type ReifiesTo Level

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Level = Expr

type SubstArg (Level' a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Level' a) = SubstArg a

data PlusLevel' t

Constructors

Plus !Integer t

Instances

TermSize PlusLevel

Defined in Agda.Syntax.Internal

Methods

termSize :: PlusLevel -> Int

tsize :: PlusLevel -> Sum Int

GetDefs PlusLevel

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike PlusLevel

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

AllMetas PlusLevel

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

NamesIn PlusLevel

Defined in Agda.Syntax.Internal.Names

Methods

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

KillRange PlusLevel

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PlusLevel

AbsTerm PlusLevel

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> PlusLevel -> PlusLevel

EqualSy PlusLevel

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: PlusLevel -> PlusLevel -> Bool

PrecomputeFreeVars PlusLevel

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: PlusLevel -> FV PlusLevel

ForceNotFree PlusLevel

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

UsableRelevance PlusLevel

Defined in Agda.TypeChecking.Irrelevance

Methods

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

MentionsMeta PlusLevel

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> PlusLevel -> Bool

AnyRigid PlusLevel

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs PlusLevel

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: PlusLevel -> OccursM PlusLevel

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

IsInstantiatedMeta PlusLevel

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta PlusLevel

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

ComputeOccurrences PlusLevel

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: PlusLevel -> OccM OccurrencesBuilder

InstantiateFull PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: PlusLevel -> ReduceM PlusLevel

Normalise PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: PlusLevel -> ReduceM PlusLevel

Reduce PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: PlusLevel -> ReduceM PlusLevel

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

Simplify PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: PlusLevel -> ReduceM PlusLevel

EmbPrj PlusLevel

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PlusLevel -> S Int32

icod_ :: PlusLevel -> S Int32

value :: Int32 -> R PlusLevel

DeBruijn PlusLevel

Defined in Agda.TypeChecking.Substitute.DeBruijn

Methods

deBruijnVar :: Int -> PlusLevel

debruijnNamedVar :: String -> Int -> PlusLevel

deBruijnView :: PlusLevel -> Maybe Int

SynEq PlusLevel

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

Pretty PlusLevel

Defined in Agda.Syntax.Internal

Methods

pretty :: PlusLevel -> Doc

prettyPrec :: Int -> PlusLevel -> Doc

prettyList :: [PlusLevel] -> Doc

Foldable PlusLevel'

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'

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'

Defined in Agda.Syntax.Internal

Methods

fmap :: (a -> b) -> PlusLevel' a -> PlusLevel' b

(<$) :: a -> PlusLevel' b -> PlusLevel' a

NFData PlusLevel

Defined in Agda.Syntax.Internal

Methods

rnf :: PlusLevel -> ()

Eq PlusLevel

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Ord PlusLevel

Defined in Agda.TypeChecking.Substitute

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)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => PlusLevel' t -> FreeM a c

Instantiate t => Instantiate (PlusLevel' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

IsMeta a => IsMeta (PlusLevel' a)

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: PlusLevel' a -> Maybe MetaId

Subst a => Subst (PlusLevel' a)

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (PlusLevel' a)

Methods

applySubst :: Substitution' (SubstArg (PlusLevel' a)) -> PlusLevel' a -> PlusLevel' a

Show t => Show (PlusLevel' t)

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> PlusLevel' t -> ShowS

show :: PlusLevel' t -> String

showList :: [PlusLevel' t] -> ShowS

type SubstArg (PlusLevel' a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (PlusLevel' a) = SubstArg a

type PlusLevel = PlusLevel' Term

type LevelAtom = Term

newtype BraveTerm

Newtypes for terms that produce a dummy, rather than crash, when applied to incompatible eliminations.

Constructors

BraveTerm

Fields

• unBrave :: Term

Instances

Apply BraveTerm

Defined in Agda.TypeChecking.Substitute

Methods

apply :: BraveTerm -> Args -> BraveTerm

applyE :: BraveTerm -> Elims -> BraveTerm

Subst BraveTerm

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg BraveTerm

Methods

applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm

DeBruijn BraveTerm

Defined in Agda.TypeChecking.Substitute

Methods

deBruijnVar :: Int -> BraveTerm

debruijnNamedVar :: String -> Int -> BraveTerm

deBruijnView :: BraveTerm -> Maybe Int

Show BraveTerm

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> BraveTerm -> ShowS

show :: BraveTerm -> String

showList :: [BraveTerm] -> ShowS

type SubstArg BraveTerm

Defined in Agda.TypeChecking.Substitute

type SubstArg BraveTerm = BraveTerm

type Blocked_ = Blocked ()

'Blocked a without the a.

type NAPs = [NamedArg DeBruijnPattern]

Named pattern arguments.

type DeBruijnPattern = Pattern' DBPatVar

type PatVarName = ArgName

Pattern variables.

data PatternInfo

Constructors

PatternInfo

Fields

• patOrigin :: PatOrigin
• patAsNames :: [Name]

Instances

KillRange PatternInfo

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PatternInfo

EmbPrj PatternInfo

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PatternInfo -> S Int32

icod_ :: PatternInfo -> S Int32

value :: Int32 -> R PatternInfo

Generic PatternInfo

Defined in Agda.Syntax.Internal

Associated Types

type Rep PatternInfo :: Type -> Type

Methods

from :: PatternInfo -> Rep PatternInfo x

to :: Rep PatternInfo x -> PatternInfo

Show PatternInfo

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> PatternInfo -> ShowS

show :: PatternInfo -> String

showList :: [PatternInfo] -> ShowS

NFData PatternInfo

Defined in Agda.Syntax.Internal

Methods

rnf :: PatternInfo -> ()

Eq PatternInfo

Defined in Agda.Syntax.Internal

Methods

(==) :: PatternInfo -> PatternInfo -> Bool

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

type Rep PatternInfo

Defined in Agda.Syntax.Internal

type Rep PatternInfo = D1 ('MetaData "PatternInfo" "Agda.Syntax.Internal" "Agda-2.6.2.2.20230105-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

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

KillRange PatOrigin

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PatOrigin

EmbPrj PatOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PatOrigin -> S Int32

icod_ :: PatOrigin -> S Int32

value :: Int32 -> R PatOrigin

Generic PatOrigin

Defined in Agda.Syntax.Internal

Associated Types

type Rep PatOrigin :: Type -> Type

Methods

from :: PatOrigin -> Rep PatOrigin x

to :: Rep PatOrigin x -> PatOrigin

Show PatOrigin

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> PatOrigin -> ShowS

show :: PatOrigin -> String

showList :: [PatOrigin] -> ShowS

NFData PatOrigin

Defined in Agda.Syntax.Internal

Methods

rnf :: PatOrigin -> ()

Eq PatOrigin

Defined in Agda.Syntax.Internal

Methods

(==) :: PatOrigin -> PatOrigin -> Bool

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

type Rep PatOrigin

Defined in Agda.Syntax.Internal

type Rep PatOrigin = D1 ('MetaData "PatOrigin" "Agda.Syntax.Internal" "Agda-2.6.2.2.20230105-inplace" 'False) (((C1 ('MetaCons "PatOSystem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatOSplit" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PatOVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "PatODot" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PatOWild" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatOCon" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PatORec" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PatOLit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatOAbsurd" 'PrefixI 'False) (U1 :: Type -> Type)))))

data ConPatternInfo

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

KillRange ConPatternInfo

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT ConPatternInfo

InstantiateFull ConPatternInfo

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ConPatternInfo -> ReduceM ConPatternInfo

Normalise ConPatternInfo

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: ConPatternInfo -> ReduceM ConPatternInfo

EmbPrj ConPatternInfo

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ConPatternInfo -> S Int32

icod_ :: ConPatternInfo -> S Int32

value :: Int32 -> R ConPatternInfo

Subst ConPatternInfo

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ConPatternInfo

Methods

applySubst :: Substitution' (SubstArg ConPatternInfo) -> ConPatternInfo -> ConPatternInfo

Generic ConPatternInfo

Defined in Agda.Syntax.Internal

Associated Types

type Rep ConPatternInfo :: Type -> Type

Methods

from :: ConPatternInfo -> Rep ConPatternInfo x

to :: Rep ConPatternInfo x -> ConPatternInfo

Show ConPatternInfo

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> ConPatternInfo -> ShowS

show :: ConPatternInfo -> String

showList :: [ConPatternInfo] -> ShowS

NFData ConPatternInfo

Defined in Agda.Syntax.Internal

Methods

rnf :: ConPatternInfo -> ()

type SubstArg ConPatternInfo

Defined in Agda.TypeChecking.Substitute

type SubstArg ConPatternInfo = Term

type Rep ConPatternInfo

Defined in Agda.Syntax.Internal

type Rep ConPatternInfo = D1 ('MetaData "ConPatternInfo" "Agda.Syntax.Internal" "Agda-2.6.2.2.20230105-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)))))

data DBPatVar

Type used when numbering pattern variables.

Constructors

DBPatVar

Fields

• dbPatVarName :: PatVarName
• dbPatVarIndex :: !Int

Instances

KillRange DBPatVar

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT DBPatVar

UsableSizeVars DeBruijnPattern

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: DeBruijnPattern -> TerM VarSet

UsableSizeVars MaskedDeBruijnPatterns

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet

PrettyTCM DBPatVar

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => DBPatVar -> m Doc

InstantiateFull DBPatVar

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: DBPatVar -> ReduceM DBPatVar

Normalise DBPatVar

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: DBPatVar -> ReduceM DBPatVar

Reduce DeBruijnPattern

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: DeBruijnPattern -> ReduceM DeBruijnPattern

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

EmbPrj DBPatVar

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DBPatVar -> S Int32

icod_ :: DBPatVar -> S Int32

value :: Int32 -> R DBPatVar

Subst DeBruijnPattern

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg DeBruijnPattern

Methods

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

DeBruijn DBPatVar

Defined in Agda.TypeChecking.Substitute.DeBruijn

Methods

deBruijnVar :: Int -> DBPatVar

debruijnNamedVar :: String -> Int -> DBPatVar

deBruijnView :: DBPatVar -> Maybe Int

Pretty DBPatVar

Defined in Agda.Syntax.Internal

Methods

pretty :: DBPatVar -> Doc

prettyPrec :: Int -> DBPatVar -> Doc

prettyList :: [DBPatVar] -> Doc

Generic DBPatVar

Defined in Agda.Syntax.Internal

Associated Types

type Rep DBPatVar :: Type -> Type

Methods

from :: DBPatVar -> Rep DBPatVar x

to :: Rep DBPatVar x -> DBPatVar

Show DBPatVar

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> DBPatVar -> ShowS

show :: DBPatVar -> String

showList :: [DBPatVar] -> ShowS

NFData DBPatVar

Defined in Agda.Syntax.Internal

Methods

rnf :: DBPatVar -> ()

Eq DBPatVar

Defined in Agda.Syntax.Internal

Methods

(==) :: DBPatVar -> DBPatVar -> Bool

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

LabelPatVars Pattern DeBruijnPattern

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel DeBruijnPattern

Methods

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

unlabelPatVars :: DeBruijnPattern -> Pattern

UsableSizeVars (Masked DeBruijnPattern)

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet

UsableSizeVars [DeBruijnPattern]

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: [DeBruijnPattern] -> TerM VarSet

ToNLPat (Arg DeBruijnPattern) (Elim' NLPat)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Arg DeBruijnPattern -> Elim' NLPat

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat

type PatVarLabel DeBruijnPattern

Defined in Agda.Syntax.Internal.Pattern

type PatVarLabel DeBruijnPattern = Int

type SubstArg DeBruijnPattern

Defined in Agda.TypeChecking.Substitute

type SubstArg DeBruijnPattern = DeBruijnPattern

type Rep DBPatVar

Defined in Agda.Syntax.Internal

type Rep DBPatVar = D1 ('MetaData "DBPatVar" "Agda.Syntax.Internal" "Agda-2.6.2.2.20230105-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)))

class PatternVars a where

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

Associated Types

type PatternVarOut a

Methods

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

Instances

PatternVars (Arg (Pattern' a))

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (Arg (Pattern' a))

Methods

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

PatternVars (NamedArg (Pattern' a))

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (NamedArg (Pattern' a))

Methods

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

PatternVars a => PatternVars [a]

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut [a]

Methods

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

type PatternSubstitution = Substitution' DeBruijnPattern

data EqualityView

View type as equality type.

Constructors

EqualityViewType EqualityTypeData

OtherType Type

reduced

IdiomType Type

reduced

Instances

TermLike EqualityView

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> EqualityView -> m EqualityView

foldTerm :: Monoid m => (Term -> m) -> EqualityView -> m

Free EqualityView

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

EqualityUnview EqualityView

Defined in Agda.TypeChecking.Monad.Builtin

Methods

equalityUnview :: EqualityView -> Type

PrettyTCM EqualityView

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => EqualityView -> m Doc

Instantiate EqualityView

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: EqualityView -> ReduceM EqualityView

InstantiateFull EqualityView

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: EqualityView -> ReduceM EqualityView

Normalise EqualityView

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: EqualityView -> ReduceM EqualityView

Reduce EqualityView

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: EqualityView -> ReduceM EqualityView

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

Simplify EqualityView

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: EqualityView -> ReduceM EqualityView

Subst EqualityView

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg EqualityView

Methods

applySubst :: Substitution' (SubstArg EqualityView) -> EqualityView -> EqualityView

type SubstArg EqualityView

Defined in Agda.TypeChecking.Substitute

type SubstArg EqualityView = Term

data EqualityTypeData

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

EqualityUnview EqualityTypeData

Defined in Agda.TypeChecking.Monad.Builtin

Methods

equalityUnview :: EqualityTypeData -> Type

Subst EqualityTypeData

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg EqualityTypeData

Methods

applySubst :: Substitution' (SubstArg EqualityTypeData) -> EqualityTypeData -> EqualityTypeData

type SubstArg EqualityTypeData

Defined in Agda.TypeChecking.Substitute

type SubstArg EqualityTypeData = Term

data PathView

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

data IntervalView

Constructors

IZero

IOne

IMin (Arg Term) (Arg Term)

IMax (Arg Term) (Arg Term)

INeg (Arg Term)

OTerm Term

Instances

Show IntervalView

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> IntervalView -> ShowS

show :: IntervalView -> String

showList :: [IntervalView] -> ShowS

type DummyTermKind = String

type ListTel' a = [Dom (a, Type)]

Telescope as list.

type ListTel = ListTel' ArgName

class TelToArgs a where

Drop the types from a telescope.

Methods

telToArgs :: a -> [Arg ArgName]

Instances

TelToArgs ListTel

Defined in Agda.Syntax.Internal

Methods

telToArgs :: ListTel -> [Arg ArgName]

TelToArgs Telescope

Defined in Agda.Syntax.Internal

Methods

telToArgs :: Telescope -> [Arg ArgName]

class SgTel a where

Constructing a singleton telescope.

Methods

sgTel :: a -> Telescope

Instances

SgTel (Dom Type)

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom Type -> Telescope

SgTel (Dom (ArgName, Type))

Defined in Agda.Syntax.Internal

Methods

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

SgTel (ArgName, Dom Type)

Defined in Agda.Syntax.Internal

Methods

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

class Suggest a where

Suggest a name if available (i.e. name is not "_")

Methods

suggestName :: a -> Maybe String

Instances

Suggest Name

Defined in Agda.Syntax.Internal

Methods

suggestName :: Name -> Maybe String

Suggest Term

Defined in Agda.Syntax.Internal

Methods

suggestName :: Term -> Maybe String

Suggest String

Defined in Agda.Syntax.Internal

Methods

suggestName :: String -> Maybe String

Suggest (Abs b)

Defined in Agda.Syntax.Internal

Methods

suggestName :: Abs b -> Maybe String

data Suggestion

Constructors

forall a.Suggest a => Suggestion a

pattern EqualityType :: Sort -> QName -> Args -> Arg Term -> Arg Term -> Arg Term -> EqualityView

pattern ClosedLevel :: Integer -> Level

Constant level n

litP :: Literal -> Pattern' a

varP :: a -> Pattern' a

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

Convert a telescope to its list form.

arity :: Type -> Nat

Doesn't do any reduction.

dontCare :: Term -> Term

Add DontCare is it is not already a DontCare.

var :: Nat -> Term

An unapplied variable.

argFromDom :: Dom' t a -> Arg a

namedArgFromDom :: Dom' t a -> NamedArg a

domFromArg :: Arg a -> Dom a

domFromNamedArg :: NamedArg a -> Dom a

defaultDom :: a -> Dom a

defaultArgDom :: ArgInfo -> a -> Dom a

defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a

clausePats :: Clause -> [Arg DeBruijnPattern]

patVarNameToString :: PatVarName -> String

nameToPatVarName :: Name -> PatVarName

defaultPatternInfo :: PatternInfo

dotP :: Term -> Pattern' a

namedVarP :: PatVarName -> Named_ Pattern

namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern

absurdP :: Int -> DeBruijnPattern

Make an absurd pattern with the given de Bruijn index.

absurdPatternName :: PatVarName

noConPatternInfo :: ConPatternInfo

toConPatternInfo :: ConInfo -> ConPatternInfo

Build partial ConPatternInfo from ConInfo

fromConPatternInfo :: ConPatternInfo -> ConInfo

Build ConInfo from ConPatternInfo.

patternInfo :: Pattern' x -> Maybe PatternInfo

Retrieve the PatternInfo from a pattern

patternOrigin :: Pattern' x -> Maybe PatOrigin

Retrieve the origin of a pattern

properlyMatching :: Pattern' a -> Bool

Does the pattern perform a match that could fail?

properlyMatching'

Arguments

:: Bool

Should absurd patterns count as proper match?

-> Bool

Should projection patterns count as proper match?

-> Pattern' a

The pattern.

-> Bool

eqtSort :: EqualityView -> Sort

eqtName :: EqualityView -> QName

eqtParams :: EqualityView -> Args

eqtType :: EqualityView -> Arg Term

eqtLhs :: EqualityView -> Arg Term

eqtRhs :: EqualityView -> Arg Term

isEqualityType :: EqualityView -> Bool

isPathType :: PathView -> Bool

isIOne :: IntervalView -> Bool

absurdBody :: Abs Term

Absurd lambdas are internally represented as identity with variable name "()".

isAbsurdBody :: Abs Term -> Bool

isAbsurdPatternName :: PatVarName -> Bool

dummyLocName :: CallStack -> String

Construct a string representing the call-site that created the dummy thing.

dummyTermWith :: DummyTermKind -> CallStack -> Term

Aux: A dummy term to constitute a dummy termlevelsort/type.

dummyLevel :: CallStack -> Level

A dummy level to constitute a level/sort created at location. Note: use macro DUMMY_LEVEL !

atomicLevel :: t -> Level' t

dummyTerm :: CallStack -> Term

A dummy term created at location. Note: use macro DUMMY_TERM !

__DUMMY_TERM__ :: HasCallStack => Term

__DUMMY_LEVEL__ :: HasCallStack => Level

dummySort :: CallStack -> Sort

A dummy sort created at location. Note: use macro DUMMY_SORT !

__DUMMY_SORT__ :: HasCallStack => Sort

dummyType :: CallStack -> Type

A dummy type created at location. Note: use macro DUMMY_TYPE !

__DUMMY_TYPE__ :: HasCallStack => Type

dummyDom :: CallStack -> Dom Type

Context entries without a type have this dummy type. Note: use macro DUMMY_DOM !

__DUMMY_DOM__ :: HasCallStack => Dom Type

varSort :: Int -> Sort

tmSort :: Term -> Sort

tmSSort :: Term -> Sort

levelPlus :: Integer -> Level -> Level

Given a constant m and level l, compute m + l

levelSuc :: Level -> Level

mkType :: Integer -> Sort

mkProp :: Integer -> Sort

mkSSet :: Integer -> Sort

isSort :: Term -> Maybe Sort

impossibleTerm :: CallStack -> Term

mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)

A traversal for the names in a telescope.

mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a

replaceEmptyName :: ArgName -> Tele a -> Tele a

telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope

telFromList :: ListTel -> Telescope

Convert a list telescope to a telescope.

listTel :: Lens' ListTel Telescope

Lens to edit a Telescope as a list.

stripDontCare :: Term -> Term

Removing a topmost DontCare constructor.

suggests :: [Suggestion] -> String

unSpine :: Term -> Term

Convert top-level postfix projections into prefix projections.

unSpine' :: (ProjOrigin -> Bool) -> Term -> Term

Convert Proj projection eliminations according to their ProjOrigin into Def projection applications.

hasElims :: Term -> Maybe (Elims -> Term, Elims)

A view distinguishing the neutrals Var, Def, and MetaV which can be projected.

pDom :: LensHiding a => a -> Doc -> Doc

prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc

module Agda.Syntax.Internal.Blockers

module Agda.Syntax.Internal.Elim

module Agda.Syntax.Abstract.Name

data MetaId

Meta-variable identifiers use the same structure as NameIds.

Constructors

MetaId

Fields

• metaId :: !Word64
• metaModule :: !ModuleNameHash

Instances

EncodeTCM MetaId

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: MetaId -> TCM Value

GetDefs MetaId

Defined in Agda.Syntax.Internal.Defs

Methods

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

NamesIn MetaId

Defined in Agda.Syntax.Internal.Names

Methods

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

Reify MetaId

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo MetaId

Methods

reify :: MonadReify m => MetaId -> m (ReifiesTo MetaId)

reifyWhen :: MonadReify m => Bool -> MetaId -> m (ReifiesTo MetaId)

HasFresh MetaId

Defined in Agda.TypeChecking.Monad.Base

Methods

freshLens :: Lens' MetaId TCState

nextFresh' :: MetaId -> MetaId

IsInstantiatedMeta MetaId

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool

UnFreezeMeta MetaId

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

PrettyTCM MetaId

Defined in Agda.TypeChecking.Pretty

Methods

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

FromTerm MetaId

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction MetaId)

PrimTerm MetaId

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: MetaId -> TCM Term

PrimType MetaId

Defined in Agda.TypeChecking.Primitive

Methods

primType :: MetaId -> TCM Type

ToTerm MetaId

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (MetaId -> Term)

toTermR :: TCM (MetaId -> ReduceM Term)

EmbPrj MetaId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: MetaId -> S Int32

icod_ :: MetaId -> S Int32

value :: Int32 -> R MetaId

Unquote MetaId

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM MetaId

Pretty MetaId

Defined in Agda.Syntax.Common

Methods

pretty :: MetaId -> Doc

prettyPrec :: Int -> MetaId -> Doc

prettyList :: [MetaId] -> Doc

ToJSON MetaId

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: MetaId -> Value

toEncoding :: MetaId -> Encoding

toJSONList :: [MetaId] -> Value

toEncodingList :: [MetaId] -> Encoding

Enum MetaId

Defined in Agda.Syntax.Common

Methods

succ :: MetaId -> MetaId

pred :: MetaId -> MetaId

toEnum :: Int -> MetaId

fromEnum :: MetaId -> Int

enumFrom :: MetaId -> [MetaId]

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

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

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

Generic MetaId

Defined in Agda.Syntax.Common

Associated Types

type Rep MetaId :: Type -> Type

Methods

from :: MetaId -> Rep MetaId x

to :: Rep MetaId x -> MetaId

Show MetaId

The record selectors are not included in the resulting strings.

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> MetaId -> ShowS

show :: MetaId -> String

showList :: [MetaId] -> ShowS

NFData MetaId

Defined in Agda.Syntax.Common

Methods

rnf :: MetaId -> ()

Eq MetaId

Defined in Agda.Syntax.Common

Methods

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

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

Ord MetaId

Defined in Agda.Syntax.Common

Methods

compare :: MetaId -> MetaId -> Ordering

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

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

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

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

max :: MetaId -> MetaId -> MetaId

min :: MetaId -> MetaId -> MetaId

Hashable MetaId

Defined in Agda.Syntax.Common

Methods

hashWithSalt :: Int -> MetaId -> Int

hash :: MetaId -> Int

Singleton MetaId MetaSet

Defined in Agda.TypeChecking.Free.Lazy

Methods

singleton :: MetaId -> MetaSet

Singleton MetaId ()

Defined in Agda.TypeChecking.Free.Lazy

Methods

singleton :: MetaId -> ()

InstantiateFull (Judgement MetaId)

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Judgement MetaId -> ReduceM (Judgement MetaId)

type ReifiesTo MetaId

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo MetaId = Expr

type Rep MetaId

Defined in Agda.Syntax.Common

type Rep MetaId = D1 ('MetaData "MetaId" "Agda.Syntax.Common" "Agda-2.6.2.2.20230105-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)))

newtype ProblemId

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

Constructors

ProblemId Nat

Instances

EncodeTCM ProblemId

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: ProblemId -> TCM Value

HasFresh ProblemId

Defined in Agda.TypeChecking.Monad.Base

Methods

freshLens :: Lens' ProblemId TCState

nextFresh' :: ProblemId -> ProblemId

PrettyTCM ProblemId

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => ProblemId -> m Doc

Pretty ProblemId

Defined in Agda.Syntax.Common

Methods

pretty :: ProblemId -> Doc

prettyPrec :: Int -> ProblemId -> Doc

prettyList :: [ProblemId] -> Doc

ToJSON ProblemId

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: ProblemId -> Value

toEncoding :: ProblemId -> Encoding

toJSONList :: [ProblemId] -> Value

toEncodingList :: [ProblemId] -> Encoding

Enum ProblemId

Defined in Agda.Syntax.Common

Methods

succ :: ProblemId -> ProblemId

pred :: ProblemId -> ProblemId

toEnum :: Int -> ProblemId

fromEnum :: ProblemId -> Int

enumFrom :: ProblemId -> [ProblemId]

enumFromThen :: ProblemId -> ProblemId -> [ProblemId]

enumFromTo :: ProblemId -> ProblemId -> [ProblemId]

enumFromThenTo :: ProblemId -> ProblemId -> ProblemId -> [ProblemId]

Num ProblemId

Defined in Agda.Syntax.Common

Methods

(+) :: ProblemId -> ProblemId -> ProblemId

(-) :: ProblemId -> ProblemId -> ProblemId

(*) :: ProblemId -> ProblemId -> ProblemId

negate :: ProblemId -> ProblemId

abs :: ProblemId -> ProblemId

signum :: ProblemId -> ProblemId

fromInteger :: Integer -> ProblemId

Integral ProblemId

Defined in Agda.Syntax.Common

Methods

quot :: ProblemId -> ProblemId -> ProblemId

rem :: ProblemId -> ProblemId -> ProblemId

div :: ProblemId -> ProblemId -> ProblemId

mod :: ProblemId -> ProblemId -> ProblemId

quotRem :: ProblemId -> ProblemId -> (ProblemId, ProblemId)

divMod :: ProblemId -> ProblemId -> (ProblemId, ProblemId)

toInteger :: ProblemId -> Integer

Real ProblemId

Defined in Agda.Syntax.Common

Methods

toRational :: ProblemId -> Rational

Show ProblemId

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> ProblemId -> ShowS

show :: ProblemId -> String

showList :: [ProblemId] -> ShowS

NFData ProblemId

Defined in Agda.Syntax.Common

Methods

rnf :: ProblemId -> ()

Eq ProblemId

Defined in Agda.Syntax.Common

Methods

(==) :: ProblemId -> ProblemId -> Bool

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

Ord ProblemId

Defined in Agda.Syntax.Common

Methods

compare :: ProblemId -> ProblemId -> Ordering

(<) :: ProblemId -> ProblemId -> Bool

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

(>) :: ProblemId -> ProblemId -> Bool

(>=) :: ProblemId -> ProblemId -> Bool

max :: ProblemId -> ProblemId -> ProblemId

min :: ProblemId -> ProblemId -> ProblemId

Monad m => MonadFresh ProblemId (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fresh :: PureConversionT m ProblemId