A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
:
!
$
%
+
.
/
<
=
>
^
-
_
All

Index - M

M	Agda.Auto.Options
Macro
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Interaction.Highlighting.Precise
3 (Data Constructor)	Agda.Syntax.Abstract
MacroDef	Agda.Syntax.Common
MacroName	Agda.Syntax.Scope.Base
main	Agda.Main
MainInterface
1 (Type/Class)	Agda.Interaction.Imports
2 (Data Constructor)	Agda.Interaction.Imports
makeAbstract	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
makeAbstractClause	Agda.Interaction.MakeCase
makeAbsurdClause	Agda.Interaction.MakeCase
makeAll	Agda.Utils.IndexedList
makeCase	Agda.Interaction.MakeCase
MakeCaseVariant	Agda.Interaction.Response
makeInstance	Agda.Syntax.Common
makeInstance'	Agda.Syntax.Common
makeOpen	Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend
makePatternVarsVisible	Agda.Interaction.MakeCase
makePi	Agda.Syntax.Concrete
makeProjection	Agda.TypeChecking.ProjectionLike
makeSubstitution	Agda.TypeChecking.Rewriting.NonLinMatch
malformed	Agda.TypeChecking.Serialise.Base
many	Agda.Utils.Parser.ReadP
many1	Agda.Utils.Parser.ReadP
ManyHoles	Agda.Utils.AffineHole
manyTill	Agda.Utils.Parser.ReadP
Map	Agda.Utils.TypeLevel
map
1 (Function)	Agda.Utils.HashMap
2 (Function)	Agda.Utils.Bag
3 (Function)	Agda.Compiler.JS.Substitution
map'	Agda.Compiler.JS.Substitution
mapAbsNames	Agda.Syntax.Internal
mapAbsNamesM	Agda.Syntax.Internal
mapAbsoluteIncludePaths	Agda.Interaction.Options.Lenses
mapAPattern	Agda.Syntax.Abstract.Pattern
mapArgInfo	Agda.Syntax.Common
mapAwakeConstraints	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapBenchmarkOn	Agda.Utils.Benchmark
mapClosure	Agda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapCommandLineOptions	Agda.Interaction.Options.Lenses
mapConName	Agda.Syntax.Internal
mapCPattern	Agda.Syntax.Concrete.Pattern
mapCurrentAccount	Agda.Utils.Benchmark
mapEither
1 (Function)	Agda.Utils.Either
2 (Function)	Agda.Utils.List
mapEither3M	Agda.Utils.Three
mapExceptT	Agda.Utils.Except
mapExpr
1 (Function)	Agda.Syntax.Concrete.Generic
2 (Function)	Agda.Syntax.Abstract.Views
mapFlag	Agda.Interaction.Options
mapFreeVariables	Agda.Syntax.Common
mapFreeVariablesArgInfo	Agda.Syntax.Common
mapFst	Agda.Utils.Tuple
mapFstM	Agda.Utils.Tuple
mapHiding	Agda.Syntax.Common
mapHidingArgInfo	Agda.Syntax.Common
mapImportDir	Agda.Syntax.Scope.Monad
mapIncludePaths	Agda.Interaction.Options.Lenses
mapInScope	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
mapKeysMonotonic	Agda.Utils.AssocList
mapLeft	Agda.Utils.Either
mapLHSHead	Agda.Syntax.Abstract.Pattern
mapLhsOriginalPattern	Agda.Syntax.Concrete.Pattern
mapLhsOriginalPatternM	Agda.Syntax.Concrete.Pattern
mapListT	Agda.Utils.ListT
mapM'	Agda.Utils.Monad
mapMaybe
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.HashMap
3 (Function)	Agda.Utils.Maybe.Strict
mapMaybeAndRest	Agda.Utils.List
mapMaybeM	Agda.Utils.Monad
mapMaybeWithKey	Agda.Utils.HashMap
mapMListT	Agda.Utils.ListT
mapMListT_alt	Agda.Utils.ListT
mapMM	Agda.Utils.Monad
mapModality	Agda.Syntax.Common
mapModalityArgInfo	Agda.Syntax.Common
MapNamedArgPattern
1 (Type/Class)	Agda.Syntax.Internal.Pattern
2 (Type/Class)	Agda.Syntax.Abstract.Pattern
mapNamedArgPattern
1 (Function)	Agda.Syntax.Internal.Pattern
2 (Function)	Agda.Syntax.Abstract.Pattern
mapNameOf	Agda.Syntax.Common
mapNameSpace	Agda.Syntax.Scope.Base
mapNameSpaceM	Agda.Syntax.Scope.Base
mapOrigin	Agda.Syntax.Common
mapOriginArgInfo	Agda.Syntax.Common
mapPairM	Agda.Utils.Tuple
mapPersistentVerbosity	Agda.Interaction.Options.Lenses
mapping	Agda.Interaction.Highlighting.Precise
mapPragmaOptions	Agda.Interaction.Options.Lenses
mapQuantity	Agda.Syntax.Common
mapQuantityMod	Agda.Syntax.Common
mapRedEnv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapRedEnvSt	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapRedSt	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapRelevance	Agda.Syntax.Common
mapRelevanceMod	Agda.Syntax.Common
mapRenaming	Agda.Syntax.Scope.Monad
mapRight	Agda.Utils.Either
MapS	Agda.Auto.Convert
mapSafeMode	Agda.Interaction.Options.Lenses
mapScope	Agda.Syntax.Scope.Base
mapScope'	Agda.Syntax.Scope.Base
mapScopeInfo	Agda.Syntax.Scope.Base
mapScopeM	Agda.Syntax.Scope.Base
mapScopeM_	Agda.Syntax.Scope.Base
mapScope_	Agda.Syntax.Scope.Base
mapSleepingConstraints	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapSnd	Agda.Utils.Tuple
mapSndM	Agda.Utils.Tuple
mapSubTries	Agda.Utils.Trie
mapTCMT	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapTimings	Agda.Utils.Benchmark
mapUsing	Agda.Syntax.Scope.Monad
mapVarMap	Agda.TypeChecking.Free.Lazy
mapVerbosity	Agda.Interaction.Options.Lenses
mapVisitedModule	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapWithEdge	Agda.Utils.Graph.AdjacencyMap.Unidirectional
mapWithIndex	Agda.Utils.IndexedList
mapWithKey
1 (Function)	Agda.Utils.HashMap
2 (Function)	Agda.Utils.AssocList
mapWithKeyM	Agda.Utils.AssocList
MArgList	Agda.Auto.Syntax
markInjective	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
markInline	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
markStatic	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Markup
1 (Data Constructor)	Agda.Syntax.Parser.Literate
2 (Data Constructor)	Agda.Interaction.Highlighting.Precise
Masked
1 (Type/Class)	Agda.Termination.Monad
2 (Data Constructor)	Agda.Termination.Monad
masked	Agda.Termination.Monad
MaskedDeBruijnPatterns	Agda.Termination.Monad
Mat	Agda.Termination.Order
mat	Agda.Termination.CallMatrix
Match
1 (Type/Class)	Agda.Utils.Haskell.Syntax
2 (Data Constructor)	Agda.Utils.Haskell.Syntax
3 (Type/Class)	Agda.TypeChecking.Patterns.Match
4 (Type/Class)	Agda.TypeChecking.DisplayForm
5 (Type/Class)	Agda.TypeChecking.Rewriting.NonLinMatch
6 (Type/Class)	Agda.TypeChecking.Coverage.Match
match
1 (Function)	Agda.Syntax.Parser.LookAhead
2 (Function)	Agda.TypeChecking.DisplayForm
3 (Function)	Agda.Interaction.Highlighting.Vim
4 (Function)	Agda.TypeChecking.Rewriting.NonLinMatch
5 (Function)	Agda.TypeChecking.Coverage.Match
match'
1 (Function)	Agda.Syntax.Parser.LookAhead
2 (Function)	Agda.TypeChecking.CompiledClause.Match
matchCommand	Agda.Interaction.CommandLine
matchCompiled	Agda.TypeChecking.CompiledClause.Match
matchCompiledE	Agda.TypeChecking.CompiledClause.Match
matchCopattern	Agda.TypeChecking.Patterns.Match
matchCopatterns	Agda.TypeChecking.Patterns.Match
matchDisplayForm	Agda.TypeChecking.DisplayForm
Matched	Agda.TypeChecking.Positivity.Occurrence
matchedArgs	Agda.TypeChecking.Patterns.Match
matches	Agda.Interaction.Highlighting.Vim
matchingBlocked	Agda.TypeChecking.Rewriting.NonLinMatch
matchPattern	Agda.TypeChecking.Patterns.Match
matchPatterns	Agda.TypeChecking.Patterns.Match
matchPatternSyn	Agda.Syntax.Abstract.PatternSynonyms
matchPatternSynP	Agda.Syntax.Abstract.PatternSynonyms
matchType	Agda.Auto.Convert
Matrix
1 (Type/Class)	Agda.Termination.SparseMatrix
2 (Data Constructor)	Agda.Termination.SparseMatrix
3 (Type/Class)	Agda.Utils.Warshall
matrix	Agda.Utils.Warshall
Max	Agda.Syntax.Internal
maxInstanceSearchDepth	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
maxInversionDepth	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
maxName	Agda.TypeChecking.Level
MaxNat
1 (Type/Class)	Agda.Utils.Monoid
2 (Data Constructor)	Agda.Utils.Monoid
maxVarOcc	Agda.TypeChecking.Free.Lazy
maxViewCons	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
maxViewMax	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
maxViewSuc_	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Maybe
1 (Type/Class)	Agda.Utils.Maybe
2 (Type/Class)	Agda.Utils.Maybe.Strict
maybe
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
MaybeAbort	Agda.TypeChecking.Injectivity
maybeAbort	Agda.Interaction.InteractionTop
maybeFastReduceTerm	Agda.TypeChecking.Reduce
maybeFlexiblePattern	Agda.TypeChecking.Rules.LHS
MaybeFree	Agda.TypeChecking.Free.Reduce
maybeLeft	Agda.Utils.Either
maybeM
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
maybeor	Agda.Auto.Typecheck
MaybePlaceholder	Agda.Syntax.Common
maybePlaceholder	Agda.Syntax.Concrete.Operators.Parser
maybePrimCon	Agda.TypeChecking.Level
maybePrimDef	Agda.TypeChecking.Level
maybeProjTurnPostfix	Agda.Syntax.Abstract.Views
MaybeRed	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MaybeReduced	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MaybeReducedArgs	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MaybeReducedElims	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
maybeRight	Agda.Utils.Either
maybeTimed	Agda.Interaction.InteractionTop
maybeToEither	Agda.Utils.Either
maybeToList
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
MaybeWarnings	Agda.Interaction.Imports
MaybeWarnings'	Agda.Interaction.Imports
mazAnyType	Agda.Compiler.MAlonzo.Misc
mazAnyTypeName	Agda.Compiler.MAlonzo.Misc
mazCoerce	Agda.Compiler.MAlonzo.Misc
mazCoerceName	Agda.Compiler.MAlonzo.Misc
mazErasedName	Agda.Compiler.MAlonzo.Misc
mazerror	Agda.Compiler.MAlonzo.Misc
mazIncompleteMatch	Agda.Compiler.MAlonzo.Misc
mazMod	Agda.Compiler.MAlonzo.Misc
mazMod'	Agda.Compiler.MAlonzo.Misc
mazName	Agda.Compiler.MAlonzo.Misc
mazRTE	Agda.Compiler.MAlonzo.Misc
mazstr	Agda.Compiler.MAlonzo.Misc
mazUnreachableError	Agda.Compiler.MAlonzo.Misc
MB	Agda.Auto.NarrowingSearch
mbcase	Agda.Auto.NarrowingSearch
mbfailed	Agda.Auto.NarrowingSearch
mbind	Agda.Auto.NarrowingSearch
mbpcase	Agda.Auto.NarrowingSearch
mbret	Agda.Auto.NarrowingSearch
MCaseSplit	Agda.Auto.Options
mcompoint	Agda.Auto.NarrowingSearch
mcons	Agda.Utils.List
MdFileType	Agda.Syntax.Common
Measure	Agda.Syntax.Concrete.Definitions
measureTime	Agda.Utils.Time
meet	Agda.TypeChecking.SizedTypes.Utils
MeetSemiLattice	Agda.TypeChecking.SizedTypes.Utils
member
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.HashMap
3 (Function)	Agda.Utils.Bag
4 (Function)	Agda.Utils.IntSet.Infinite
5 (Function)	Agda.Utils.Trie
MemberId
1 (Type/Class)	Agda.Compiler.JS.Syntax
2 (Data Constructor)	Agda.Compiler.JS.Syntax
Memo	Agda.TypeChecking.Serialise.Base
memo	Agda.Utils.Memo
memoise
1 (Function)	Agda.Utils.Parser.MemoisedCPS
2 (Function)	Agda.Syntax.Concrete.Operators.Parser.Monad
memoiseIfPrinting
1 (Function)	Agda.Utils.Parser.MemoisedCPS
2 (Function)	Agda.Syntax.Concrete.Operators.Parser.Monad
MemoKey	Agda.Syntax.Concrete.Operators.Parser.Monad
memoModules	Agda.Syntax.Scope.Monad
memoNames	Agda.Syntax.Scope.Monad
memoRec	Agda.Utils.Memo
memoToScopeInfo	Agda.Syntax.Scope.Monad
memoUnsafe	Agda.Utils.Memo
memoUnsafeH	Agda.Utils.Memo
mentions	Agda.TypeChecking.SizedTypes.WarshallSolver
MentionsMeta	Agda.TypeChecking.MetaVars.Mention
mentionsMeta	Agda.TypeChecking.MetaVars.Mention
merge	Agda.Interaction.Highlighting.Precise
mergeC	Agda.Interaction.Highlighting.Precise
mergeEdges	Agda.TypeChecking.Positivity
mergeElim	Agda.TypeChecking.Patterns.Match
mergeElims	Agda.TypeChecking.Patterns.Match
mergeHiding	Agda.Syntax.Common
mergeInterface	Agda.Interaction.Imports
mergeNames	Agda.Syntax.Scope.Base
mergeNotations	Agda.Syntax.Fixity
mergePatternSynDefs	Agda.Syntax.Abstract.PatternSynonyms
mergeScope	Agda.Syntax.Scope.Base
mergeScopes	Agda.Syntax.Scope.Base
Meta
1 (Data Constructor)	Agda.Auto.NarrowingSearch
2 (Data Constructor)	Agda.Syntax.Reflected
MetaArg	Agda.TypeChecking.Positivity.Occurrence
MetaCannotDependOn	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaEnv	Agda.Auto.NarrowingSearch
metaFrozen	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
metaHelperType	Agda.Interaction.BasicOps
MetaId
1 (Type/Class)	Agda.Syntax.Common, Agda.Syntax.Internal
2 (Data Constructor)	Agda.Syntax.Common, Agda.Syntax.Internal
metaId	Agda.Syntax.Common, Agda.Syntax.Internal
MetaInfo
1 (Type/Class)	Agda.Syntax.Info
2 (Data Constructor)	Agda.Syntax.Info
3 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
4 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaInstantiation	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaIrrelevantSolution	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaKind	Agda.TypeChecking.MetaVars
MetaLevel	Agda.Syntax.Internal
MetaliseOKH	Agda.Auto.Syntax
metaliseOKH	Agda.Auto.Syntax
metaliseokh	Agda.Auto.Syntax
MetaNameSuggestion	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
metaNameSuggestion	Agda.Syntax.Info
metaNumber	Agda.Syntax.Info
metaOccurs	Agda.TypeChecking.MetaVars.Occurs
MetaOccursInItself	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
metaParseExpr	Agda.Interaction.CommandLine
MetaPriority
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
metaRange	Agda.Syntax.Info
MetaS	Agda.Syntax.Internal
metaScope	Agda.Syntax.Info
metasCreatedBy	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaSet	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
MetaStore	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaV	Agda.Syntax.Internal
MetaVar	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Metavar
1 (Type/Class)	Agda.Auto.NarrowingSearch
2 (Data Constructor)	Agda.Auto.NarrowingSearch
MetaVariable	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
meta_not_constructor	Agda.Auto.Typecheck
MExp	Agda.Auto.Syntax
mextrarefs	Agda.Auto.NarrowingSearch
miClosRange	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MId	Agda.Auto.Syntax
Middle	Agda.Syntax.Common
miGeneralizable	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
miInterface	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
miMetaOccursCheck	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mimicGHCi	Agda.Interaction.EmacsTop
miNameSuggestion	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
minfoAsName	Agda.Syntax.Info
minfoAsTo	Agda.Syntax.Info
minfoDirective	Agda.Syntax.Info
minfoOpenShort	Agda.Syntax.Info
minfoRange	Agda.Syntax.Info
minus	Agda.Interaction.Highlighting.Range
miPrimitive	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MissingClauses	Agda.Syntax.Internal
MissingDefinitions	Agda.Syntax.Concrete.Definitions
MissingDefinitions_	Agda.Interaction.Options.Warnings
MissingWithClauses	Agda.Syntax.Concrete.Definitions
miWarnings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MIx
1 (Type/Class)	Agda.Termination.SparseMatrix
2 (Data Constructor)	Agda.Termination.SparseMatrix
Mixed	Agda.TypeChecking.Positivity.Occurrence
mkAbs	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
mkAbsolute	Agda.Utils.FileName
mkBoundName	Agda.Syntax.Concrete
mkBoundName_	Agda.Syntax.Concrete
mkCall	Agda.Termination.CallGraph
mkCall'	Agda.Termination.CallGraph
mkCon	Agda.TypeChecking.Records
mkDef	Agda.Syntax.Translation.ReflectedToAbstract
mkDefInfo	Agda.Syntax.Info
mkDefInfoInstance	Agda.Syntax.Info
mkExceptT	Agda.Utils.Except
mkIf	Agda.Compiler.MAlonzo.Compiler
mkLam	Agda.TypeChecking.Substitute
mkLet
1 (Function)	Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Function)	Agda.Syntax.Abstract
mkMatrix	Agda.Utils.Warshall
MkName	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mkName	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mkName_	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mkNotation	Agda.Syntax.Notation
mkPi	Agda.TypeChecking.Substitute
mkPragma	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mkPrimFun1	Agda.TypeChecking.Primitive
mkPrimFun1TCM	Agda.TypeChecking.Primitive
mkPrimFun2	Agda.TypeChecking.Primitive
mkPrimFun4	Agda.TypeChecking.Primitive
mkPrimInjective	Agda.TypeChecking.Primitive
mkPrimLevelMax	Agda.TypeChecking.Primitive
mkPrimLevelSuc	Agda.TypeChecking.Primitive
mkPrimLevelZero	Agda.TypeChecking.Primitive
mkPrimSetOmega	Agda.TypeChecking.Primitive
mkProp	Agda.Syntax.Internal
mkSet	Agda.Syntax.Translation.ReflectedToAbstract
mkTApp	Agda.Syntax.Treeless, Agda.Compiler.Backend
mkTLam	Agda.Syntax.Treeless, Agda.Compiler.Backend
mkType	Agda.Syntax.Internal
mkWeakIORef	Agda.Utils.IORef
MM	Agda.Auto.NarrowingSearch
mmbpcase	Agda.Auto.NarrowingSearch
mmcase	Agda.Auto.NarrowingSearch
mmmcase	Agda.Auto.NarrowingSearch
mmpcase	Agda.Auto.NarrowingSearch
MName	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mnameFromList	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mnameToConcrete	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mnameToList	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mnameToQName	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
MNormal	Agda.Auto.Options
mobs	Agda.Auto.NarrowingSearch
Modality
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
modalityOfConst	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Mode
1 (Type/Class)	Agda.Utils.Pretty
2 (Type/Class)	Agda.Auto.Options
3 (Type/Class)	Agda.Interaction.Imports
mode	Agda.Utils.Pretty
modFile	Agda.TypeChecking.Serialise.Base
modifyAbsoluteIncludePaths	Agda.Interaction.Options.Lenses
modifyAbstractClause	Agda.Auto.Convert
modifyAbstractExpr	Agda.Auto.Convert
modifyAllowedReductions	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyArgOccurrences	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyAwakeConstraints	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyBenchmark
1 (Function)	Agda.Utils.Benchmark
2 (Function)	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyCommandLineOptions	Agda.Interaction.Options.Lenses
modifyContext	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyCurrentNameSpace	Agda.Syntax.Scope.Monad
modifyCurrentScope	Agda.Syntax.Scope.Monad
modifyCurrentScopeM	Agda.Syntax.Scope.Monad
modifyFunClauses	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyGlobalDefinition	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyImportedSignature	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyIncludePaths	Agda.Interaction.Options.Lenses
modifyInstanceDefs	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyInteractionPoints	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyIORef	Agda.Utils.IORef
modifyIORef'	Agda.Utils.IORef
modifyLocalVars	Agda.Syntax.Scope.Monad
modifyMetaStore	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyNamedScope	Agda.Syntax.Scope.Monad
modifyNamedScopeM	Agda.Syntax.Scope.Monad
modifyNameSpace	Agda.Syntax.Scope.Base
modifyOccursCheckDefs	Agda.TypeChecking.MetaVars.Occurs
modifyOldInteractionScopes	Agda.Interaction.InteractionTop
modifyPatternSyns	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyPersistentState	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyPersistentVerbosity	Agda.Interaction.Options.Lenses
modifyPragmaOptions	Agda.Interaction.Options.Lenses
modifySafeMode	Agda.Interaction.Options.Lenses
modifyScope	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyScopes	Agda.Syntax.Scope.Monad
modifyScope_	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifySignature	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifySleepingConstraints	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyStatistics	Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifySystem	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTC	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTC'	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTCLens	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTCLensM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTheInteractionPoints	Agda.Interaction.InteractionTop
modifyVerbosity	Agda.Interaction.Options.Lenses
modName	Agda.Compiler.JS.Syntax
modname	Agda.Compiler.JS.Pretty
modQuantity	Agda.Syntax.Common
modRelevance	Agda.Syntax.Common
Module
1 (Type/Class)	Agda.Utils.Haskell.Syntax
2 (Data Constructor)	Agda.Utils.Haskell.Syntax
3 (Type/Class)	Agda.Compiler.JS.Syntax
4 (Data Constructor)	Agda.Compiler.JS.Syntax
5 (Type/Class)	Agda.Syntax.Concrete
6 (Data Constructor)	Agda.Syntax.Concrete
7 (Data Constructor)	Agda.Interaction.Highlighting.Precise
ModuleApplication
1 (Type/Class)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.Syntax.Abstract
ModuleArityMismatch	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleAssignment
1 (Type/Class)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Concrete
ModuleContents	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
moduleContents	Agda.Interaction.BasicOps
ModuleDefinedInOtherFile	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleDoesntExport	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleDoesntExport_	Agda.Interaction.Options.Warnings
moduleHash	Agda.Interaction.Imports
ModuleId	Agda.Interaction.Highlighting.Dot
ModuleInfo
1 (Type/Class)	Agda.Syntax.Info
2 (Data Constructor)	Agda.Syntax.Info
3 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
4 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleMacro	Agda.Syntax.Concrete
ModuleMap	Agda.Syntax.Scope.Base
ModuleName
1 (Type/Class)	Agda.Utils.Haskell.Syntax
2 (Data Constructor)	Agda.Utils.Haskell.Syntax
3 (Type/Class)	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
4 (Data Constructor)	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
moduleName	Agda.Interaction.FindFile
ModuleNameDoesntMatchFileName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
moduleNameParser
1 (Function)	Agda.Syntax.Parser.Parser
2 (Function)	Agda.Syntax.Parser
moduleNameParts	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
moduleNameRange	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
moduleNameToFileName	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
ModuleNameUnexpected	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
moduleParamsToApply	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
moduleParser
1 (Function)	Agda.Syntax.Parser.Parser
2 (Function)	Agda.Syntax.Parser
ModulePragma	Agda.Utils.Haskell.Syntax
ModulesInScope	Agda.Syntax.Scope.Base
ModuleTag	Agda.Syntax.Scope.Base
ModuleToSource	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadBench	Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
MonadChange	Agda.Utils.Update
MonadDebug	Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadError	Agda.Utils.Except
MonadFixityError	Agda.Syntax.Concrete.Fixity
MonadGetDefs	Agda.Syntax.Internal.Defs
MonadPlus	Agda.Utils.Monad
MonadReduce	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTCEnv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTCM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTCState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTer	Agda.Termination.Monad
moreQuantity	Agda.Syntax.Common
moreRelevant	Agda.Syntax.Common
moreUsableModality	Agda.Syntax.Common
MOT	Agda.Auto.Convert
Move
1 (Data Constructor)	Agda.Auto.NarrowingSearch
2 (Type/Class)	Agda.Auto.SearchControl
Move'	Agda.Auto.NarrowingSearch
moveCost	Agda.Auto.NarrowingSearch
moveNext	Agda.Auto.NarrowingSearch
movePos	Agda.Syntax.Position
movePosByString	Agda.Syntax.Position
mparens	Agda.Utils.Pretty
mplus	Agda.Utils.Monad
mpret	Agda.Auto.NarrowingSearch
mprincipalpresent	Agda.Auto.NarrowingSearch
MRefine	Agda.Auto.Options
mul
1 (Function)	Agda.Termination.Semiring
2 (Function)	Agda.Termination.SparseMatrix
multiLineText
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
MultipleEllipses	Agda.Syntax.Concrete.Definitions
MultipleFixityDecls	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MultiplePolarityPragmas	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
munch	Agda.Utils.Parser.ReadP
munch1	Agda.Utils.Parser.ReadP
mustBeFinite	Agda.TypeChecking.SizedTypes.WarshallSolver
mustBePi	Agda.TypeChecking.Telescope
MutId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Mutual
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
MutualBlock
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mutualBlockOf	Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mutualChecks	Agda.TypeChecking.Rules.Decl
MutualId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MutualInfo
1 (Type/Class)	Agda.Syntax.Info
2 (Data Constructor)	Agda.Syntax.Info
mutualInfo	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mutuallyRecursive	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MutualNames	Agda.Termination.Monad
mutualNames	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mutualPositivityCheck	Agda.Syntax.Info
mutualRange	Agda.Syntax.Info
mutualTermCheck	Agda.Syntax.Info
mvFrozen	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvInfo	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvInstantiation	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvJudgement	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvListeners	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvPermutation	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvPriority	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MyMB	Agda.Auto.Syntax
MyPB	Agda.Auto.Syntax
mzero	Agda.Utils.Monad