Agda-2.2.4: 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.Utils.QuickCheck >*< 1 (Function) Agda.Termination.CallGraph 2 (Function) Agda.TypeChecking.Positivity >+< Agda.TypeChecking.Positivity >-> Agda.Utils.Serialise >< 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.Syntax.Internal 2 (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 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 addSlash Agda.Utils.FileName 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 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 alreadyVisited Agda.Interaction.Imports 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 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 andM Agda.Compiler.Agate.Classify AnyWhere Agda.Syntax.Concrete APatName Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop App 1 (Data Constructor) Agda.Syntax.Concrete 2 (Data Constructor) Agda.Syntax.Abstract 3 (Data Constructor) Agda.TypeChecking.EtaContract appBrackets Agda.Syntax.Fixity appendErrorToEmacsFile Agda.Interaction.Highlighting.Emacs appendFile Agda.Utils.IO 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 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 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 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 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 BiMonad Agda.Utils.Serialise 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 bindBuiltinName Agda.TypeChecking.Monad.Builtin bindBuiltinNil Agda.TypeChecking.Rules.Builtin bindBuiltinPrimitive Agda.TypeChecking.Rules.Builtin bindBuiltinSuc Agda.TypeChecking.Rules.Builtin bindBuiltinType Agda.TypeChecking.Rules.Builtin bindBuiltinType1 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 bindS Agda.Utils.Serialise 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 Block Agda.TypeChecking.Coverage.Match Blocked 1 (Type/Class) Agda.Syntax.Internal 2 (Data Constructor) Agda.Syntax.Internal blocked Agda.Syntax.Internal BlockedConst Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad 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 brackets 1 (Function) Agda.Utils.Pretty 2 (Function) Agda.TypeChecking.Pretty bsToString Agda.Utils.Serialise 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 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 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 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 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 canonicalName Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad CantSplit Agda.TypeChecking.Coverage cat Agda.Utils.Pretty catchConstraint Agda.TypeChecking.Constraints catchException Agda.TypeChecking.Monad.Exception catchImpossible Agda.Utils.Impossible catMaybes Agda.Utils.Maybe cdecl Agda.Compiler.MAlonzo.Compiler 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 charS Agda.Utils.Serialise 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.Imports 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 1 (Function) Agda.Utils.ReadP 2 (Function) Agda.TypeChecking.Coverage.Match choose Agda.Utils.QuickCheck chop Agda.Utils.List Chr Agda.Utils.Pretty cirBuiltin Agda.Interaction.Imports cirDecoded Agda.Interaction.Imports cirInterface Agda.Interaction.Imports cirSignature Agda.Interaction.Imports cirVisited Agda.Interaction.Imports 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.Syntax.Concrete.Definitions 2 (Data Constructor) Agda.Syntax.Concrete.Definitions 3 (Type/Class) Agda.Syntax.Internal 4 (Data Constructor) Agda.Syntax.Internal 5 (Type/Class) Agda.Syntax.Abstract 6 (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 clearSyntaxInfo Agda.Interaction.Highlighting.Emacs clearUndoHistory Agda.Utils.Monad.Undo clEnv Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad closeBrace Agda.Syntax.Parser.Layout 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_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_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_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_reset Agda.Interaction.GhciTop cmd_solveAll Agda.Interaction.GhciTop cmd_undo 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 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 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 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 Comparison Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad 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 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 Constructor 1 (Type/Class) Agda.Syntax.Concrete 2 (Type/Class) Agda.Syntax.Abstract 3 (Data Constructor) Agda.Interaction.Highlighting.Precise 4 (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 CreateInterfaceResult Agda.Interaction.Imports createMetaInfo Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad createModule Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop Ctx 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 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 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.Interaction.Highlighting.Precise 2 (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 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.Syntax.Internal 2 (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 deserialise Agda.Utils.Serialise deserialiseLazy Agda.Utils.Serialise 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_infoD Agda.Interaction.GhciTop Dist Agda.Utils.Warshall Distance Agda.Utils.Warshall distinct Agda.Utils.List divConf Agda.TypeChecking.Test.Generators Doc 1 (Type/Class) Agda.Utils.Pretty 2 (Type/Class) Agda.TypeChecking.Pretty 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 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 doubleQuotes Agda.Utils.Pretty DPI Agda.TypeChecking.Rules.LHS dropArgs Agda.Compiler.Agate.Common dropDecodedModule Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad dropDirectory Agda.Utils.FileName dropI Agda.Syntax.Position, Agda.Interaction.GhciTop 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 EitherOrBoth Agda.Utils.Map El Agda.Syntax.Internal el Agda.TypeChecking.Primitive elements Agda.Utils.QuickCheck Ellipsis Agda.Syntax.Concrete emacsStr Agda.Interaction.GhciTop 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 ensureInductive Agda.TypeChecking.Rules.Builtin 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 equals Agda.Utils.Pretty equalSort Agda.TypeChecking.Conversion equalTerm Agda.TypeChecking.Conversion equalType Agda.TypeChecking.Conversion errInput Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop errMsg Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop Error 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 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 extractNthElement Agda.Utils.List 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 FileType Agda.Interaction.Imports filterKeys Agda.Utils.Map filterScope Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop findClause Agda.Interaction.MakeCase findFile Agda.Interaction.Imports findIdx Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop 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 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 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 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.Syntax.Concrete 2 (Data Constructor) Agda.Syntax.Internal 3 (Data Constructor) Agda.Syntax.Abstract 4 (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 getAllModules Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad 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 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 getContents Agda.Utils.IO 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 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 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 getLexInput Agda.Syntax.Parser.Alex getLexState Agda.Syntax.Parser.Monad getLine Agda.Utils.IO getLocalVars Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop 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 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 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 getUndoStack Agda.Utils.Monad.Undo getUndoStateNumber Agda.Utils.Monad.Undo 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 handleDeclarationException Agda.Interaction.Exceptions, Agda.Interaction.GhciTop handleParseException Agda.Interaction.Exceptions, Agda.Interaction.GhciTop handleTypeErrorException Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad 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 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 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 hGetLine Agda.Utils.IO Hidden 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 1 (Type/Class) Agda.Interaction.Highlighting.Precise 2 (Data Constructor) Agda.Interaction.Highlighting.Precise highMetaPriority Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad 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 hPutStr Agda.Utils.IO hPutStrLn Agda.Utils.IO 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 Id 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 IFun 1 (Type/Class) Agda.Utils.Serialise 2 (Data Constructor) Agda.Utils.Serialise 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 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 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 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 info Agda.Interaction.Highlighting.Precise 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 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 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 interact Agda.Utils.IO 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 InterfaceFile Agda.Interaction.Imports 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 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 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 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 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 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 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 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.Syntax.Concrete 2 (Data Constructor) Agda.Syntax.Internal 3 (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 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 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 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 LinePragma Agda.Syntax.Concrete 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 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 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 makeOpen Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad makeSubstitution Agda.TypeChecking.Rules.LHS.Unify 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.Utils.Serialise 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 mapUndoT Agda.Utils.Monad.Undo 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 matchFileName Agda.Interaction.Imports 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 maxDiscard Agda.Utils.QuickCheck 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 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 mazCurMName Agda.Compiler.MAlonzo.Misc mazCurrentMod 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 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 MetaArg Agda.TypeChecking.Positivity MetaCannotDependOn Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad 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 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 MetaVariable Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad metaVariable Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop 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 MIx 1 (Type/Class) Agda.Termination.Matrix 2 (Data Constructor) Agda.Termination.Matrix mIxInvariant Agda.Termination.Matrix 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 mkUndo Agda.Interaction.BasicOps MName Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop mnameFromFileName Agda.Compiler.MAlonzo.Misc 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 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 (Data Constructor) Agda.Syntax.Concrete 2 (Data Constructor) Agda.Interaction.Highlighting.Precise ModuleArityMismatch 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 ModuleMacro Agda.Syntax.Concrete ModuleName Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop ModuleNameDoesntMatchFileName Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad 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 MonadException Agda.TypeChecking.Monad.Exception MonadTCM Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad MonadUndo Agda.Utils.Monad.Undo 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 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 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 name Agda.Utils.FileName nameBindingSite Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop nameChar Agda.Utils.FileName 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.Syntax.Common 2 (Type/Class) Agda.TypeChecking.Primitive 3 (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 newArgsMeta Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop newArgsMetaCtx Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop newCall Agda.Utils.Trace newEdge Agda.Utils.Warshall NewFlex Agda.Utils.Warshall newLayoutContext Agda.Syntax.Parser.Layout newMeta 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 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 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 1 (Type/Class) Agda.Syntax.Concrete.Definitions 2 (Data Constructor) 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 NoInsertNeeded Agda.TypeChecking.Implicit NoInv Agda.TypeChecking.Injectivity 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 nonEmptyName Agda.Utils.FileName 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 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 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 NotBlocked Agda.Syntax.Internal notBlocked Agda.Syntax.Internal NotDelayed Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad note Agda.Interaction.Highlighting.Precise NotHidden 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 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 nubFiles Agda.Utils.FileName Number Agda.Interaction.Highlighting.Precise numOfMainS Agda.Compiler.Alonzo.Main numOfName Agda.Compiler.Alonzo.Names numOfQName Agda.Compiler.Alonzo.Names numTests Agda.Utils.QuickCheck 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, Agda.Interaction.GhciTop occurs Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop occursAs Agda.TypeChecking.Positivity occursCheck 1 (Function) Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop 2 (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 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 openBinaryFile Agda.Utils.IO 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 optGenerateEmacsFile 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 optUnreachableCheck Agda.Interaction.Options optVerbose Agda.Interaction.Options 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 PageMode Agda.Utils.Pretty 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 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.Utils.Serialise 2 (Data Constructor) Agda.Utils.Serialise 3 (Type/Class) Agda.Syntax.Parser.Monad 4 (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 path Agda.Utils.FileName pathOfLength Agda.Utils.FileName 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 pconName Agda.Compiler.MAlonzo.Primitives Perm Agda.Utils.Permutation Permutation Agda.Utils.Permutation permute Agda.Utils.Permutation pfail Agda.Utils.ReadP pHidden Agda.Syntax.Concrete.Pretty Pi 1 (Data Constructor) Agda.Syntax.Concrete 2 (Data Constructor) Agda.Syntax.Internal 3 (Data Constructor) Agda.Syntax.Abstract piAbstractTerm Agda.TypeChecking.Abstract piApply Agda.TypeChecking.Substitute piBrackets Agda.Syntax.Fixity piFreq Agda.TypeChecking.Test.Generators PiHead Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad plugHole Agda.Syntax.Internal.Pattern 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 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.Syntax.Concrete 2 (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 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 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 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 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 PrimType Agda.TypeChecking.Primitive primType Agda.TypeChecking.Primitive primZero Agda.TypeChecking.Monad.Builtin print Agda.Utils.IO printAlDecl Agda.Compiler.Alonzo.Haskell printAlModule Agda.Compiler.Alonzo.Haskell printConstants Agda.Compiler.Agate.Main Printer 1 (Type/Class) Agda.Utils.Serialise 2 (Data Constructor) Agda.Utils.Serialise printHsDecls Agda.Compiler.Alonzo.Haskell printHsMain Agda.Compiler.Alonzo.Haskell printHsModule Agda.Compiler.Alonzo.Haskell printShowConstants Agda.Compiler.Agate.Main printUsage Agda.Main printVersion Agda.Main 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 promote Agda.Utils.QuickCheck proofIrrelevance Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad Prop 1 (Type/Class) Agda.Utils.QuickCheck 2 (Data Constructor) Agda.Syntax.Concrete 3 (Data Constructor) Agda.Syntax.Internal 4 (Data Constructor) Agda.Syntax.Abstract prop Agda.Syntax.Internal 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_dropDirectory Agda.Utils.FileName 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_pathOfLength Agda.Utils.FileName prop_reorderTelStable Agda.TypeChecking.Tests prop_smaller Agda.Utils.Warshall prop_splitPath Agda.Utils.FileName prop_splitPath_unsplitPath Agda.Utils.FileName 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 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 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 putStrLn Agda.Utils.IO putUndoStack Agda.Utils.Monad.Undo 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 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 readFile Agda.Utils.IO readInterface Agda.Interaction.Imports readline Agda.Interaction.Monad readLn Agda.Utils.IO readM Agda.Utils.Monad ReadP Agda.Utils.ReadP readTextFile Agda.Utils.IO 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 recArgOccurrences Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad RecBehaviour Agda.Termination.Lexicographic recBehaviourInvariant Agda.Termination.Lexicographic recClause 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 recSort 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 refine Agda.Interaction.BasicOps refineMeta Agda.Interaction.CommandLine.CommandLine 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 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 replicateS Agda.Utils.Serialise 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 response Agda.Interaction.GhciTop 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 returnS Agda.Utils.Serialise reverseP Agda.Utils.Permutation Rewrite Agda.Interaction.BasicOps rewrite Agda.Interaction.BasicOps 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 RightAssoc Agda.Syntax.Fixity 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 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 runParser Agda.Utils.Serialise runPrinter Agda.Utils.Serialise runTCM Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad runTests Agda.Utils.TestHelpers runUndoT Agda.Utils.Monad.Undo RVar Agda.Utils.Warshall sameVars Agda.TypeChecking.Conversion sample Agda.Utils.QuickCheck sample' Agda.Utils.QuickCheck satisfy Agda.Utils.ReadP SClause Agda.TypeChecking.Coverage 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 scSubst Agda.TypeChecking.Coverage scTel Agda.TypeChecking.Coverage 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 sequenceS Agda.Utils.Serialise Serialisable Agda.Utils.Serialise serialise Agda.Utils.Serialise serialiser Agda.Utils.Serialise 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 setExtension Agda.Utils.FileName 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 setUndo Agda.Utils.Monad.Undo setVisitedModules Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad setWorkingDirectory Agda.Interaction.Imports 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 showImplicitArgs Agda.Interaction.GhciTop showImplicitArguments Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad 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 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 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 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 skipBlock Agda.Syntax.Parser.Comments skipMany Agda.Utils.ReadP skipMany1 Agda.Utils.ReadP skipSpaces Agda.Utils.ReadP slash Agda.Utils.FileName slashes Agda.Utils.FileName sLub Agda.Syntax.Internal smallestPos Agda.Interaction.Highlighting.Precise Smart 1 (Data Constructor) Agda.Utils.QuickCheck 2 (Type/Class) Agda.Utils.QuickCheck 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 (Type/Class) Agda.Syntax.Internal 2 (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 sortOfConst Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad source 1 (Function) Agda.Termination.CallGraph 2 (Function) Agda.Interaction.Highlighting.Precise SourceFile Agda.Interaction.Imports 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 splitExt Agda.Utils.FileName splitFilePath Agda.Utils.FileName SplitPanic Agda.TypeChecking.Rules.LHS.Problem splitPath Agda.Utils.FileName 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 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 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 stMutualBlocks Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad stOptions Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad store Agda.Utils.Pointer storeDecodedModule Agda.TypeChecking.Monad.Imports, 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 stringS Agda.Utils.Serialise 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 Agda.TypeChecking.Rules.LHS.Unify 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 1 (Data Constructor) Agda.Utils.QuickCheck 2 (Data Constructor) Agda.Interaction.Imports suchThat Agda.Utils.QuickCheck suchThatMaybe Agda.Utils.QuickCheck Suffix 1 (Type/Class) Agda.Utils.Suffix 2 (Type/Class) Agda.Utils.List 3 (Type/Class) Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete 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.Termination.CallGraph TBind 1 (Data Constructor) Agda.Syntax.Concrete 2 (Data Constructor) Agda.Syntax.Abstract 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 Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad 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 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 tellEmacsToReloadSyntaxInfo Agda.Interaction.GhciTop tellEmacsToUpdateGoals 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 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 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.Utils.Warshall 11 (Function) Agda.Interaction.Options 12 (Function) Agda.Interaction.Highlighting.Range 13 (Function) Agda.Interaction.Highlighting.Precise 14 (Function) Agda.Interaction.Highlighting.Generate 15 (Function) Agda.Interaction.Highlighting.Emacs 16 (Function) Agda.TypeChecking.Tests 17 (Function) Agda.Compiler.MAlonzo.Encode testSuite Agda.Tests text 1 (Function) Agda.Utils.Pretty 2 (Function) Agda.TypeChecking.Pretty TextDetails Agda.Utils.Pretty theDef Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad theInteractionPoints Agda.Interaction.GhciTop theState Agda.Interaction.GhciTop theTCState Agda.Interaction.GhciTop theTopLevel Agda.Interaction.GhciTop theUndoStack 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 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.Imports 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 toMap Agda.Interaction.Highlighting.Precise 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 Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop topoSort Agda.Utils.Permutation ToTerm Agda.TypeChecking.Primitive toTerm Agda.TypeChecking.Primitive 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 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 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.Syntax.Internal 2 (Type/Class) Agda.Syntax.Internal TypeAndDef Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop typeArity Agda.Compiler.Alonzo.Main TypeCheckingDone Agda.Interaction.Highlighting.Generate TypeCheckingNotDone Agda.Interaction.Highlighting.Generate TypeCheckingState Agda.Interaction.Highlighting.Generate TypeCmp Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad 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 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.Utils.Monad.Undo UndoT 1 (Type/Class) Agda.Utils.Monad.Undo 2 (Data Constructor) Agda.Utils.Monad.Undo 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 unlistenToMeta Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad 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 UnsolvedMeta Agda.Interaction.Highlighting.Precise UnsolvedMetas Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad unsolvedMetaVariables Agda.Interaction.Imports unsplitPath Agda.Utils.FileName unStr Agda.TypeChecking.Primitive unTCM Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad untypedAbs Agda.Compiler.Agate.UntypedPrinter unUndoT Agda.Utils.Monad.Undo 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 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 validParameters Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop ValueCmp Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad Var 1 (Data Constructor) Agda.Syntax.Internal 2 (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 Agda.Interaction.Imports warshall Agda.Utils.Warshall warshallG Agda.Utils.Warshall 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 withBinaryFile Agda.Utils.IO 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 writeEmacsFile Agda.Interaction.Highlighting.Emacs writeFile Agda.Utils.IO 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 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