| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Contents | Index

Search:

!!! | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
$!! | Agda.Syntax.Strict
$$
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
$+$ | Agda.Utils.Pretty
+++ | Agda.Utils.ReadP
-*- | Agda.Utils.Tuple
--> | Agda.TypeChecking.Primitive
.&&. | Agda.Syntax.Parser.Alex
.&. | Agda.Utils.QuickCheck
.*. | Agda.Termination.CallGraph
.||. | Agda.Syntax.Parser.Alex
/\
1 (Function) | Agda.Utils.Tuple
2 (Function) | Agda.TypeChecking.Polarity
<#> | Agda.TypeChecking.Primitive
<$> | Agda.Utils.Monad
<*> | Agda.Utils.Monad
<++ | Agda.Utils.ReadP
<+>
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
<.> | Agda.Utils.Monad
<>
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
<@> | Agda.TypeChecking.Primitive
=: | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
=:= | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
=== | Agda.Utils.FileName
==> | Agda.Utils.QuickCheck
>*<
1 (Function) | Agda.Termination.CallGraph
2 (Function) | Agda.TypeChecking.Positivity
>+< | Agda.TypeChecking.Positivity
>< | Agda.Utils.QuickCheck
A | Agda.Interaction.GhciTop
AbortAssign | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
abortAssign | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
Abs
1 (Type/Class) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Auto.Syntax
3 (Type/Class) | Agda.Syntax.Internal
4 (Data Constructor) | Agda.Syntax.Internal
absApp | Agda.TypeChecking.Substitute
absBody | Agda.Syntax.Internal
AbsModule | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
AbsName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
absName | Agda.Syntax.Internal
absolute | Agda.Utils.FileName
AbsolutePath | Agda.Utils.FileName
AbsToCon | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
Abstract
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.TypeChecking.Substitute
abstract | Agda.TypeChecking.Substitute
abstractArgs | Agda.TypeChecking.Substitute
AbstractDef | Agda.Syntax.Common
abstractFromType | Agda.TypeChecking.Primitive
AbstractMode
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AbstractModule | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
AbstractName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
abstractPrim | Agda.TypeChecking.Primitive
AbstractRHS | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
AbstractTerm | Agda.TypeChecking.Abstract
abstractTerm | Agda.TypeChecking.Abstract
abstractToConcrete | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
abstractToConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
abstractToConcrete_ | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
Absurd | Agda.Syntax.Concrete
AbsurdLam
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
AbsurdP
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
AbsurdPatternRequiresNoRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AbsurdRHS
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
Access | Agda.Syntax.Common
actOnMeta | Agda.Interaction.CommandLine.CommandLine
actualConstructor | Agda.TypeChecking.Rules.Def
add
1 (Function) | Agda.Termination.Semiring
2 (Function) | Agda.Termination.Matrix
addColumn | Agda.Termination.Matrix
addConstant | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addConstraint | Agda.Utils.Warshall
addConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
addCtx | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxs | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxTel | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addDecl | Agda.Interaction.BasicOps
addDisplayForm | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addEdge | Agda.Utils.Warshall
addEquality | Agda.TypeChecking.Rules.LHS.Unify
addFinalNewLine | Agda.Utils.String
addFlex | Agda.Utils.Warshall
addHaskellCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addHaskellImport | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
addHaskellType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addImport | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
addImportCycleCheck | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
addImportedThings | Agda.Interaction.Imports
addInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
addLetBinding | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addModuleToScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
addNamesToScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
addNameToScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
addNewConstraints | Agda.TypeChecking.Constraints
addNode | Agda.Utils.Warshall
addRow | Agda.Termination.Matrix
addSection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addSuffix | Agda.Utils.Suffix
addVar | Agda.Compiler.Alonzo.PatternMonad
addWildcard | Agda.Compiler.Alonzo.PatternMonad
ADef | Agda.TypeChecking.Positivity
AdjList | Agda.Utils.Warshall
AlComment | Agda.Compiler.Alonzo.Haskell
ALConPar | Agda.Auto.Syntax
ALCons | Agda.Auto.Syntax
AlDecl
1 (Type/Class) | Agda.Compiler.Alonzo.Haskell
2 (Data Constructor) | Agda.Compiler.Alonzo.Haskell
AlexEOF | Agda.Syntax.Parser.Lexer
AlexError | Agda.Syntax.Parser.Lexer
alexGetChar | Agda.Syntax.Parser.Alex
AlexInput
1 (Type/Class) | Agda.Syntax.Parser.Alex
2 (Data Constructor) | Agda.Syntax.Parser.Alex
alexInputPrevChar | Agda.Syntax.Parser.Alex
AlexReturn | Agda.Syntax.Parser.Lexer
alexScanUser | Agda.Syntax.Parser.Lexer
AlexSkip | Agda.Syntax.Parser.Lexer
AlexToken | Agda.Syntax.Parser.Lexer
allEqual | Agda.Utils.List
allHoles | Agda.Syntax.Internal.Pattern
allHolesWithContents | Agda.Syntax.Internal.Pattern
allM | Agda.Compiler.Agate.Classify
allNames | Agda.Syntax.Abstract
allNamesInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
alloc | Agda.Utils.Pointer
allPaths | Agda.Utils.Graph
allThingsInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
allVars | Agda.TypeChecking.Free
ALNil | Agda.Auto.Syntax
alreadyVisited | Agda.Interaction.Imports
Ambiguous | Agda.Interaction.FindFile
AmbiguousModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousQName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
AmbiguousTopLevelModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
amodName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
anameKind | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
anameName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
AnArg | Agda.TypeChecking.Positivity
And | Agda.Auto.NarrowingSearch
andM | Agda.Compiler.Agate.Classify
AnyWhere | Agda.Syntax.Concrete
APatName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
App
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Abstract
4 (Data Constructor) | Agda.TypeChecking.EtaContract
appBrackets | Agda.Syntax.Fixity
Application | Agda.Syntax.Abstract.Views
Apply
1 (Data Constructor) | Agda.Syntax.Abstract
2 (Type/Class) | Agda.TypeChecking.Substitute
apply | Agda.TypeChecking.Substitute
applyImportDirective | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
applyImportDirectiveM | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
applySection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
AppP | Agda.Syntax.Concrete
appP | Agda.Syntax.Concrete.Operators.Parser
apps | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
AppV | Agda.Syntax.Concrete.Operators.Parser
AppView
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Type/Class) | Agda.Syntax.Abstract.Views
appView
1 (Function) | Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Abstract.Views
Arbitrary | Agda.Utils.QuickCheck
arbitrary | Agda.Utils.QuickCheck
arbitraryBoundedIntegral | Agda.Utils.QuickCheck
arbitraryBoundedRandom | Agda.Utils.QuickCheck
arbitrarySizedFractional | Agda.Utils.QuickCheck
arbitrarySizedIntegral | Agda.Utils.QuickCheck
Arc | Agda.Utils.Warshall
Arg
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
argHiding | Agda.Syntax.Common
ArgList | Agda.Auto.Syntax
argName | Agda.Syntax.Internal
ArgNode | Agda.TypeChecking.Positivity
ArgPat | Agda.TypeChecking.With
argpatts | Agda.Compiler.MAlonzo.Compiler
Args
1 (Data Constructor) | Agda.Utils.QuickCheck
2 (Type/Class) | Agda.Utils.QuickCheck
3 (Type/Class) | Agda.Syntax.Internal
ArgumentCtx | Agda.Syntax.Fixity
ArgumentTo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Arity | Agda.Syntax.Common
arity | Agda.Syntax.Internal
arrow | Agda.Syntax.Concrete.Pretty
As | Agda.Syntax.Concrete
AsB | Agda.TypeChecking.Rules.LHS
AsBinding | Agda.TypeChecking.Rules.LHS
AsIs | Agda.Interaction.BasicOps
AsName
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
asName | Agda.Syntax.Concrete
AsP
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
Aspect | Agda.Interaction.Highlighting.Precise
aspect | Agda.Interaction.Highlighting.Precise
asRange | Agda.Syntax.Concrete
Assign | Agda.Interaction.BasicOps
assignS | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
assignSort | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
assignTerm | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
assignV | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
associative | Agda.Utils.TestHelpers
asView | Agda.TypeChecking.Rules.LHS.Split
atomP | Agda.Syntax.Concrete.Operators.Parser
auto | Agda.Auto.Auto
axHsDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Axiom
1 (Data Constructor) | Agda.Syntax.Concrete.Definitions
2 (Data Constructor) | Agda.Syntax.Abstract
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
axiomName | Agda.Syntax.Abstract
B | Agda.Utils.Map
backupPos | Agda.Syntax.Position, Agda.Interaction.GhciTop
BadImplicits | Agda.TypeChecking.Implicit
begin | Agda.Syntax.Parser.LexActions
beginningOf | Agda.Syntax.Position, Agda.Interaction.GhciTop
begin_ | Agda.Syntax.Parser.LexActions
between | Agda.Utils.ReadP
BinAppView | Agda.TypeChecking.EtaContract
binAppView | Agda.TypeChecking.EtaContract
Bind | Agda.Syntax.Internal
bindAsPatterns | Agda.TypeChecking.Rules.LHS
bindBuiltin | Agda.TypeChecking.Rules.Builtin
bindBuiltinBool | Agda.TypeChecking.Rules.Builtin
bindBuiltinCons | Agda.TypeChecking.Rules.Builtin
bindBuiltinEquality | Agda.TypeChecking.Rules.Builtin
bindBuiltinLevelSuc | Agda.TypeChecking.Rules.Builtin
bindBuiltinLevelZero | Agda.TypeChecking.Rules.Builtin
bindBuiltinName | Agda.TypeChecking.Monad.Builtin
bindBuiltinNil | Agda.TypeChecking.Rules.Builtin
bindBuiltinPrimitive | Agda.TypeChecking.Rules.Builtin
bindBuiltinRefl | Agda.TypeChecking.Rules.Builtin
bindBuiltinSuc | Agda.TypeChecking.Rules.Builtin
bindBuiltinSuc' | Agda.TypeChecking.Rules.Builtin
bindBuiltinType | Agda.TypeChecking.Rules.Builtin
bindBuiltinType1 | Agda.TypeChecking.Rules.Builtin
bindBuiltinZero | Agda.TypeChecking.Rules.Builtin
bindBuiltinZero' | Agda.TypeChecking.Rules.Builtin
bindConstructor | Agda.TypeChecking.Rules.Builtin
bindLHSVars | Agda.TypeChecking.Rules.LHS
bindModule | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
bindName | Agda.Syntax.Scope.Monad
bindParameters | Agda.TypeChecking.Rules.Data
bindPostulate | Agda.TypeChecking.Rules.Builtin
bindPrimitive | Agda.TypeChecking.Monad.Builtin
bindQModule | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
bindToConcrete | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
bindVariable | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
binop | Agda.Syntax.Concrete.Operators.Parser
Blind
1 (Data Constructor) | Agda.Utils.QuickCheck
2 (Type/Class) | Agda.Utils.QuickCheck
BlkInfo | Agda.Auto.NarrowingSearch
Block | Agda.TypeChecking.Coverage.Match
Blocked
1 (Data Constructor) | Agda.Auto.NarrowingSearch
2 (Type/Class) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Internal
blocked | Agda.Syntax.Internal
BlockedConst | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BlockedLevel | Agda.TypeChecking.Level
blockingMeta | Agda.Syntax.Internal
blockOfLines | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
blockTerm | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
bltQual | Agda.Compiler.MAlonzo.Misc
bltQual' | Agda.Compiler.MAlonzo.Primitives
BName | Agda.Syntax.Concrete
bnameFixity | Agda.Syntax.Concrete
Body | Agda.Syntax.Internal
bol | Agda.Syntax.Parser.Lexer
boolSemiring | Agda.Termination.Semiring
BothWithAndRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Bound | Agda.Interaction.Highlighting.Precise
BoundName | Agda.Syntax.Concrete
boundName | Agda.Syntax.Concrete
braces
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
bracket | Agda.Utils.Monad
brackets
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
buildClosure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
buildConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
buildGraph | Agda.Utils.Warshall
buildInterface | Agda.Interaction.Imports
buildList | Agda.TypeChecking.Primitive
buildMPatterns | Agda.TypeChecking.Coverage.Match
buildOccurrenceGraph | Agda.TypeChecking.Positivity
buildWithFunction | Agda.TypeChecking.With
Builtin
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinBool | Agda.TypeChecking.Monad.Builtin
builtinChar | Agda.TypeChecking.Monad.Builtin
builtinCons | Agda.TypeChecking.Monad.Builtin
builtinConstructors | Agda.TypeChecking.Rules.Builtin
builtinDatatypes | Agda.TypeChecking.Rules.Builtin
builtinEquality | Agda.TypeChecking.Monad.Builtin
builtinFalse | Agda.TypeChecking.Monad.Builtin
builtinFloat | Agda.TypeChecking.Monad.Builtin
BuiltinInParameterisedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinInteger | Agda.TypeChecking.Monad.Builtin
builtinIO | Agda.TypeChecking.Monad.Builtin
builtinLevel | Agda.TypeChecking.Monad.Builtin
builtinLevelKit | Agda.TypeChecking.Level
builtinLevelMax | Agda.TypeChecking.Monad.Builtin
builtinLevelSuc | Agda.TypeChecking.Monad.Builtin
builtinLevelZero | Agda.TypeChecking.Monad.Builtin
builtinList | Agda.TypeChecking.Monad.Builtin
BuiltinMustBeConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinNat | Agda.TypeChecking.Monad.Builtin
builtinNatDivSucAux | Agda.TypeChecking.Monad.Builtin
builtinNatEquals | Agda.TypeChecking.Monad.Builtin
builtinNatLess | Agda.TypeChecking.Monad.Builtin
builtinNatMinus | Agda.TypeChecking.Monad.Builtin
builtinNatModSucAux | Agda.TypeChecking.Monad.Builtin
builtinNatPlus | Agda.TypeChecking.Monad.Builtin
builtinNatTimes | Agda.TypeChecking.Monad.Builtin
builtinNil | Agda.TypeChecking.Monad.Builtin
builtinPostulates | Agda.TypeChecking.Rules.Builtin
BuiltinPragma
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
builtinPrimitives | Agda.TypeChecking.Rules.Builtin
builtinRefl | Agda.TypeChecking.Monad.Builtin
builtinSize | Agda.TypeChecking.Monad.Builtin
builtinSizeInf | Agda.TypeChecking.Monad.Builtin
builtinSizeSuc | Agda.TypeChecking.Monad.Builtin
builtinString | Agda.TypeChecking.Monad.Builtin
builtinSuc | Agda.TypeChecking.Monad.Builtin
BuiltinThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinTrue | Agda.TypeChecking.Monad.Builtin
builtinTypes | Agda.TypeChecking.Monad.Builtin
builtinZero | Agda.TypeChecking.Monad.Builtin
CAction | Agda.Auto.Syntax
calc | Agda.Auto.NarrowingSearch
CALConcat | Agda.Auto.Syntax
Call
1 (Type/Class) | Agda.Termination.CallGraph
2 (Data Constructor) | Agda.Termination.CallGraph
3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
callGHC | Agda.Compiler.MAlonzo.Compiler
CallGraph | Agda.Termination.CallGraph
callGraphInvariant | Agda.Termination.CallGraph
callInvariant | Agda.Termination.CallGraph
CallMatrix
1 (Type/Class) | Agda.Termination.CallGraph
2 (Data Constructor) | Agda.Termination.CallGraph
callMatrixInvariant | Agda.Termination.CallGraph
calls | Agda.Termination.Lexicographic
CallTrace | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CALNil | Agda.Auto.Syntax
canonicalName | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
CantSplit | Agda.TypeChecking.Coverage
CArgList | Agda.Auto.Syntax
cat | Agda.Utils.Pretty
catchConstraint | Agda.TypeChecking.Constraints
catchException | Agda.TypeChecking.Monad.Exception
catchImpossible | Agda.Utils.Impossible
catMaybes | Agda.Utils.Maybe
cdcont | Agda.Auto.Syntax
cdecl | Agda.Compiler.MAlonzo.Compiler
cdname | Agda.Auto.Syntax
cdorigin | Agda.Auto.Syntax
cdtype | Agda.Auto.Syntax
CExp | Agda.Auto.Syntax
chainl | Agda.Utils.ReadP
chainl1 | Agda.Utils.ReadP
chainr | Agda.Utils.ReadP
chainr1 | Agda.Utils.ReadP
char
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.Utils.ReadP
checkArgs | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
CheckArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkArguments | Agda.TypeChecking.Rules.Term
checkArguments' | Agda.TypeChecking.Rules.Term
checkArguments_ | Agda.TypeChecking.Rules.Term
checkAxiom | Agda.TypeChecking.Rules.Decl
CheckClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkClause | Agda.TypeChecking.Rules.Def
CheckConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkConstructor | Agda.TypeChecking.Rules.Data
checkConstructorType | Agda.Compiler.MAlonzo.Compiler
checkCover | Agda.Compiler.MAlonzo.Compiler
checkCoverage | Agda.TypeChecking.Coverage
CheckDataDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkDataDef | Agda.TypeChecking.Rules.Data
checkDecl | Agda.TypeChecking.Rules.Decl, Agda.TypeChecker, Agda.Interaction.GhciTop
checkDecls | Agda.TypeChecking.Rules.Decl, Agda.TypeChecker, Agda.Interaction.GhciTop
checkDefinition | Agda.TypeChecking.Rules.Decl
CheckDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkDotPattern | Agda.TypeChecking.Rules.LHS
checkEqualities | Agda.TypeChecking.Rules.LHS.Unify
CheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkExpr | Agda.TypeChecking.Rules.Term, Agda.TypeChecker, Agda.Interaction.GhciTop
checkForImportCycle | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
CheckFunDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkFunDef | Agda.TypeChecking.Rules.Def
checkHeadApplication | Agda.TypeChecking.Rules.Term
checkImport | Agda.TypeChecking.Rules.Decl
checkInjectivity | Agda.TypeChecking.Injectivity
checkLeftHandSide | Agda.TypeChecking.Rules.LHS
CheckLetBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkLetBinding | Agda.TypeChecking.Rules.Term
checkLetBindings | Agda.TypeChecking.Rules.Term
checkLiteral | Agda.TypeChecking.Rules.Term
checkModuleArity | Agda.TypeChecking.Rules.Decl
checkModuleName | Agda.Interaction.FindFile
checkMutual | Agda.TypeChecking.Rules.Decl
checkOpts | Agda.Interaction.Options
CheckPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CheckPatternShadowing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CheckPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkPragma | Agda.TypeChecking.Rules.Decl
CheckPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkPrimitive | Agda.TypeChecking.Rules.Decl
CheckRecDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkRecDef | Agda.TypeChecking.Rules.Record
checkRecordProjections | Agda.TypeChecking.Rules.Record
checkSection | Agda.TypeChecking.Rules.Decl
CheckSectionApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkSectionApplication | Agda.TypeChecking.Rules.Decl
checkSizeIndex | Agda.TypeChecking.Polarity
checkStrictlyPositive | Agda.TypeChecking.Positivity
checkTelescope | Agda.TypeChecking.Rules.Term
checkTypedBinding | Agda.TypeChecking.Rules.Term
checkTypedBindings | Agda.TypeChecking.Rules.Term
checkTypeOfMain | Agda.Compiler.MAlonzo.Primitives
checkTypeSignature | Agda.TypeChecking.Rules.Decl
checkWhere | Agda.TypeChecking.Rules.Def
checkWithFunction | Agda.TypeChecking.Rules.Def
Child | Agda.Utils.Trace
ChildCall | Agda.Utils.Trace
Choice | Agda.Auto.NarrowingSearch
choice
1 (Function) | Agda.Utils.ReadP
2 (Function) | Agda.TypeChecking.Coverage.Match
choose
1 (Function) | Agda.Utils.QuickCheck
2 (Function) | Agda.Auto.NarrowingSearch
choosePrioMeta | Agda.Auto.NarrowingSearch
chop | Agda.Utils.List
Chr | Agda.Utils.Pretty
ClashingDefinition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingFileNamesFor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingModuleImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
classify | Agda.Utils.QuickCheck
Clause
1 (Type/Class) | Agda.Auto.Syntax
2 (Type/Class) | Agda.Syntax.Concrete.Definitions
3 (Data Constructor) | Agda.Syntax.Concrete.Definitions
4 (Type/Class) | Agda.Syntax.Internal
5 (Data Constructor) | Agda.Syntax.Internal
6 (Type/Class) | Agda.Syntax.Abstract
7 (Data Constructor) | Agda.Syntax.Abstract
clause
1 (Function) | Agda.Compiler.MAlonzo.Compiler
2 (Function) | Agda.Compiler.Alonzo.PatternMonad
clauseBod | Agda.Compiler.Alonzo.Main
ClauseBody | Agda.Syntax.Internal
clauseBody | Agda.Syntax.Internal
clausebody | Agda.Compiler.MAlonzo.Compiler
clausePats | Agda.Syntax.Internal
clausePerm | Agda.Syntax.Internal
clauseRange | Agda.Syntax.Internal
clauseTel | Agda.Syntax.Internal
clearMetaListeners | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
clEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Clos
1 (Type/Class) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Auto.Syntax
closeBrace | Agda.Syntax.Parser.Layout
ClosedLevel | Agda.TypeChecking.Level
closify | Agda.Auto.Typecheck
Closure
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
clScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
clSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
clTrace | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
clValue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
cm | Agda.Termination.CallGraph
cmd_auto | Agda.Interaction.GhciTop
cmd_compile | Agda.Interaction.GhciTop
cmd_compute | Agda.Interaction.GhciTop
cmd_compute_toplevel | Agda.Interaction.GhciTop
cmd_constraints | Agda.Interaction.GhciTop
cmd_context | Agda.Interaction.GhciTop
cmd_give | Agda.Interaction.GhciTop
cmd_goals | Agda.Interaction.GhciTop
cmd_goal_type | Agda.Interaction.GhciTop
cmd_goal_type_context | Agda.Interaction.GhciTop
cmd_goal_type_context_and | Agda.Interaction.GhciTop
cmd_goal_type_context_infer | Agda.Interaction.GhciTop
cmd_infer | Agda.Interaction.GhciTop
cmd_infer_toplevel | Agda.Interaction.GhciTop
cmd_intro | Agda.Interaction.GhciTop
cmd_load | Agda.Interaction.GhciTop
cmd_load' | Agda.Interaction.GhciTop
cmd_make_case | Agda.Interaction.GhciTop
cmd_metas | Agda.Interaction.GhciTop
cmd_refine | Agda.Interaction.GhciTop
cmd_refine_or_intro | Agda.Interaction.GhciTop
cmd_reset | Agda.Interaction.GhciTop
cmd_solveAll | Agda.Interaction.GhciTop
cmd_write_highlighting_info | Agda.Interaction.GhciTop
CmpEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CmpInType | Agda.Interaction.BasicOps
CmpLeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CmpSorts | Agda.Interaction.BasicOps
CmpTeles | Agda.Interaction.BasicOps
CmpTypes | Agda.Interaction.BasicOps
cnt | Agda.Compiler.Alonzo.PatternMonad
cnvh | Agda.Auto.Convert
CoArbitrary | Agda.Utils.QuickCheck
coarbitrary | Agda.Utils.QuickCheck
coarbitraryIntegral | Agda.Utils.QuickCheck
coarbitraryReal | Agda.Utils.QuickCheck
coarbitraryShow | Agda.Utils.QuickCheck
code | Agda.Syntax.Parser.Lexer
CoInductive | Agda.Syntax.Common
col | Agda.Termination.Matrix
coldescr | Agda.Utils.Warshall
collect | Agda.Utils.QuickCheck
colon | Agda.Utils.Pretty
cols | Agda.Termination.Matrix
Column | Agda.Termination.Lexicographic
columns | Agda.Termination.Lexicographic
comma
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
Command | Agda.Interaction.CommandLine.CommandLine
command | Agda.Interaction.GhciTop
CommandLineOptions | Agda.Interaction.Options
commandLineOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Comment | Agda.Interaction.Highlighting.Precise
commutative | Agda.Utils.TestHelpers
commuteM | Agda.Utils.Monad
comp | Agda.Auto.Typecheck
comp' | Agda.Auto.Typecheck
compactP | Agda.Utils.Permutation
compareArgs | Agda.TypeChecking.Conversion
compareAtom | Agda.TypeChecking.Conversion
compareSizes | Agda.TypeChecking.SizedTypes
compareSort | Agda.TypeChecking.Conversion
compareTel | Agda.TypeChecking.Conversion
compareTerm | Agda.TypeChecking.Conversion
compareType | Agda.TypeChecking.Conversion
compargs | Agda.Auto.Typecheck
Comparison | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
comphn' | Agda.Auto.Typecheck
CompilationError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
compile | Agda.Compiler.MAlonzo.Compiler
CompiledDataPragma
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
CompiledPragma
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
CompiledTypePragma
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
compilerMain
1 (Function) | Agda.Compiler.MAlonzo.Compiler
2 (Function) | Agda.Compiler.Alonzo.Main
3 (Function) | Agda.Compiler.Agate.Main
complete | Agda.Termination.CallGraph
composeP | Agda.Utils.Permutation
composePol | Agda.TypeChecking.Polarity
compress | Agda.Interaction.Highlighting.Precise
CompressedFile | Agda.Interaction.Highlighting.Precise
computeEdge | Agda.TypeChecking.Positivity
computeGreatestFixedPoint | Agda.Compiler.Agate.Classify
computeLeastFixedPoint | Agda.Compiler.Agate.Classify
computeMaxArity | Agda.Compiler.Agate.Main
computeNeighbourhood | Agda.TypeChecking.Coverage
ComputeOccurrences | Agda.TypeChecking.Positivity
computeOccurrences | Agda.TypeChecking.Positivity
computePolarity | Agda.TypeChecking.Polarity
computeSizeConstraint | Agda.TypeChecking.SizedTypes
Con
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Abstract
conAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ConArgType | Agda.TypeChecking.Positivity
concatMapM | Agda.Utils.Monad
concatOccurs | Agda.TypeChecking.Positivity
ConcreteDef | Agda.Syntax.Common
ConcreteMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
concreteToAbstract | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
concreteToAbstract_ | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
conData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
condecl | Agda.Compiler.MAlonzo.Compiler
conFreq | Agda.TypeChecking.Test.Generators
ConHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
conhqn | Agda.Compiler.MAlonzo.Misc
conHsCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
conInd | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ConMP | Agda.TypeChecking.Coverage.Match
ConName
1 (Data Constructor) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
2 (Type/Class) | Agda.TypeChecking.Test.Generators
3 (Data Constructor) | Agda.TypeChecking.Test.Generators
conName | Agda.Compiler.Alonzo.Names
ConP
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Abstract
conPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ConPos | Agda.TypeChecking.With
conQName | Agda.Compiler.Alonzo.Names
conQStr | Agda.Compiler.Alonzo.Names
consDefs | Agda.Compiler.Alonzo.Main
consForName | Agda.Compiler.Alonzo.Main
conSrcCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Const | Agda.Auto.Syntax
ConstDef
1 (Type/Class) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Auto.Syntax
Constr
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
conStr | Agda.Compiler.Alonzo.Names
Constraint
1 (Type/Class) | Agda.Utils.Warshall
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ConstraintClosure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Constraints
1 (Type/Class) | Agda.Utils.Warshall
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ConstRef | Agda.Auto.Syntax
Constructor
1 (Data Constructor) | Agda.Auto.Syntax
2 (Type/Class) | Agda.Syntax.Concrete
3 (Type/Class) | Agda.Syntax.Abstract
4 (Data Constructor) | Agda.Interaction.Highlighting.Precise
5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
constructorArity | Agda.Compiler.MAlonzo.Compiler
constructorForm | Agda.TypeChecking.Primitive
ConstructorMismatch | Agda.TypeChecking.Rules.LHS.Unify
constructorMismatch | Agda.TypeChecking.Rules.LHS.Unify
ConstructorName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
ConstructorPatternInWrongDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
constructorsInClause | Agda.TypeChecking.With
constructorsInClauses | Agda.TypeChecking.With
constructs | Agda.TypeChecking.Rules.Data
Cont | Agda.Utils.Monad
containsAbsurdPattern | Agda.TypeChecking.Rules.Def
contClause | Agda.Compiler.Alonzo.Main
Context | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ContextEntry | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
contextOfMeta | Agda.Interaction.BasicOps
Continue | Agda.Interaction.CommandLine.CommandLine
continueAfter | Agda.Interaction.CommandLine.CommandLine
ContinueIn | Agda.Interaction.CommandLine.CommandLine
continuous | Agda.Syntax.Position, Agda.Interaction.GhciTop
continuousPerLine | Agda.Syntax.Position, Agda.Interaction.GhciTop
Contravariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
convertLineEndings | Agda.Utils.Unicode
copyScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
count | Agda.Utils.ReadP
Covariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
cover
1 (Function) | Agda.Utils.QuickCheck
2 (Function) | Agda.TypeChecking.Coverage
CoverageCantSplitOn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CoverageCantSplitType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CoverageFailure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Covering | Agda.TypeChecking.Coverage
CoverM | Agda.TypeChecking.Coverage
createInterface | Agda.Interaction.Imports
createMetaInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
createModule | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
ctparent | Agda.Auto.NarrowingSearch
ctpriometa | Agda.Auto.NarrowingSearch
CTree
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
ctsub | Agda.Auto.NarrowingSearch
Ctx
1 (Type/Class) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ctxEntry | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CtxId
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ctxId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
curDefs | Agda.Compiler.MAlonzo.Misc
curHsMod | Agda.Compiler.MAlonzo.Misc
curIF | Agda.Compiler.MAlonzo.Misc
curMName | Agda.Compiler.MAlonzo.Misc
Current | Agda.Utils.Trace
CurrentCall | Agda.Utils.Trace
CurrentDir | Agda.Interaction.Imports
CurrentInput | Agda.Syntax.Parser.Alex
currentModule | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
currentMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
curSig | Agda.Compiler.MAlonzo.Misc
CyclicModuleDependency | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Data | Agda.Syntax.Concrete
dataAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataCons | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataDef
1 (Data Constructor) | Agda.Syntax.Concrete.Definitions
2 (Data Constructor) | Agda.Syntax.Abstract
dataHsType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataInduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataIxs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataMustEndInSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataName | Agda.Compiler.Alonzo.Names
dataOrRecordType | Agda.TypeChecking.Rules.LHS.Unify
dataPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Datatype
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
deBruijnIndex | Agda.Interaction.MakeCase
DeBruijnPat | Agda.Termination.TermCheck
debug | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad
decDigit | Agda.Utils.Char
Declaration
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
DeclarationException | Agda.Syntax.Concrete.Definitions
DeclarationPanic | Agda.Syntax.Concrete.Definitions
DeclCont | Agda.Auto.Syntax
DeclInfo
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
declName | Agda.Syntax.Info
declRange | Agda.Syntax.Info
declsForPrim | Agda.Compiler.MAlonzo.Primitives
decode | Agda.TypeChecking.Serialise
DecodedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
decodeFile | Agda.TypeChecking.Serialise
decompress | Agda.Interaction.Highlighting.Precise
decrConf | Agda.TypeChecking.Test.Generators
Def
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Abstract
defAbstract
1 (Function) | Agda.Syntax.Info
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defAccess | Agda.Syntax.Info
DefArg | Agda.TypeChecking.Positivity
defaultDisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defaultFixity | Agda.Syntax.Fixity
defaultFrequencies | Agda.TypeChecking.Test.Generators
defaultImportDir | Agda.Syntax.Concrete
defaultOptions | Agda.Interaction.Options
defaultParseFlags | Agda.Syntax.Parser.Monad
defClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defDelayed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defDisplay | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defFixity | Agda.Syntax.Info
defFreq | Agda.TypeChecking.Test.Generators
DefinedName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
DefInfo
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
defInfo | Agda.Syntax.Info
Definition
1 (Type/Class) | Agda.Syntax.Abstract
2 (Data Constructor) | Agda.Syntax.Abstract
3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
definition | Agda.Compiler.MAlonzo.Compiler
Definitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
definitions | Agda.Compiler.MAlonzo.Compiler
definitionSite | Agda.Interaction.Highlighting.Precise
defMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Defn
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DefName
1 (Data Constructor) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
2 (Type/Class) | Agda.TypeChecking.Test.Generators
3 (Data Constructor) | Agda.TypeChecking.Test.Generators
defName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DefNode | Agda.TypeChecking.Positivity
DefP | Agda.Syntax.Abstract
Defs | Agda.Compiler.Alonzo.PatternMonad
defs | Agda.Compiler.Alonzo.PatternMonad
defType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Delayed
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DependentPatternMatchingOnCodata | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
deref | Agda.Utils.Pointer
dfName | Agda.Compiler.Alonzo.Names
dfNameSub | Agda.Compiler.Alonzo.Names
dfQName | Agda.Compiler.Alonzo.Names
dfQStr | Agda.Compiler.Alonzo.Names
dfStr | Agda.Compiler.Alonzo.Names
diagonal | Agda.Termination.Matrix
DifferentArities | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
disableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Display | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
displayErrorAndExit | Agda.Interaction.GhciTop
DisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
displayForm | Agda.TypeChecking.DisplayForm
displayFormsEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
displayStatus | Agda.Interaction.GhciTop
DisplayTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
display_info | Agda.Interaction.GhciTop
display_info' | Agda.Interaction.GhciTop
display_infoD | Agda.Interaction.GhciTop
Dist | Agda.Utils.Warshall
Distance | Agda.Utils.Warshall
distinct | Agda.Utils.List
divConf | Agda.TypeChecking.Test.Generators
DLub | Agda.Syntax.Internal
dLub | Agda.TypeChecking.Substitute
Doc
1 (Type/Class) | Agda.Utils.Pretty
2 (Type/Class) | Agda.TypeChecking.Pretty
doclos | Agda.Auto.Typecheck
DoesNotConstructAnElementOf | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DomainFree
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
DomainFull
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
DontExpandLast | Agda.TypeChecking.Rules.Term
DontKnow
1 (Data Constructor) | Agda.TypeChecking.Patterns.Match
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Unify
DontOpen | Agda.Syntax.Concrete
dontReifyInteractionPoints | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DontTouchMe | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
DoOpen | Agda.Syntax.Concrete
dopat | Agda.Auto.Typecheck
dopats | Agda.Auto.Typecheck
dorule | Agda.Auto.Typecheck
dorules | Agda.Auto.Typecheck
Dot | Agda.Syntax.Concrete
DotP
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Abstract
DotPatternCtx | Agda.Syntax.Fixity
DotPatternInst | Agda.TypeChecking.Rules.LHS
dotPatternInsts | Agda.TypeChecking.Rules.LHS
DottedPattern | Agda.Interaction.Highlighting.Precise
DotVars | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
dotVars | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
double | Agda.Utils.Pretty
doubleblock | Agda.Auto.NarrowingSearch
doubleQuotes | Agda.Utils.Pretty
DPI | Agda.TypeChecking.Rules.LHS
dropArgs | Agda.Compiler.Agate.Common
dropDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
dropI | Agda.Syntax.Position, Agda.Interaction.GhciTop
dryInstantiate | Agda.Auto.NarrowingSearch
dsubname | Agda.Compiler.MAlonzo.Misc
DTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dummy | Agda.Compiler.MAlonzo.Misc
dummyLoc | Agda.Compiler.Alonzo.Haskell
DuplicateBuiltinBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DuplicateConstructors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DuplicateFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DWithApp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eatNextChar | Agda.Syntax.Parser.LookAhead
Edge
1 (Type/Class) | Agda.TypeChecking.Positivity
2 (Data Constructor) | Agda.TypeChecking.Positivity
edges
1 (Function) | Agda.Utils.Graph
2 (Function) | Agda.Utils.Warshall
EE | Agda.Auto.Syntax
EitherOrBoth | Agda.Utils.Map
El | Agda.Syntax.Internal
el | Agda.TypeChecking.Primitive
elements | Agda.Utils.QuickCheck
Ellipsis | Agda.Syntax.Concrete
Elr | Agda.Auto.Syntax
Elrs | Agda.Auto.Syntax
ElrsCons | Agda.Auto.Syntax
ElrsNil | Agda.Auto.Syntax
ElrsWeak | Agda.Auto.Syntax
EmbPrj | Agda.TypeChecking.Serialise
empty
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.Utils.Trie
3 (Function) | Agda.Utils.Graph
4 (Function) | Agda.Termination.CallGraph
5 (Function) | Agda.TypeChecking.Pretty
emptyConstraints | Agda.Utils.Warshall
emptyLayout | Agda.Syntax.Parser.Layout
emptyNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
emptyScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
emptyScopeInfo | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
emptySignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
emptySolution | Agda.Utils.Warshall
EmptyTel | Agda.Syntax.Internal
emptyUState | Agda.TypeChecking.Rules.LHS.Unify
empty_layout | Agda.Syntax.Parser.Lexer
enableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
encode | Agda.TypeChecking.Serialise
encodeFile | Agda.TypeChecking.Serialise
encodeModuleName | Agda.Compiler.MAlonzo.Encode
end | Agda.Syntax.Parser.LexActions
endBy | Agda.Utils.ReadP
endBy1 | Agda.Utils.ReadP
endWith | Agda.Syntax.Parser.LexActions
end_ | Agda.Syntax.Parser.LexActions
enterClosure | Agda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad
enumCompilableTypeFamilies | Agda.Compiler.Agate.Classify
enumConstructors | Agda.Compiler.Agate.Main
enumOptimizableConstants | Agda.Compiler.Agate.Classify
enumTypeFamilies | Agda.Compiler.Agate.Classify
Env | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
envAbstractMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envAnonymousModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envContext | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envDisplayFormsEnabled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envImportPath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envLetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envMutualBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envReifyInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envReplace | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eof | Agda.Syntax.Parser.LexActions
Equal | Agda.TypeChecking.Rules.LHS.Unify
equalArgs | Agda.TypeChecking.Conversion
equalAtom | Agda.TypeChecking.Conversion
Equality | Agda.TypeChecking.Rules.LHS.Unify
equalLevel | Agda.TypeChecking.Conversion
equals | Agda.Utils.Pretty
equalSort | Agda.TypeChecking.Conversion
equalTerm | Agda.TypeChecking.Conversion
equalType | Agda.TypeChecking.Conversion
errError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
errHighlighting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
errInput | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
errMsg | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
Error
1 (Data Constructor) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
errorTitle | Agda.Interaction.GhciTop
errPos | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
errPrevToken | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
escape
1 (Function) | Agda.Interaction.Highlighting.Vim
2 (Function) | Agda.Compiler.Agate.TranslateName
escapeContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
etaContract | Agda.TypeChecking.EtaContract
etaContractRecord | Agda.TypeChecking.Records
etaExpandClause | Agda.TypeChecking.Positivity
etaExpandListeners | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
etaExpandMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
etaExpandRecord | Agda.TypeChecking.Records
ETel
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
evalIn | Agda.Interaction.CommandLine.CommandLine
evalInCurrent | Agda.Interaction.BasicOps
evalInMeta | Agda.Interaction.BasicOps
evalTerm | Agda.Interaction.CommandLine.CommandLine
everythingBut | Agda.Utils.Generics
everythingInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
everywhereBut' | Agda.Utils.Generics
everywhereButM' | Agda.Utils.Generics
Exception | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ExceptionT
1 (Type/Class) | Agda.TypeChecking.Monad.Exception
2 (Data Constructor) | Agda.TypeChecking.Monad.Exception
ExitCode | Agda.Interaction.CommandLine.CommandLine
Exp | Agda.Auto.Syntax
ExpandHidden | Agda.TypeChecking.Rules.Term
ExpandLast | Agda.TypeChecking.Rules.Term
expandLitPattern | Agda.TypeChecking.Rules.LHS.Split
expandP | Agda.Utils.Permutation
expectFailure | Agda.Utils.QuickCheck
Expr
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
ExprInfo | Agda.Syntax.Info
exprInfo | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
exprParser
1 (Function) | Agda.Syntax.Parser.Parser
2 (Function) | Agda.Syntax.Parser, Agda.Interaction.GhciTop
ExprRange | Agda.Syntax.Info
ExprSource | Agda.Syntax.Info
ExprView | Agda.Syntax.Concrete.Operators.Parser
exprView | Agda.Syntax.Concrete.Operators.Parser
extendConf | Agda.TypeChecking.Test.Generators
extendSolution | Agda.Utils.Warshall
ExtendTel | Agda.Syntax.Internal
extendWithTelConf | Agda.TypeChecking.Test.Generators
extractblkinfos | Agda.Auto.NarrowingSearch
extractNthElement | Agda.Utils.List
Failed | Agda.Auto.NarrowingSearch
failOnException | Agda.Interaction.Exceptions, Agda.Interaction.GhciTop
Failure | Agda.Utils.QuickCheck
fakeD | Agda.Compiler.MAlonzo.Misc
fakeDQ | Agda.Compiler.MAlonzo.Misc
fakeDS | Agda.Compiler.MAlonzo.Misc
fakeExp | Agda.Compiler.MAlonzo.Misc
fakeType | Agda.Compiler.MAlonzo.Misc
fcat | Agda.Utils.Pretty
fCtx | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Field
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Abstract
4 (Data Constructor) | Agda.Interaction.Highlighting.Precise
FieldOutsideRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Fields
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
File | Agda.Interaction.Highlighting.Precise
FileNotFound | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
filePath | Agda.Utils.FileName
filterKeys | Agda.Utils.Map
filterScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
finally | Agda.Utils.Monad
findClause | Agda.Interaction.MakeCase
FindError | Agda.Interaction.FindFile
findErrorToTypeError | Agda.Interaction.FindFile
findFile | Agda.Interaction.FindFile
findFile' | Agda.Interaction.FindFile
findFile'' | Agda.Interaction.FindFile
findIdx | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
findInterfaceFile | Agda.Interaction.FindFile
findMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
findPath | Agda.Utils.Graph
Finite | Agda.Utils.Warshall
fInteger | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fInteraction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
firstPart | Agda.TypeChecking.Telescope
fitsIn | Agda.TypeChecking.Rules.Data
Fixed
1 (Data Constructor) | Agda.Utils.QuickCheck
2 (Type/Class) | Agda.Utils.QuickCheck
Fixity | Agda.Syntax.Fixity
fixityLevel | Agda.Syntax.Fixity
fixSize | Agda.TypeChecking.Test.Generators
fixSizeConf | Agda.TypeChecking.Test.Generators
Flag | Agda.Interaction.Options
flattenSubmodules | Agda.Compiler.Alonzo.Main
flattenSubstitution | Agda.TypeChecking.Rules.LHS.Unify
flattenTel | Agda.TypeChecking.Telescope
Flex | Agda.Utils.Warshall
flexiblePatterns | Agda.TypeChecking.Rules.LHS
flexibleVariables | Agda.TypeChecking.SizedTypes
FlexibleVars | Agda.TypeChecking.Rules.LHS.Problem
flexibleVars | Agda.TypeChecking.Free
FlexId | Agda.Utils.Warshall
flexScope | Agda.Utils.Warshall
float | Agda.Utils.Pretty
fMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fmExp | Agda.Auto.Convert
fmExps | Agda.Auto.Convert
FMode | Agda.Auto.Syntax
fmType | Agda.Auto.Convert
fMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Focus
1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem
focusCon | Agda.TypeChecking.Rules.LHS.Problem
focusConArgs | Agda.TypeChecking.Rules.LHS.Problem
focusDatatype | Agda.TypeChecking.Rules.LHS.Problem
focusHoleIx | Agda.TypeChecking.Rules.LHS.Problem
focusIndices | Agda.TypeChecking.Rules.LHS.Problem
focusOutPat | Agda.TypeChecking.Rules.LHS.Problem
focusParams | Agda.TypeChecking.Rules.LHS.Problem
focusRange | Agda.TypeChecking.Rules.LHS.Problem
foldClauses | Agda.Compiler.Alonzo.Main
foldTerm | Agda.Syntax.Internal.Generic
followedBy | Agda.Syntax.Parser.LexActions
forAll | Agda.Utils.QuickCheck
forAllShrink | Agda.Utils.QuickCheck
force | Agda.Syntax.Strict
forceData | Agda.TypeChecking.Rules.Data
forceM | Agda.Utils.Monad
forcePi | Agda.TypeChecking.Rules.Term
forEachArgM | Agda.Compiler.Agate.Common
forgetM | Agda.Utils.Monad
Free | Agda.TypeChecking.Free
freeIn | Agda.TypeChecking.Free
freeInIgnoringSorts | Agda.TypeChecking.Free
FreeVars | Agda.TypeChecking.Free
freeVars | Agda.TypeChecking.Free
freeVarsToApply | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
Freqs | Agda.TypeChecking.Test.Generators
Frequencies | Agda.TypeChecking.Test.Generators
frequency | Agda.Utils.QuickCheck
Fresh | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fresh | Agda.Utils.Fresh
freshAbstractName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
freshAbstractName_ | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
freshAbstractQName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
freshName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
freshName_ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
freshNoName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
freshNoName_ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
FreshThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
from | Agda.Interaction.Highlighting.Range
fromCurrentModule | Agda.Compiler.Alonzo.Main
fromDiagonals | Agda.Termination.Lexicographic
fromIndexList | Agda.Termination.Matrix
fromJust | Agda.Utils.Maybe
fromList
1 (Function) | Agda.Utils.Graph
2 (Function) | Agda.Termination.CallGraph
fromLists | Agda.Termination.Matrix
fromLiteral | Agda.TypeChecking.Primitive
fromMaybe | Agda.Utils.Maybe
fromMaybeM | Agda.Utils.Maybe
frommy | Agda.Auto.Convert
frommyExp | Agda.Auto.Convert
frommyExps | Agda.Auto.Convert
frommyType | Agda.Auto.Convert
fromReducedTerm | Agda.TypeChecking.Primitive
FromTerm | Agda.TypeChecking.Primitive
fromTerm | Agda.TypeChecking.Primitive
FromTermFunction | Agda.TypeChecking.Primitive
fsep
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
fullRender | Agda.Utils.Pretty
Fun
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Internal
4 (Data Constructor) | Agda.Syntax.Abstract
5 (Type/Class) | Agda.TypeChecking.Primitive
funAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FunClause | Agda.Syntax.Concrete
funClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Function
1 (Data Constructor) | Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FunctionCtx | Agda.Syntax.Fixity
FunctionInverse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
functionInverse | Agda.TypeChecking.Injectivity
FunctionSpaceDomainCtx | Agda.Syntax.Fixity
FunDef
1 (Data Constructor) | Agda.Syntax.Concrete.Definitions
2 (Data Constructor) | Agda.Syntax.Abstract
funDelayed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funFreq | Agda.TypeChecking.Test.Generators
funInv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FunV | Agda.Syntax.Internal
FunView | Agda.Syntax.Internal
funView | Agda.Syntax.Internal
fuseRange | Agda.Syntax.Position, Agda.Interaction.GhciTop
fuseRanges | Agda.Syntax.Position, Agda.Interaction.GhciTop
FV | Agda.TypeChecking.Free
fwords
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
gApply | Agda.TypeChecking.Primitive
gather | Agda.Utils.ReadP
GaveUp | Agda.Utils.QuickCheck
Gen | Agda.Utils.QuickCheck
genArgs | Agda.TypeChecking.Test.Generators
GenC | Agda.TypeChecking.Test.Generators
genC | Agda.TypeChecking.Test.Generators
genConf | Agda.TypeChecking.Test.Generators
generateErrorInfo | Agda.Interaction.Highlighting.Generate
generateHTML | Agda.Interaction.Highlighting.HTML
generateSyntaxInfo | Agda.Interaction.Highlighting.Generate
generateVimFile | Agda.Interaction.Highlighting.Vim
GenericError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
GenericSplitError | Agda.TypeChecking.Coverage
GenericUnifyException | Agda.TypeChecking.Rules.LHS.Unify
genGraph | Agda.Utils.Warshall
genGraph_ | Agda.Utils.Warshall
genPath | Agda.Utils.Warshall
get | Agda.Utils.ReadP
getAllArgs | Agda.Auto.Typecheck
getAnonymousVariables | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
getArgOccurrence | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getArity | Agda.TypeChecking.Polarity
getBuiltin | Agda.TypeChecking.Monad.Builtin
getBuiltin' | Agda.TypeChecking.Monad.Builtin
getBuiltinThings | Agda.TypeChecking.Monad.Builtin
getConArities | Agda.Compiler.Alonzo.Main
getConArity | Agda.Compiler.Alonzo.Main
getConst | Agda.Auto.Convert
getConstInfo | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getConstraint | Agda.Interaction.BasicOps
getConstraints
1 (Function) | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
2 (Function) | Agda.Interaction.BasicOps
getConstructorArity | Agda.Compiler.Agate.Main
getContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getContextArgs | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getContextId | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getContextPrecedence | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
getContextTelescope | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getContextTerms | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getCurrentModule | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
getCurrentRange | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
getCurrentScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
getDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getDecodedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getDefFreeVars | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getDefinitions | Agda.Compiler.Alonzo.Main
getEnv | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
getEqs | Agda.Auto.Convert
getFixity | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
getHaskellImports | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getHsType | Agda.Compiler.HaskellTypes
getHsVar | Agda.Compiler.HaskellTypes
getImportedSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getImportPath | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getImports | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getIncludeDirs | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
getinfo | Agda.Auto.SearchControl
getInput | Agda.Syntax.Parser.LookAhead
getInputFile | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
getInstantiatedMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInteractionMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInteractionPoints | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInteractionRange | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInteractionScope | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInterface | Agda.Interaction.Imports
getInterface' | Agda.Interaction.Imports
getLexInput | Agda.Syntax.Parser.Alex
getLexState | Agda.Syntax.Parser.Monad
getLocalVars | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
getMeta | Agda.Auto.Convert
getMetaEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaListeners | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaPriority | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaRange | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaSig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaStore | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getModuleFreeVars | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getMutualBlocks | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
getNamedScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
getNArgs | Agda.Auto.Typecheck
getOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
getOpenMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getParseFlags | Agda.Syntax.Parser.Monad
getParseInterval | Agda.Syntax.Parser.Monad
getPclause | Agda.Compiler.Alonzo.PatternMonad
getPcnt | Agda.Compiler.Alonzo.PatternMonad
getPDefs | Agda.Compiler.Alonzo.PatternMonad
getPlst | Agda.Compiler.Alonzo.PatternMonad
getPolarity | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getPolarity' | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getPrimitive | Agda.TypeChecking.Monad.Builtin
getRange | Agda.Syntax.Position, Agda.Interaction.GhciTop
getRanges | Agda.Interaction.Highlighting.Range
getRangesA | Agda.Interaction.Highlighting.Range
getRecordConstructor | Agda.TypeChecking.Records
getRecordConstructorType | Agda.TypeChecking.Records
getRecordDef | Agda.TypeChecking.Records
getRecordFieldNames | Agda.TypeChecking.Records
getRecordFieldTypes | Agda.TypeChecking.Records
getScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getSecFreeVars | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getSizeConstraints | Agda.TypeChecking.SizedTypes
getSizeMetas | Agda.TypeChecking.SizedTypes
getSolvedInteractionPoints | Agda.Interaction.BasicOps
getSort | Agda.Syntax.Internal
getStatistics | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad
getSub | Agda.TypeChecking.Rules.LHS.Unify
getTrace | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
getVarInfo | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getVerbosity | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
getVisitedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getVisitedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
give | Agda.Interaction.BasicOps
giveExpr | Agda.Interaction.BasicOps
giveMeta | Agda.Interaction.CommandLine.CommandLine
give_gen | Agda.Interaction.GhciTop
GM | Agda.Utils.Warshall
GoalCommand | Agda.Interaction.GhciTop
gpi | Agda.TypeChecking.Primitive
Graph
1 (Type/Class) | Agda.Utils.Graph
2 (Data Constructor) | Agda.Utils.Graph
3 (Type/Class) | Agda.Utils.Warshall
4 (Data Constructor) | Agda.Utils.Warshall
graph | Agda.Utils.Warshall
groupBy' | Agda.Utils.List
groupOn | Agda.Utils.List
growGraph | Agda.Utils.Graph
growingElements | Agda.Utils.QuickCheck
gshow' | Agda.Compiler.MAlonzo.Misc
Guard | Agda.Interaction.BasicOps
guardConstraint | Agda.TypeChecking.Constraints
Guarded | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
handleAbort | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
handleParseException | Agda.Interaction.Exceptions, Agda.Interaction.GhciTop
HandlePartSol | Agda.Auto.NarrowingSearch
HandleSol | Agda.Auto.NarrowingSearch
hang | Agda.Utils.Pretty
hasCompiledData | Agda.Compiler.MAlonzo.Primitives
HasFresh | Agda.Utils.Fresh
hash | Agda.Utils.Hash
hasInputFile | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
HaskellCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
HaskellKind | Agda.Compiler.HaskellTypes
haskellKind | Agda.Compiler.HaskellTypes
HaskellRepresentation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
HaskellType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
haskellType | Agda.Compiler.HaskellTypes
HasMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
HasPolarity | Agda.TypeChecking.Polarity
HasRange | Agda.Syntax.Position, Agda.Interaction.GhciTop
HasType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
hasUniversePolymorphism | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
haveSizedTypes | Agda.TypeChecking.SizedTypes
hcat | Agda.Utils.Pretty
Head | Agda.Syntax.Abstract.Views
HeadCon | Agda.Syntax.Abstract.Views
HeadDef | Agda.Syntax.Abstract.Views
HeadNormal | Agda.Interaction.BasicOps
headSymbol | Agda.TypeChecking.Injectivity
headToExpr | Agda.Syntax.Abstract.Views
HeadVar | Agda.Syntax.Abstract.Views
help | Agda.Interaction.CommandLine.CommandLine
hequalMetavar | Agda.Auto.NarrowingSearch
Here
1 (Data Constructor) | Agda.TypeChecking.Positivity
2 (Data Constructor) | Agda.TypeChecking.With
here | Agda.TypeChecking.Positivity
hexDigit | Agda.Utils.Char
hGetContents | Agda.Utils.IO.Locale
Hidden
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Common
HiddenArg | Agda.Syntax.Concrete
hiddenArgumentCtx | Agda.Syntax.Fixity
HiddenArgV | Agda.Syntax.Concrete.Operators.Parser
hiddenFreq | Agda.TypeChecking.Test.Generators
HiddenFreqs
1 (Type/Class) | Agda.TypeChecking.Test.Generators
2 (Data Constructor) | Agda.TypeChecking.Test.Generators
hiddenFreqs | Agda.TypeChecking.Test.Generators
HiddenP | Agda.Syntax.Concrete
Hiding
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Concrete
HighlightingInfo | Agda.Interaction.Highlighting.Precise
highMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
hn' | Agda.Auto.Typecheck
HNALConPar | Agda.Auto.Syntax
HNALCons | Agda.Auto.Syntax
HNALNil | Agda.Auto.Syntax
HNApp | Agda.Auto.Syntax
HNArgList | Agda.Auto.Syntax
hnarglist | Agda.Auto.Typecheck
hnc | Agda.Auto.Typecheck
HNDone | Agda.Auto.Typecheck
HNExp | Agda.Auto.Syntax
HNFun | Agda.Auto.Syntax
HNLam | Agda.Auto.Syntax
HNMeta | Agda.Auto.Typecheck
hnn | Agda.Auto.Typecheck
hnn' | Agda.Auto.Typecheck
HNPi | Agda.Auto.Syntax
HNRes | Agda.Auto.Typecheck
HNSort | Agda.Auto.Syntax
Hole
1 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Internal.Pattern
hole | Agda.Syntax.Parser.Comments
holes | Agda.Utils.List
hPi | Agda.TypeChecking.Primitive
hsAp | Agda.Compiler.Alonzo.Haskell
hsApp | Agda.Compiler.HaskellTypes
hsCast
1 (Function) | Agda.Compiler.MAlonzo.Compiler
2 (Function) | Agda.Compiler.Alonzo.Haskell
hsCast' | Agda.Compiler.MAlonzo.Compiler
hsCon | Agda.Compiler.Alonzo.Haskell
HsDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
hsep
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
hsError | Agda.Compiler.Alonzo.Haskell
hsForall | Agda.Compiler.HaskellTypes
hsFun | Agda.Compiler.HaskellTypes
hsImport | Agda.Compiler.Alonzo.Haskell
hsKFun | Agda.Compiler.HaskellTypes
hsLam | Agda.Compiler.Alonzo.Haskell
hslit | Agda.Compiler.MAlonzo.Compiler
hsModule | Agda.Compiler.Alonzo.Haskell
hsModuleImporting | Agda.Compiler.Alonzo.Haskell
hsPreludeName | Agda.Compiler.Alonzo.Haskell
hsPreludeTypedExp | Agda.Compiler.Alonzo.Haskell
hsQImport | Agda.Compiler.Alonzo.Haskell
hsStar | Agda.Compiler.HaskellTypes
HsType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
hsTypedExp | Agda.Compiler.Alonzo.Haskell
hsUndefined | Agda.Compiler.Alonzo.Haskell
hsVar
1 (Function) | Agda.Compiler.HaskellTypes
2 (Function) | Agda.Compiler.Alonzo.Haskell
hsVarUQ | Agda.Compiler.MAlonzo.Misc
iBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
icnvh | Agda.Auto.Convert
Id
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
Ident | Agda.Syntax.Concrete
identifier | Agda.Syntax.Parser.LexActions
identity | Agda.Utils.TestHelpers
IdentP | Agda.Syntax.Concrete
idP | Agda.Utils.Permutation
idSub | Agda.TypeChecking.Substitute
iEnd | Agda.Syntax.Position, Agda.Interaction.GhciTop
ifM | Agda.Utils.Monad
IgnoreAbstractMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ignoreAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
ignoreBlocking | Agda.Syntax.Internal
ignoreInterfaces | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
iHaskellImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iHighlighting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ihname | Agda.Compiler.MAlonzo.Misc
iImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iInsideScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IlltypedPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IM | Agda.Interaction.Monad
iModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ImpInsert | Agda.TypeChecking.Implicit
impInsert | Agda.TypeChecking.Implicit
ImplicitInsertion | Agda.TypeChecking.Implicit
ImplicitP | Agda.Syntax.Abstract
Import
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
ImportDirective
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
importDirRange | Agda.Syntax.Concrete
ImportedModule | Agda.Syntax.Concrete
ImportedName
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
importedName | Agda.Syntax.Concrete
importedNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ImportedNS | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ImportPragma | Agda.Syntax.Concrete
imports | Agda.Compiler.MAlonzo.Compiler
importsForPrim | Agda.Compiler.MAlonzo.Primitives
Impossible
1 (Type/Class) | Agda.Utils.Impossible
2 (Data Constructor) | Agda.Utils.Impossible
ImpossiblePragma | Agda.Syntax.Concrete
impossibleTerm | Agda.Syntax.Internal
impRTP | Agda.Compiler.Alonzo.Haskell
impRTS | Agda.Compiler.Alonzo.Haskell
imp_dir | Agda.Syntax.Parser.Lexer
inAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
inc | Agda.Utils.Warshall
InClause | Agda.TypeChecking.Positivity
IncompletePattern | Agda.Interaction.Highlighting.Precise
IncompletePatternMatching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inConcreteMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
inContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
incPcnt | Agda.Compiler.Alonzo.PatternMonad
InDefOf | Agda.TypeChecking.Positivity
indent | Agda.Utils.String
Index
1 (Data Constructor) | Agda.Utils.Suffix
2 (Type/Class) | Agda.Termination.CallGraph
Induction | Agda.Syntax.Common
Inductive | Agda.Syntax.Common
inductiveCheck | Agda.TypeChecking.Rules.Builtin
Inf | Agda.Syntax.Internal
InferDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inferDef | Agda.TypeChecking.Rules.Term
InferExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inferExpr | Agda.TypeChecking.Rules.Term, Agda.TypeChecker, Agda.Interaction.GhciTop
inferHead | Agda.TypeChecking.Rules.Term
InferVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Infinite | Agda.Utils.Warshall
infinite | Agda.Utils.Warshall
Infix | Agda.Syntax.Concrete
InfixDef | Agda.Syntax.Common
infixlP | Agda.Syntax.Concrete.Operators.Parser
infixP | Agda.Syntax.Concrete.Operators.Parser
infixrP | Agda.Syntax.Concrete.Operators.Parser
Info | Agda.Syntax.Info
infoDecl | Agda.Compiler.Alonzo.Main
infodecl | Agda.Compiler.MAlonzo.Compiler
infoOnException | Agda.Interaction.GhciTop
initEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
initGraph | Agda.Utils.Warshall
initMapS | Agda.Auto.Convert
initPState | Agda.Compiler.Alonzo.PatternMonad
initState
1 (Function) | Agda.Syntax.Parser.Monad
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
3 (Function) | Agda.Interaction.GhciTop
inMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
inNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
InScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
InScopeTag | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
inScopeTag | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
insert
1 (Function) | Agda.Utils.Trie
2 (Function) | Agda.Utils.Graph
3 (Function) | Agda.Termination.CallGraph
insertImplicit | Agda.TypeChecking.Implicit
insertImplicitPatterns | Agda.TypeChecking.Rules.LHS.Implicit
insertImplicitProblem | Agda.TypeChecking.Rules.LHS.Implicit
insertPatterns | Agda.TypeChecking.Rules.Def
insertWithKeyM | Agda.Utils.Map
InsideOperandCtx | Agda.Syntax.Fixity
insideScope | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
Instantiate | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
instantiate | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
Instantiated | Agda.Interaction.BasicOps
instantiateDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
InstantiateFull | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
instantiateFull | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
instantiatePattern | Agda.TypeChecking.Rules.LHS
instantiateTel | Agda.TypeChecking.Rules.LHS.Instantiate
inState | Agda.Syntax.Parser.LexActions
InstS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InstV | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
int | Agda.Utils.Pretty
integer | Agda.Utils.Pretty
integerSemiring | Agda.Termination.Semiring
Interaction
1 (Type/Class) | Agda.Interaction.GhciTop
2 (Data Constructor) | Agda.Interaction.GhciTop
interaction | Agda.Interaction.CommandLine.CommandLine
InteractionId
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
interactionLoop | Agda.Interaction.CommandLine.CommandLine
InteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Interface
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InternalError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
internalError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Interval
1 (Type/Class) | Agda.Syntax.Position, Agda.Interaction.GhciTop
2 (Data Constructor) | Agda.Syntax.Position, Agda.Interaction.GhciTop
intervalInvariant | Agda.Syntax.Position, Agda.Interaction.GhciTop
intMap | Agda.Utils.Warshall
introTactic | Agda.Interaction.BasicOps
Inv | Agda.TypeChecking.Injectivity
InvalidPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Invariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Inverse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inverseScopeLookup | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
inverseScopeLookupModule | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
inverseScopeLookupName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
invertP | Agda.Utils.Permutation
InvView | Agda.TypeChecking.Injectivity
io | Agda.TypeChecking.Primitive
IOException | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iotastep | Agda.Auto.Typecheck
ioTCM | Agda.Interaction.GhciTop
ioTCM_ | Agda.Interaction.GhciTop
IsAbstract | Agda.Syntax.Common
isBelow | Agda.Utils.Warshall
isBlockedTerm | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
isCoinductive | Agda.TypeChecking.Rules.Data
iScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isDatatype | Agda.TypeChecking.Coverage
IsEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isEmpty
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.Termination.Matrix
IsEmptyType | Agda.Interaction.BasicOps
isEmptyType | Agda.TypeChecking.Empty
isEmptyTypeC | Agda.TypeChecking.Empty
IsExpr | Agda.Syntax.Concrete.Operators.Parser
isHaskellKind | Agda.Compiler.HaskellTypes
isHole | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
iSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isImported | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
isIndependent | Agda.Interaction.GhciTop
IsInfix | Agda.Syntax.Common
isInfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isInModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
isInteractionMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isJust | Agda.Utils.Maybe
isLeft | Agda.Utils.Either
isLiterate | Agda.Interaction.Options
isMain | Agda.Compiler.Alonzo.Main
isNewerThan | Agda.Interaction.Imports
isNoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isNonfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isNothing | Agda.Utils.Maybe
isntTypeConf | Agda.TypeChecking.Test.Generators
isOperator
1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
isPostfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isPrefix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isRecord | Agda.TypeChecking.Records
isRight | Agda.Utils.Either
isSizeType | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSolvedProblem | Agda.TypeChecking.Rules.LHS
IsSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isSortMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isString | Agda.Utils.Generics
isSubModuleOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
isSuccess | Agda.Utils.QuickCheck
iStart | Agda.Syntax.Position, Agda.Interaction.GhciTop
isType | Agda.TypeChecking.Rules.Term
IsTypeCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isTypeConf | Agda.TypeChecking.Test.Generators
IsType_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isType_ | Agda.TypeChecking.Rules.Term
isUnicodeId | Agda.Utils.Unicode
isVar | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
isVisited | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
isWellScoped | Agda.TypeChecking.Test.Generators
isZero | Agda.Utils.TestHelpers
Item | Agda.TypeChecking.Positivity
iterate' | Agda.Utils.Function
Judgement | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
judgementInteractionId | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
judgToOutputForm | Agda.Interaction.BasicOps
Just | Agda.Utils.Maybe
JustSort | Agda.Interaction.BasicOps
JustType | Agda.Interaction.BasicOps
keepComments | Agda.Syntax.Parser.Comments
keepCommentsM | Agda.Syntax.Parser.Comments
Keyword
1 (Type/Class) | Agda.Syntax.Parser.Tokens
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
keyword
1 (Function) | Agda.Syntax.Parser.LexActions
2 (Function) | Agda.Interaction.Highlighting.Vim
killAbs | Agda.TypeChecking.Test.Generators
KillRange | Agda.Syntax.Position, Agda.Interaction.GhciTop
killRange | Agda.Syntax.Position, Agda.Interaction.GhciTop
killRange1 | Agda.Syntax.Position, Agda.Interaction.GhciTop
killRange2 | Agda.Syntax.Position, Agda.Interaction.GhciTop
killRange3 | Agda.Syntax.Position, Agda.Interaction.GhciTop
killRange4 | Agda.Syntax.Position, Agda.Interaction.GhciTop
killRange5 | Agda.Syntax.Position, Agda.Interaction.GhciTop
killRange6 | Agda.Syntax.Position, Agda.Interaction.GhciTop
killRange7 | Agda.Syntax.Position, Agda.Interaction.GhciTop
KillVar | Agda.TypeChecking.Test.Generators
killVar | Agda.TypeChecking.Test.Generators
KindOfName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
KwAbstract | Agda.Syntax.Parser.Tokens
KwBUILTIN | Agda.Syntax.Parser.Tokens
KwCoData | Agda.Syntax.Parser.Tokens
KwCOMPILED | Agda.Syntax.Parser.Tokens
KwCOMPILED_DATA | Agda.Syntax.Parser.Tokens
KwCOMPILED_TYPE | Agda.Syntax.Parser.Tokens
KwConstructor | Agda.Syntax.Parser.Tokens
KwData | Agda.Syntax.Parser.Tokens
KwField | Agda.Syntax.Parser.Tokens
KwForall | Agda.Syntax.Parser.Tokens
KwHiding | Agda.Syntax.Parser.Tokens
KwIMPORT | Agda.Syntax.Parser.Tokens
KwImport | Agda.Syntax.Parser.Tokens
KwIMPOSSIBLE | Agda.Syntax.Parser.Tokens
KwIn | Agda.Syntax.Parser.Tokens
KwInfix | Agda.Syntax.Parser.Tokens
KwInfixL | Agda.Syntax.Parser.Tokens
KwInfixR | Agda.Syntax.Parser.Tokens
KwLet | Agda.Syntax.Parser.Tokens
KwLINE | Agda.Syntax.Parser.Tokens
KwModule | Agda.Syntax.Parser.Tokens
KwMutual | Agda.Syntax.Parser.Tokens
KwOpen | Agda.Syntax.Parser.Tokens
KwOPTIONS | Agda.Syntax.Parser.Tokens
KwPostulate | Agda.Syntax.Parser.Tokens
KwPrimitive | Agda.Syntax.Parser.Tokens
KwPrivate | Agda.Syntax.Parser.Tokens
KwProp | Agda.Syntax.Parser.Tokens
KwPublic | Agda.Syntax.Parser.Tokens
KwRecord | Agda.Syntax.Parser.Tokens
KwRenaming | Agda.Syntax.Parser.Tokens
KwRewrite | Agda.Syntax.Parser.Tokens
KwSet | Agda.Syntax.Parser.Tokens
KwTo | Agda.Syntax.Parser.Tokens
KwUsing | Agda.Syntax.Parser.Tokens
KwWhere | Agda.Syntax.Parser.Tokens
KwWith | Agda.Syntax.Parser.Tokens
L
1 (Data Constructor) | Agda.Utils.Map
2 (Data Constructor) | Agda.Interaction.GhciTop
label | Agda.Utils.QuickCheck
labels | Agda.Utils.QuickCheck
Lam
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Internal
4 (Data Constructor) | Agda.Syntax.Abstract
lambda | Agda.Syntax.Concrete.Pretty
LamBinding
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
lamBrackets | Agda.Syntax.Fixity
lamFreq | Agda.TypeChecking.Test.Generators
Layout | Agda.Syntax.Parser.Monad
layout | Agda.Syntax.Parser.Lexer
LayoutContext | Agda.Syntax.Parser.Monad
layoutKeywords | Agda.Syntax.Parser.Tokens
lbrace | Agda.Utils.Pretty
lbrack | Agda.Utils.Pretty
Le | Agda.Termination.CallGraph
LeftAssoc | Agda.Syntax.Fixity
LeftDisjunct | Agda.Auto.NarrowingSearch
leftDistributive | Agda.Utils.TestHelpers
LeftHandSide | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
LeftMode | Agda.Utils.Pretty
LeftOfArrow | Agda.TypeChecking.Positivity
LeftOperandCtx | Agda.Syntax.Fixity
LegendMatrix
1 (Type/Class) | Agda.Utils.Warshall
2 (Data Constructor) | Agda.Utils.Warshall
Leq | Agda.TypeChecking.SizedTypes
leqLevel | Agda.TypeChecking.Conversion
leqSort | Agda.TypeChecking.Conversion
leqType | Agda.TypeChecking.Conversion
Let
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
LetApply | Agda.Syntax.Abstract
LetBind | Agda.Syntax.Abstract
LetBinding | Agda.Syntax.Abstract
LetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
LetDef | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
LetDefs | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
LetInfo | Agda.Syntax.Info
LetOpen | Agda.Syntax.Abstract
LetRange | Agda.Syntax.Info
letters | Agda.Compiler.Alonzo.Main
LevelAtom | Agda.TypeChecking.Level
LevelKit
1 (Type/Class) | Agda.TypeChecking.Level
2 (Data Constructor) | Agda.TypeChecking.Level
levelMax | Agda.TypeChecking.Level
levelSuc | Agda.TypeChecking.Level
levelSucFunction | Agda.TypeChecking.Level
LevelView | Agda.TypeChecking.Level
levelView | Agda.TypeChecking.Level
levelZero | Agda.TypeChecking.Level
LexAction | Agda.Syntax.Parser.Alex
lexer | Agda.Syntax.Parser.Lexer
lexError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser.LexActions
lexInput | Agda.Syntax.Parser.Alex
LexOrder | Agda.Termination.Lexicographic
lexOrder | Agda.Termination.Lexicographic
lexPos | Agda.Syntax.Parser.Alex
LexPredicate | Agda.Syntax.Parser.Alex
lexPrevChar | Agda.Syntax.Parser.Alex
LexState | Agda.Syntax.Parser.Monad
lexToken | Agda.Syntax.Parser.LexActions
LHS
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Type/Class) | Agda.Syntax.Abstract
4 (Data Constructor) | Agda.Syntax.Abstract
LHSInfo | Agda.Syntax.Info
LHSRange | Agda.Syntax.Info
liftEither | Agda.Utils.Monad
liftP | Agda.Syntax.Parser.LookAhead
liftTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
lineLength | Agda.Utils.Pretty
Lisp | Agda.Interaction.GhciTop
list | Agda.TypeChecking.Primitive
listenToMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
listOf | Agda.Utils.QuickCheck
listOf1 | Agda.Utils.QuickCheck
listOfElements | Agda.Utils.TestHelpers
listToMaybe | Agda.Utils.Maybe
Lit
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Abstract
LitChar | Agda.Syntax.Literal
litChar | Agda.Syntax.Parser.StringLiterals
Literal | Agda.Syntax.Literal
literal
1 (Function) | Agda.Syntax.Parser.LexActions
2 (Function) | Agda.Compiler.MAlonzo.Compiler
literate | Agda.Syntax.Parser.Lexer
LitFloat | Agda.Syntax.Literal
LitFocus | Agda.TypeChecking.Rules.LHS.Problem
litFreq | Agda.TypeChecking.Test.Generators
LitInt | Agda.Syntax.Literal
LitLevel | Agda.Syntax.Literal
LitMP | Agda.TypeChecking.Coverage.Match
LitP
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Abstract
LitString | Agda.Syntax.Literal
litString | Agda.Syntax.Parser.StringLiterals
litType | Agda.TypeChecking.Rules.Term
loadFile | Agda.Interaction.CommandLine.CommandLine
localNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
localScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
localToAbstract | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
LocalV | Agda.Syntax.Concrete.Operators.Parser
LocalVars | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
LocalVsImportedModuleClash | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
longNameLength | Agda.Interaction.GhciTop
look | Agda.Utils.ReadP
LookAhead | Agda.Syntax.Parser.LookAhead
lookup | Agda.Utils.Graph
lookupConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
lookupEdge | Agda.Utils.Warshall
lookupInteractionId | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
lookupMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
lookupMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
lookupPath | Agda.Utils.Trie
lookupPrimitiveFunction | Agda.TypeChecking.Primitive
lookupSection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
LowerMeta | Agda.Interaction.GhciTop
lowerMeta | Agda.Interaction.GhciTop
lowMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
lparen | Agda.Utils.Pretty
lst | Agda.Compiler.Alonzo.PatternMonad
Lt | Agda.Termination.CallGraph
Lub | Agda.Syntax.Internal
Lvl
1 (Type/Class) | Agda.TypeChecking.Primitive
2 (Data Constructor) | Agda.TypeChecking.Primitive
main | Agda.Main
makeAbstract | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
makeAbstractClause | Agda.Interaction.MakeCase
makeAbsurdClause | Agda.Interaction.MakeCase
makeCase | Agda.Interaction.MakeCase
makeClosed | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
makeConfiguration | Agda.TypeChecking.Test.Generators
makeEnv | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
makeIncludeDirsAbsolute | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
makeOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
makeSubstitution | Agda.TypeChecking.Rules.LHS.Unify
malonzoDir | Agda.Compiler.MAlonzo.Compiler
many | Agda.Utils.ReadP
many1 | Agda.Utils.ReadP
manyTill | Agda.Utils.ReadP
mapFlag | Agda.Interaction.Options
mapMaybe | Agda.Utils.Maybe
mapMaybeM | Agda.Utils.Monad
mapNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapNameSpaceM | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapNodes | Agda.Utils.Warshall
MapS | Agda.Auto.Convert
mapScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapScopeM | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapScopeM_ | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapScope_ | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapSize | Agda.Utils.QuickCheck
mapTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MArgList | Agda.Auto.Syntax
Mat | Agda.Termination.CallGraph
mat | Agda.Termination.CallGraph
Match
1 (Type/Class) | Agda.TypeChecking.Coverage.Match
2 (Type/Class) | Agda.TypeChecking.Patterns.Match
3 (Type/Class) | Agda.TypeChecking.DisplayForm
match
1 (Function) | Agda.Syntax.Parser.LookAhead
2 (Function) | Agda.TypeChecking.Coverage.Match
3 (Function) | Agda.Interaction.Highlighting.Vim
4 (Function) | Agda.TypeChecking.DisplayForm
match' | Agda.Syntax.Parser.LookAhead
matchCall | Agda.Utils.Trace
matchCalls | Agda.Utils.Trace
matchClause | Agda.TypeChecking.Coverage.Match
matchCommand | Agda.Interaction.CommandLine.CommandLine
matchDisplayForm | Agda.TypeChecking.DisplayForm
matches | Agda.Interaction.Highlighting.Vim
MatchLit | Agda.TypeChecking.Coverage.Match
matchLits | Agda.TypeChecking.Coverage.Match
matchPat | Agda.TypeChecking.Coverage.Match
matchPats | Agda.TypeChecking.Coverage.Match
matchPattern | Agda.TypeChecking.Patterns.Match
matchPatterns | Agda.TypeChecking.Patterns.Match
matchTrace | Agda.Utils.Trace
Matrix
1 (Type/Class) | Agda.Termination.Matrix
2 (Type/Class) | Agda.Utils.Warshall
matrix
1 (Function) | Agda.Termination.Matrix
2 (Function) | Agda.Utils.Warshall
matrixInvariant | Agda.Termination.Matrix
matrixUsingRowGen | Agda.Termination.Matrix
Max | Agda.TypeChecking.Level
maxDiscard | Agda.Utils.QuickCheck
maxName | Agda.TypeChecking.Level
maxSize | Agda.Utils.QuickCheck
maxSuccess | Agda.Utils.QuickCheck
Maybe | Agda.Utils.Maybe
maybe | Agda.Utils.Maybe
maybeCoGen | Agda.Utils.TestHelpers
maybeGen | Agda.Utils.TestHelpers
maybePrefixMatch | Agda.Utils.List
maybePrimCon | Agda.TypeChecking.Level
maybePrimDef | Agda.TypeChecking.Level
maybeQualConName | Agda.Compiler.Alonzo.Main
maybeQualDefName | Agda.Compiler.Alonzo.Main
maybeQualName | Agda.Compiler.Alonzo.Main
maybeToList | Agda.Utils.Maybe
mazBoolToHBool | Agda.Compiler.MAlonzo.Primitives
mazCharToInteger | Agda.Compiler.MAlonzo.Primitives
mazCoerce | Agda.Compiler.MAlonzo.Misc
mazerror | Agda.Compiler.MAlonzo.Misc
mazHBoolToBool | Agda.Compiler.MAlonzo.Primitives
mazHListToList | Agda.Compiler.MAlonzo.Primitives
mazIntegerToNat | Agda.Compiler.MAlonzo.Primitives
mazIntToNat | Agda.Compiler.MAlonzo.Primitives
mazListToHList | Agda.Compiler.MAlonzo.Primitives
mazListToString | Agda.Compiler.MAlonzo.Primitives
mazMod | Agda.Compiler.MAlonzo.Misc
mazMod' | Agda.Compiler.MAlonzo.Misc
mazName | Agda.Compiler.MAlonzo.Misc
mazNatToInt | Agda.Compiler.MAlonzo.Primitives
mazNatToInteger | Agda.Compiler.MAlonzo.Primitives
mazstr | Agda.Compiler.MAlonzo.Misc
mazStringToList | Agda.Compiler.MAlonzo.Primitives
MB | Agda.Auto.NarrowingSearch
mbcase | Agda.Auto.NarrowingSearch
mbfailed | Agda.Auto.NarrowingSearch
mbind | Agda.Auto.NarrowingSearch
mbpcase | Agda.Auto.NarrowingSearch
mbret | Agda.Auto.NarrowingSearch
mcompoint | Agda.Auto.NarrowingSearch
mergeInterface | Agda.Interaction.Imports
mergeNames | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mergeScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mergeScopes | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
Meta | Agda.Auto.NarrowingSearch
MetaArg | Agda.TypeChecking.Positivity
MetaCannotDependOn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaEnv | Agda.Auto.NarrowingSearch
MetaId
1 (Type/Class) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Internal
MetaInfo
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
3 (Type/Class) | Agda.Interaction.Highlighting.Precise
4 (Data Constructor) | Agda.Interaction.Highlighting.Precise
5 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
metaInstance | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
MetaInstantiation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaLevel | Agda.TypeChecking.Level
metaNumber | Agda.Syntax.Info
MetaOccursInItself | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
metaParseExpr | Agda.Interaction.CommandLine.CommandLine
MetaPriority
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
metaRange | Agda.Syntax.Info
MetaS | Agda.Syntax.Internal
metaScope | Agda.Syntax.Info
MetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaV | Agda.Syntax.Internal
MetaVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Metavar
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
MetaVariable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
metaVariable | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
MExp | Agda.Auto.Syntax
MId | Agda.Auto.Syntax
miInterface | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
minfoAsName | Agda.Syntax.Info
minfoAsTo | Agda.Syntax.Info
minfoRange | Agda.Syntax.Info
MissingDefinition | Agda.Syntax.Concrete.Definitions
MissingTypeSignature | Agda.Syntax.Concrete.Definitions
MissingWithClauses | Agda.Syntax.Concrete.Definitions
miTimeStamp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
miWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MIx
1 (Type/Class) | Agda.Termination.Matrix
2 (Data Constructor) | Agda.Termination.Matrix
mIxInvariant | Agda.Termination.Matrix
mkAbsolute | Agda.Utils.FileName, Agda.Interaction.GhciTop
mkBoundName_ | Agda.Syntax.Concrete
mkContextEntry | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
mkDefInfo | Agda.Syntax.Info
mkMatrix | Agda.Utils.Warshall
mkName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mkName_ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mkPrimFun1 | Agda.TypeChecking.Primitive
mkPrimFun2 | Agda.TypeChecking.Primitive
mkPrimFun4 | Agda.TypeChecking.Primitive
MkStr | Agda.Utils.QuickCheck
mkType | Agda.Syntax.Internal
MM | Agda.Auto.NarrowingSearch
mmbpcase | Agda.Auto.NarrowingSearch
mmcase | Agda.Auto.NarrowingSearch
mmmcase | Agda.Auto.NarrowingSearch
mmpcase | Agda.Auto.NarrowingSearch
MName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mnameFromList | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mnameToConcrete | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mnameToList | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mobs | Agda.Auto.NarrowingSearch
Mode | Agda.Utils.Pretty
mode | Agda.Utils.Pretty
modifyCurrentNameSpace | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyCurrentScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyCurrentScopeM | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyImportedSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
modifyNamedScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyNamedScopeM | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
modifyScopeInfo | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyScopes | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifySignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
modSub | Agda.TypeChecking.Rules.LHS.Unify
Module
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Interaction.Highlighting.Precise
ModuleArityMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ModuleDefinedInOtherFile | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ModuleDoesntExport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ModuleInfo
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ModuleMacro | Agda.Syntax.Concrete
ModuleName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
moduleName | Agda.Interaction.Imports
moduleName' | Agda.Interaction.Imports
ModuleNameDoesntMatchFileName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
moduleNameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
moduleNameToFileName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
moduleParser
1 (Function) | Agda.Syntax.Parser.Parser
2 (Function) | Agda.Syntax.Parser, Agda.Interaction.GhciTop
ModulesInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
moduleStr | Agda.Compiler.Alonzo.Names
ModuleTag | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ModuleToSource | Agda.Interaction.FindFile
MonadException | Agda.TypeChecking.Monad.Exception
MonadTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
movePos | Agda.Syntax.Position, Agda.Interaction.GhciTop
movePosByString | Agda.Syntax.Position, Agda.Interaction.GhciTop
mparen | Agda.Syntax.Concrete.Operators
mparens | Agda.Utils.Pretty
MPat | Agda.TypeChecking.Coverage.Match
mpret | Agda.Auto.NarrowingSearch
mprincipalpresent | Agda.Auto.NarrowingSearch
msubs | Agda.Auto.Typecheck
mul
1 (Function) | Agda.Termination.Semiring
2 (Function) | Agda.Termination.Matrix
MultipleFixityDecls | Agda.Syntax.Concrete.Definitions
munch | Agda.Utils.ReadP
munch1 | Agda.Utils.ReadP
MutId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Mutual | Agda.Syntax.Concrete
MutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvInstantiation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvJudgement | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvListeners | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MyMB | Agda.Auto.Syntax
MyPB | Agda.Auto.Syntax
Name
1 (Type/Class) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
3 (Type/Class) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
4 (Data Constructor) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
5 (Data Constructor) | Agda.Interaction.Highlighting.Precise
nameBindingSite | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
nameConcrete | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
Named
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
named | Agda.Syntax.Common
NamedArg | Agda.Syntax.Common
NamedClause
1 (Type/Class) | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
2 (Data Constructor) | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
namedThing | Agda.Syntax.Common
nameFixity | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
nameFreq | Agda.TypeChecking.Test.Generators
NameFreqs
1 (Type/Class) | Agda.TypeChecking.Test.Generators
2 (Data Constructor) | Agda.TypeChecking.Test.Generators
nameFreqs | Agda.TypeChecking.Test.Generators
NameId
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
nameId | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
NameKind | Agda.Interaction.Highlighting.Precise
nameModifiers | Agda.Interaction.GhciTop
nameOf | Agda.Syntax.Common
nameOfBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
NamePart | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NamesInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
namesInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
NameSpace
1 (Type/Class) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
2 (Data Constructor) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
NameSpaceId | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
NameTag | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
Nat
1 (Type/Class) | Agda.Auto.Syntax
2 (Type/Class) | Agda.Syntax.Common
3 (Type/Class) | Agda.TypeChecking.Primitive
4 (Data Constructor) | Agda.TypeChecking.Primitive
natural | Agda.Utils.TestHelpers
neg | Agda.TypeChecking.Polarity
Negative | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
neighbours | Agda.Utils.Graph
nest
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
nestedComment | Agda.Syntax.Parser.Comments
NeutralLevel | Agda.TypeChecking.Level
newArgsMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newArgsMetaCtx | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newCall | Agda.Utils.Trace
newCTree | Agda.Auto.NarrowingSearch
newEdge | Agda.Utils.Warshall
NewFlex | Agda.Utils.Warshall
newLayoutContext | Agda.Syntax.Parser.Layout
newMeta
1 (Function) | Agda.Auto.NarrowingSearch
2 (Function) | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
newMeta' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
NewModuleName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
NewModuleQName
1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
NewName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
newPlaceholder | Agda.Auto.NarrowingSearch
newQuestionMark | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newRecordMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newRecordMetaCtx | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newSortMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newSortMetaCtx | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newSubConstraints | Agda.Auto.NarrowingSearch
newTelMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newTypeMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newTypeMeta_ | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newValueMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newValueMeta' | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newValueMetaCtx | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newValueMetaCtx' | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
nextChar | Agda.Syntax.Parser.LookAhead
nextFresh | Agda.Utils.Fresh
nextName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
nextNode | Agda.Utils.Warshall
nextPolarity | Agda.TypeChecking.Conversion
nextSuffix | Agda.Utils.Suffix
Nice | Agda.Syntax.Concrete.Definitions
NiceConstructor | Agda.Syntax.Concrete.Definitions
NiceDeclaration | Agda.Syntax.Concrete.Definitions
niceDeclarations | Agda.Syntax.Concrete.Definitions
NiceDef | Agda.Syntax.Concrete.Definitions
NiceDefinition | Agda.Syntax.Concrete.Definitions
NiceField | Agda.Syntax.Concrete.Definitions
NiceImport | Agda.Syntax.Concrete.Definitions
NiceModule | Agda.Syntax.Concrete.Definitions
NiceModuleMacro | Agda.Syntax.Concrete.Definitions
NiceOpen | Agda.Syntax.Concrete.Definitions
NicePragma | Agda.Syntax.Concrete.Definitions
NiceTypeSignature | Agda.Syntax.Concrete.Definitions
No
1 (Data Constructor) | Agda.TypeChecking.Coverage.Match
2 (Data Constructor) | Agda.TypeChecking.Patterns.Match
NoApp | Agda.TypeChecking.EtaContract
NoBind | Agda.Syntax.Internal
NoBindingForBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoBody | Agda.Syntax.Internal
noConstraints | Agda.TypeChecking.Constraints
Node
1 (Type/Class) | Agda.Utils.Warshall
2 (Type/Class) | Agda.TypeChecking.Positivity
NodeId | Agda.Utils.Warshall
nodeMap | Agda.Utils.Warshall
nodes | Agda.Utils.Graph
NoExpectedFailure | Agda.Utils.QuickCheck
NoFunV | Agda.Syntax.Internal
NoId | Agda.Auto.Syntax
NoInsertNeeded | Agda.TypeChecking.Implicit
NoInv | Agda.TypeChecking.Injectivity
noiotastep | Agda.Auto.Typecheck
noiotastep' | Agda.Auto.Typecheck
NoLayout | Agda.Syntax.Parser.Monad
noLiterals | Agda.TypeChecking.Test.Generators
noMatchLit | Agda.TypeChecking.Coverage.Match
noModuleName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
noMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
NoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
noName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
noName_ | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NonApplication | Agda.Syntax.Abstract.Views
NonAssoc | Agda.Syntax.Fixity
NonEmpty | Agda.Utils.QuickCheck
NonEmptyList | Agda.Utils.QuickCheck
nonfixP | Agda.Syntax.Concrete.Operators.Parser
NonNegative
1 (Data Constructor) | Agda.Utils.QuickCheck
2 (Type/Class) | Agda.Utils.QuickCheck
NonPositively | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NonZero
1 (Data Constructor) | Agda.Utils.QuickCheck
2 (Type/Class) | Agda.Utils.QuickCheck
NoParent | Agda.Utils.Trace
NoParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noPatternMatchingOnCodata | Agda.TypeChecking.Rules.LHS
Nope | Agda.Syntax.Info
NoPrio | Agda.Auto.NarrowingSearch
noProp | Agda.TypeChecking.Test.Generators
noRange | Agda.Syntax.Position, Agda.Interaction.GhciTop
NoReduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoRHSRequiresAbsurdPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
norm
1 (Function) | Agda.Auto.Typecheck
2 (Function) | Agda.Auto.Convert
normal | Agda.Syntax.Parser.Lexer
Normalise | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
normalise | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
Normalised | Agda.Interaction.BasicOps
normalMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noShadowingOfConstructors | Agda.TypeChecking.Rules.LHS
noShrink | Agda.TypeChecking.Test.Generators
NoSuchBuiltinName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoSuchModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoSuchName | Agda.TypeChecking.Implicit
NoSuchPrimitiveFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoSuffix | Agda.Utils.Suffix
not' | Agda.Syntax.Parser.Alex
NotADatatype | Agda.TypeChecking.Coverage
notAHaskellKind | Agda.Compiler.HaskellTypes
notAHaskellType | Agda.Compiler.HaskellTypes
NotAllowedInMutual | Agda.Syntax.Concrete.Definitions
NotAModuleExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotAnExpression | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotAProperTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotAValidLetBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotB | Agda.Auto.NarrowingSearch
NotBlocked | Agda.Syntax.Internal
notBlocked | Agda.Syntax.Internal
NotDelayed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
note | Agda.Interaction.Highlighting.Precise
NotFound | Agda.Interaction.FindFile
NotHidden
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Common
notHiddenFreq | Agda.TypeChecking.Test.Generators
Nothing | Agda.Utils.Maybe
NothingAppliedToHiddenArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NothingToSplit | Agda.TypeChecking.Rules.LHS.Problem
nothingToSplitError | Agda.TypeChecking.Rules.LHS.Instantiate
NotImplemented | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotInductive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotInjective | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotInScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
notInScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
NotLeqSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotM | Agda.Auto.NarrowingSearch
NotPB | Agda.Auto.NarrowingSearch
noTrace | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
notSoNiceDeclarations | Agda.Syntax.Concrete.Definitions
NotStrictlyPositive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotSupported | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoType
1 (Type/Class) | Agda.TypeChecking.Test.Generators
2 (Data Constructor) | Agda.TypeChecking.Test.Generators
NoUnify | Agda.TypeChecking.Rules.LHS.Unify
NoWhere | Agda.Syntax.Concrete
NoWithFunction | Agda.TypeChecking.Rules.Def
nPi | Agda.TypeChecking.Primitive
nsModules | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
nsNames | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
Number | Agda.Interaction.Highlighting.Precise
numOfMainS | Agda.Compiler.Alonzo.Main
numOfName | Agda.Compiler.Alonzo.Names
numOfQName | Agda.Compiler.Alonzo.Names
numTests | Agda.Utils.QuickCheck
O | Agda.Auto.Convert
Occ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
OccClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
occClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
OccCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
occConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
occDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
occFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
OccPos | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
occPosition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Occurrence | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Occurrences | Agda.TypeChecking.Positivity
occurrences | Agda.TypeChecking.Positivity
Occurs | Agda.TypeChecking.MetaVars.Occurs
occurs | Agda.TypeChecking.MetaVars.Occurs
occursAs | Agda.TypeChecking.Positivity
occursCheck
1 (Function) | Agda.Auto.SearchControl
2 (Function) | Agda.TypeChecking.MetaVars.Occurs
3 (Function) | Agda.TypeChecking.Rules.LHS.Unify
OccursWhere | Agda.TypeChecking.Positivity
octDigit | Agda.Utils.Char
ofExpr | Agda.Interaction.BasicOps
offsideRule | Agda.Syntax.Parser.Layout
ofName | Agda.Interaction.BasicOps
OfType | Agda.Interaction.BasicOps
OfType' | Agda.Interaction.BasicOps
OHCon | Agda.Syntax.Internal.Pattern
OHPats | Agda.Syntax.Internal.Pattern
OK | Agda.Auto.NarrowingSearch
OldModuleName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
OldName
1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
OldQName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
on | Agda.Interaction.Highlighting.Vim
one | Agda.Termination.Semiring
OneHolePattern | Agda.Syntax.Internal.Pattern
OneHolePatterns | Agda.Syntax.Internal.Pattern
OneLineMode | Agda.Utils.Pretty
oneof | Agda.Utils.QuickCheck
onSub | Agda.TypeChecking.Rules.LHS.Unify
onTrace | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
Op | Agda.TypeChecking.Primitive
OpApp | Agda.Syntax.Concrete
OpAppP | Agda.Syntax.Concrete
OpAppV | Agda.Syntax.Concrete.Operators.Parser
opBrackets | Agda.Syntax.Fixity
Open
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
4 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
openBrace | Agda.Syntax.Parser.Layout
openModule_ | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
OpenShortHand | Agda.Syntax.Concrete
OpenThing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
oplus | Agda.Utils.SemiRing
opP | Agda.Syntax.Concrete.Operators.Parser
optAllowUnsolved | Agda.Interaction.Options
optCompile | Agda.Interaction.Options
optCompileAlonzo | Agda.Interaction.Options
optCompileMAlonzo | Agda.Interaction.Options
optCompletenessCheck | Agda.Interaction.Options
optCSSFile | Agda.Interaction.Options
optDisablePositivity | Agda.Interaction.Options
optGenerateHTML | Agda.Interaction.Options
optGenerateVimFile | Agda.Interaction.Options
optGhcFlags | Agda.Interaction.Options
optHTMLDir | Agda.Interaction.Options
optIgnoreInterfaces | Agda.Interaction.Options
optIncludeDirs | Agda.Interaction.Options
optInputFile | Agda.Interaction.Options
optInteractive | Agda.Interaction.Options
option | Agda.Utils.ReadP
optional | Agda.Utils.ReadP
optionError | Agda.Main
Options | Agda.Interaction.Options
OptionsPragma
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
optMAlonzoDir | Agda.Interaction.Options
optProgramName | Agda.Interaction.Options
optProofIrrelevance | Agda.Interaction.Options
optRunTests | Agda.Interaction.Options
optShowHelp | Agda.Interaction.Options
optShowImplicit | Agda.Interaction.Options
optShowVersion | Agda.Interaction.Options
optSizedTypes | Agda.Interaction.Options
optTerminationCheck | Agda.Interaction.Options
optUniverseCheck | Agda.Interaction.Options
optUniversePolymorphism | Agda.Interaction.Options
optUnreachableCheck | Agda.Interaction.Options
optVerbose | Agda.Interaction.Options
Or | Agda.Auto.NarrowingSearch
Order | Agda.Termination.CallGraph
Ordered | Agda.Utils.QuickCheck
OrderedList | Agda.Utils.QuickCheck
orderedList | Agda.Utils.QuickCheck
orderFields | Agda.TypeChecking.Records
OtherAspect | Agda.Interaction.Highlighting.Precise
otherAspects | Agda.Interaction.Highlighting.Precise
OtherSize | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
OtherV | Agda.Syntax.Concrete.Operators.Parser
otimes | Agda.Utils.SemiRing
Out | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
outFile | Agda.Compiler.MAlonzo.Compiler
outFile' | Agda.Compiler.MAlonzo.Compiler
OutputForm | Agda.Interaction.BasicOps
OutputForm' | Agda.Interaction.BasicOps
outputFormId | Agda.Interaction.BasicOps
outputHsModule | Agda.Compiler.Alonzo.Haskell
outsideScope | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
overlapping | Agda.Interaction.Highlighting.Range
OverlappingProjects | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PageMode | Agda.Utils.Pretty
par | Agda.Auto.Print
Paren | Agda.Syntax.Concrete
paren | Agda.Syntax.Concrete.Operators
ParenP | Agda.Syntax.Concrete
parens
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
Parent | Agda.Utils.Trace
ParentCall | Agda.Utils.Trace
ParenV | Agda.Syntax.Concrete.Operators.Parser
pargs | Agda.Auto.Print
parse
1 (Function) | Agda.Utils.ReadP
2 (Function) | Agda.Syntax.Parser.Monad
3 (Function) | Agda.Syntax.Parser, Agda.Interaction.GhciTop
parseAndDoAtToplevel | Agda.Interaction.GhciTop
parseApplication | Agda.Syntax.Concrete.Operators
ParseError
1 (Type/Class) | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
2 (Data Constructor) | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
parseError | Agda.Syntax.Parser.Monad
parseErrorAt | Agda.Syntax.Parser.Monad
parseExpr | Agda.Interaction.CommandLine.CommandLine
parseExprIn | Agda.Interaction.BasicOps
ParseFailed | Agda.Syntax.Parser.Monad
parseFile | Agda.Syntax.Parser.Monad
parseFile' | Agda.Syntax.Parser, Agda.Interaction.GhciTop
ParseFlags
1 (Type/Class) | Agda.Syntax.Parser.Monad
2 (Data Constructor) | Agda.Syntax.Parser.Monad
parseFlags | Agda.Syntax.Parser.Monad
parseInp | Agda.Syntax.Parser.Monad
parseKeepComments | Agda.Syntax.Parser.Monad
parseLastPos | Agda.Syntax.Parser.Monad
parseLayout | Agda.Syntax.Parser.Monad
parseLexState | Agda.Syntax.Parser.Monad
parseLHS | Agda.Syntax.Concrete.Operators
parseLiterate | Agda.Syntax.Parser, Agda.Interaction.GhciTop
ParseOk | Agda.Syntax.Parser.Monad
parsePluginOptions | Agda.Interaction.Options
parsePos | Agda.Syntax.Parser.Monad
parsePosString
1 (Function) | Agda.Syntax.Parser.Monad
2 (Function) | Agda.Syntax.Parser, Agda.Interaction.GhciTop
parsePragmaOptions | Agda.Interaction.Options
parsePrevChar | Agda.Syntax.Parser.Monad
parsePrevToken | Agda.Syntax.Parser.Monad
Parser
1 (Type/Class) | Agda.Syntax.Parser.Monad
2 (Type/Class) | Agda.Syntax.Parser, Agda.Interaction.GhciTop
ParseResult | Agda.Syntax.Parser.Monad
parseStandardOptions | Agda.Interaction.Options
ParseState | Agda.Syntax.Parser.Monad
partP | Agda.Syntax.Concrete.Operators.Parser
Pat | Agda.Auto.Syntax
PatConApp | Agda.Auto.Syntax
PatExp | Agda.Auto.Syntax
PatInfo | Agda.Syntax.Info
PatName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
PatRange | Agda.Syntax.Info
PatSource | Agda.Syntax.Info
patsToTerms | Agda.TypeChecking.With
Pattern
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Internal
3 (Type/Class) | Agda.Syntax.Abstract
Pattern' | Agda.Syntax.Abstract
PatternErr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PatternShadowsConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
patternViolation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PatVar | Agda.Auto.Syntax
PB | Agda.Auto.NarrowingSearch
PBlocked | Agda.Auto.NarrowingSearch
pcargs | Agda.Auto.Typecheck
pcexp | Agda.Auto.Typecheck
pconName | Agda.Compiler.MAlonzo.Primitives
PDoubleBlocked | Agda.Auto.NarrowingSearch
PEConApp | Agda.Auto.Typecheck
PEConPar | Agda.Auto.Typecheck
pelr | Agda.Auto.Print
PENo | Agda.Auto.Typecheck
Perm | Agda.Utils.Permutation
Permutation | Agda.Utils.Permutation
permute | Agda.Utils.Permutation
PersistentOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
PEval | Agda.Auto.Typecheck
pexp | Agda.Auto.Print
pfail | Agda.Utils.ReadP
pHidden | Agda.Syntax.Concrete.Pretty
phnargs | Agda.Auto.Typecheck
phnexp | Agda.Auto.Typecheck
Pi
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Internal
4 (Data Constructor) | Agda.Syntax.Abstract
piAbstractTerm | Agda.TypeChecking.Abstract
piApply | Agda.TypeChecking.Substitute
piBrackets | Agda.Syntax.Fixity
pickid | Agda.Auto.Typecheck
pid | Agda.Auto.Print
piFreq | Agda.TypeChecking.Test.Generators
PiHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
plugHole | Agda.Syntax.Internal.Pattern
Plus | Agda.TypeChecking.Level
PlusView | Agda.TypeChecking.Level
PM | Agda.Compiler.Alonzo.PatternMonad
Pn | Agda.Syntax.Position, Agda.Interaction.GhciTop
polarities | Agda.TypeChecking.Polarity
Polarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
polarity | Agda.TypeChecking.Polarity
popContext | Agda.Syntax.Parser.Monad
popLexState | Agda.Syntax.Parser.Monad
popMapS | Agda.Auto.Convert
posCol | Agda.Syntax.Position, Agda.Interaction.GhciTop
Position | Agda.Syntax.Position, Agda.Interaction.GhciTop
positionInvariant | Agda.Syntax.Position, Agda.Interaction.GhciTop
Positive
1 (Data Constructor) | Agda.Utils.QuickCheck
2 (Type/Class) | Agda.Utils.QuickCheck
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
positive | Agda.Utils.TestHelpers
positivityCheckEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
posLine | Agda.Syntax.Position, Agda.Interaction.GhciTop
posPos | Agda.Syntax.Position, Agda.Interaction.GhciTop
postfixP | Agda.Syntax.Concrete.Operators.Parser
postop | Agda.Syntax.Concrete.Operators.Parser
posToRange | Agda.Syntax.Position, Agda.Interaction.GhciTop
PostponedTypeCheckingProblem | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
postponeTypeCheckingProblem | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
postponeTypeCheckingProblem_ | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
Postulate
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Interaction.Highlighting.Precise
Pragma
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Type/Class) | Agda.Syntax.Abstract
4 (Data Constructor) | Agda.Syntax.Abstract
PragmaOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Precedence | Agda.Syntax.Fixity
Pred | Agda.TypeChecking.Primitive
Prefix | Agda.Utils.List
PrefixDef | Agda.Syntax.Common
prefixP | Agda.Syntax.Concrete.Operators.Parser
preMeta | Agda.Interaction.GhciTop
preop | Agda.Syntax.Concrete.Operators.Parser
preserveDecodedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
Pretty | Agda.Utils.Pretty
pretty
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
prettyA
1 (Function) | Agda.Syntax.Abstract.Pretty
2 (Function) | Agda.TypeChecking.Pretty
PrettyContext
1 (Type/Class) | Agda.TypeChecking.Pretty
2 (Data Constructor) | Agda.TypeChecking.Pretty
prettyContext | Agda.Interaction.GhciTop
prettyError | Agda.TypeChecking.Errors, Agda.Interaction.GhciTop
prettyGraph | Agda.TypeChecking.Positivity
prettyList | Agda.TypeChecking.Pretty
prettyPrec | Agda.Utils.Pretty
prettyPrint | Agda.Compiler.MAlonzo.Pretty
prettySplitError | Agda.Interaction.MakeCase
PrettyTCM | Agda.TypeChecking.Pretty, Agda.TypeChecking.Errors, Agda.Interaction.GhciTop
prettyTCM | Agda.TypeChecking.Pretty, Agda.TypeChecking.Errors, Agda.Interaction.GhciTop
prettyTypeOfMeta | Agda.Interaction.GhciTop
preUscore | Agda.Interaction.GhciTop
PreviousInput | Agda.Syntax.Parser.Alex
Prim | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primBody | Agda.Compiler.MAlonzo.Primitives
primBool | Agda.TypeChecking.Monad.Builtin
primChar | Agda.TypeChecking.Monad.Builtin
primClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primCons | Agda.TypeChecking.Monad.Builtin
Prime | Agda.Utils.Suffix
primEquality | Agda.TypeChecking.Monad.Builtin
primFalse | Agda.TypeChecking.Monad.Builtin
primFloat | Agda.TypeChecking.Monad.Builtin
PrimFun
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primFunArity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primFunImplementation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primFunName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PrimImpl | Agda.TypeChecking.Primitive
primInteger | Agda.TypeChecking.Monad.Builtin
primIO | Agda.TypeChecking.Monad.Builtin
Primitive
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
3 (Data Constructor) | Agda.Interaction.Highlighting.Precise
4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PrimitiveFunction | Agda.Syntax.Concrete.Definitions
primitiveFunctions | Agda.TypeChecking.Primitive
PrimitiveImpl | Agda.TypeChecking.Primitive
PrimitiveType | Agda.Interaction.Highlighting.Precise
primLevel | Agda.TypeChecking.Monad.Builtin
primLevelMax | Agda.TypeChecking.Monad.Builtin
primLevelSuc | Agda.TypeChecking.Monad.Builtin
primLevelZero | Agda.TypeChecking.Monad.Builtin
primList | Agda.TypeChecking.Monad.Builtin
primName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primNat | Agda.TypeChecking.Monad.Builtin
primNatDivSucAux | Agda.TypeChecking.Monad.Builtin
primNatEquality | Agda.TypeChecking.Monad.Builtin
primNatLess | Agda.TypeChecking.Monad.Builtin
primNatMinus | Agda.TypeChecking.Monad.Builtin
primNatModSucAux | Agda.TypeChecking.Monad.Builtin
primNatPlus | Agda.TypeChecking.Monad.Builtin
primNatTimes | Agda.TypeChecking.Monad.Builtin
primNil | Agda.TypeChecking.Monad.Builtin
primRefl | Agda.TypeChecking.Monad.Builtin
primSize | Agda.TypeChecking.Monad.Builtin
primSizeInf | Agda.TypeChecking.Monad.Builtin
primSizeSuc | Agda.TypeChecking.Monad.Builtin
primString | Agda.TypeChecking.Monad.Builtin
primSuc | Agda.TypeChecking.Monad.Builtin
PrimTerm | Agda.TypeChecking.Primitive
primTerm | Agda.TypeChecking.Primitive
primTrue | Agda.TypeChecking.Monad.Builtin
primTrustMe | Agda.TypeChecking.Primitive
PrimType | Agda.TypeChecking.Primitive
primType | Agda.TypeChecking.Primitive
primZero | Agda.TypeChecking.Monad.Builtin
print | Agda.Utils.IO.Locale
printAlDecl | Agda.Compiler.Alonzo.Haskell
printAlModule | Agda.Compiler.Alonzo.Haskell
printCExp | Agda.Auto.Typecheck
printClause | Agda.Auto.Print
printConst | Agda.Auto.Print
printConstants | Agda.Compiler.Agate.Main
PrintConstr | Agda.Auto.NarrowingSearch
printCTree | Agda.Auto.NarrowingSearch
printCtx | Agda.Auto.Typecheck
printExp | Agda.Auto.Print
printHNExp | Agda.Auto.Typecheck
printHsDecls | Agda.Compiler.Alonzo.Haskell
printHsMain | Agda.Compiler.Alonzo.Haskell
printHsModule | Agda.Compiler.Alonzo.Haskell
printId | Agda.Auto.Print
printPat | Agda.Auto.Print
printPats | Agda.Auto.Print
printref | Agda.Auto.NarrowingSearch
printShowConstants | Agda.Compiler.Agate.Main
printUsage | Agda.Main
printVersion | Agda.Main
Prio | Agda.Auto.NarrowingSearch
prioCompare | Agda.Auto.SearchControl
prioCompareArgList | Agda.Auto.SearchControl
prioCompChoice | Agda.Auto.SearchControl
prioCompIota | Agda.Auto.SearchControl
prioInferredTypeUnknown | Agda.Auto.SearchControl
PrioMeta
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
prioNo | Agda.Auto.SearchControl
prioPreCompare | Agda.Auto.SearchControl
prioTypecheck | Agda.Auto.SearchControl
prioTypecheckArgList | Agda.Auto.SearchControl
prioTypeUnknown | Agda.Auto.SearchControl
Private | Agda.Syntax.Concrete
PrivateAccess | Agda.Syntax.Common
PrivateNS | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
Problem
1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem
Problem' | Agda.TypeChecking.Rules.LHS.Problem
problemInPat | Agda.TypeChecking.Rules.LHS.Problem
problemOutPat | Agda.TypeChecking.Rules.LHS.Problem
ProblemPart | Agda.TypeChecking.Rules.LHS.Problem
problemTel | Agda.TypeChecking.Rules.LHS.Problem
processArgPat | Agda.Compiler.Alonzo.Main
processArgPats | Agda.Compiler.Alonzo.Main
processBody | Agda.Compiler.Alonzo.Main
processClause | Agda.Compiler.Alonzo.Main
processCon | Agda.Compiler.Alonzo.Main
processDef | Agda.Compiler.Alonzo.Main
processDefWithDebug | Agda.Compiler.Alonzo.Main
processLit | Agda.Compiler.Alonzo.Main
processPat | Agda.Compiler.Alonzo.Main
processTerm | Agda.Compiler.Alonzo.Main
processVap | Agda.Compiler.Alonzo.Main
ProjectRoot | Agda.Interaction.Imports
projectRoot | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
promote | Agda.Utils.QuickCheck
proofIrrelevance | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Prop
1 (Type/Class) | Agda.Utils.QuickCheck
2 (Type/Class) | Agda.Auto.NarrowingSearch
3 (Data Constructor) | Agda.Syntax.Concrete
4 (Data Constructor) | Agda.Syntax.Internal
5 (Data Constructor) | Agda.Syntax.Abstract
prop | Agda.Syntax.Internal
propagatePrio | Agda.Auto.NarrowingSearch
Property | Agda.Utils.QuickCheck
property | Agda.Utils.QuickCheck
propFreq | Agda.TypeChecking.Test.Generators
PropMustBeSingleton | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
prop_disjoint | Agda.Utils.Warshall
prop_extractNthElement | Agda.Utils.List
prop_flattenTelInv | Agda.TypeChecking.Tests
prop_flattenTelScope | Agda.TypeChecking.Tests
prop_groupBy' | Agda.Utils.List
prop_path | Agda.Utils.Warshall
prop_reorderTelStable | Agda.TypeChecking.Tests
prop_smaller | Agda.Utils.Warshall
prop_splitTelescopePermScope | Agda.TypeChecking.Tests
prop_splitTelescopeScope | Agda.TypeChecking.Tests
prop_stable | Agda.Utils.Warshall
prop_telToListInv | Agda.TypeChecking.Tests
prop_wellScopedVars | Agda.TypeChecking.Test.Generators
psep | Agda.Compiler.Agate.Common
PSt | Agda.Compiler.Alonzo.PatternMonad
PState
1 (Data Constructor) | Agda.Syntax.Parser.Monad
2 (Type/Class) | Agda.Compiler.Alonzo.PatternMonad
PStr | Agda.Utils.Pretty
ptcCompare | Agda.Auto.Typecheck
ptcCompareArgList | Agda.Auto.Typecheck
ptcNoIotaStep | Agda.Auto.Typecheck
ptcTypeCheck | Agda.Auto.Typecheck
ptcTypecheckArgList | Agda.Auto.Typecheck
ptcTypeUnknown | Agda.Auto.Typecheck
ptext | Agda.Utils.Pretty
Ptr | Agda.Utils.Pointer
PublicAccess | Agda.Syntax.Common
publicModules | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
PublicNS | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
publicOpen | Agda.Syntax.Concrete
punctuate
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
pureTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
pushContext | Agda.Syntax.Parser.Monad
pushCurrentContext | Agda.Syntax.Parser.Monad
pushLexState | Agda.Syntax.Parser.Monad
putPcnt | Agda.Compiler.Alonzo.PatternMonad
putPlst | Agda.Compiler.Alonzo.PatternMonad
putStr | Agda.Utils.IO.Locale
putStrLn | Agda.Utils.IO.Locale
pwords
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
Q | Agda.Interaction.GhciTop
QName
1 (Type/Class) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
3 (Type/Class) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
4 (Data Constructor) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qnameFromList | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qnameModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qnameName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qnameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
qnameToConcrete | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qnameToList | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
QPB | Agda.Auto.NarrowingSearch
QPBlocked | Agda.Auto.NarrowingSearch
QPDoubleBlocked | Agda.Auto.NarrowingSearch
Qual | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
qualify
1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qualifyM | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qualifyQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
QuestionMark
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
quickCheck | Agda.Utils.QuickCheck
quickCheck' | Agda.Utils.QuickCheck
quickCheckResult | Agda.Utils.QuickCheck
quickCheckWith | Agda.Utils.QuickCheck
quickCheckWith' | Agda.Utils.QuickCheck
quickCheckWithResult | Agda.Utils.QuickCheck
quote | Agda.Utils.String
quotes | Agda.Utils.Pretty
R | Agda.Utils.Map
Raise | Agda.TypeChecking.Substitute
raise | Agda.TypeChecking.Substitute
raiseFrom | Agda.TypeChecking.Substitute
Range
1 (Type/Class) | Agda.Syntax.Position, Agda.Interaction.GhciTop
2 (Data Constructor) | Agda.Syntax.Position, Agda.Interaction.GhciTop
3 (Type/Class) | Agda.Interaction.Highlighting.Range
4 (Data Constructor) | Agda.Interaction.Highlighting.Range
RangeAndPragma
1 (Type/Class) | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
2 (Data Constructor) | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
rangeInvariant
1 (Function) | Agda.Syntax.Position, Agda.Interaction.GhciTop
2 (Function) | Agda.Interaction.Highlighting.Range
ranges | Agda.Utils.QuickCheck
rangeToInterval | Agda.Syntax.Position, Agda.Interaction.GhciTop
rational | Agda.Utils.Pretty
RawApp | Agda.Syntax.Concrete
RawAppP | Agda.Syntax.Concrete
RB | Agda.Termination.Lexicographic
rbrace | Agda.Utils.Pretty
rbrack | Agda.Utils.Pretty
RConst | Agda.Utils.Warshall
readBinaryFile' | Agda.Utils.IO.Binary
readInterface | Agda.Interaction.Imports
readline | Agda.Interaction.Monad
readM | Agda.Utils.Monad
ReadP | Agda.Utils.ReadP
readTextFile | Agda.Utils.IO.UTF8
reason | Agda.Utils.QuickCheck
rebindClause | Agda.TypeChecking.Rebind
rebindPrimitive | Agda.TypeChecking.Primitive
Rec
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
recAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recalc | Agda.Auto.NarrowingSearch
recalcs | Agda.Auto.NarrowingSearch
recArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
RecBehaviour | Agda.Termination.Lexicographic
recBehaviourInvariant | Agda.Termination.Lexicographic
reccalc | Agda.Auto.NarrowingSearch
recClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recConType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
RecDef
1 (Data Constructor) | Agda.Syntax.Concrete.Definitions
2 (Data Constructor) | Agda.Syntax.Abstract
recFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Record
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recordModule | Agda.TypeChecking.Records
recPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recTel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recursive | Agda.Syntax.Concrete.Operators.Parser
redBind | Agda.TypeChecking.Primitive
redReturn | Agda.TypeChecking.Primitive
Reduce | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
reduce | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
reduceB | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
reduceCon | Agda.TypeChecking.Rules.Term
Reduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
reduceHead | Agda.TypeChecking.Injectivity
RefCreateEnv | Agda.Auto.NarrowingSearch
Refinable | Agda.Auto.NarrowingSearch
refine | Agda.Interaction.BasicOps
refinements | Agda.Auto.NarrowingSearch
refineMeta | Agda.Interaction.CommandLine.CommandLine
RefInfo | Agda.Auto.Syntax
refreshStr | Agda.Interaction.GhciTop
Reify | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
reify | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
reifyApp | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
reifyDisplayForm | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
reifyDisplayFormP | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
reifyPatterns | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
Rel | Agda.TypeChecking.Primitive
RelativeTo | Agda.Interaction.Imports
removeInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
Ren | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
rename | Agda.TypeChecking.Telescope
renameCanonicalNames | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
renamedCanonicalNames | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
Renaming
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
renaming
1 (Function) | Agda.Syntax.Concrete
2 (Function) | Agda.TypeChecking.Telescope
renamingR | Agda.TypeChecking.Telescope
rEnd | Agda.Syntax.Position, Agda.Interaction.GhciTop
render | Agda.Utils.Pretty
renderStyle | Agda.Utils.Pretty
renFrom | Agda.Syntax.Concrete
renTo | Agda.Syntax.Concrete
renToRange | Agda.Syntax.Concrete
reorderTel | Agda.TypeChecking.Telescope
RepeatedVariablesInPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
repl | Agda.Compiler.MAlonzo.Primitives
replay | Agda.Utils.QuickCheck
reportS | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
reportSDoc | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
reportSLn | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
resetState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
resize | Agda.Utils.QuickCheck
resizeConf | Agda.TypeChecking.Test.Generators
ResolvedName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
resolveModule | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
resolveName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
respond | Agda.Interaction.GhciTop
response | Agda.Interaction.GhciTop
responseString | Agda.Interaction.GhciTop
Restore
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
restrictPrivate | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
Result
1 (Type/Class) | Agda.Utils.QuickCheck
2 (Type/Class) | Agda.Termination.TermCheck
retryConstraints | Agda.Interaction.CommandLine.CommandLine
Return | Agda.Interaction.CommandLine.CommandLine
reverseP | Agda.Utils.Permutation
Rewrite | Agda.Interaction.BasicOps
rewrite | Agda.Interaction.BasicOps
RewriteRHS | Agda.Syntax.Abstract
RHS
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Type/Class) | Agda.Syntax.Abstract
4 (Data Constructor) | Agda.Syntax.Abstract
ribbonsPerLine | Agda.Utils.Pretty
RIEnv | Agda.Auto.Syntax
RightAssoc | Agda.Syntax.Fixity
RightDisjunct | Agda.Auto.NarrowingSearch
rightDistributive | Agda.Utils.TestHelpers
RightHandSide | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
RightOperandCtx | Agda.Syntax.Fixity
Rigid
1 (Type/Class) | Agda.Utils.Warshall
2 (Data Constructor) | Agda.Utils.Warshall
3 (Data Constructor) | Agda.TypeChecking.SizedTypes
RigidId | Agda.Utils.Warshall
rigidVars | Agda.TypeChecking.Free
RIMainInfo | Agda.Auto.Syntax
RIUnifInfo | Agda.Auto.Syntax
rollback | Agda.Syntax.Parser.LookAhead
roundFixBrackets | Agda.Syntax.Fixity
row | Agda.Termination.Matrix
rowdescr | Agda.Utils.Warshall
rows | Agda.Termination.Matrix
rparen | Agda.Utils.Pretty
rStart | Agda.Syntax.Position, Agda.Interaction.GhciTop
rtmError | Agda.Compiler.MAlonzo.Misc
rtmMod | Agda.Compiler.MAlonzo.Misc
rtmQual | Agda.Compiler.MAlonzo.Misc
rtmVar | Agda.Compiler.MAlonzo.Misc
rToR | Agda.Interaction.Highlighting.Range
rtpCon | Agda.Compiler.Alonzo.Names
rtpQName | Agda.Compiler.Alonzo.Names
runAbsToCon | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
runAgda | Agda.Main
runExceptionT | Agda.TypeChecking.Monad.Exception
runIM | Agda.Interaction.Monad
runLookAhead | Agda.Syntax.Parser.LookAhead
runNice | Agda.Syntax.Concrete.Definitions
runProp | Agda.Auto.NarrowingSearch
runTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runTCM' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runTests | Agda.Utils.TestHelpers
runUndo | Agda.Auto.NarrowingSearch
RVar | Agda.Utils.Warshall
S
1 (Type/Class) | Agda.Auto.Convert
2 (Data Constructor) | Agda.Auto.Convert
sameVars | Agda.TypeChecking.Conversion
sample | Agda.Utils.QuickCheck
sample' | Agda.Utils.QuickCheck
satisfy | Agda.Utils.ReadP
sccomcount | Agda.Auto.NarrowingSearch
scflip | Agda.Auto.NarrowingSearch
sChecked | Agda.Interaction.GhciTop
SClause | Agda.TypeChecking.Coverage
sConsts | Agda.Auto.Convert
Scope
1 (Type/Class) | Agda.Utils.Warshall
2 (Type/Class) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
3 (Data Constructor) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ScopeCheckDeclaration | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ScopeCheckDefinition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ScopeCheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
scopeCheckImport | Agda.Interaction.Imports
ScopeCheckLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
scopeCurrent | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ScopedDecl | Agda.Syntax.Abstract
ScopedDef | Agda.Syntax.Abstract
ScopedExpr | Agda.Syntax.Abstract
scopeImported | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeImports | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ScopeInfo
1 (Type/Class) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
2 (Data Constructor) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeLocals | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeLookup | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ScopeM | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
scopeModules | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeParents | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopePrecedence | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopePrivate | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopePublic | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scPats | Agda.TypeChecking.Coverage
scPerm | Agda.TypeChecking.Coverage
scsub1 | Agda.Auto.NarrowingSearch
scsub2 | Agda.Auto.NarrowingSearch
scSubst | Agda.TypeChecking.Coverage
scTel | Agda.TypeChecking.Coverage
sCurMeta | Agda.Auto.Convert
secFreeVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
secondPart | Agda.TypeChecking.Telescope
secTelescope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Section
1 (Data Constructor) | Agda.Syntax.Abstract
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Sections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
semi | Agda.Utils.Pretty
SemiRing | Agda.Utils.SemiRing
Semiring
1 (Type/Class) | Agda.Termination.Semiring
2 (Data Constructor) | Agda.Termination.Semiring
semiringInvariant | Agda.Termination.Semiring
sep
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
sepBy | Agda.Utils.ReadP
sepBy1 | Agda.Utils.ReadP
seqc | Agda.Auto.NarrowingSearch
sEqs | Agda.Auto.Convert
Set
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
set | Agda.Syntax.Internal
set0 | Agda.Syntax.Internal
setArgOccurrences | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setBuiltinThings | Agda.TypeChecking.Monad.Builtin
setCommandLineOptions
1 (Function) | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
2 (Function) | Agda.Interaction.GhciTop
setContextPrecedence | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
setCurrentModule | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
setCurrentRange | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
setDecodedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
setFreqs | Agda.TypeChecking.Test.Generators
setImportedSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setInput | Agda.Syntax.Parser.LookAhead
setInputFile | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setInterface | Agda.Compiler.MAlonzo.Misc
setLastPos | Agda.Syntax.Parser.Monad
setLexInput | Agda.Syntax.Parser.Alex
setLocalVars | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
setMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
SetN | Agda.Syntax.Concrete
setOptionsFromPragma | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setOptionsFromPragmas | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setParsePos | Agda.Syntax.Parser.Monad
setPolarity | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setPrevToken | Agda.Syntax.Parser.Monad
SetRange
1 (Type/Class) | Agda.Syntax.Position, Agda.Interaction.GhciTop
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
setRange | Agda.Syntax.Position, Agda.Interaction.GhciTop
setScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setScopeAccess | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
setShowImplicitArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setTopLevelModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setTrace | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
setVisitedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
several | Agda.Interaction.Highlighting.Precise
ShadowedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeApplicationOf | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeAppliedToTheDatatypeParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeASort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBePi | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeRecordType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldEndInApplicationOfTheDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
shouldReifyInteractionPoints | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
showA | Agda.Syntax.Abstract.Pretty
showAsOptimizedConstructor | Agda.Compiler.Agate.OptimizedPrinter
ShowAsOptimizedKind | Agda.Compiler.Agate.OptimizedPrinter
showAsOptimizedKind | Agda.Compiler.Agate.OptimizedPrinter
ShowAsOptimizedTerm | Agda.Compiler.Agate.OptimizedPrinter
showAsOptimizedTerm | Agda.Compiler.Agate.OptimizedPrinter
ShowAsOptimizedType | Agda.Compiler.Agate.OptimizedPrinter
showAsOptimizedType | Agda.Compiler.Agate.OptimizedPrinter
showAsUntypedConstructor | Agda.Compiler.Agate.UntypedPrinter
ShowAsUntypedTerm | Agda.Compiler.Agate.UntypedPrinter
showAsUntypedTerm | Agda.Compiler.Agate.UntypedPrinter
showBehaviour | Agda.Termination.CallGraph
showChar' | Agda.Syntax.Concrete.Pretty
showClause | Agda.Compiler.Agate.Common
showComparison | Agda.Interaction.BasicOps
showConstraints | Agda.Interaction.CommandLine.CommandLine
showContext | Agda.Interaction.CommandLine.CommandLine
showHighlightingInfo | Agda.Interaction.Highlighting.Emacs
showImplicitArgs | Agda.Interaction.GhciTop
showImplicitArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
showIndex | Agda.Utils.String
showMetas | Agda.Interaction.CommandLine.CommandLine
showNumIId | Agda.Interaction.GhciTop
showOptimizedClause | Agda.Compiler.Agate.OptimizedPrinter
showOptimizedDefinitions | Agda.Compiler.Agate.OptimizedPrinter
showOptimizedLiteral | Agda.Compiler.Agate.Common
showPat | Agda.TypeChecking.With
showScope | Agda.Interaction.CommandLine.CommandLine
showStatus | Agda.Interaction.GhciTop
showString' | Agda.Syntax.Concrete.Pretty
showTypeDeclaration | Agda.Compiler.Agate.OptimizedPrinter
showTypeDeclarations | Agda.Compiler.Agate.OptimizedPrinter
showTypeParameter | Agda.Compiler.Agate.OptimizedPrinter
showUntypedApp | Agda.Compiler.Agate.UntypedPrinter
showUntypedClause | Agda.Compiler.Agate.UntypedPrinter
showUntypedDefinition | Agda.Compiler.Agate.UntypedPrinter
showUntypedLiteral | Agda.Compiler.Agate.Common
showValueDefinition | Agda.Compiler.Agate.OptimizedPrinter
showValueDefinitions | Agda.Compiler.Agate.OptimizedPrinter
shrink | Agda.Utils.QuickCheck
Shrink2
1 (Data Constructor) | Agda.Utils.QuickCheck
2 (Type/Class) | Agda.Utils.QuickCheck
ShrinkC | Agda.TypeChecking.Test.Generators
shrinkC | Agda.TypeChecking.Test.Generators
Shrinking
1 (Data Constructor) | Agda.Utils.QuickCheck
2 (Type/Class) | Agda.Utils.QuickCheck
shrinking | Agda.Utils.QuickCheck
shrinkInit | Agda.Utils.QuickCheck
shrinkIntegral | Agda.Utils.QuickCheck
shrinkNothing | Agda.Utils.QuickCheck
shrinkRealFrac | Agda.Utils.QuickCheck
ShrinkState | Agda.Utils.QuickCheck
shrinkState | Agda.Utils.QuickCheck
SiblingCall | Agda.Utils.Trace
Sig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigDefinitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigMName | Agda.Compiler.MAlonzo.Misc
Signature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigSections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
singleConstructorType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
singleton
1 (Function) | Agda.Utils.Trie
2 (Function) | Agda.Utils.Graph
3 (Function) | Agda.Interaction.Highlighting.Precise
Size
1 (Type/Class) | Agda.Termination.Matrix
2 (Data Constructor) | Agda.Termination.Matrix
size
1 (Function) | Agda.Utils.Size
2 (Function) | Agda.Termination.Matrix
3 (Function) | Agda.Termination.Lexicographic
SizeConst | Agda.Utils.Warshall
SizeConstraint | Agda.TypeChecking.SizedTypes
Sized | Agda.Utils.Size
sized | Agda.Utils.QuickCheck
SizedList
1 (Type/Class) | Agda.TypeChecking.Test.Generators
2 (Data Constructor) | Agda.TypeChecking.Test.Generators
SizeExpr
1 (Type/Class) | Agda.Utils.Warshall
2 (Type/Class) | Agda.TypeChecking.SizedTypes
sizeExpr | Agda.TypeChecking.SizedTypes
SizeInf | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeInvariant | Agda.Termination.Matrix
SizeMeta | Agda.TypeChecking.SizedTypes
sizePolarity | Agda.TypeChecking.Polarity
sizeRigid | Agda.Utils.Warshall
SizeSuc | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeSuc | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeType | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
SizeVar | Agda.Utils.Warshall
SizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
Skip | Agda.Auto.Syntax
skipBlock | Agda.Syntax.Parser.Comments
skipMany | Agda.Utils.ReadP
skipMany1 | Agda.Utils.ReadP
skipSpaces | Agda.Utils.ReadP
sLub | Agda.Syntax.Internal
smallestPos | Agda.Interaction.Highlighting.Precise
Smart
1 (Data Constructor) | Agda.Utils.QuickCheck
2 (Type/Class) | Agda.Utils.QuickCheck
sMetas | Agda.Auto.Convert
Solution | Agda.Utils.Warshall
solve | Agda.Utils.Warshall
solveConstraint | Agda.TypeChecking.Constraints
solveConstraints | Agda.TypeChecking.Constraints
solveSizeConstraints | Agda.TypeChecking.SizedTypes
SomeWhere | Agda.Syntax.Concrete
Sort
1 (Data Constructor) | Agda.Auto.Syntax
2 (Type/Class) | Agda.Auto.Syntax
3 (Type/Class) | Agda.Syntax.Internal
4 (Data Constructor) | Agda.Syntax.Internal
sort | Agda.Syntax.Internal
SortCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sortFreq | Agda.TypeChecking.Test.Generators
SortFreqs
1 (Type/Class) | Agda.TypeChecking.Test.Generators
2 (Data Constructor) | Agda.TypeChecking.Test.Generators
sortFreqs | Agda.TypeChecking.Test.Generators
SortHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sortInteractionPoints | Agda.Interaction.GhciTop
SortLevel | Agda.Auto.Syntax
sortOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
source | Agda.Termination.CallGraph
SourceToModule | Agda.Interaction.FindFile
sourceToModule | Agda.Interaction.FindFile
space | Agda.Utils.Pretty
splashScreen | Agda.Interaction.CommandLine.CommandLine
Split | Agda.TypeChecking.Rules.LHS.Problem
split | Agda.TypeChecking.Coverage
split' | Agda.TypeChecking.Coverage
SplitClause | Agda.TypeChecking.Coverage
splitClause | Agda.TypeChecking.Coverage
splitClauseWithAbs | Agda.TypeChecking.Coverage
SplitError
1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem
2 (Type/Class) | Agda.TypeChecking.Coverage
SplitPanic | Agda.TypeChecking.Rules.LHS.Problem
splitPerm | Agda.TypeChecking.Telescope
SplitProblem | Agda.TypeChecking.Rules.LHS.Problem
splitProblem | Agda.TypeChecking.Rules.LHS.Split
SplitTel
1 (Type/Class) | Agda.TypeChecking.Telescope
2 (Data Constructor) | Agda.TypeChecking.Telescope
splitTelescope | Agda.TypeChecking.Telescope
splitType | Agda.Compiler.Agate.Common
square | Agda.Termination.Matrix
srcFile | Agda.Syntax.Position, Agda.Interaction.GhciTop
SRes | Agda.Auto.NarrowingSearch
sShowImplicitArguments | Agda.Interaction.GhciTop
sSuc | Agda.Syntax.Internal
standardOptions_ | Agda.Interaction.Options
startPos | Agda.Syntax.Position, Agda.Interaction.GhciTop
State
1 (Type/Class) | Agda.Interaction.GhciTop
2 (Data Constructor) | Agda.Interaction.GhciTop
Statistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Status
1 (Type/Class) | Agda.Interaction.GhciTop
2 (Data Constructor) | Agda.Interaction.GhciTop
status | Agda.Interaction.GhciTop
stBuiltinThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stdArgs | Agda.Utils.QuickCheck
stDecodedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stFreshThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stHaskellImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stLocalBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
store | Agda.Utils.Pointer
storeDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
stPersistentOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Str
1 (Type/Class) | Agda.Utils.QuickCheck
2 (Data Constructor) | Agda.Utils.Pretty
3 (Type/Class) | Agda.TypeChecking.Primitive
4 (Data Constructor) | Agda.TypeChecking.Primitive
Strict | Agda.Syntax.Strict
strict | Agda.Syntax.Strict
String | Agda.Interaction.Highlighting.Precise
string | Agda.Utils.ReadP
stripImplicits | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
stripNoNames | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
stripWithClausePatterns | Agda.TypeChecking.With
stScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stTrace | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stVisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Style
1 (Type/Class) | Agda.Utils.Pretty
2 (Data Constructor) | Agda.Utils.Pretty
style | Agda.Utils.Pretty
Sub
1 (Data Constructor) | Agda.Auto.Syntax
2 (Type/Class) | Agda.TypeChecking.Rules.LHS.Unify
sub | Agda.Auto.Typecheck
SubConstraints
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
Subst | Agda.TypeChecking.Substitute
subst | Agda.TypeChecking.Substitute
Substitution | Agda.TypeChecking.Rules.LHS.Problem
substs | Agda.TypeChecking.Substitute
substUnder | Agda.TypeChecking.Substitute
Suc | Agda.Syntax.Internal
Success | Agda.Utils.QuickCheck
suchThat | Agda.Utils.QuickCheck
suchThatMaybe | Agda.Utils.QuickCheck
sucName | Agda.TypeChecking.Level
Suffix
1 (Type/Class) | Agda.Utils.Suffix
2 (Type/Class) | Agda.Utils.List
suffixView | Agda.Utils.Suffix
supremum | Agda.Termination.CallGraph
SymArrow | Agda.Syntax.Parser.Tokens
SymAs | Agda.Syntax.Parser.Tokens
SymBar | Agda.Syntax.Parser.Tokens
Symbol
1 (Type/Class) | Agda.Syntax.Parser.Tokens
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
symbol | Agda.Syntax.Parser.LexActions
SymCloseBrace | Agda.Syntax.Parser.Tokens
SymCloseParen | Agda.Syntax.Parser.Tokens
SymClosePragma | Agda.Syntax.Parser.Tokens
SymCloseVirtualBrace | Agda.Syntax.Parser.Tokens
SymColon | Agda.Syntax.Parser.Tokens
SymDot | Agda.Syntax.Parser.Tokens
SymEllipsis | Agda.Syntax.Parser.Tokens
SymEqual | Agda.Syntax.Parser.Tokens
SymLambda | Agda.Syntax.Parser.Tokens
SymOpenBrace | Agda.Syntax.Parser.Tokens
SymOpenParen | Agda.Syntax.Parser.Tokens
SymOpenPragma | Agda.Syntax.Parser.Tokens
SymOpenVirtualBrace | Agda.Syntax.Parser.Tokens
SymQuestionMark | Agda.Syntax.Parser.Tokens
SymSemi | Agda.Syntax.Parser.Tokens
SymUnderscore | Agda.Syntax.Parser.Tokens
SymVirtualSemi | Agda.Syntax.Parser.Tokens
sync | Agda.Syntax.Parser.LookAhead
takeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
takeEqualities | Agda.TypeChecking.Rules.LHS.Unify
takeI | Agda.Syntax.Position, Agda.Interaction.GhciTop
takenNameStr | Agda.Interaction.GhciTop
Target | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
target | Agda.Termination.CallGraph
TBind
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
tcargs | Agda.Auto.Typecheck
tcConstructorNames | Agda.TypeChecking.Test.Generators
tcDefinedNames | Agda.TypeChecking.Test.Generators
TCEnv
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TCErr
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TCErr' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
tcErrString | Agda.TypeChecking.Errors, Agda.Interaction.GhciTop
tcExp | Agda.Auto.Typecheck
tcFixSize | Agda.TypeChecking.Test.Generators
tcFreeVariables | Agda.TypeChecking.Test.Generators
tcFrequencies | Agda.TypeChecking.Test.Generators
tcIsType | Agda.TypeChecking.Test.Generators
tcLiterals | Agda.TypeChecking.Test.Generators
TCM
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
tcSearch | Agda.Auto.Typecheck
TCSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TelCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
teleArgNames | Agda.TypeChecking.Telescope
teleArgs | Agda.TypeChecking.Telescope
teleLam | Agda.Syntax.Internal
teleNames | Agda.TypeChecking.Telescope
telePi | Agda.TypeChecking.Substitute
telePi_ | Agda.TypeChecking.Substitute
Telescope
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Internal
3 (Type/Class) | Agda.Syntax.Abstract
telFromList | Agda.Syntax.Internal
tellEmacsToJumpToError | Agda.Interaction.GhciTop
telToList | Agda.Syntax.Internal
TelV | Agda.TypeChecking.Substitute
telVars | Agda.TypeChecking.Substitute
TelView | Agda.TypeChecking.Substitute
telView | Agda.TypeChecking.Substitute
telViewM | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
Term
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
3 (Type/Class) | Agda.Syntax.Internal
term | Agda.Compiler.MAlonzo.Compiler
TermConf | Agda.TypeChecking.Test.Generators
TermConfiguration | Agda.TypeChecking.Test.Generators
termDecls | Agda.Termination.TermCheck
TermFreqs
1 (Type/Class) | Agda.TypeChecking.Test.Generators
2 (Data Constructor) | Agda.TypeChecking.Test.Generators
termFreqs | Agda.TypeChecking.Test.Generators
TermFunDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TermHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
terminates | Agda.Termination.Termination
TerminationCheckFailed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TerminationProblem | Agda.Interaction.Highlighting.Precise
terminationProblems | Agda.Interaction.Imports
TermLike | Agda.Syntax.Internal.Generic
Testable | Agda.Utils.QuickCheck
tests
1 (Function) | Agda.Utils.List
2 (Function) | Agda.Utils.FileName, Agda.Interaction.FindFile
3 (Function) | Agda.Utils.Either
4 (Function) | Agda.Termination.Semiring
5 (Function) | Agda.Termination.Matrix
6 (Function) | Agda.Termination.CallGraph
7 (Function) | Agda.Termination.Lexicographic
8 (Function) | Agda.Termination.Termination
9 (Function) | Agda.Syntax.Position, Agda.Interaction.GhciTop
10 (Function) | Agda.Syntax.Parser.Parser
11 (Function) | Agda.Utils.Warshall
12 (Function) | Agda.Interaction.Options
13 (Function) | Agda.Interaction.Highlighting.Range
14 (Function) | Agda.Interaction.Highlighting.Precise
15 (Function) | Agda.Interaction.Highlighting.Generate
16 (Function) | Agda.Interaction.Highlighting.Emacs
17 (Function) | Agda.TypeChecking.Tests
18 (Function) | Agda.Compiler.MAlonzo.Encode
testSuite | Agda.Tests
text
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
TextDetails | Agda.Utils.Pretty
theCurrentFile | Agda.Interaction.GhciTop
theDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
theInteractionPoints | Agda.Interaction.GhciTop
theState | Agda.Interaction.GhciTop
theTCState | Agda.Interaction.GhciTop
ThingsInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
thingsInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
thread | Agda.Utils.Monad
throwException | Agda.TypeChecking.Monad.Exception
throwImpossible | Agda.Utils.Impossible
tick | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad
times | Agda.Compiler.Alonzo.Main
tlmname | Agda.Compiler.MAlonzo.Misc
tlmodOf | Agda.Compiler.MAlonzo.Misc
TMAll | Agda.Auto.Convert
TMode | Agda.Auto.Convert
TNoBind
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
to | Agda.Interaction.Highlighting.Range
ToAbstract | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
toAbstract | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
ToConcrete | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
toConcrete | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
toggleImplicitArgs | Agda.Interaction.GhciTop
toIFile | Agda.Interaction.FindFile
TokComment | Agda.Syntax.Parser.Tokens
TokDummy | Agda.Syntax.Parser.Tokens
Token | Agda.Syntax.Parser.Tokens
token | Agda.Syntax.Parser.LexActions
TokenLength | Agda.Syntax.Parser.Alex
tokensParser
1 (Function) | Agda.Syntax.Parser.Parser
2 (Function) | Agda.Syntax.Parser, Agda.Interaction.GhciTop
TokEOF | Agda.Syntax.Parser.Tokens
TokId | Agda.Syntax.Parser.Tokens
TokKeyword | Agda.Syntax.Parser.Tokens
TokLiteral | Agda.Syntax.Parser.Tokens
TokQId | Agda.Syntax.Parser.Tokens
TokSetN | Agda.Syntax.Parser.Tokens
TokString | Agda.Syntax.Parser.Tokens
TokSymbol | Agda.Syntax.Parser.Tokens
TokTeX | Agda.Syntax.Parser.Tokens
toList
1 (Function) | Agda.Termination.CallGraph
2 (Function) | Agda.Interaction.Highlighting.Range
toLists | Agda.Termination.Matrix
TOM | Agda.Auto.Convert
toMap | Agda.Interaction.Highlighting.Precise
tomy | Agda.Auto.Convert
tomyBody | Agda.Auto.Convert
tomyClause | Agda.Auto.Convert
tomyClauses | Agda.Auto.Convert
tomyExp | Agda.Auto.Convert
tomyExps | Agda.Auto.Convert
tomyIneq | Agda.Auto.Convert
tomyPat | Agda.Auto.Convert
tomyType | Agda.Auto.Convert
TooFewFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TooManyArgumentsInLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TooManyFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
topContext | Agda.Syntax.Parser.Monad
TopCtx | Agda.Syntax.Fixity
TopLevel
1 (Data Constructor) | Agda.Utils.Trace
2 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
3 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
topLevelDecls | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
TopLevelInfo
1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
TopLevelModuleName
1 (Type/Class) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
topLevelModuleName
1 (Function) | Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
topoSort | Agda.Utils.Permutation
topSearch | Agda.Auto.NarrowingSearch
ToTerm | Agda.TypeChecking.Primitive
toTerm | Agda.TypeChecking.Primitive
toTopLevelModuleName
1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
toVim | Agda.Interaction.Highlighting.Vim
Trace | Agda.Utils.Trace
traceCall | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceCallCPS | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceCallCPS_ | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceCallE | Agda.TypeChecking.Rules.Term
traceCall_ | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceFun | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
traceFun' | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
transitiveClosure | Agda.Utils.Graph
translateNameAsOptimizedConstructor | Agda.Compiler.Agate.TranslateName
translateNameAsOptimizedTerm | Agda.Compiler.Agate.TranslateName
translateNameAsOptimizedType | Agda.Compiler.Agate.TranslateName
translateNameAsUntypedConstructor | Agda.Compiler.Agate.TranslateName
translateNameAsUntypedTerm | Agda.Compiler.Agate.TranslateName
Trav | Agda.Auto.NarrowingSearch
traverse | Agda.Auto.NarrowingSearch
traverseTerm | Agda.Syntax.Internal.Generic
traverseTermM | Agda.Syntax.Internal.Generic
treatAbstractly | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
treatAbstractly' | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
Trie | Agda.Utils.Trie
trivial | Agda.TypeChecking.SizedTypes
tryOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
tset | Agda.TypeChecking.Primitive
tvaldecl | Agda.Compiler.MAlonzo.Compiler
Type
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Internal
3 (Type/Class) | Agda.Syntax.Internal
TypeAndDef | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
typeArity | Agda.Compiler.Alonzo.Main
typeCheck | Agda.Interaction.Imports
TypeCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TypedAssign | Agda.Interaction.BasicOps
TypedBinding
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
TypedBindings
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Type/Class) | Agda.Syntax.Abstract
4 (Data Constructor) | Agda.Syntax.Abstract
TypeError
1 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
typeError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
typeIn | Agda.Interaction.CommandLine.CommandLine
typeInCurrent | Agda.Interaction.BasicOps
typeInMeta | Agda.Interaction.BasicOps
typeInType | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
typeOf | Agda.Interaction.CommandLine.CommandLine
typeOfBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
typeOfBV' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
typeOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
typeOfMeta | Agda.Interaction.BasicOps
typeOfMetaMI | Agda.Interaction.BasicOps
typeOfMetas | Agda.Interaction.BasicOps
typeOfSizeInf | Agda.TypeChecking.Rules.Builtin
typeOfSizeSuc | Agda.TypeChecking.Rules.Builtin
typeOfVar | Agda.TypeChecking.Coverage
TypeSig | Agda.Syntax.Concrete
TypeSignature
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
U | Agda.TypeChecking.Rules.LHS.Unify
umodifyIORef | Agda.Auto.NarrowingSearch
unAmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
unAppView | Agda.Syntax.Abstract.Views
unArg | Agda.Syntax.Common
UnBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unConName | Agda.TypeChecking.Test.Generators
uncurry3 | Agda.Utils.Tuple
unDefName | Agda.TypeChecking.Test.Generators
underAbstraction | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
underAbstraction_ | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
underContext | Agda.Compiler.Agate.Common
underDatatypeParameters | Agda.Compiler.Agate.OptimizedPrinter
Underscore
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
Undo | Agda.Auto.NarrowingSearch
unEl | Agda.Syntax.Internal
UnequalHiding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalSorts | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalTelescopes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalTerms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalTypes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnexpectedWithPatterns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unExprView | Agda.Syntax.Concrete.Operators.Parser
unflattenTel | Agda.TypeChecking.Telescope
unfoldDefinition | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
unfoldVap | Agda.Compiler.Alonzo.Main
unGraph | Agda.Utils.Graph
uniConstr | Agda.TypeChecking.Rules.LHS.Unify
UnificationResult | Agda.TypeChecking.Rules.LHS.Unify
Unifies | Agda.TypeChecking.Rules.LHS.Unify
Unify | Agda.TypeChecking.Rules.LHS.Unify
UnifyException | Agda.TypeChecking.Rules.LHS.Unify
unifyIndices | Agda.TypeChecking.Rules.LHS.Unify
unifyIndices_ | Agda.TypeChecking.Rules.LHS.Unify
UnifyState | Agda.TypeChecking.Rules.LHS.Unify
UninstantiatedDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UninstantiatedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
union
1 (Function) | Agda.Utils.Trie
2 (Function) | Agda.Utils.Graph
3 (Function) | Agda.Termination.CallGraph
unions | Agda.Utils.Graph
unionSignatures | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
unionWithM | Agda.Utils.Map
uniSub | Agda.TypeChecking.Rules.LHS.Unify
Unknown
1 (Data Constructor) | Agda.Termination.CallGraph
2 (Data Constructor) | Agda.TypeChecking.Positivity
UnknownName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
UnknownNamesInFixityDecl | Agda.Syntax.Concrete.Definitions
unlessM | Agda.Utils.Monad
unLevelAtom | Agda.TypeChecking.Level
unLevelView | Agda.TypeChecking.Level
unlistenToMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unLvl | Agda.TypeChecking.Primitive
unnamed | Agda.Syntax.Common
unNat | Agda.TypeChecking.Primitive
unNoType | Agda.TypeChecking.Test.Generators
unqhname | Agda.Compiler.MAlonzo.Misc
unqualify | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
UnreachableClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsafeCoerceMod | Agda.Compiler.MAlonzo.Misc
unSizedList | Agda.TypeChecking.Test.Generators
unSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
UnsolvedConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsolvedConstraints | Agda.Interaction.Imports
UnsolvedMeta | Agda.Interaction.Highlighting.Precise
UnsolvedMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsolvedMetaVariables | Agda.Interaction.Imports
unStr | Agda.TypeChecking.Primitive
unTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
untypedAbs | Agda.Compiler.Agate.UntypedPrinter
unUnify | Agda.TypeChecking.Rules.LHS.Unify
Unused | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unVarName | Agda.TypeChecking.Test.Generators
unYesType | Agda.TypeChecking.Test.Generators
updateCall | Agda.Utils.Trace
updateMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
updateMetaVar | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updateMetaVarRange | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updatePtr | Agda.Utils.Pointer
updateWithConstructorRanges | Agda.TypeChecking.With
ureadIORef | Agda.Auto.NarrowingSearch
ureadmodifyIORef | Agda.Auto.NarrowingSearch
ureduce | Agda.TypeChecking.Rules.LHS.Unify
usage | Agda.Interaction.Options
usedSeed | Agda.Utils.QuickCheck
usedSize | Agda.Utils.QuickCheck
useInjectivity | Agda.TypeChecking.Injectivity
UseLit | Agda.TypeChecking.Test.Generators
useLitChar | Agda.TypeChecking.Test.Generators
UseLiterals | Agda.TypeChecking.Test.Generators
useLitFloat | Agda.TypeChecking.Test.Generators
useLitInt | Agda.TypeChecking.Test.Generators
useLitString | Agda.TypeChecking.Test.Generators
useNamesFromPattern | Agda.TypeChecking.Rules.LHS
Using | Agda.Syntax.Concrete
UsingOrHiding | Agda.Syntax.Concrete
usingOrHiding | Agda.Syntax.Concrete
USt | Agda.TypeChecking.Rules.LHS.Unify
uwriteIORef | Agda.Auto.NarrowingSearch
validParameters | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
ValueCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Var
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Abstract
var | Agda.TypeChecking.Primitive
VarArg | Agda.TypeChecking.Positivity
varFreq | Agda.TypeChecking.Test.Generators
variant | Agda.Utils.QuickCheck
VarMP | Agda.TypeChecking.Coverage.Match
VarName
1 (Data Constructor) | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
2 (Type/Class) | Agda.TypeChecking.Test.Generators
3 (Data Constructor) | Agda.TypeChecking.Test.Generators
VarP
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Abstract
vars | Agda.Compiler.Alonzo.PatternMonad
vcat
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
vecApp | Agda.Compiler.Alonzo.Main
vector | Agda.Utils.QuickCheck
vectorOf | Agda.Utils.QuickCheck
VerboseKey | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
verboseS | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
version | Agda.Version
vimFile | Agda.Interaction.Highlighting.Vim
VisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
visitModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
wakeupConstraints | Agda.TypeChecking.Constraints
Warnings
1 (Type/Class) | Agda.Interaction.Imports
2 (Data Constructor) | Agda.Interaction.Imports
warningsToError | Agda.Interaction.Imports
warshall | Agda.Utils.Warshall
warshallG | Agda.Utils.Warshall
Weak | Agda.Auto.Syntax
weak | Agda.Auto.Typecheck
weaken | Agda.Auto.Convert
weakens | Agda.Auto.Convert
Weight | Agda.Utils.Warshall
whatInduction | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
whenFail | Agda.Utils.QuickCheck
whenFail' | Agda.Utils.QuickCheck
whenM | Agda.Utils.Monad
WhereClause | Agda.Syntax.Concrete
WildMP | Agda.TypeChecking.Coverage.Match
WildP
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
withAnonymousModule | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
WithApp
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
withAppBrackets | Agda.Syntax.Fixity
WithArgCtx | Agda.Syntax.Fixity
WithClausePatternMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
withConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
withContextPrecedence | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
withCurrentModule
1 (Function) | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
2 (Function) | Agda.Syntax.Scope.Monad
withDisplayForm | Agda.TypeChecking.With
withEnv | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
withFresh | Agda.Utils.Fresh
WithFunction | Agda.TypeChecking.Rules.Def
withFunctionDomain | Agda.Compiler.Agate.Common
WithFunctionProblem | Agda.TypeChecking.Rules.Def
withFunctionType | Agda.TypeChecking.With
WithFunCtx | Agda.Syntax.Fixity
withImportPath | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
within | Agda.Utils.QuickCheck
withInteractionId | Agda.Interaction.BasicOps
withInterval | Agda.Syntax.Parser.LexActions
withInterval' | Agda.Syntax.Parser.LexActions
withInterval_ | Agda.Syntax.Parser.LexActions
withLayout | Agda.Syntax.Parser.LexActions, Agda.Syntax.Parser.Layout
withLocalVars | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
withMetaId | Agda.Interaction.BasicOps
withMetaInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
withRangeOf | Agda.Syntax.Position, Agda.Interaction.GhciTop
withRangesOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
withRangesOfQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
WithRHS | Agda.Syntax.Abstract
withScope
1 (Function) | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
2 (Function) | Agda.Syntax.Translation.AbstractToConcrete
withScope_ | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
withSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
withTopLevelModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
withTrace | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
wordsBy | Agda.Utils.List
writeFile | Agda.Utils.IO.UTF8
writeInterface | Agda.Interaction.Imports
writeModule | Agda.Compiler.MAlonzo.Compiler
WrongHidingInApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WrongHidingInLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WrongHidingInLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WrongNumberOfConstructorArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WSM | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
xForPrim | Agda.Compiler.MAlonzo.Primitives
xhqn | Agda.Compiler.MAlonzo.Misc
xqual | Agda.Compiler.MAlonzo.Misc
Yes
1 (Data Constructor) | Agda.TypeChecking.Coverage.Match
2 (Data Constructor) | Agda.TypeChecking.Patterns.Match
yesMatchLit | Agda.TypeChecking.Coverage.Match
YesReduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
YesType
1 (Type/Class) | Agda.TypeChecking.Test.Generators
2 (Data Constructor) | Agda.TypeChecking.Test.Generators
zero | Agda.Termination.Semiring
zeroName | Agda.TypeChecking.Level
zeroWidthText | Agda.Utils.Pretty
ZigZagMode | Agda.Utils.Pretty
zipNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
zipScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
zipScope_ | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
zipWith | Agda.Termination.Matrix
zipWithM' | Agda.Utils.Monad
|-> | Agda.TypeChecking.Rules.LHS.Unify