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

Agda.Syntax.Internal

Synopsis

Documentation

data Term Source #

Raw values.

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

Constructors

Var !Int Elims

x es neutral

Lam ArgInfo (Abs Term)

Terms are beta normal. Relevance is ignored

Lit Literal 
Def QName Elims

f es, possibly a delta/iota-redex

Con ConHead ConInfo Elims

c es or record { fs = es } es allows only Apply and IApply eliminations, and IApply only for data constructors.

Pi (Dom Type) (Abs Type)

dependent or non-dependent function space

Sort Sort 
Level Level 
MetaV !MetaId Elims 
DontCare Term

Irrelevant stuff in relevant position, but created in an irrelevant context. Basically, an internal version of the irrelevance axiom .irrAx : .A -> A.

Dummy String Elims

A (part of a) term or type which is only used for internal purposes. Replaces the Sort Prop hack. The String typically describes the location where we create this dummy, but can contain other information as well. The second field accumulates eliminations in case we apply a dummy term to more of them. Dummy terms should never be used in places where they can affect type checking, so syntactic checks are free to ignore the eliminators, which are only there to ease debugging when a dummy term incorrectly leaks into a relevant position.

Instances

Instances details
Pretty Level Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty Type Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

LensSort Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

Suggest Term Source # 
Instance details

Defined in Agda.Syntax.Internal

TelToArgs ListTel Source # 
Instance details

Defined in Agda.Syntax.Internal

TelToArgs Telescope Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize Level Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize Term Source # 
Instance details

Defined in Agda.Syntax.Internal

GetDefs Level Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Sort Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Telescope Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Term Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Type Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike Level Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike Sort Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike Term Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike Type Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

AllMetas Level Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Sort Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Term Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Type Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

NamesIn Level Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn Sort Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn Term Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn CompiledClauses Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

KillRange Level Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Substitution Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Term Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Reify Level Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Level Source #

Reify Sort Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Sort Source #

Reify Telescope Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope Source #

Reify Term Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Term Source #

Reify Type Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Type Source #

TerSetSizeDepth ListTel Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

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

TerSetSizeDepth Telescope Source # 
Instance details

Defined in Agda.Termination.Monad

AbsTerm Level Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

AbsTerm PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

AbsTerm Sort Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

AbsTerm Term Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

AbsTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy Level Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

EqualSy Sort Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy Term Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy Type Source #

Ignores sorts.

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

IsPrefixOf Args Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

IsPrefixOf Elims Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

IsPrefixOf Term Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

CheckInternal Elims Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

CheckInternal Level Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

CheckInternal PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

CheckInternal Sort Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

CheckInternal Term Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

CheckInternal Type Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

DropArgs Telescope Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Defined in Agda.TypeChecking.DropArgs

DropArgs Term Source #

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

Instance details

Defined in Agda.TypeChecking.DropArgs

Methods

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

DropArgs CompiledClauses Source #

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

Instance details

Defined in Agda.TypeChecking.DropArgs

Free Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Term Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

PrecomputeFreeVars Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

PrecomputeFreeVars PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

PrecomputeFreeVars Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

PrecomputeFreeVars Term Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

PrecomputeFreeVars Type Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

ForceNotFree Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree Term Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree Type Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

UsableModality Level Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableModality Sort Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableModality Term Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableRelevance Level Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableRelevance PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableRelevance Sort Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableRelevance Term Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

NoProjectedVar Term Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars

ReduceAndEtaContract Term Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars

MentionsMeta Elim Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

MentionsMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

MentionsMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

MentionsMeta Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

MentionsMeta Term Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

MentionsMeta Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

AnyRigid Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

AnyRigid PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

AnyRigid Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

AnyRigid Term Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

AnyRigid Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs Elims Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs Term Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

AddContext Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

IsInstantiatedMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

IsInstantiatedMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

IsInstantiatedMeta Term Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

UnFreezeMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

UnFreezeMeta Sort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta Term Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta Type Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

IsSizeType Term Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

ComputeOccurrences Level Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences Term Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences Type Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

PrettyTCM Elim Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Level Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Sort Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Term Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Type Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrimTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Type -> TCM Term Source #

PrimType Type Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primType :: Type -> TCM Type Source #

ToTerm Term Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Instantiate Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

IsMeta Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Elim Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Type Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Sort -> ReduceM Sort

Simplify Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Term -> ReduceM Term

GetMatchables Term Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

EmbPrj Blocked_ Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Level Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj NotBlocked Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Sort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Term Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

TeleNoAbs ListTel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

TeleNoAbs Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Term Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Type Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Apply Term Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Apply CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Term Source #

DeBruijn Level Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

DeBruijn PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

DeBruijn Term Source #

We can substitute Terms for variables.

Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

SynEq Level Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

SynEq Sort Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Term Source #

Syntactic term equality ignores DontCare stuff.

Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Type Source #

Syntactic equality ignores sorts.

Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

PiApplyM Term Source # 
Instance details

Defined in Agda.TypeChecking.Telescope

Show Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Term -> ShowS #

show :: Term -> String #

showList :: [Term] -> ShowS #

NFData Level Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Level -> () #

NFData PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: PlusLevel -> () #

NFData Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Sort -> () #

NFData Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Term -> () #

NFData Type Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Type -> () #

Eq Level Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq NotBlocked Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Eq PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Eq Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Eq Term Source #

Syntactic Term equality, ignores stuff below DontCare and sharing.

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq SingleLevel Source # 
Instance details

Defined in Agda.TypeChecking.Level

Ord Level Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Ord Sort Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Ord Term Source # 
Instance details

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 #

Match NLPSort Sort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Match NLPType Type Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Match NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Match NLPat Term Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

NLPatToTerm Nat Term Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

NLPatToTerm NLPSort Sort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

NLPatToTerm NLPType Type Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

NLPatToTerm NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

NLPatToTerm NLPat Term Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

PatternFrom Level NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

PatternFrom Sort NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

PatternFrom Term NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

PatternFrom Type NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

MonadError Blocked_ NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

throwError :: Blocked_ -> NLM a #

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

Conversion TOM Term (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

Conversion TOM Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.TypeChecking.Patterns.Internal

PatternFrom Elims [Elim' NLPat] Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Conversion MOT (Exp O) Term Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Term Source #

Conversion MOT (Exp O) Type Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type Source #

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Defined in Agda.Syntax.Internal

LensSort (Type' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

SgTel (Dom Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

SgTel (Dom (ArgName, Type)) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal.Defs

Methods

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

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

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

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

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

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

Defined in Agda.Syntax.Internal.Names

Methods

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

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Dom i) Source #

Methods

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

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

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

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy a => EqualSy (Dom a) Source #

Ignore the tactic.

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

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

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Irrelevance

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

Defined in Agda.TypeChecking.Irrelevance

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

Defined in Agda.TypeChecking.Irrelevance

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

Defined in Agda.TypeChecking.Irrelevance

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

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs (Abs Term) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs (Abs Type) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

AddContext (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Dom Type -> Nat Source #

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Dom (String, Type)) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames Telescope) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

IsSizeType a => IsSizeType (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

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

Defined in Agda.TypeChecking.Monad.SizedTypes

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

Defined in Agda.TypeChecking.Positivity

PrettyTCM (Arg Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Arg Type) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (NamedArg Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Named_ Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Type' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

ToTerm (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Instantiate a => Instantiate (Blocked a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Int32 Source #

icod_ :: Dom a -> S Int32 Source #

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

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

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

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

Apply t => Apply (Blocked t) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Blocked a) Source #

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

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) Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

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

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

Defined in Agda.Syntax.Internal

Methods

rnf :: Dom e -> () #

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

Syntactic Type equality, ignores sort annotations.

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

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) Source # 
Instance details

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 #

Match [Elim' NLPat] Elims Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

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

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Dom a -> Dom b Source #

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

SgTel (ArgName, Dom Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Dom r, Name) Source #

AddContext (Name, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Monad.Context

AddContext (Text, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Context

type TypeOf Elims Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf Elims = (Type, Elims -> Term)
type TypeOf Level Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf Level = ()
type TypeOf PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf PlusLevel = ()
type TypeOf Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf Sort = ()
type TypeOf Term Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf Type Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf Type = ()
type ReifiesTo Level Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Sort Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Telescope Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Term Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Type Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type SubstArg Term Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type TypeOf (Abs Term) Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Abs Term) = (Dom Type, Abs Type)
type TypeOf (Abs Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Dom a) Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Dom a) = TypeOf a
type TypeOf [PlusLevel] Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf [PlusLevel] = ()
type ReifiesTo (Dom i) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Dom i) = Arg (ReifiesTo i)
type SubstArg (Blocked a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type AbsOfRef (Dom r, Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

data Clause Source #

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

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

clauseTel ~ permute clausePerm (patternVars namedClausePats)

Terms in dot patterns are valid in the clause telescope.

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

Constructors

Clause 

Fields

  • clauseLHSRange :: Range
     
  • clauseFullRange :: Range
     
  • clauseTel :: Telescope

    Δ: The types of the pattern variables in dependency order.

  • namedClausePats :: NAPs

    Δ ⊢ ps. The de Bruijn indices refer to Δ.

  • clauseBody :: Maybe Term

    Just v with Δ ⊢ v for a regular clause, or Nothing for an absurd one.

  • clauseType :: Maybe (Arg Type)

    Δ ⊢ t. The type of the rhs under clauseTel. Used, e.g., by TermCheck. Can be Irrelevant if we encountered an irrelevant projection pattern on the lhs.

  • clauseCatchall :: Bool

    Clause has been labelled as CATCHALL.

  • clauseExact :: Maybe Bool

    Pattern matching of this clause is exact, no catch-all case. Computed by the coverage checker. Nothing means coverage checker has not run yet (clause may be inexact). Just False means clause is not exact. Just True means clause is exact.

  • clauseRecursive :: Maybe Bool

    clauseBody contains recursive calls; computed by termination checker. Nothing means that termination checker has not run yet, or that clauseBody contains meta-variables; these could be filled with recursive calls later! Just False means definitely no recursive call. Just True means definitely a recursive call.

  • clauseUnreachable :: Maybe Bool

    Clause has been labelled as unreachable by the coverage checker. Nothing means coverage checker has not run yet (clause may be unreachable). Just False means clause is not unreachable. Just True means clause is unreachable.

  • clauseEllipsis :: ExpandedEllipsis

    Was this clause created by expansion of an ellipsis?

  • clauseWhereModule :: Maybe ModuleName

    Keeps track of the module name associate with the clause's where clause.

Instances

Instances details
Pretty Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

GetDefs Clause Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

NamesIn Clause Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

FunArity Clause Source #

Get the number of initial Apply patterns in a clause.

Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

funArity :: Clause -> Int Source #

HasRange Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

DropArgs Clause Source #

NOTE: does not work for recursive functions.

Instance details

Defined in Agda.TypeChecking.DropArgs

Methods

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

DropArgs FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.DropArgs

Free Clause Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Occurs Clause Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

ComputeOccurrences Clause Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

PrettyTCM Clause Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

NormaliseProjP Clause Source # 
Instance details

Defined in Agda.TypeChecking.Records

InstantiateFull Clause Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

EmbPrj Clause Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Abstract Clause Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Clause Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Null Clause Source #

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

Instance details

Defined in Agda.Syntax.Internal

Generic Clause Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Internal

NFData Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Clause -> () #

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

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.Auto.Convert

Methods

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

FunArity [Clause] Source #

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

Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

funArity :: [Clause] -> Int Source #

Reify (QNamed Clause) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (QNamed Clause) Source #

PrettyTCM (QNamed Clause) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

type Rep Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

type Rep Clause = D1 ('MetaData "Clause" "Agda.Syntax.Internal" "Agda-2.6.3.20230914-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) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

data Dom' t e Source #

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

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

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

Constructors

Dom 

Fields

Instances

Instances details
TelToArgs ListTel Source # 
Instance details

Defined in Agda.Syntax.Internal

TelToArgs Telescope Source # 
Instance details

Defined in Agda.Syntax.Internal

GetDefs Telescope Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

Reify Telescope Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope Source #

TerSetSizeDepth ListTel Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

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

TerSetSizeDepth Telescope Source # 
Instance details

Defined in Agda.Termination.Monad

DropArgs Telescope Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Defined in Agda.TypeChecking.DropArgs

AddContext Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

PrettyTCM Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Reduce Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

TeleNoAbs ListTel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

TeleNoAbs Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Defined in Agda.Syntax.Internal

SgTel (Dom Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

SgTel (Dom (ArgName, Type)) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal.Defs

Methods

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

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

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Dom i) Source #

Methods

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

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

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

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy a => EqualSy (Dom a) Source #

Ignore the tactic.

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

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

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Irrelevance

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

Defined in Agda.TypeChecking.Irrelevance

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

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

AddContext (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Dom Type -> Nat Source #

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Dom (String, Type)) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames Telescope) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

IsSizeType a => IsSizeType (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

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

Defined in Agda.TypeChecking.Positivity

PrettyTCM (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

ToTerm (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Int32 Source #

icod_ :: Dom a -> S Int32 Source #

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

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

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) Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

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

Decoration (Dom' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable (Dom' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: Dom' t a -> Bool #

length :: Dom' t a -> Int #

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

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

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

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

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

Traversable (Dom' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor (Dom' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

Defined in Agda.Syntax.Internal

Methods

rnf :: Dom e -> () #

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

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) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Dom a -> Dom b Source #

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

LensAnnotation (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

LensArgInfo (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

LensCohesion (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

LensFreeVariables (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

LensHiding (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

LensLock (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

LensModality (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

LensNamed (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

type NameOf (Dom' t e) Source #

Methods

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

LensOrigin (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

LensQuantity (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

LensRelevance (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

Methods

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

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

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

SgTel (ArgName, Dom Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

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

Defined in Agda.Syntax.Internal.Names

Methods

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

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

Defined in Agda.Syntax.Internal

Methods

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

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

Defined in Agda.Syntax.Internal

Methods

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

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Dom r, Name) Source #

AddContext (Name, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Monad.Context

AddContext (Text, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Dom' a b) Source #

Methods

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

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

Defined in Agda.Syntax.Internal

Methods

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

show :: Dom' t e -> String #

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

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

Ignores Origin and FreeVariables and tactic.

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

type ReifiesTo Telescope Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type TypeOf (Dom a) Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Dom a) = TypeOf a
type ReifiesTo (Dom i) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Dom i) = Arg (ReifiesTo i)
type NameOf (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

type NameOf (Dom' t e) = NamedName
type AbsOfRef (Dom r, Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type SubstArg (Dom' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Dom' a b) = SubstArg a

type Pattern Source #

Arguments

 = Pattern' PatVarName

The PatVarName is a name suggestion.

data DataOrRecord Source #

Instances

Instances details
CopatternMatchingAllowed DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Internal

PatternMatchingAllowed DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Internal

EmbPrj DataOrRecord Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Generic DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep DataOrRecord :: Type -> Type #

Show DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Internal

NFData DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: DataOrRecord -> () #

Eq DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Internal

type Rep DataOrRecord Source # 
Instance details

Defined in Agda.Syntax.Internal

type Rep DataOrRecord = D1 ('MetaData "DataOrRecord" "Agda.Syntax.Internal" "Agda-2.6.3.20230914-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] Source #

Type of argument lists.

data Substitution' a Source #

Substitutions.

Constructors

IdS

Identity substitution. Γ ⊢ IdS : Γ

EmptyS Impossible

Empty substitution, lifts from the empty context. First argument is IMPOSSIBLE. Apply this to closed terms you want to use in a non-empty context. Γ ⊢ EmptyS : ()

a :# (Substitution' a) infixr 4

Substitution extension, `cons'. Γ ⊢ u : Aρ Γ ⊢ ρ : Δ ---------------------- Γ ⊢ u :# ρ : Δ, A

Strengthen Impossible !Int (Substitution' a)

Strengthening substitution. First argument is IMPOSSIBLE. In 'Strengthen err n ρ the number n must be non-negative. This substitution should only be applied to values t for which none of the variables 0 up to n - 1 are free in t[ρ], and in that case n is subtracted from all free de Bruijn indices in t[ρ]. Γ ⊢ ρ : Δ |Θ| = n --------------------------- Γ ⊢ Strengthen n ρ : Δ, Θ @

Wk !Int (Substitution' a)

Weakening substitution, lifts to an extended context. Γ ⊢ ρ : Δ ------------------- Γ, Ψ ⊢ Wk |Ψ| ρ : Δ

Lift !Int (Substitution' a)

Lifting substitution. Use this to go under a binder. Lift 1 ρ == var 0 :# Wk 1 ρ. Γ ⊢ ρ : Δ ------------------------- Γ, Ψρ ⊢ Lift |Ψ| ρ : Δ, Ψ

Instances

Instances details
KillRange Substitution Source # 
Instance details

Defined in Agda.Syntax.Internal

InstantiateFull Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Foldable Substitution' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: Substitution' a -> Bool #

length :: Substitution' a -> Int #

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

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

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

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

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

Traversable Substitution' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor Substitution' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Eq Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Ord Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal.Names

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

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Substitution' a) Source #

Null (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Generic (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

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

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

Methods

rnf :: Substitution' a -> () #

type SubstArg (Substitution' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Substitution' a) = a
type Rep (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Binder.

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

Constructors

Abs

The body has (at least) one free variable. Danger: unAbs doesn't shift variables properly

Fields

NoAbs 

Fields

Instances

Instances details
Decoration Abs Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Abs Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

toList :: Abs a -> [a] #

null :: Abs a -> Bool #

length :: Abs a -> Int #

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

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

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

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

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

Traversable Abs Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor Abs Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Conversion MOT a b => Conversion MOT (Abs a) (Abs b) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

Pretty t => Pretty (Abs t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Abs t -> Doc Source #

prettyPrec :: Int -> Abs t -> Doc Source #

prettyList :: [Abs t] -> Doc Source #

Suggest (Abs b) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal.Defs

Methods

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

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

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

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

Defined in Agda.Syntax.Internal.Names

Methods

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

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

Defined in Agda.Syntax.Internal

(Free i, Reify i) => Reify (Abs i) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Abs i) Source #

Methods

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

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

(TermSubst a, AbsTerm a) => AbsTerm (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

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

Ignores absName.

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

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

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

(Subst a, UsableRelevance a) => UsableRelevance (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

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

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

(Subst a, AnyRigid a) => AnyRigid (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs (Abs Term) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs (Abs Type) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source #

Does not worry about raising.

Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

UnFreezeMeta a => UnFreezeMeta (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

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

Defined in Agda.TypeChecking.Positivity

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

Defined in Agda.TypeChecking.Reduce

Methods

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

(Subst a, InstantiateFull a) => InstantiateFull (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

(Subst a, Normalise a) => Normalise (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

(Subst a, Reduce a) => Reduce (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

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

(Subst a, Simplify a) => Simplify (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

NLPatVars a => NLPatVars (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Abs a -> S Int32 Source #

icod_ :: Abs a -> S Int32 Source #

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

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Abs a) Source #

Methods

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

(Subst a, SynEq a) => SynEq (Abs a) Source # 
Instance details

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)

Sized a => Sized (Abs a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

size :: Abs a -> Int Source #

natSize :: Abs a -> Peano Source #

Generic (Abs a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

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

Methods

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

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

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

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Abs a -> ShowS #

show :: Abs a -> String #

showList :: [Abs a] -> ShowS #

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

Defined in Agda.Syntax.Internal

Methods

rnf :: Abs a -> () #

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

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

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

(Subst a, Ord a) => Ord (Abs a) Source # 
Instance details

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) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Abs a -> Abs b Source #

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

type TypeOf (Abs Term) Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Abs Term) = (Dom Type, Abs Type)
type TypeOf (Abs Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

type ReifiesTo (Abs i) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Abs i) = (Name, ReifiesTo i)
type SubstArg (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Abs a) = SubstArg a
type Rep (Abs a) Source # 
Instance details

Defined in Agda.Syntax.Internal

class LensSort a where Source #

Minimal complete definition

lensSort

Instances

Instances details
LensSort Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

LensSort (Type' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

type Elims Source #

Arguments

 = [Elim]

eliminations ordered left-to-right.

class TermSize a where Source #

The size of a term is roughly the number of nodes in its syntax tree. This number need not be precise for logical correctness of Agda, it is only used for reporting (and maybe decisions regarding performance).

Not counting towards the term size are:

  • sort and color annotations,
  • projections.

Minimal complete definition

tsize

Methods

termSize :: a -> Int Source #

tsize :: a -> Sum Int Source #

Instances

Instances details
TermSize Level Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize Term Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

(Foldable t, TermSize a) => TermSize (t a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

termSize :: t a -> Int Source #

tsize :: t a -> Sum Int Source #

data ConHead Source #

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

Instances

Instances details
CopatternMatchingAllowed ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

LensConName ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

NamesIn ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

HasRange ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

SetRange ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

PrettyTCM ConHead Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

InstantiateFull ConHead Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

EmbPrj ConHead Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Generic ConHead Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Internal

NFData ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: ConHead -> () #

Eq ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Ord ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

type Rep ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

type Rep ConHead = D1 ('MetaData "ConHead" "Agda.Syntax.Internal" "Agda-2.6.3.20230914-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 Source #

Minimal complete definition

getConName

Methods

getConName :: a -> QName Source #

setConName :: QName -> a -> a Source #

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

Instances

Instances details
LensConName ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

data Type'' t a Source #

Types are terms with a sort annotation.

Constructors

El 

Fields

Instances

Instances details
Pretty Type Source # 
Instance details

Defined in Agda.Syntax.Internal

TelToArgs ListTel Source # 
Instance details

Defined in Agda.Syntax.Internal

TelToArgs Telescope Source # 
Instance details

Defined in Agda.Syntax.Internal

GetDefs Telescope Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Type Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike Type Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

AllMetas Type Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

Reify Telescope Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope Source #

Reify Type Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Type Source #

TerSetSizeDepth ListTel Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

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

TerSetSizeDepth Telescope Source # 
Instance details

Defined in Agda.Termination.Monad

AbsTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy Type Source #

Ignores sorts.

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

CheckInternal Type Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

DropArgs Telescope Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Defined in Agda.TypeChecking.DropArgs

PrecomputeFreeVars Type Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

ForceNotFree Type Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

MentionsMeta Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

AnyRigid Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

AddContext Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

UnFreezeMeta Type Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

ComputeOccurrences Type Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

PrettyTCM Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Type Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrimTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Type -> TCM Term Source #

PrimType Type Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primType :: Type -> TCM Type Source #

ToTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Reduce Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Type Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

TeleNoAbs ListTel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

TeleNoAbs Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Type Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

SynEq Type Source #

Syntactic equality ignores sorts.

Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

NFData Type Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Type -> () #

Match NLPType Type Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

NLPatToTerm NLPType Type Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

PatternFrom Type NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Conversion TOM Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

Conversion MOT (Exp O) Type Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type Source #

LensSort (Type' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

SgTel (Dom Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

SgTel (Dom (ArgName, Type)) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal.Names

Methods

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

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.TypeChecking.Irrelevance

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

Defined in Agda.TypeChecking.Irrelevance

Occurs (Abs Type) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

AddContext (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Dom Type -> Nat Source #

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Dom (String, Type)) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames Telescope) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Monad.SizedTypes

PrettyTCM (Arg Type) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Type' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

ToTerm (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

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

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

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

Decoration (Type'' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable (Type'' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: Type'' t a -> Bool #

length :: Type'' t a -> Int #

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

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

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

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

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

Traversable (Type'' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor (Type'' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

Syntactic Type equality, ignores sort annotations.

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

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) Source # 
Instance details

Defined in Agda.Syntax.Internal

AddContext (Name, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Monad.Context

AddContext (Text, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Context

IsMeta a => IsMeta (Type'' t a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

(Coercible a Term, Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Type'' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Type'' a b) Source #

Methods

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

(Show t, Show a) => Show (Type'' t a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

show :: Type'' t a -> String #

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

type TypeOf Type Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf Type = ()
type ReifiesTo Telescope Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Type Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type TypeOf (Abs Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

type SubstArg (Type'' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

data Sort' t Source #

Sorts.

Constructors

Univ Univ (Level' t)

Prop ℓ, Set ℓ, SSet ℓ.

Inf Univ !Integer

Propωᵢ, (S)Setωᵢ.

SizeUniv

SizeUniv, a sort inhabited by type Size.

LockUniv

LockUniv, a sort for locks.

LevelUniv

LevelUniv, a sort inhabited by type Level. When --level-universe isn't on, this universe reduces to Set 0

IntervalUniv

IntervalUniv, a sort inhabited by the cubical interval.

PiSort (Dom' t t) (Sort' t) (Abs (Sort' t))

Sort of the pi type.

FunSort (Sort' t) (Sort' t)

Sort of a (non-dependent) function type.

UnivSort (Sort' t)

Sort of another sort.

MetaS !MetaId [Elim' t] 
DefS QName [Elim' t]

A postulated sort.

DummyS String

A (part of a) term or type which is only used for internal purposes. Replaces the abuse of Prop for a dummy sort. The String typically describes the location where we create this dummy, but can contain other information as well.

Instances

Instances details
Pretty Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

LensSort Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

GetDefs Sort Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike Sort Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

AllMetas Sort Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

NamesIn Sort Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

KillRange Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

Reify Sort Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Sort Source #

AbsTerm Sort Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy Sort Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

CheckInternal Sort Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

Free Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

PrecomputeFreeVars Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

ForceNotFree Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

UsableModality Sort Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableRelevance Sort Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

MentionsMeta Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

AnyRigid Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

UnFreezeMeta Sort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

PrettyTCM Sort Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

Instantiate Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Sort -> ReduceM Sort

EmbPrj Sort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Abstract Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

SynEq Sort Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

NFData Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Sort -> () #

Eq Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Ord Sort Source # 
Instance details

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 #

Match NLPSort Sort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

NLPatToTerm NLPSort Sort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

PatternFrom Sort NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Sort' a) Source #

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

Defined in Agda.Syntax.Internal

Methods

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

show :: Sort' t -> String #

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

type TypeOf Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf Sort = ()
type ReifiesTo Sort Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type SubstArg (Sort' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Sort' a) = SubstArg a

type Type' a = Type'' Term a Source #

data Tele a Source #

Sequence of types. An argument of the first type is bound in later types and so on.

Constructors

EmptyTel 
ExtendTel a (Abs (Tele a))

Abs is never NoAbs.

Instances

Instances details
TelToArgs Telescope Source # 
Instance details

Defined in Agda.Syntax.Internal

GetDefs Telescope Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

Reify Telescope Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope Source #

TerSetSizeDepth Telescope Source # 
Instance details

Defined in Agda.Termination.Monad

DropArgs Telescope Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Defined in Agda.TypeChecking.DropArgs

AddContext Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

PrettyTCM Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Reduce Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

TeleNoAbs Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Foldable Tele Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

toList :: Tele a -> [a] #

null :: Tele a -> Bool #

length :: Tele a -> Int #

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

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

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

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

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

Traversable Tele Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor Tele Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike a => AllMetas (Tele a) Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

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

Defined in Agda.Syntax.Internal.Names

Methods

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

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

MentionsMeta a => MentionsMeta (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

AddContext (KeepNames Telescope) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Positivity

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

Defined in Agda.TypeChecking.Reduce

Methods

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

(Subst a, InstantiateFull a) => InstantiateFull (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

(Subst a, Normalise a) => Normalise (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

(Subst a, Simplify a) => Simplify (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Tele a -> S Int32 Source #

icod_ :: Tele a -> S Int32 Source #

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

TermSubst a => Apply (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Tele a -> Args -> Tele a Source #

applyE :: Tele a -> Elims -> Tele a Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Tele a) Source #

Null (Tele a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

empty :: Tele a Source #

null :: Tele a -> Bool Source #

Sized (Tele a) Source #

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

Instance details

Defined in Agda.Syntax.Internal

Methods

size :: Tele a -> Int Source #

natSize :: Tele a -> Peano Source #

Generic (Tele a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

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

Methods

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

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

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

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Tele a -> ShowS #

show :: Tele a -> String #

showList :: [Tele a] -> ShowS #

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

Defined in Agda.Syntax.Internal

Methods

rnf :: Tele a -> () #

(Subst a, Eq a) => Eq (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

(Subst a, Ord a) => Ord (Tele a) Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type SubstArg (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Tele a) = SubstArg a
type Rep (Tele a) Source # 
Instance details

Defined in Agda.Syntax.Internal

type Rep (Tele a) = D1 ('MetaData "Tele" "Agda.Syntax.Internal" "Agda-2.6.3.20230914-inplace" 'False) (C1 ('MetaCons "EmptyTel" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExtendTel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Abs (Tele a)))))

data UnivSize Source #

Constructors

USmall

PropSetSSet ℓ.

ULarge

(PropSetSSet)ωᵢ.

Instances

Instances details
Show UnivSize Source # 
Instance details

Defined in Agda.Syntax.Internal

Eq UnivSize Source # 
Instance details

Defined in Agda.Syntax.Internal

data Level' t Source #

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

Instances details
Pretty Level Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize Level Source # 
Instance details

Defined in Agda.Syntax.Internal

GetDefs Level Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike Level Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

AllMetas Level Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

NamesIn Level Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

KillRange Level Source # 
Instance details

Defined in Agda.Syntax.Internal

Reify Level Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Level Source #

AbsTerm Level Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy Level Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

CheckInternal Level Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

Free Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

PrecomputeFreeVars Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

ForceNotFree Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

UsableModality Level Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableRelevance Level Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

MentionsMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

AnyRigid Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

IsInstantiatedMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

UnFreezeMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

ComputeOccurrences Level Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

PrettyTCM Level Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

Instantiate Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

EmbPrj Level Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

DeBruijn Level Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

SynEq Level Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

Foldable Level' Source # 
Instance details

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' Source # 
Instance details

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' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

NFData Level Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Level -> () #

Eq Level Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Ord Level Source # 
Instance details

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 #

Match NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

NLPatToTerm NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

PatternFrom Level NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

IsMeta a => IsMeta (Level' a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Subst a => Subst (Level' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Level' a) Source #

Show t => Show (Level' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

show :: Level' t -> String #

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

type TypeOf Level Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf Level = ()
type ReifiesTo Level Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type SubstArg (Level' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Level' a) = SubstArg a

data PlusLevel' t Source #

Constructors

Plus !Integer t 

Instances

Instances details
Pretty PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

GetDefs PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

AllMetas PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

NamesIn PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

KillRange PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

AbsTerm PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

EqualSy PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

CheckInternal PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

PrecomputeFreeVars PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

ForceNotFree PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

UsableRelevance PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

MentionsMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

AnyRigid PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

IsInstantiatedMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

UnFreezeMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

ComputeOccurrences PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

InstantiateFull PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

EmbPrj PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

DeBruijn PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

SynEq PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Foldable PlusLevel' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: PlusLevel' a -> Bool #

length :: PlusLevel' a -> Int #

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

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

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

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

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

Traversable PlusLevel' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor PlusLevel' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

NFData PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: PlusLevel -> () #

Eq PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Ord PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Free t => Free (PlusLevel' t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Instantiate t => Instantiate (PlusLevel' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

IsMeta a => IsMeta (PlusLevel' a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst a => Subst (PlusLevel' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (PlusLevel' a) Source #

Show t => Show (PlusLevel' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf PlusLevel = ()
type TypeOf [PlusLevel] Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf [PlusLevel] = ()
type SubstArg (PlusLevel' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

newtype BraveTerm Source #

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

Constructors

BraveTerm 

Fields

type Blocked_ = Blocked () Source #

'Blocked a without the a.

type NAPs = [NamedArg DeBruijnPattern] Source #

Named pattern arguments.

type PatVarName = ArgName Source #

Pattern variables.

data PatternInfo Source #

Constructors

PatternInfo 

Instances

Instances details
KillRange PatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

EmbPrj PatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Generic PatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep PatternInfo :: Type -> Type #

Show PatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

NFData PatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: PatternInfo -> () #

Eq PatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

type Rep PatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

type Rep PatternInfo = D1 ('MetaData "PatternInfo" "Agda.Syntax.Internal" "Agda-2.6.3.20230914-inplace" 'False) (C1 ('MetaCons "PatternInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "patOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatOrigin) :*: S1 ('MetaSel ('Just "patAsNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])))

data PatOrigin Source #

Origin of the pattern: what did the user write in this position?

Constructors

PatOSystem

Pattern inserted by the system

PatOSplit

Pattern generated by case split

PatOVar Name

User wrote a variable pattern

PatODot

User wrote a dot pattern

PatOWild

User wrote a wildcard pattern

PatOCon

User wrote a constructor pattern

PatORec

User wrote a record pattern

PatOLit

User wrote a literal pattern

PatOAbsurd

User wrote an absurd pattern

Instances

Instances details
KillRange PatOrigin Source # 
Instance details

Defined in Agda.Syntax.Internal

EmbPrj PatOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Generic PatOrigin Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep PatOrigin :: Type -> Type #

Show PatOrigin Source # 
Instance details

Defined in Agda.Syntax.Internal

NFData PatOrigin Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: PatOrigin -> () #

Eq PatOrigin Source # 
Instance details

Defined in Agda.Syntax.Internal

type Rep PatOrigin Source # 
Instance details

Defined in Agda.Syntax.Internal

type Rep PatOrigin = D1 ('MetaData "PatOrigin" "Agda.Syntax.Internal" "Agda-2.6.3.20230914-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 Pattern' x Source #

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

Constructors

VarP PatternInfo x
x
DotP PatternInfo Term
.t
ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]

c ps The subpatterns do not contain any projection copatterns.

LitP PatternInfo Literal

E.g. 5, "hello".

ProjP ProjOrigin QName

Projection copattern. Can only appear by itself.

IApplyP PatternInfo Term Term x

Path elimination pattern, like VarP but keeps track of endpoints.

DefP PatternInfo QName [NamedArg (Pattern' x)]

Used for HITs, the QName should be the one from primHComp.

Instances

Instances details
UsableSizeVars DeBruijnPattern Source # 
Instance details

Defined in Agda.Termination.Monad

UsableSizeVars MaskedDeBruijnPatterns Source # 
Instance details

Defined in Agda.Termination.Monad

Reduce DeBruijnPattern Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst DeBruijnPattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg DeBruijnPattern Source #

Subst Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Pattern Source #

Subst SplitPattern Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

Associated Types

type SubstArg SplitPattern Source #

Foldable Pattern' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: Pattern' a -> Bool #

length :: Pattern' a -> Int #

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

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

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

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

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

Traversable Pattern' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor Pattern' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

LabelPatVars Pattern DeBruijnPattern Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel DeBruijnPattern Source #

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

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

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

Instance details

Defined in Agda.Syntax.Internal.Pattern

PatternLike a (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

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

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

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

Defined in Agda.TypeChecking.Patterns.Internal

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

Defined in Agda.Auto.Convert

Methods

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

IsProjP (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

Associated Types

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

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

Defined in Agda.Syntax.Internal

Associated Types

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

NamesIn (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

CountPatternVars (Pattern' x) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

PatternVarModalities (Pattern' x) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar (Pattern' x) Source #

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

Defined in Agda.Syntax.Internal

UsableSizeVars (Masked DeBruijnPattern) Source # 
Instance details

Defined in Agda.Termination.Monad

UsableSizeVars [DeBruijnPattern] Source # 
Instance details

Defined in Agda.Termination.Monad

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

Defined in Agda.TypeChecking.Pretty

Methods

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

NormaliseProjP (Pattern' x) Source # 
Instance details

Defined in Agda.TypeChecking.Records

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

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Reduce

IsFlexiblePattern (Pattern' a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.TypeChecking.Telescope.Path

Methods

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

Generic (Pattern' x) Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

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

Methods

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

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

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

Defined in Agda.Syntax.Internal

Methods

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

show :: Pattern' x -> String #

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

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

Defined in Agda.Syntax.Internal

Methods

rnf :: Pattern' x -> () #

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

Defined in Agda.TypeChecking.Rewriting.Clause

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

Defined in Agda.TypeChecking.Rewriting.Clause

type PatVarLabel DeBruijnPattern Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

type SubstArg DeBruijnPattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg SplitPattern Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

type PatVar (Pattern' x) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

type PatVar (Pattern' x) = x
type Rep (Pattern' x) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

data ConPatternInfo Source #

The ConPatternInfo states whether the constructor belongs to a record type (True) or data type (False). In the former case, the PatOrigin of the conPInfo says whether the record pattern orginates from the expansion of an implicit pattern. The Type is the type of the whole record pattern. The scope used for the type is given by any outer scope plus the clause's telescope (clauseTel).

Constructors

ConPatternInfo 

Fields

  • conPInfo :: PatternInfo

    Information on the origin of the pattern.

  • conPRecord :: Bool

    False if data constructor. True if record constructor.

  • conPFallThrough :: Bool

    Should the match block on non-canonical terms or can it proceed to the catch-all clause?

  • conPType :: Maybe (Arg Type)

    The type of the whole constructor pattern. Should be present (Just) if constructor pattern is is generated ordinarily by type-checking. Could be absent (Nothing) if pattern comes from some plugin (like Agsy). Needed e.g. for with-clause stripping.

  • conPLazy :: Bool

    Lazy patterns are generated by the forcing translation in the unifier (unifyStep) and are dropped by the clause compiler (TODO: not yet) (compileClauses) when the variables they bind are unused. The GHC backend compiles lazy matches to lazy patterns in Haskell (TODO: not yet).

Instances

Instances details
KillRange ConPatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

InstantiateFull ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

EmbPrj ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Subst ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ConPatternInfo Source #

Generic ConPatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep ConPatternInfo :: Type -> Type #

Show ConPatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

NFData ConPatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: ConPatternInfo -> () #

type SubstArg ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type Rep ConPatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Type used when numbering pattern variables.

Constructors

DBPatVar 

Instances

Instances details
Pretty DBPatVar Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange DBPatVar Source # 
Instance details

Defined in Agda.Syntax.Internal

UsableSizeVars DeBruijnPattern Source # 
Instance details

Defined in Agda.Termination.Monad

UsableSizeVars MaskedDeBruijnPatterns Source # 
Instance details

Defined in Agda.Termination.Monad

PrettyTCM DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

InstantiateFull DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce DeBruijnPattern Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

EmbPrj DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Subst DeBruijnPattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg DeBruijnPattern Source #

DeBruijn DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

Generic DBPatVar Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Internal

NFData DBPatVar Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: DBPatVar -> () #

Eq DBPatVar Source # 
Instance details

Defined in Agda.Syntax.Internal

LabelPatVars Pattern DeBruijnPattern Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel DeBruijnPattern Source #

UsableSizeVars (Masked DeBruijnPattern) Source # 
Instance details

Defined in Agda.Termination.Monad

UsableSizeVars [DeBruijnPattern] Source # 
Instance details

Defined in Agda.Termination.Monad

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

Defined in Agda.TypeChecking.Rewriting.Clause

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

Defined in Agda.TypeChecking.Rewriting.Clause

type PatVarLabel DeBruijnPattern Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

type SubstArg DeBruijnPattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type Rep DBPatVar Source # 
Instance details

Defined in Agda.Syntax.Internal

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

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

Associated Types

type PatternVarOut a Source #

Instances

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

Defined in Agda.Syntax.Internal

Associated Types

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

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

Defined in Agda.Syntax.Internal

Associated Types

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

PatternVars a => PatternVars [a] Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut [a] Source #

Methods

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

data EqualityView Source #

View type as equality type.

Instances

Instances details
TermLike EqualityView Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

Free EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

EqualityUnview EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

PrettyTCM EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Instantiate EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg EqualityView Source #

type SubstArg EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data EqualityTypeData Source #

Constructors

EqualityTypeData 

Fields

data PathView Source #

View type as path type.

Constructors

PathType 

Fields

OType Type

reduced

data IntervalView Source #

Constructors

IZero 
IOne 
IMin (Arg Term) (Arg Term) 
IMax (Arg Term) (Arg Term) 
INeg (Arg Term) 
OTerm Term 

Instances

Instances details
Show IntervalView Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Telescope as list.

class TelToArgs a where Source #

Drop the types from a telescope.

Methods

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

Instances

Instances details
TelToArgs ListTel Source # 
Instance details

Defined in Agda.Syntax.Internal

TelToArgs Telescope Source # 
Instance details

Defined in Agda.Syntax.Internal

class SgTel a where Source #

Constructing a singleton telescope.

Methods

sgTel :: a -> Telescope Source #

Instances

Instances details
SgTel (Dom Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

SgTel (Dom (ArgName, Type)) Source # 
Instance details

Defined in Agda.Syntax.Internal

SgTel (ArgName, Dom Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

class Suggest a where Source #

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

Instances

Instances details
Suggest Name Source # 
Instance details

Defined in Agda.Syntax.Internal

Suggest Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Suggest String Source # 
Instance details

Defined in Agda.Syntax.Internal

Suggest (Abs b) Source # 
Instance details

Defined in Agda.Syntax.Internal

data Suggestion Source #

Constructors

forall a.Suggest a => Suggestion a 

type family TypeOf a Source #

Instances

Instances details
type TypeOf Elims Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf Elims = (Type, Elims -> Term)
type TypeOf Level Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf Level = ()
type TypeOf PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf PlusLevel = ()
type TypeOf Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf Sort = ()
type TypeOf Term Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf Type Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf Type = ()
type TypeOf NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type TypeOf (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Arg a) = Dom (TypeOf a)
type TypeOf (Abs Term) Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Abs Term) = (Dom Type, Abs Type)
type TypeOf (Abs Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Dom a) Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf (Dom a) = TypeOf a
type TypeOf [PlusLevel] Source # 
Instance details

Defined in Agda.Syntax.Internal

type TypeOf [PlusLevel] = ()
type TypeOf [Elim' NLPat] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type TypeOf [Elim' NLPat] = (Type, Elims -> Term)

pattern Type :: Level' t -> Sort' t Source #

pattern Prop :: Level' t -> Sort' t Source #

pattern SSet :: Level' t -> Sort' t Source #

pattern ClosedLevel :: Integer -> Level Source #

Constant level n

varP :: a -> Pattern' a Source #

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

Convert a telescope to its list form.

arity :: Type -> Nat Source #

Doesn't do any reduction.

dontCare :: Term -> Term Source #

Add DontCare is it is not already a DontCare.

argFromDom :: Dom' t a -> Arg a Source #

isStrictDataSort :: Sort' t -> Bool Source #

Is this a strict universe inhabitable by data types?

absurdP :: Int -> DeBruijnPattern Source #

Make an absurd pattern with the given de Bruijn index.

patternInfo :: Pattern' x -> Maybe PatternInfo Source #

Retrieve the PatternInfo from a pattern

patternOrigin :: Pattern' x -> Maybe PatOrigin Source #

Retrieve the origin of a pattern

properlyMatching :: Pattern' a -> Bool Source #

Does the pattern perform a match that could fail?

properlyMatching' Source #

Arguments

:: Bool

Should absurd patterns count as proper match?

-> Bool

Should projection patterns count as proper match?

-> Pattern' a

The pattern.

-> Bool 

absurdBody :: Abs Term Source #

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

var :: Nat -> Term Source #

An unapplied variable.

dummyLocName :: CallStack -> String Source #

Construct a string representing the call-site that created the dummy thing.

dummyTermWith :: DummyTermKind -> CallStack -> Term Source #

Aux: A dummy term to constitute a dummy termlevelsort/type.

dummyLevel :: CallStack -> Level Source #

A dummy level to constitute a level/sort created at location. Note: use macro DUMMY_LEVEL !

dummyTerm :: CallStack -> Term Source #

A dummy term created at location. Note: use macro DUMMY_TERM !

dummySort :: CallStack -> Sort Source #

A dummy sort created at location. Note: use macro DUMMY_SORT !

dummyType :: CallStack -> Type Source #

A dummy type created at location. Note: use macro DUMMY_TYPE !

dummyDom :: CallStack -> Dom Type Source #

Context entries without a type have this dummy type. Note: use macro DUMMY_DOM !

levelPlus :: Integer -> Level -> Level Source #

Given a constant m and level l, compute m + l

mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a) Source #

A traversal for the names in a telescope.

telFromList :: ListTel -> Telescope Source #

Convert a list telescope to a telescope.

listTel :: Lens' Telescope ListTel Source #

Lens to edit a Telescope as a list.

stripDontCare :: Term -> Term Source #

Removing a topmost DontCare constructor.

unSpine :: Term -> Term Source #

Convert top-level postfix projections into prefix projections.

unSpine' :: (ProjOrigin -> Bool) -> Term -> Term Source #

Convert Proj projection eliminations according to their ProjOrigin into Def projection applications.

hasElims :: Term -> Maybe (Elims -> Term, Elims) Source #

A view distinguishing the neutrals Var, Def, and MetaV which can be projected.

pDom :: LensHiding a => a -> Doc -> Doc Source #

data MetaId Source #

Meta-variable identifiers use the same structure as NameIds.

Constructors

MetaId 

Instances

Instances details
EncodeTCM MetaId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Pretty MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

GetDefs MetaId Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => MetaId -> m () Source #

NamesIn MetaId Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> MetaId -> m Source #

Reify MetaId Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo MetaId Source #

HasFresh MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

IsInstantiatedMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

UnFreezeMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source #

PrettyTCM MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => MetaId -> m Doc Source #

FromTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimType MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

EmbPrj MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Unquote MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Enum MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Generic MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep MetaId :: Type -> Type #

Methods

from :: MetaId -> Rep MetaId x #

to :: Rep MetaId x -> MetaId #

Show MetaId Source #

The record selectors are not included in the resulting strings.

Instance details

Defined in Agda.Syntax.Common

NFData MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: MetaId -> () #

Eq MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(==) :: MetaId -> MetaId -> Bool #

(/=) :: MetaId -> MetaId -> Bool #

Ord MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Hashable MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

hashWithSalt :: Int -> MetaId -> Int

hash :: MetaId -> Int

ToJSON MetaId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Singleton MetaId MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Singleton MetaId () Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

singleton :: MetaId -> () Source #

InstantiateFull (Judgement MetaId) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

type ReifiesTo MetaId Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type Rep MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep MetaId = D1 ('MetaData "MetaId" "Agda.Syntax.Common" "Agda-2.6.3.20230914-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 Source #

A "problem" consists of a set of constraints and the same constraint can be part of multiple problems.

Constructors

ProblemId Nat 

Instances

Instances details
EncodeTCM ProblemId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Pretty ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

HasFresh ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Enum ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Num ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Integral ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Real ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Show ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

NFData ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: ProblemId -> () #

Eq ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Ord ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

ToJSON ProblemId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Monad m => MonadFresh ProblemId (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Orphan instances

NFData IsFibrant Source # 
Instance details

Methods

rnf :: IsFibrant -> () #