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

main	Agda.Main
mainName	Agda.Compiler.Epic.Interface
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
makeForcedArgs	Agda.Compiler.Epic.ForceConstrs
makeInstance	Agda.Syntax.Common
makeOpen	Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
makeProjection	Agda.TypeChecking.ProjectionLike
makeSubstitution	Agda.TypeChecking.Rules.LHS.Unify
MAlonzo	Agda.Interaction.InteractionTop
many	Agda.Utils.ReadP
many1	Agda.Utils.ReadP
manyTill	Agda.Utils.ReadP
map
1 (Function)	Agda.Utils.HashMap
2 (Function)	Agda.Compiler.JS.Substitution
map'	Agda.Compiler.JS.Substitution
mapArgHiding	Agda.Syntax.Common
mapArgRelevance	Agda.Syntax.Common
mapCon	Agda.Compiler.Epic.Primitive
mapDomHiding	Agda.Syntax.Common
mapDomRelevance	Agda.Syntax.Common
mapEither
1 (Function)	Agda.Utils.List
2 (Function)	Agda.Utils.Either
mapFlag	Agda.Interaction.Options
mapFst	Agda.Utils.Tuple
mapFstM	Agda.Utils.Tuple
mapLeft	Agda.Utils.Either
mapLHSHead	Agda.Syntax.Abstract
mapM'	Agda.Utils.Monad
mapMaybe	Agda.Utils.Maybe
mapMaybeM	Agda.Utils.Monad
mapNameSpace	Agda.Syntax.Scope.Base
mapNameSpaceM	Agda.Syntax.Scope.Base
mapNodes	Agda.Utils.Warshall
mapPairM	Agda.Utils.Tuple
mapping	Agda.Compiler.JS.Compiler
mapping'	Agda.Compiler.JS.Compiler
mapRight	Agda.Utils.Either
MapS	Agda.Auto.Convert
mapScope	Agda.Syntax.Scope.Base
mapScopeM	Agda.Syntax.Scope.Base
mapScopeM_	Agda.Syntax.Scope.Base
mapScope_	Agda.Syntax.Scope.Base
mapSize	Agda.Utils.QuickCheck
mapSnd	Agda.Utils.Tuple
mapSndM	Agda.Utils.Tuple
mapTCMT	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MArgList	Agda.Auto.Syntax
markStatic	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
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.Compiler.JS.Case
2 (Function)	Agda.TypeChecking.Coverage.Match
3 (Function)	Agda.Syntax.Parser.LookAhead
4 (Function)	Agda.Interaction.Highlighting.Vim
5 (Function)	Agda.TypeChecking.DisplayForm
6 (Function)	Agda.TypeChecking.CompiledClause.Match
match'
1 (Function)	Agda.Syntax.Parser.LookAhead
2 (Function)	Agda.TypeChecking.CompiledClause.Match
matchClause	Agda.TypeChecking.Coverage.Match
matchCommand	Agda.Interaction.CommandLine.CommandLine
matchCompiled	Agda.TypeChecking.CompiledClause.Match
matchDisplayForm	Agda.TypeChecking.DisplayForm
Matched	Agda.TypeChecking.Positivity
matches	Agda.Interaction.Highlighting.Vim
MatchLit	Agda.TypeChecking.Coverage.Match
matchLits	Agda.TypeChecking.Coverage.Match
matchPat	Agda.TypeChecking.Coverage.Match
matchPats	Agda.TypeChecking.Coverage.Match
matchPattern	Agda.TypeChecking.Patterns.Match
matchPatterns	Agda.TypeChecking.Patterns.Match
matchType	Agda.Auto.Convert
Matrix
1 (Type/Class)	Agda.Termination.Matrix
2 (Type/Class)	Agda.Termination.SparseMatrix
3 (Type/Class)	Agda.Utils.Warshall
matrix
1 (Function)	Agda.Termination.Matrix
2 (Function)	Agda.Termination.SparseMatrix
3 (Function)	Agda.Utils.Warshall
matrixInvariant
1 (Function)	Agda.Termination.Matrix
2 (Function)	Agda.Termination.SparseMatrix
matrixUsingRowGen
1 (Function)	Agda.Termination.Matrix
2 (Function)	Agda.Termination.SparseMatrix
Max	Agda.Syntax.Internal
maxDiscardRatio	Agda.Utils.QuickCheck
maxName	Agda.TypeChecking.Level
maxSize	Agda.Utils.QuickCheck
maxSuccess	Agda.Utils.QuickCheck
maxViewCons	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
maxViewMax	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
maxViewSuc_	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
Maybe	Agda.Utils.Maybe
maybe	Agda.Utils.Maybe
maybeCoGen	Agda.Utils.TestHelpers
maybeGen	Agda.Utils.TestHelpers
maybeor	Agda.Auto.Typecheck
maybePrefixMatch	Agda.Utils.List
maybePrimCon	Agda.TypeChecking.Level
maybePrimDef	Agda.TypeChecking.Level
MaybeRed	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MaybeReduced	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MaybeReducedArgs	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
maybeToList	Agda.Utils.Maybe
MayNotPostpone	Agda.TypeChecking.Rules.LHS.Unify
MayPostpone	Agda.TypeChecking.Rules.LHS.Unify
mazBoolToHBool	Agda.Compiler.MAlonzo.Primitives
mazCharToInteger	Agda.Compiler.MAlonzo.Primitives
mazCoerce	Agda.Compiler.MAlonzo.Misc
mazerror	Agda.Compiler.MAlonzo.Misc
mazHBoolToBool	Agda.Compiler.MAlonzo.Primitives
mazHListToList	Agda.Compiler.MAlonzo.Primitives
mazIncompleteMatch	Agda.Compiler.MAlonzo.Misc
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
mazRTE	Agda.Compiler.MAlonzo.Misc
mazstr	Agda.Compiler.MAlonzo.Misc
mazStringToList	Agda.Compiler.MAlonzo.Primitives
MB	Agda.Auto.NarrowingSearch
mbcase	Agda.Auto.NarrowingSearch
mbfailed	Agda.Auto.NarrowingSearch
mbind	Agda.Auto.NarrowingSearch
mbpcase	Agda.Auto.NarrowingSearch
mbret	Agda.Auto.NarrowingSearch
mcompoint	Agda.Auto.NarrowingSearch
member
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.HashMap
MemberId
1 (Type/Class)	Agda.Compiler.JS.Syntax
2 (Data Constructor)	Agda.Compiler.JS.Syntax
MentionsMeta	Agda.TypeChecking.MetaVars.Mention
mentionsMeta	Agda.TypeChecking.MetaVars.Mention
mergeGroups	Agda.Compiler.Epic.Injection
mergeInterface	Agda.Interaction.Imports
mergeNames	Agda.Syntax.Scope.Base
mergeScope	Agda.Syntax.Scope.Base
mergeScopes	Agda.Syntax.Scope.Base
Meta	Agda.Auto.NarrowingSearch
MetaArg	Agda.TypeChecking.Positivity
MetaCannotDependOn	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaElim	Agda.TypeChecking.Eliminators
MetaEnv	Agda.Auto.NarrowingSearch
MetaId
1 (Type/Class)	Agda.Syntax.Internal
2 (Data Constructor)	Agda.Syntax.Internal
MetaInfo
1 (Type/Class)	Agda.Interaction.Highlighting.Precise
2 (Data Constructor)	Agda.Interaction.Highlighting.Precise
3 (Type/Class)	Agda.Syntax.Info
4 (Data Constructor)	Agda.Syntax.Info
5 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
6 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaInstantiation	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaKind	Agda.TypeChecking.MetaVars
MetaLevel	Agda.Syntax.Internal
metaliseokh	Agda.Auto.Syntax
MetaNameSuggestion	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
metaNameSuggestion	Agda.Syntax.Info
metaNumber	Agda.Syntax.Info
metaOccurs	Agda.TypeChecking.MetaVars.Occurs
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
metaScope	Agda.Syntax.Info
MetaSh	Agda.TypeChecking.Rules.LHS.Unify
MetaStore	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaV	Agda.Syntax.Internal
MetaVar	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Metavar
1 (Type/Class)	Agda.Auto.NarrowingSearch
2 (Data Constructor)	Agda.Auto.NarrowingSearch
MetaVariable	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
meta_not_constructor	Agda.Auto.Typecheck
MExp	Agda.Auto.Syntax
mextrarefs	Agda.Auto.NarrowingSearch
mhead	Agda.Utils.List
miClosRange	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MId	Agda.Auto.Syntax
miInterface	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
miMetaOccursCheck	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mimicGHCi	Agda.Interaction.GhcTop
miNameSuggestion	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
MissingDataSignature	Agda.Syntax.Concrete.Definitions
MissingDefinition	Agda.Syntax.Concrete.Definitions
MissingTypeSignature	Agda.Syntax.Concrete.Definitions
MissingWithClauses	Agda.Syntax.Concrete.Definitions
miTimeStamp	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
miWarnings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MIx
1 (Type/Class)	Agda.Termination.Matrix
2 (Data Constructor)	Agda.Termination.Matrix
3 (Type/Class)	Agda.Termination.SparseMatrix
4 (Data Constructor)	Agda.Termination.SparseMatrix
Mixed	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mIxInvariant
1 (Function)	Agda.Termination.Matrix
2 (Function)	Agda.Termination.SparseMatrix
mkAbs	Agda.TypeChecking.Substitute
mkAbsolute	Agda.Utils.FileName
mkBoundName_	Agda.Syntax.Concrete
mkCon	Agda.Compiler.Epic.Forcing
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
mkName_	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
mkNotation	Agda.Syntax.Notation
mkPi	Agda.TypeChecking.Substitute
mkPrimFun1	Agda.TypeChecking.Primitive
mkPrimFun1TCM	Agda.TypeChecking.Primitive
mkPrimFun2	Agda.TypeChecking.Primitive
mkPrimFun4	Agda.TypeChecking.Primitive
mkPrimLevelMax	Agda.TypeChecking.Primitive
mkPrimLevelSuc	Agda.TypeChecking.Primitive
mkPrimLevelZero	Agda.TypeChecking.Primitive
MkStr	Agda.Utils.QuickCheck
mkType	Agda.Syntax.Internal
mkUnused	Agda.TypeChecking.Polarity
mlevel	Agda.TypeChecking.Conversion
MM	Agda.Auto.NarrowingSearch
mm	Agda.Auto.CaseSplit
mmbpcase	Agda.Auto.NarrowingSearch
mmcase	Agda.Auto.NarrowingSearch
mmmcase	Agda.Auto.NarrowingSearch
mmpcase	Agda.Auto.NarrowingSearch
MName	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
mnameFromList	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
mnameToConcrete	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
mnameToList	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
mnameToQName	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
mobs	Agda.Auto.NarrowingSearch
Mode	Agda.Utils.Pretty
mode	Agda.Utils.Pretty
modifyAbstractClause	Agda.Auto.Convert
modifyAbstractExpr	Agda.Auto.Convert
modifyContext	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
modifyContextEntries	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
modifyContextEntry	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
modifyCurrentNameSpace	Agda.Syntax.Scope.Monad
modifyCurrentScope	Agda.Syntax.Scope.Monad
modifyCurrentScopeM	Agda.Syntax.Scope.Monad
modifyEI	Agda.Compiler.Epic.CompileState
modifyImportedSignature	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
modifyMetaStore	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
modifyNamedScope	Agda.Syntax.Scope.Monad
modifyNamedScopeM	Agda.Syntax.Scope.Monad
modifyOccursCheckDefs	Agda.TypeChecking.MetaVars.Occurs
modifyPatternSyns	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
modifyScope	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
modifyScopeInfo	Agda.Syntax.Scope.Monad
modifyScopes	Agda.Syntax.Scope.Monad
modifySignature	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
modName	Agda.Compiler.JS.Syntax
modname	Agda.Compiler.JS.Pretty
modSub	Agda.TypeChecking.Rules.LHS.Unify
Module
1 (Type/Class)	Agda.Compiler.JS.Syntax
2 (Data Constructor)	Agda.Compiler.JS.Syntax
3 (Type/Class)	Agda.Syntax.Concrete
4 (Data Constructor)	Agda.Syntax.Concrete
5 (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
moduleContents	Agda.Interaction.BasicOps
ModuleDefinedInOtherFile	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ModuleDoesntExport	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ModuleInfo
1 (Type/Class)	Agda.Syntax.Info
2 (Data Constructor)	Agda.Syntax.Info
3 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
4 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ModuleMacro	Agda.Syntax.Concrete
ModuleName	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
moduleName	Agda.Interaction.FindFile
moduleName'	Agda.Interaction.FindFile
ModuleNameDoesntMatchFileName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
moduleNameParts	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
moduleNameToFileName	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
moduleParser
1 (Function)	Agda.Syntax.Parser.Parser
2 (Function)	Agda.Syntax.Parser
ModulesInScope	Agda.Syntax.Scope.Base
ModuleTag	Agda.Syntax.Scope.Base
ModuleToSource	Agda.Interaction.FindFile
MonadException	Agda.TypeChecking.Monad.Exception
MonadTCM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
moreRelevant	Agda.Syntax.Common
movePos	Agda.Syntax.Position
movePosByString	Agda.Syntax.Position
mparen	Agda.Syntax.Concrete.Operators
mparens	Agda.Utils.Pretty
MPat	Agda.TypeChecking.Coverage.Match
mpret	Agda.Auto.NarrowingSearch
mprincipalpresent	Agda.Auto.NarrowingSearch
mul
1 (Function)	Agda.Termination.Semiring
2 (Function)	Agda.Termination.Matrix
3 (Function)	Agda.Termination.SparseMatrix
MultipleFixityDecls	Agda.Syntax.Concrete.Definitions
multiply	Agda.Termination.Semiring
munch	Agda.Utils.ReadP
munch1	Agda.Utils.ReadP
MutId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Mutual
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
MutualId	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MutualInfo
1 (Type/Class)	Agda.Syntax.Info
2 (Data Constructor)	Agda.Syntax.Info
mutuallyRecursive	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
mutualRange	Agda.Syntax.Info
mutualTermCheck	Agda.Syntax.Info
mvFrozen	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
mvPermutation	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvPriority	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MyMB	Agda.Auto.Syntax
MyPB	Agda.Auto.Syntax