Agda.Syntax.Internal

Documentation

type Args = [Arg Term]

Type of argument lists.

type Type = Type' Term

data Clause

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

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

clauseTel ~ permute clausePerm (patternVars namedClausePats)

Terms in dot patterns are valid in the clause telescope.

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

Constructors

Clause

Fields

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

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

• namedClausePats :: NAPs

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

• clauseBody :: Maybe Term

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

• clauseType :: Maybe (Arg Type)

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

• clauseCatchall :: Bool

  Clause has been labelled as CATCHALL.

• clauseExact :: Maybe Bool

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

• clauseRecursive :: Maybe Bool

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

• clauseUnreachable :: Maybe Bool

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

• clauseEllipsis :: ExpandedEllipsis

  Was this clause created by expansion of an ellipsis?

• clauseWhereModule :: Maybe ModuleName

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

Instances

Pretty Clause

Defined in Agda.Syntax.Internal

Methods

pretty :: Clause -> Doc

prettyPrec :: Int -> Clause -> Doc

prettyList :: [Clause] -> Doc

GetDefs Clause

Defined in Agda.Syntax.Internal.Defs

Methods

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

NamesIn Clause

Defined in Agda.Syntax.Internal.Names

Methods

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

FunArity Clause

Get the number of initial Apply patterns in a clause.

Defined in Agda.Syntax.Internal.Pattern

Methods

funArity :: Clause -> Int

HasRange Clause

Defined in Agda.Syntax.Internal

Methods

getRange :: Clause -> Range

KillRange Clause

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Clause

DropArgs Clause

NOTE: does not work for recursive functions.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Clause -> Clause

DropArgs FunctionInverse

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> FunctionInverse -> FunctionInverse

Free Clause

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Occurs Clause

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Clause -> OccursM Clause

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

ComputeOccurrences Clause

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Clause -> OccM OccurrencesBuilder

PrettyTCM Clause

Defined in Agda.TypeChecking.Pretty

Methods

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

NormaliseProjP Clause

Defined in Agda.TypeChecking.Records

Methods

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

InstantiateFull Clause

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Clause -> ReduceM Clause

InstantiateFull FunctionInverse

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse

EmbPrj Clause

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Clause -> S Int32

icod_ :: Clause -> S Int32

value :: Int32 -> R Clause

Abstract Clause

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Clause -> Clause

Abstract FunctionInverse

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> FunctionInverse -> FunctionInverse

Apply Clause

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Clause -> Args -> Clause

applyE :: Clause -> Elims -> Clause

Apply FunctionInverse

Defined in Agda.TypeChecking.Substitute

Methods

apply :: FunctionInverse -> Args -> FunctionInverse

applyE :: FunctionInverse -> Elims -> FunctionInverse

Null Clause

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

Defined in Agda.Syntax.Internal

Methods

empty :: Clause

null :: Clause -> Bool

Generic Clause

Defined in Agda.Syntax.Internal

Associated Types

type Rep Clause :: Type -> Type

Methods

from :: Clause -> Rep Clause x

to :: Rep Clause x -> Clause

Show Clause

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Clause -> ShowS

show :: Clause -> String

showList :: [Clause] -> ShowS

NFData Clause

Defined in Agda.Syntax.Internal

Methods

rnf :: Clause -> ()

FunArity [Clause]

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

Defined in Agda.Syntax.Internal.Pattern

Methods

funArity :: [Clause] -> Int

Reify (QNamed Clause)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (QNamed Clause)

Methods

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

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

PrettyTCM (QNamed Clause)

Defined in Agda.TypeChecking.Pretty

Methods

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

type Rep Clause

Defined in Agda.Syntax.Internal

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

type ReifiesTo (QNamed Clause)

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (QNamed Clause) = Clause

data Term

Raw values.

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

Constructors

Var !Int Elims

x es neutral

Lam ArgInfo (Abs Term)

Terms are beta normal. Relevance is ignored

Lit Literal

Def QName Elims

f es, possibly a delta/iota-redex

Con ConHead ConInfo Elims

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

Pi (Dom Type) (Abs Type)

dependent or non-dependent function space

Sort Sort

Level Level

MetaV !MetaId Elims

DontCare Term

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

Dummy String Elims

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

Instances

Pretty Level

Defined in Agda.Syntax.Internal

Methods

pretty :: Level -> Doc

prettyPrec :: Int -> Level -> Doc

prettyList :: [Level] -> Doc

Pretty PlusLevel

Defined in Agda.Syntax.Internal

Methods

pretty :: PlusLevel -> Doc

prettyPrec :: Int -> PlusLevel -> Doc

prettyList :: [PlusLevel] -> Doc

Pretty Sort

Defined in Agda.Syntax.Internal

Methods

pretty :: Sort -> Doc

prettyPrec :: Int -> Sort -> Doc

prettyList :: [Sort] -> Doc

Pretty Term

Defined in Agda.Syntax.Internal

Methods

pretty :: Term -> Doc

prettyPrec :: Int -> Term -> Doc

prettyList :: [Term] -> Doc

Pretty Type

Defined in Agda.Syntax.Internal

Methods

pretty :: Type -> Doc

prettyPrec :: Int -> Type -> Doc

prettyList :: [Type] -> Doc

Pretty CompiledClauses

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: CompiledClauses -> Doc

prettyPrec :: Int -> CompiledClauses -> Doc

prettyList :: [CompiledClauses] -> Doc

LensSort Sort

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort Sort

getSort :: Sort -> Sort

Suggest Term

Defined in Agda.Syntax.Internal

Methods

suggestName :: Term -> Maybe String

TelToArgs ListTel

Defined in Agda.Syntax.Internal

Methods

telToArgs :: ListTel -> [Arg ArgName]

TelToArgs Telescope

Defined in Agda.Syntax.Internal

Methods

telToArgs :: Telescope -> [Arg ArgName]

TermSize Level

Defined in Agda.Syntax.Internal

Methods

termSize :: Level -> Int

tsize :: Level -> Sum Int

TermSize PlusLevel

Defined in Agda.Syntax.Internal

Methods

termSize :: PlusLevel -> Int

tsize :: PlusLevel -> Sum Int

TermSize Sort

Defined in Agda.Syntax.Internal

Methods

termSize :: Sort -> Int

tsize :: Sort -> Sum Int

TermSize Term

Defined in Agda.Syntax.Internal

Methods

termSize :: Term -> Int

tsize :: Term -> Sum Int

GetDefs Level

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs PlusLevel

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Sort

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Telescope

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Term

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Type

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike Level

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike PlusLevel

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike Sort

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike Term

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike Type

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

AllMetas Level

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas PlusLevel

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Sort

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Term

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

AllMetas Type

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

NamesIn Level

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn PlusLevel

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn Sort

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn Term

Defined in Agda.Syntax.Internal.Names

Methods

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

NamesIn CompiledClauses

Defined in Agda.Syntax.Internal.Names

Methods

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

KillRange Level

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Level

KillRange PlusLevel

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PlusLevel

KillRange Sort

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Sort

KillRange Substitution

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Substitution

KillRange Term

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Term

KillRange CompiledClauses

Defined in Agda.TypeChecking.CompiledClause

Methods

killRange :: KillRangeT CompiledClauses

Reify Level

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Level

Methods

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

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

Reify Sort

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Sort

Methods

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

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

Reify Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope

Methods

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

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

Reify Term

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Term

Methods

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

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

Reify Type

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Type

Methods

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

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

TerSetSizeDepth ListTel

Defined in Agda.Termination.Monad

Methods

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

TerSetSizeDepth Telescope

Defined in Agda.Termination.Monad

Methods

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

AbsTerm Level

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Level -> Level

AbsTerm PlusLevel

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> PlusLevel -> PlusLevel

AbsTerm Sort

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Sort -> Sort

AbsTerm Term

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Term -> Term

AbsTerm Type

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Type -> Type

EqualSy Level

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Level -> Level -> Bool

EqualSy PlusLevel

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: PlusLevel -> PlusLevel -> Bool

EqualSy Sort

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Sort -> Sort -> Bool

EqualSy Term

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Term -> Term -> Bool

EqualSy Type

Ignores sorts.

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Type -> Type -> Bool

IsPrefixOf Args

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Args -> Args -> Maybe Elims

IsPrefixOf Elims

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Elims -> Elims -> Maybe Elims

IsPrefixOf Term

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Term -> Term -> Maybe Elims

CheckInternal Elims

Defined in Agda.TypeChecking.CheckInternal

Methods

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

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

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

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

CheckInternal Level

Defined in Agda.TypeChecking.CheckInternal

Methods

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

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

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

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

CheckInternal PlusLevel

Defined in Agda.TypeChecking.CheckInternal

Methods

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

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

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

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

CheckInternal Sort

Defined in Agda.TypeChecking.CheckInternal

Methods

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

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

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

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

CheckInternal Term

Defined in Agda.TypeChecking.CheckInternal

Methods

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

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

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

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

CheckInternal Type

Defined in Agda.TypeChecking.CheckInternal

Methods

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

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

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

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

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Telescope -> Telescope

DropArgs Term

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

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Term -> Term

DropArgs CompiledClauses

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

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> CompiledClauses -> CompiledClauses

Free Level

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Sort

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Term

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

PrecomputeFreeVars Level

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Level -> FV Level

PrecomputeFreeVars PlusLevel

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: PlusLevel -> FV PlusLevel

PrecomputeFreeVars Sort

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Sort -> FV Sort

PrecomputeFreeVars Term

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Term -> FV Term

PrecomputeFreeVars Type

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Type -> FV Type

ForceNotFree Level

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree PlusLevel

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree Sort

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree Term

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree Type

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

UsableModality Level

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableModality Sort

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableModality Term

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance Level

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance PlusLevel

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance Sort

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance Term

Defined in Agda.TypeChecking.Irrelevance

Methods

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

NoProjectedVar Term

Defined in Agda.TypeChecking.MetaVars

Methods

noProjectedVar :: Term -> Either ProjectedVar ()

ReduceAndEtaContract Term

Defined in Agda.TypeChecking.MetaVars

Methods

reduceAndEtaContract :: Term -> TCM Term

MentionsMeta Elim

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Elim -> Bool

MentionsMeta Level

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Level -> Bool

MentionsMeta PlusLevel

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> PlusLevel -> Bool

MentionsMeta Sort

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Sort -> Bool

MentionsMeta Term

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Term -> Bool

MentionsMeta Type

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Type -> Bool

AnyRigid Level

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

AnyRigid PlusLevel

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

AnyRigid Sort

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

AnyRigid Term

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

AnyRigid Type

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs Elims

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Elims -> OccursM Elims

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

Occurs Level

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Level -> OccursM Level

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

Occurs PlusLevel

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: PlusLevel -> OccursM PlusLevel

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

Occurs Sort

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Sort -> OccursM Sort

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

Occurs Term

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Term -> OccursM Term

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

Occurs Type

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Type -> OccursM Type

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

AddContext Telescope

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Telescope -> Nat

IsInstantiatedMeta Level

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

IsInstantiatedMeta PlusLevel

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

IsInstantiatedMeta Term

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta Level

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta PlusLevel

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta Sort

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta Term

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta Type

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

IsSizeType Term

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

ComputeOccurrences Level

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Level -> OccM OccurrencesBuilder

ComputeOccurrences PlusLevel

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: PlusLevel -> OccM OccurrencesBuilder

ComputeOccurrences Term

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Term -> OccM OccurrencesBuilder

ComputeOccurrences Type

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Type -> OccM OccurrencesBuilder

PrettyTCM Elim

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Level

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Sort

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Telescope

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Term

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Type

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ContextEntry

Defined in Agda.TypeChecking.Pretty

Methods

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

PrimTerm Type

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Type -> TCM Term

PrimType Type

Defined in Agda.TypeChecking.Primitive

Methods

primType :: Type -> TCM Type

ToTerm Term

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Term -> Term)

toTermR :: TCM (Term -> ReduceM Term)

ToTerm Type

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Type -> Term)

toTermR :: TCM (Type -> ReduceM Term)

Instantiate Level

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Level -> ReduceM Level

Instantiate Sort

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Sort -> ReduceM Sort

Instantiate Term

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Term -> ReduceM Term

InstantiateFull Level

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Level -> ReduceM Level

InstantiateFull PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: PlusLevel -> ReduceM PlusLevel

InstantiateFull Sort

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Sort -> ReduceM Sort

InstantiateFull Substitution

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Substitution -> ReduceM Substitution

InstantiateFull Term

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Term -> ReduceM Term

InstantiateFull CompiledClauses

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses

IsMeta Term

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Term -> Maybe MetaId

Normalise Level

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Level -> ReduceM Level

Normalise PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: PlusLevel -> ReduceM PlusLevel

Normalise Sort

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Sort -> ReduceM Sort

Normalise Term

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Term -> ReduceM Term

Reduce Elim

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Elim -> ReduceM Elim

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

Reduce Level

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Level -> ReduceM Level

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

Reduce PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: PlusLevel -> ReduceM PlusLevel

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

Reduce Sort

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Sort -> ReduceM Sort

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

Reduce Telescope

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Telescope -> ReduceM Telescope

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

Reduce Term

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Term -> ReduceM Term

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

Reduce Type

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Type -> ReduceM Type

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

Simplify Level

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Level -> ReduceM Level

Simplify PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: PlusLevel -> ReduceM PlusLevel

Simplify Sort

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Sort -> ReduceM Sort

Simplify Term

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Term -> ReduceM Term

GetMatchables Term

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Term -> [QName]

EmbPrj Blocked_

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Blocked_ -> S Int32

icod_ :: Blocked_ -> S Int32

value :: Int32 -> R Blocked_

EmbPrj Level

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Level -> S Int32

icod_ :: Level -> S Int32

value :: Int32 -> R Level

EmbPrj NotBlocked

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NotBlocked -> S Int32

icod_ :: NotBlocked -> S Int32

value :: Int32 -> R NotBlocked

EmbPrj PlusLevel

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PlusLevel -> S Int32

icod_ :: PlusLevel -> S Int32

value :: Int32 -> R PlusLevel

EmbPrj Sort

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Sort -> S Int32

icod_ :: Sort -> S Int32

value :: Int32 -> R Sort

EmbPrj Term

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Term -> S Int32

icod_ :: Term -> S Int32

value :: Int32 -> R Term

EmbPrj CompiledClauses

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompiledClauses -> S Int32

icod_ :: CompiledClauses -> S Int32

value :: Int32 -> R CompiledClauses

TeleNoAbs ListTel

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: ListTel -> Term -> Term

TeleNoAbs Telescope

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: Telescope -> Term -> Term

Abstract Sort

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Sort -> Sort

Abstract Telescope

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Telescope -> Telescope

Abstract Term

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Term -> Term

Abstract Type

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Type -> Type

Abstract CompiledClauses

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> CompiledClauses -> CompiledClauses

Apply Sort

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Sort -> Args -> Sort

applyE :: Sort -> Elims -> Sort

Apply Term

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Term -> Args -> Term

applyE :: Term -> Elims -> Term

Apply CompiledClauses

Defined in Agda.TypeChecking.Substitute

Methods

apply :: CompiledClauses -> Args -> CompiledClauses

applyE :: CompiledClauses -> Elims -> CompiledClauses

Subst Term

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Term

Methods

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

DeBruijn Level

Defined in Agda.TypeChecking.Substitute.DeBruijn

Methods

deBruijnVar :: Int -> Level

debruijnNamedVar :: String -> Int -> Level

deBruijnView :: Level -> Maybe Int

DeBruijn PlusLevel

Defined in Agda.TypeChecking.Substitute.DeBruijn

Methods

deBruijnVar :: Int -> PlusLevel

debruijnNamedVar :: String -> Int -> PlusLevel

deBruijnView :: PlusLevel -> Maybe Int

DeBruijn Term

We can substitute Terms for variables.

Defined in Agda.TypeChecking.Substitute.DeBruijn

Methods

deBruijnVar :: Int -> Term

debruijnNamedVar :: String -> Int -> Term

deBruijnView :: Term -> Maybe Int

SynEq Level

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq PlusLevel

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Sort

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Term

Syntactic term equality ignores DontCare stuff.

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Type

Syntactic equality ignores sorts.

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

PiApplyM Term

Defined in Agda.TypeChecking.Telescope

Methods

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

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

Show Term

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

NFData Level

Defined in Agda.Syntax.Internal

Methods

rnf :: Level -> ()

NFData PlusLevel

Defined in Agda.Syntax.Internal

Methods

rnf :: PlusLevel -> ()

NFData Sort

Defined in Agda.Syntax.Internal

Methods

rnf :: Sort -> ()

NFData Term

Defined in Agda.Syntax.Internal

Methods

rnf :: Term -> ()

NFData Type

Defined in Agda.Syntax.Internal

Methods

rnf :: Type -> ()

Eq Level

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq NotBlocked

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq PlusLevel

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq Sort

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq Substitution

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq Term

Syntactic Term equality, ignores stuff below DontCare and sharing.

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq SingleLevel

Defined in Agda.TypeChecking.Level

Methods

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

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

Ord Level

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Level -> Level -> Ordering

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

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

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

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

max :: Level -> Level -> Level

min :: Level -> Level -> Level

Ord PlusLevel

Defined in Agda.TypeChecking.Substitute

Methods

compare :: PlusLevel -> PlusLevel -> Ordering

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

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

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

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

max :: PlusLevel -> PlusLevel -> PlusLevel

min :: PlusLevel -> PlusLevel -> PlusLevel

Ord Sort

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Sort -> Sort -> Ordering

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

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

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

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

max :: Sort -> Sort -> Sort

min :: Sort -> Sort -> Sort

Ord Substitution

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Substitution -> Substitution -> Ordering

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

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

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

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

max :: Substitution -> Substitution -> Substitution

min :: Substitution -> Substitution -> Substitution

Ord Term

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Term -> Term -> Ordering

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

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

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

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

max :: Term -> Term -> Term

min :: Term -> Term -> Term

Match NLPSort Sort

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

Match NLPType Type

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

Match NLPat Level

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

Match NLPat Term

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

NLPatToTerm Nat Term

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

NLPatToTerm NLPSort Sort

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

NLPatToTerm NLPType Type

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

NLPatToTerm NLPat Level

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

NLPatToTerm NLPat Term

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

PatternFrom Level NLPat

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

PatternFrom Sort NLPSort

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

PatternFrom Term NLPat

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

PatternFrom Type NLPType

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

MonadError Blocked_ NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

throwError :: Blocked_ -> NLM a

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

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

Defined in Agda.TypeChecking.Patterns.Internal

Methods

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

PatternFrom Elims [Elim' NLPat]

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> TypeOf Elims -> Elims -> TCM [Elim' NLPat]

Pretty a => Pretty (Blocked a)

Defined in Agda.Syntax.Internal

Methods

pretty :: Blocked a -> Doc

prettyPrec :: Int -> Blocked a -> Doc

prettyList :: [Blocked a] -> Doc

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

Defined in Agda.Syntax.Internal

Methods

pretty :: Tele (Dom a) -> Doc

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

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

LensSort a => LensSort (Dom a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' (Dom a) Sort

getSort :: Dom a -> Sort

LensSort (Type' a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' (Type' a) Sort

getSort :: Type' a -> Sort

SgTel (Dom Type)

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom Type -> Telescope

SgTel (Dom (ArgName, Type))

Defined in Agda.Syntax.Internal

Methods

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

GetDefs a => GetDefs (Dom a)

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike a => TermLike (Blocked a)

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

TermLike a => TermLike (Dom a)

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

NamesIn a => NamesIn (Type' a)

Defined in Agda.Syntax.Internal.Names

Methods

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

KillRange a => KillRange (Blocked a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Blocked a)

KillRange a => KillRange (Type' a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Type' a)

Reify i => Reify (Dom i)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Dom i)

Methods

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

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

AbsTerm a => AbsTerm (Dom a)

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy a => EqualSy (Dom a)

Ignore the tactic.

Defined in Agda.TypeChecking.Abstract

Methods

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

Free t => Free (Dom t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free t => Free (Type' t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

PrecomputeFreeVars a => PrecomputeFreeVars (Dom a)

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

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

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

UsableModality a => UsableModality (Dom a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance a => UsableModality (Type' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance a => UsableRelevance (Dom a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance a => UsableRelevance (Type' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

MentionsMeta t => MentionsMeta (Dom t)

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

AnyRigid a => AnyRigid (Dom a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs (Abs Term)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

Occurs (Abs Type)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

Occurs a => Occurs (Dom a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

AddContext (Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Dom Type -> Nat

AddContext (Dom (Name, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Dom (String, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames Telescope)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: KeepNames Telescope -> Nat

IsSizeType a => IsSizeType (Dom a)

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

IsSizeType a => IsSizeType (Type' a)

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

ComputeOccurrences a => ComputeOccurrences (Dom a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Dom a -> OccM OccurrencesBuilder

PrettyTCM (Arg Term)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Arg Type)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (NamedArg Term)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Named_ Term)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM a => PrettyTCM (Blocked a)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Dom Type)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Type' NLPat)

Defined in Agda.TypeChecking.Pretty

Methods

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

ToTerm (Dom Type)

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Dom Type -> Term)

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

Instantiate a => Instantiate (Blocked a)

Defined in Agda.TypeChecking.Reduce

Methods

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

Instantiate t => Instantiate (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Reduce t => Reduce (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Simplify t => Simplify (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

GetMatchables a => GetMatchables (Dom a)

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Dom a -> [QName]

EmbPrj a => EmbPrj (Dom a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Int32

icod_ :: Dom a -> S Int32

value :: Int32 -> R (Dom a)

EmbPrj a => EmbPrj (Type' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Type' a -> S Int32

icod_ :: Type' a -> S Int32

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

Apply t => Apply (Blocked t)

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Subst a => Subst (Blocked a)

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Blocked a)

Methods

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

SynEq a => SynEq (Dom a)

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

Unquote a => Unquote (Dom a)

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Dom a)

NFData e => NFData (Dom e)

Defined in Agda.Syntax.Internal

Methods

rnf :: Dom e -> ()

Eq t => Eq (Blocked t)

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq a => Eq (Type' a)

Syntactic Type equality, ignores sort annotations.

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Ord a => Ord (Dom a)

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

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

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

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

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

Ord a => Ord (Type' a)

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

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

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

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

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

Match [Elim' NLPat] Elims

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Dom a -> Dom b

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

SgTel (ArgName, Dom Type)

Defined in Agda.Syntax.Internal

Methods

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

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Dom r, Name)

Methods

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

AddContext (Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 (Arg Name), Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 (NamedArg Name), Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 (WithHiding Name), Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Text, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([Arg Name], Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([NamedArg Name], Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([WithHiding Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

type TypeOf Elims

Defined in Agda.Syntax.Internal

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

type TypeOf Level

Defined in Agda.Syntax.Internal

type TypeOf Level = ()

type TypeOf PlusLevel

Defined in Agda.Syntax.Internal

type TypeOf PlusLevel = ()

type TypeOf Sort

Defined in Agda.Syntax.Internal

type TypeOf Sort = ()

type TypeOf Term

Defined in Agda.Syntax.Internal

type TypeOf Term = Type

type TypeOf Type

Defined in Agda.Syntax.Internal

type TypeOf Type = ()

type ReifiesTo Level

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Level = Expr

type ReifiesTo Sort

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Sort = Expr

type ReifiesTo Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Telescope = Telescope

type ReifiesTo Term

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Term = Expr

type ReifiesTo Type

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Type = Type

type SubstArg Term

Defined in Agda.TypeChecking.Substitute

type SubstArg Term = Term

type TypeOf (Abs Term)

Defined in Agda.Syntax.Internal

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

type TypeOf (Abs Type)

Defined in Agda.Syntax.Internal

type TypeOf (Abs Type) = Dom Type

type TypeOf (Dom a)

Defined in Agda.Syntax.Internal

type TypeOf (Dom a) = TypeOf a

type TypeOf [PlusLevel]

Defined in Agda.Syntax.Internal

type TypeOf [PlusLevel] = ()

type ReifiesTo (Dom i)

Defined in Agda.Syntax.Translation.InternalToAbstract

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

type SubstArg (Blocked a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Blocked a) = SubstArg a

type AbsOfRef (Dom r, Name)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Dom r, Name) = TypedBinding

type Pattern

Arguments

 = Pattern' PatVarName

The PatVarName is a name suggestion.

type Telescope = Tele (Dom Type)

type Substitution = Substitution' Term

data Dom' t e

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

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

cubical

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

Constructors

Dom

Fields

• domInfo :: ArgInfo
• domName :: Maybe NamedName

  e.g. x in {x = y : A} -> B.

• domIsFinite :: Bool

  Is this a Π-type (False), or a partial type (True)?

• domTactic :: Maybe t

  "@tactic e".

• unDom :: e

Instances

TelToArgs ListTel

Defined in Agda.Syntax.Internal

Methods

telToArgs :: ListTel -> [Arg ArgName]

TelToArgs Telescope

Defined in Agda.Syntax.Internal

Methods

telToArgs :: Telescope -> [Arg ArgName]

GetDefs Telescope

Defined in Agda.Syntax.Internal.Defs

Methods

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

Reify Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope

Methods

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

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

TerSetSizeDepth ListTel

Defined in Agda.Termination.Monad

Methods

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

TerSetSizeDepth Telescope

Defined in Agda.Termination.Monad

Methods

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

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Telescope -> Telescope

AddContext Telescope

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Telescope -> Nat

PrettyTCM Telescope

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ContextEntry

Defined in Agda.TypeChecking.Pretty

Methods

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

Reduce Telescope

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Telescope -> ReduceM Telescope

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

TeleNoAbs ListTel

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: ListTel -> Term -> Term

TeleNoAbs Telescope

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: Telescope -> Term -> Term

Abstract Telescope

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Telescope -> Telescope

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

Defined in Agda.Syntax.Internal

Methods

pretty :: Tele (Dom a) -> Doc

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

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

LensSort a => LensSort (Dom a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' (Dom a) Sort

getSort :: Dom a -> Sort

SgTel (Dom Type)

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom Type -> Telescope

SgTel (Dom (ArgName, Type))

Defined in Agda.Syntax.Internal

Methods

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

GetDefs a => GetDefs (Dom a)

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike a => TermLike (Dom a)

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

Reify i => Reify (Dom i)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Dom i)

Methods

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

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

AbsTerm a => AbsTerm (Dom a)

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy a => EqualSy (Dom a)

Ignore the tactic.

Defined in Agda.TypeChecking.Abstract

Methods

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

Free t => Free (Dom t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

PrecomputeFreeVars a => PrecomputeFreeVars (Dom a)

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

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

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

UsableModality a => UsableModality (Dom a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

UsableRelevance a => UsableRelevance (Dom a)

Defined in Agda.TypeChecking.Irrelevance

Methods

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

MentionsMeta t => MentionsMeta (Dom t)

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

AnyRigid a => AnyRigid (Dom a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs a => Occurs (Dom a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

AddContext (Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Dom Type -> Nat

AddContext (Dom (Name, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Dom (String, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames Telescope)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: KeepNames Telescope -> Nat

IsSizeType a => IsSizeType (Dom a)

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

ComputeOccurrences a => ComputeOccurrences (Dom a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Dom a -> OccM OccurrencesBuilder

PrettyTCM (Dom Type)

Defined in Agda.TypeChecking.Pretty

Methods

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

ToTerm (Dom Type)

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Dom Type -> Term)

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

Normalise t => Normalise (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Reduce t => Reduce (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Simplify t => Simplify (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

GetMatchables a => GetMatchables (Dom a)

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Dom a -> [QName]

EmbPrj a => EmbPrj (Dom a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Int32

icod_ :: Dom a -> S Int32

value :: Int32 -> R (Dom a)

SynEq a => SynEq (Dom a)

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

Unquote a => Unquote (Dom a)

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Dom a)

Decoration (Dom' t)

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable (Dom' t)

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: Dom' t a -> Bool

length :: Dom' t a -> Int

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

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

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

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

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

Traversable (Dom' t)

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor (Dom' t)

Defined in Agda.Syntax.Internal

Methods

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

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

NFData e => NFData (Dom e)

Defined in Agda.Syntax.Internal

Methods

rnf :: Dom e -> ()

Ord a => Ord (Dom a)

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

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

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

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

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

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

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Dom a -> Dom b

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

LensAnnotation (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getAnnotation :: Dom' t e -> Annotation

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

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

LensArgInfo (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getArgInfo :: Dom' t e -> ArgInfo

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

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

LensCohesion (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getCohesion :: Dom' t e -> Cohesion

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

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

LensFreeVariables (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getFreeVariables :: Dom' t e -> FreeVariables

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

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

LensHiding (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getHiding :: Dom' t e -> Hiding

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

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

LensLock (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getLock :: Dom' t e -> Lock

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

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

LensModality (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getModality :: Dom' t e -> Modality

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

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

LensNamed (Dom' t e)

Defined in Agda.Syntax.Internal

Associated Types

type NameOf (Dom' t e)

Methods

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

LensOrigin (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getOrigin :: Dom' t e -> Origin

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

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

LensQuantity (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getQuantity :: Dom' t e -> Quantity

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

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

LensRelevance (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

getRelevance :: Dom' t e -> Relevance

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

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

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

Defined in Agda.Syntax.Internal

Methods

pretty :: Dom' t e -> Doc

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

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

SgTel (ArgName, Dom Type)

Defined in Agda.Syntax.Internal

Methods

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

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

Defined in Agda.Syntax.Internal.MetaVars

Methods

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

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

Defined in Agda.Syntax.Internal.Names

Methods

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

HasRange a => HasRange (Dom' t a)

Defined in Agda.Syntax.Internal

Methods

getRange :: Dom' t a -> Range

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

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Dom' t a)

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Dom r, Name)

Methods

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

AddContext (Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 (WithHiding Name), Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Text, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([WithHiding Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Dom' a b)

Methods

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

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

Defined in Agda.Syntax.Internal

Methods

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

show :: Dom' t e -> String

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

Eq a => Eq (Dom' t a)

Ignores Origin and FreeVariables and tactic.

Defined in Agda.Syntax.Internal

Methods

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

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

type ReifiesTo Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Telescope = Telescope

type TypeOf (Dom a)

Defined in Agda.Syntax.Internal

type TypeOf (Dom a) = TypeOf a

type ReifiesTo (Dom i)

Defined in Agda.Syntax.Translation.InternalToAbstract

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

type NameOf (Dom' t e)

Defined in Agda.Syntax.Internal

type NameOf (Dom' t e) = NamedName

type AbsOfRef (Dom r, Name)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Dom r, Name) = TypedBinding

type SubstArg (Dom' a b)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Dom' a b) = SubstArg a

type Dom = Dom' Term

type Level = Level' Term

type Elim = Elim' Term

type Sort = Sort' Term

type DataOrRecord = DataOrRecord' PatternOrCopattern

data Substitution' a

Substitutions.

Constructors

IdS

Identity substitution. Γ ⊢ IdS : Γ

EmptyS Impossible

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

a :# (Substitution' a) infixr 4

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

Strengthen Impossible !Int (Substitution' a)

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

Wk !Int (Substitution' a)

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

Lift !Int (Substitution' a)

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

Instances

KillRange Substitution

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Substitution

InstantiateFull Substitution

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Substitution -> ReduceM Substitution

Foldable Substitution'

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

toList :: Substitution' a -> [a]

null :: Substitution' a -> Bool

length :: Substitution' a -> Int

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

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

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

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

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

Traversable Substitution'

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor Substitution'

Defined in Agda.Syntax.Internal

Methods

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

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

Eq Substitution

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Ord Substitution

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Substitution -> Substitution -> Ordering

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

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

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

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

max :: Substitution -> Substitution -> Substitution

min :: Substitution -> Substitution -> Substitution

Pretty a => Pretty (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

pretty :: Substitution' a -> Doc

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

prettyList :: [Substitution' a] -> Doc

TermSize a => TermSize (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

termSize :: Substitution' a -> Int

tsize :: Substitution' a -> Sum Int

NamesIn a => NamesIn (Substitution' a)

Defined in Agda.Syntax.Internal.Names

Methods

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

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

Defined in Agda.TypeChecking.Pretty

Methods

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

EmbPrj a => EmbPrj (Substitution' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Substitution' a -> S Int32

icod_ :: Substitution' a -> S Int32

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

EndoSubst a => Subst (Substitution' a)

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Substitution' a)

Methods

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

Null (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

empty :: Substitution' a

null :: Substitution' a -> Bool

Generic (Substitution' a)

Defined in Agda.Syntax.Internal

Associated Types

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

Methods

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

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

Show a => Show (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

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

show :: Substitution' a -> String

showList :: [Substitution' a] -> ShowS

NFData a => NFData (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

rnf :: Substitution' a -> ()

type SubstArg (Substitution' a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Substitution' a) = a

type Rep (Substitution' a)

Defined in Agda.Syntax.Internal

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

data Abs a

Binder.

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

Constructors

Abs

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

Fields

• absName :: ArgName
• unAbs :: a

NoAbs

Fields

• absName :: ArgName
• unAbs :: a

Instances

Decoration Abs

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Abs

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

toList :: Abs a -> [a]

null :: Abs a -> Bool

length :: Abs a -> Int

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

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

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

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

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

Traversable Abs

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Functor Abs

Defined in Agda.Syntax.Internal

Methods

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

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

Pretty t => Pretty (Abs t)

Defined in Agda.Syntax.Internal

Methods

pretty :: Abs t -> Doc

prettyPrec :: Int -> Abs t -> Doc

prettyList :: [Abs t] -> Doc

Suggest (Abs b)

Defined in Agda.Syntax.Internal

Methods

suggestName :: Abs b -> Maybe String

GetDefs a => GetDefs (Abs a)

Defined in Agda.Syntax.Internal.Defs

Methods

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

TermLike a => TermLike (Abs a)

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

NamesIn a => NamesIn (Abs a)

Defined in Agda.Syntax.Internal.Names

Methods

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

KillRange a => KillRange (Abs a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Abs a)

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Abs i)

Methods

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

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

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

Defined in Agda.TypeChecking.Abstract

Methods

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

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

Ignores absName.

Defined in Agda.TypeChecking.Abstract

Methods

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

Free t => Free (Abs t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

PrecomputeFreeVars a => PrecomputeFreeVars (Abs a)

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

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

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Irrelevance

Methods

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

MentionsMeta t => MentionsMeta (Abs t)

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs (Abs Term)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

Occurs (Abs Type)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

IsInstantiatedMeta a => IsInstantiatedMeta (Abs a)

Does not worry about raising.

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta a => UnFreezeMeta (Abs a)

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

ComputeOccurrences a => ComputeOccurrences (Abs a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Abs a -> OccM OccurrencesBuilder

Instantiate t => Instantiate (Abs t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

GetMatchables a => GetMatchables (Abs a)

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Abs a -> [QName]

NLPatVars a => NLPatVars (Abs a)

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatVarsUnder :: Int -> Abs a -> IntSet

nlPatVars :: Abs a -> IntSet

EmbPrj a => EmbPrj (Abs a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Abs a -> S Int32

icod_ :: Abs a -> S Int32

value :: Int32 -> R (Abs a)

Subst a => Subst (Abs a)

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Abs a)

Methods

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

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

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

Sized a => Sized (Abs a)

Defined in Agda.Syntax.Internal

Methods

size :: Abs a -> Int

natSize :: Abs a -> Peano

Generic (Abs a)

Defined in Agda.Syntax.Internal

Associated Types

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

Methods

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

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

Show a => Show (Abs a)

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Abs a -> ShowS

show :: Abs a -> String

showList :: [Abs a] -> ShowS

NFData a => NFData (Abs a)

Defined in Agda.Syntax.Internal

Methods

rnf :: Abs a -> ()

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

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Abs a -> Abs a -> Ordering

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

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

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

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

max :: Abs a -> Abs a -> Abs a

min :: Abs a -> Abs a -> Abs a

ToNLPat a b => ToNLPat (Abs a) (Abs b)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Abs a -> Abs b

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

type TypeOf (Abs Term)

Defined in Agda.Syntax.Internal

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

type TypeOf (Abs Type)

Defined in Agda.Syntax.Internal

type TypeOf (Abs Type) = Dom Type

type ReifiesTo (Abs i)

Defined in Agda.Syntax.Translation.InternalToAbstract

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

type SubstArg (Abs a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Abs a) = SubstArg a

type Rep (Abs a)

Defined in Agda.Syntax.Internal

type Rep (Abs a) = D1 ('MetaData "Abs" "Agda.Syntax.Internal" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "Abs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "NoAbs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

class LensSort a where

Minimal complete definition

lensSort

Methods

lensSort :: Lens' a Sort

getSort :: a -> Sort

Instances

LensSort Sort

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort Sort

getSort :: Sort -> Sort

LensSort a => LensSort (Arg a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' (Arg a) Sort

getSort :: Arg a -> Sort

LensSort a => LensSort (Dom a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' (Dom a) Sort

getSort :: Dom a -> Sort

LensSort (Type' a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' (Type' a) Sort

getSort :: Type' a -> Sort

type Elims

Arguments

 = [Elim]

eliminations ordered left-to-right.

class TermSize a where

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

Not counting towards the term size are:

• sort and color annotations,
• projections.

Minimal complete definition

tsize

Methods

termSize :: a -> Int

tsize :: a -> Sum Int

Instances

TermSize Level

Defined in Agda.Syntax.Internal

Methods

termSize :: Level -> Int

tsize :: Level -> Sum Int

TermSize PlusLevel

Defined in Agda.Syntax.Internal

Methods

termSize :: PlusLevel -> Int

tsize :: PlusLevel -> Sum Int

TermSize Sort

Defined in Agda.Syntax.Internal

Methods

termSize :: Sort -> Int

tsize :: Sort -> Sum Int

TermSize Term

Defined in Agda.Syntax.Internal

Methods

termSize :: Term -> Int

tsize :: Term -> Sum Int

TermSize a => TermSize (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

termSize :: Substitution' a -> Int

tsize :: Substitution' a -> Sum Int

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

Defined in Agda.Syntax.Internal

Methods

termSize :: t a -> Int

tsize :: t a -> Sum Int

type Blocked = Blocked' Term

type NotBlocked = NotBlocked' Term

type NamedArgs = [NamedArg Term]

data DataOrRecord' p

Constructors

IsData

IsRecord p

Instances

CopatternMatchingAllowed DataOrRecord

Defined in Agda.Syntax.Internal

Methods

copatternMatchingAllowed :: DataOrRecord -> Bool

PatternMatchingAllowed DataOrRecord

Defined in Agda.Syntax.Internal

Methods

patternMatchingAllowed :: DataOrRecord -> Bool

KillRange DataOrRecord

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT DataOrRecord

EmbPrj DataOrRecord

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DataOrRecord -> S Int32

icod_ :: DataOrRecord -> S Int32

value :: Int32 -> R DataOrRecord

NFData DataOrRecord

Defined in Agda.Syntax.Internal

Methods

rnf :: DataOrRecord -> ()

NFData DataOrRecordE

Defined in Agda.TypeChecking.Monad.Base

Methods

rnf :: DataOrRecordE -> ()

Generic (DataOrRecord' p)

Defined in Agda.Syntax.Internal

Associated Types

type Rep (DataOrRecord' p) :: Type -> Type

Methods

from :: DataOrRecord' p -> Rep (DataOrRecord' p) x

to :: Rep (DataOrRecord' p) x -> DataOrRecord' p

Show p => Show (DataOrRecord' p)

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> DataOrRecord' p -> ShowS

show :: DataOrRecord' p -> String

showList :: [DataOrRecord' p] -> ShowS

Eq p => Eq (DataOrRecord' p)

Defined in Agda.Syntax.Internal

Methods

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

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

type Rep (DataOrRecord' p)

Defined in Agda.Syntax.Internal

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

data ConHead

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

Constructors

ConHead

Fields

• conName :: QName

  The name of the constructor.

• conDataRecord :: DataOrRecord

  Data or record constructor?

• conInductive :: Induction

  Record constructors can be coinductive.

• conFields :: [Arg QName]

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

Instances

CopatternMatchingAllowed ConHead

Defined in Agda.Syntax.Internal

Methods

copatternMatchingAllowed :: ConHead -> Bool

Pretty ConHead

Defined in Agda.Syntax.Internal

Methods

pretty :: ConHead -> Doc

prettyPrec :: Int -> ConHead -> Doc

prettyList :: [ConHead] -> Doc

LensConName ConHead

Defined in Agda.Syntax.Internal

Methods

getConName :: ConHead -> QName

setConName :: QName -> ConHead -> ConHead

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

NamesIn ConHead

Defined in Agda.Syntax.Internal.Names

Methods

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

HasRange ConHead

Defined in Agda.Syntax.Internal

Methods

getRange :: ConHead -> Range

KillRange ConHead

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT ConHead

SetRange ConHead

Defined in Agda.Syntax.Internal

Methods

setRange :: Range -> ConHead -> ConHead

PrettyTCM ConHead

Defined in Agda.TypeChecking.Pretty

Methods

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

InstantiateFull ConHead

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ConHead -> ReduceM ConHead

EmbPrj ConHead

D