Agda-2.5.3: A dependently typed functional programming language and proof assistant

Index - M

MAgda.Auto.Options
Macro 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
3 (Data Constructor)Agda.Syntax.Abstract
MacroDefAgda.Syntax.Common
MacroNameAgda.Syntax.Scope.Base
mainAgda.Main
MainInterface 
1 (Type/Class)Agda.Interaction.Imports
2 (Data Constructor)Agda.Interaction.Imports
makeAbstractAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
makeAbstractClauseAgda.Interaction.MakeCase
makeAbsurdClauseAgda.Interaction.MakeCase
makeAllAgda.Utils.IndexedList
makeCaseAgda.Interaction.MakeCase
MakeCaseVariantAgda.Interaction.Response
makeClosedAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend
makeEnvAgda.Syntax.Translation.AbstractToConcrete
makeGlobalAgda.TypeChecking.Monad.Local, Agda.TypeChecking.Monad, Agda.Compiler.Backend
makeInstanceAgda.Syntax.Common
makeInstance'Agda.Syntax.Common
makeLocalAgda.TypeChecking.Monad.Local, Agda.TypeChecking.Monad, Agda.Compiler.Backend
makeOpenAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend
makePatternVarsVisibleAgda.Interaction.MakeCase
makeProjectionAgda.TypeChecking.ProjectionLike
makeSubstitutionAgda.TypeChecking.Rewriting.NonLinMatch
malformedAgda.TypeChecking.Serialise.Base
manyAgda.Utils.Parser.ReadP
many1Agda.Utils.Parser.ReadP
manyTillAgda.Utils.Parser.ReadP
MapAgda.Utils.TypeLevel
map 
1 (Function)Agda.Utils.HashMap
2 (Function)Agda.Utils.Bag
3 (Function)Agda.Compiler.JS.Substitution
map'Agda.Compiler.JS.Substitution
mapAbsNamesAgda.Syntax.Internal
mapAbsNamesMAgda.Syntax.Internal
mapAbsoluteIncludePathsAgda.Interaction.Options.Lenses
mapArgInfoAgda.Syntax.Common
mapAwakeConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapBenchmarkOnAgda.Utils.Benchmark
mapBlockingVarConsAgda.TypeChecking.Coverage.Match
mapClosureAgda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapCommandLineOptionsAgda.Interaction.Options.Lenses
mapConNameAgda.Syntax.Internal
mapContextAgda.Compiler.MAlonzo.Compiler
mapCurrentAccountAgda.Utils.Benchmark
mapEither 
1 (Function)Agda.Utils.Either
2 (Function)Agda.Utils.List
mapExceptTAgda.Utils.Except
mapExpr 
1 (Function)Agda.Syntax.Concrete.Generic
2 (Function)Agda.Syntax.Abstract.Views
mapFlagAgda.Interaction.Options
mapFstAgda.Utils.Tuple
mapFstMAgda.Utils.Tuple
mapHidingAgda.Syntax.Common
mapImportDirAgda.Syntax.Scope.Monad
mapIncludePathsAgda.Interaction.Options.Lenses
mapKeysMonotonicAgda.Utils.AssocList
mapLeftAgda.Utils.Either
mapLHSHeadAgda.Syntax.Abstract
mapLhsOriginalPatternAgda.Syntax.Concrete
mapM'Agda.Utils.Monad
mapMaybe 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.HashMap
3 (Function)Agda.Utils.Maybe.Strict
mapMaybeAndRestAgda.Utils.List
mapMaybeMAgda.Utils.Monad
mapMaybeWithKeyAgda.Utils.HashMap
mapMListTAgda.Utils.ListT
mapMListT_altAgda.Utils.ListT
MapNamedArgAgda.Syntax.Internal.Pattern
mapNamedArgAgda.Syntax.Internal.Pattern
MapNamedArgPatternAgda.Syntax.Abstract.Pattern
mapNamedArgPatternAgda.Syntax.Abstract.Pattern
mapNameSpaceAgda.Syntax.Scope.Base
mapNameSpaceMAgda.Syntax.Scope.Base
mapNameSupplyAgda.Compiler.MAlonzo.Compiler
mapOriginAgda.Syntax.Common
mapPairMAgda.Utils.Tuple
mapPersistentVerbosityAgda.Interaction.Options.Lenses
mappingAgda.Interaction.Highlighting.Precise
mapPragmaOptionsAgda.Interaction.Options.Lenses
mapRedEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapRedEnvStAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapRedStAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapRelevanceAgda.Syntax.Common
mapRenamingAgda.Syntax.Scope.Monad
mapRightAgda.Utils.Either
MapSAgda.Auto.Convert
mapSafeModeAgda.Interaction.Options.Lenses
mapScopeAgda.Syntax.Scope.Base
mapScope'Agda.Syntax.Scope.Base
mapScopeInfoAgda.Syntax.Scope.Base
mapScopeMAgda.Syntax.Scope.Base
mapScopeM_Agda.Syntax.Scope.Base
mapScope_Agda.Syntax.Scope.Base
mapSleepingConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapSndAgda.Utils.Tuple
mapSndMAgda.Utils.Tuple
mapSubTriesAgda.Utils.Trie
mapTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapTimingsAgda.Utils.Benchmark
mapUsingAgda.Syntax.Scope.Monad
mapVerbosityAgda.Interaction.Options.Lenses
mapWithEdgeAgda.Utils.Graph.AdjacencyMap.Unidirectional
mapWithIndexAgda.Utils.IndexedList
mapWithKey 
1 (Function)Agda.Utils.HashMap
2 (Function)Agda.Utils.AssocList
mapWithKeyMAgda.Utils.AssocList
MArgListAgda.Auto.Syntax
markInjectiveAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
markInlineAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
markStaticAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MarkupAgda.Syntax.Parser.Literate
Masked 
1 (Type/Class)Agda.Termination.Monad
2 (Data Constructor)Agda.Termination.Monad
maskedAgda.Termination.Monad
MaskedDeBruijnPatternsAgda.Termination.Monad
MatAgda.Termination.Order
matAgda.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
matchClauseAgda.TypeChecking.Coverage.Match
matchCommandAgda.Interaction.CommandLine
matchCompiledAgda.TypeChecking.CompiledClause.Match
matchCompiledEAgda.TypeChecking.CompiledClause.Match
matchCopatternAgda.TypeChecking.Patterns.Match
matchCopatternsAgda.TypeChecking.Patterns.Match
matchDisplayFormAgda.TypeChecking.DisplayForm
MatchedAgda.TypeChecking.Positivity.Occurrence
matchedArgsAgda.TypeChecking.Patterns.Match
matchesAgda.Interaction.Highlighting.Vim
matchingBlockedAgda.TypeChecking.Rewriting.NonLinMatch
MatchLitAgda.TypeChecking.Coverage.Match
matchLitsAgda.TypeChecking.Coverage.Match
matchPatAgda.TypeChecking.Coverage.Match
matchPatsAgda.TypeChecking.Coverage.Match
matchPatternAgda.TypeChecking.Patterns.Match
matchPatternsAgda.TypeChecking.Patterns.Match
MatchResultAgda.TypeChecking.Coverage.Match
matchTypeAgda.Auto.Convert
Matrix 
1 (Type/Class)Agda.Termination.SparseMatrix
2 (Data Constructor)Agda.Termination.SparseMatrix
3 (Type/Class)Agda.Utils.Warshall
matrixAgda.Utils.Warshall
MaxAgda.Syntax.Internal
maxInstanceSearchDepthAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
maxNameAgda.TypeChecking.Level
MaxNat 
1 (Type/Class)Agda.Utils.Monoid
2 (Data Constructor)Agda.Utils.Monoid
maxVarOccAgda.TypeChecking.Free.Lazy
maxViewConsAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
maxViewMaxAgda.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
3 (Data Constructor)Agda.TypeChecking.InstanceArguments
maybe 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
MaybeAbortAgda.TypeChecking.Injectivity
maybeAbortAgda.Interaction.InteractionTop
maybeFastReduceTermAgda.TypeChecking.Reduce
maybeFlexiblePatternAgda.TypeChecking.Rules.LHS
maybeLeftAgda.Utils.Either
maybeM 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
maybeorAgda.Auto.Typecheck
MaybePlaceholderAgda.Syntax.Common
maybePlaceholderAgda.Syntax.Concrete.Operators.Parser
MaybePostfixProjPAgda.Syntax.Abstract
maybePostfixProjPAgda.Syntax.Abstract
maybePrimConAgda.TypeChecking.Level
maybePrimDefAgda.TypeChecking.Level
maybeProjTurnPostfixAgda.Syntax.Abstract.Views
MaybeRedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MaybeReducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MaybeReducedArgsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MaybeReducedElimsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
maybeRightAgda.Utils.Either
maybeTimedAgda.Interaction.InteractionTop
maybeToEitherAgda.Utils.Either
maybeToList 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
MaybeWarningsAgda.Interaction.Imports
MaybeWarnings'Agda.Interaction.Imports
mazCoerceAgda.Compiler.MAlonzo.Misc
mazCoerceNameAgda.Compiler.MAlonzo.Misc
mazErasedNameAgda.Compiler.MAlonzo.Misc
mazerrorAgda.Compiler.MAlonzo.Misc
mazIncompleteMatchAgda.Compiler.MAlonzo.Misc
mazModAgda.Compiler.MAlonzo.Misc
mazMod'Agda.Compiler.MAlonzo.Misc
mazNameAgda.Compiler.MAlonzo.Misc
mazRTEAgda.Compiler.MAlonzo.Misc
mazstrAgda.Compiler.MAlonzo.Misc
mazUnreachableErrorAgda.Compiler.MAlonzo.Misc
MBAgda.Auto.NarrowingSearch
mbcaseAgda.Auto.NarrowingSearch
mbfailedAgda.Auto.NarrowingSearch
mbindAgda.Auto.NarrowingSearch
mbpcaseAgda.Auto.NarrowingSearch
mbretAgda.Auto.NarrowingSearch
MCaseSplitAgda.Auto.Options
mcompointAgda.Auto.NarrowingSearch
mconsAgda.Utils.List
MeasureAgda.Syntax.Concrete.Definitions
measureTimeAgda.Utils.Time
meetAgda.TypeChecking.SizedTypes.Utils
MeetSemiLatticeAgda.TypeChecking.SizedTypes.Utils
member 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.HashMap
3 (Function)Agda.Utils.Bag
4 (Function)Agda.Utils.Trie
MemberId 
1 (Type/Class)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
MemoAgda.TypeChecking.Serialise.Base
memoAgda.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
MemoKeyAgda.Syntax.Concrete.Operators.Parser.Monad
memoModulesAgda.Syntax.Scope.Monad
memoNamesAgda.Syntax.Scope.Monad
memoRecAgda.Utils.Memo
memoToScopeInfoAgda.Syntax.Scope.Monad
memoUnsafeAgda.Utils.Memo
memoUnsafeHAgda.Utils.Memo
mentionsAgda.TypeChecking.SizedTypes.WarshallSolver
MentionsMetaAgda.TypeChecking.MetaVars.Mention
mentionsMetaAgda.TypeChecking.MetaVars.Mention
mergeAgda.Interaction.Highlighting.Precise
mergeCAgda.Interaction.Highlighting.Precise
mergeHidingAgda.Syntax.Common
mergeInterfaceAgda.Interaction.Imports
mergeNamesAgda.Syntax.Scope.Base
mergeNotationsAgda.Syntax.Fixity
mergeScopeAgda.Syntax.Scope.Base
mergeScopesAgda.Syntax.Scope.Base
Meta 
1 (Data Constructor)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Syntax.Reflected
MetaArgAgda.TypeChecking.Positivity.Occurrence
MetaCannotDependOnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaEnvAgda.Auto.NarrowingSearch
metaHelperTypeAgda.Interaction.BasicOps
MetaId 
1 (Type/Class)Agda.Syntax.Common, Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Common, Agda.Syntax.Internal
metaIdAgda.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
MetaInstantiationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaKindAgda.TypeChecking.MetaVars
MetaLevelAgda.Syntax.Internal
MetaliseOKHAgda.Auto.Syntax
metaliseOKHAgda.Auto.Syntax
metaliseokhAgda.Auto.Syntax
MetaNameSuggestionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
metaNameSuggestionAgda.Syntax.Info
metaNumberAgda.Syntax.Info
metaOccursAgda.TypeChecking.MetaVars.Occurs
MetaOccursInItselfAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
metaParseExprAgda.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
metaRangeAgda.Syntax.Info
metaScopeAgda.Syntax.Info
metasCreatedByAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaSetAgda.TypeChecking.Free.Lazy
MetaStoreAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaVAgda.Syntax.Internal
MetaVarAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Metavar 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
MetaVariableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
meta_not_constructorAgda.Auto.Typecheck
MExpAgda.Auto.Syntax
mextrarefsAgda.Auto.NarrowingSearch
miClosRangeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MIdAgda.Auto.Syntax
MiddleAgda.Syntax.Common
miInterfaceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
miMetaOccursCheckAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mimicGHCiAgda.Interaction.EmacsTop
miNameSuggestionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
minfoAsNameAgda.Syntax.Info
minfoAsToAgda.Syntax.Info
minfoDirectiveAgda.Syntax.Info
minfoOpenShortAgda.Syntax.Info
minfoRangeAgda.Syntax.Info
minusAgda.Interaction.Highlighting.Range
MissingClausesAgda.Syntax.Internal
MissingDataSignatureAgda.Syntax.Concrete.Definitions
MissingDefinitionAgda.Syntax.Concrete.Definitions
MissingTypeSignatureAgda.Syntax.Concrete.Definitions
MissingWithClausesAgda.Syntax.Concrete.Definitions
miWarningsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MIx 
1 (Type/Class)Agda.Termination.SparseMatrix
2 (Data Constructor)Agda.Termination.SparseMatrix
MixedAgda.TypeChecking.Positivity.Occurrence
mkAbsAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
mkAbsoluteAgda.Utils.FileName
mkBoundNameAgda.Syntax.Concrete
mkBoundName_Agda.Syntax.Concrete
mkCallAgda.Termination.CallGraph
mkCall'Agda.Termination.CallGraph
mkContextEntryAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mkDefAgda.Syntax.Translation.ReflectedToAbstract
mkDefInfoAgda.Syntax.Info
mkDefInfoInstanceAgda.Syntax.Info
mkExceptTAgda.Utils.Except
mkLamAgda.TypeChecking.Substitute
mkLet 
1 (Function)Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Function)Agda.Syntax.Abstract
mkMatrixAgda.Utils.Warshall
MkNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mkNameAgda.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
mkNotationAgda.Syntax.Notation
mkPiAgda.TypeChecking.Substitute
mkPragmaAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mkPrimFun1Agda.TypeChecking.Primitive
mkPrimFun1TCMAgda.TypeChecking.Primitive
mkPrimFun2Agda.TypeChecking.Primitive
mkPrimFun4Agda.TypeChecking.Primitive
mkPrimLevelMaxAgda.TypeChecking.Primitive
mkPrimLevelSucAgda.TypeChecking.Primitive
mkPrimLevelZeroAgda.TypeChecking.Primitive
mkSetAgda.Syntax.Translation.ReflectedToAbstract
mkSharedAgda.TypeChecking.Serialise.Base
mkTAppAgda.Syntax.Treeless, Agda.Compiler.Backend
mkTLamAgda.Syntax.Treeless, Agda.Compiler.Backend
mkTypeAgda.Syntax.Internal
mkWeakIORefAgda.Utils.IORef
MMAgda.Auto.NarrowingSearch
mmbpcaseAgda.Auto.NarrowingSearch
mmcaseAgda.Auto.NarrowingSearch
mmmcaseAgda.Auto.NarrowingSearch
mmpcaseAgda.Auto.NarrowingSearch
MNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mnameFromListAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mnameToConcreteAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mnameToListAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mnameToQNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
MNormalAgda.Auto.Options
mobsAgda.Auto.NarrowingSearch
Mode 
1 (Type/Class)Agda.Utils.Pretty
2 (Type/Class)Agda.Auto.Options
3 (Type/Class)Agda.Interaction.Imports
modeAgda.Utils.Pretty
modFileAgda.TypeChecking.Serialise.Base
modifyAbsoluteIncludePathsAgda.Interaction.Options.Lenses
modifyAbstractClauseAgda.Auto.Convert
modifyAbstractExprAgda.Auto.Convert
modifyAllowedReductionsAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyArgOccurrencesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyAwakeConstraintsAgda.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
modifyCommandLineOptionsAgda.Interaction.Options.Lenses
modifyContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyContextEntriesAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyContextEntryAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyCurrentNameSpaceAgda.Syntax.Scope.Monad
modifyCurrentScopeAgda.Syntax.Scope.Monad
modifyCurrentScopeMAgda.Syntax.Scope.Monad
modifyFunClausesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyGlobalDefinitionAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyImportedSignatureAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyIncludePathsAgda.Interaction.Options.Lenses
modifyInstanceDefsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyInteractionPointsAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyIORefAgda.Utils.IORef
modifyIORef'Agda.Utils.IORef
modifyLocalVarsAgda.Syntax.Scope.Monad
modifyMetaStoreAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyNamedScopeAgda.Syntax.Scope.Monad
modifyNamedScopeMAgda.Syntax.Scope.Monad
modifyNameSpaceAgda.Syntax.Scope.Base
modifyOccursCheckDefsAgda.TypeChecking.MetaVars.Occurs
modifyOldInteractionScopesAgda.Interaction.InteractionTop
modifyPatternSynsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyPersistentStateAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyPersistentVerbosityAgda.Interaction.Options.Lenses
modifyPragmaOptionsAgda.Interaction.Options.Lenses
modifySafeModeAgda.Interaction.Options.Lenses
modifyScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyScopesAgda.Syntax.Scope.Monad
modifyScope_Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifySignatureAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifySleepingConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyStatisticsAgda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTheInteractionPointsAgda.Interaction.InteractionTop
modifyVerbosityAgda.Interaction.Options.Lenses
modNameAgda.Compiler.JS.Syntax
modnameAgda.Compiler.JS.Pretty
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
ModuleArityMismatchAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleAssignment 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
ModuleContentsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
moduleContentsAgda.Interaction.BasicOps
ModuleDefinedInOtherFileAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleDoesntExportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
moduleHashAgda.Interaction.Imports
ModuleIdAgda.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
ModuleMacroAgda.Syntax.Concrete
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
moduleNameAgda.Interaction.FindFile
moduleName'Agda.Interaction.FindFile
ModuleNameDoesntMatchFileNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
moduleNameParser 
1 (Function)Agda.Syntax.Parser.Parser
2 (Function)Agda.Syntax.Parser
moduleNamePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
moduleNameRangeAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
moduleNameToFileNameAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
ModuleNameUnexpectedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleParamDictAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleParametersAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleParamsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
moduleParamsToApplyAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
moduleParser 
1 (Function)Agda.Syntax.Parser.Parser
2 (Function)Agda.Syntax.Parser
ModulePragmaAgda.Utils.Haskell.Syntax
ModulesInScopeAgda.Syntax.Scope.Base
ModuleTagAgda.Syntax.Scope.Base
ModuleToSourceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadBenchAgda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
MonadChangeAgda.Utils.Update
MonadDebugAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadErrorAgda.Utils.Except
MonadGetDefsAgda.Syntax.Internal.Defs
MonadPlusAgda.Utils.Monad
MonadTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTerAgda.Termination.Monad
moreRelevantAgda.Syntax.Common
MOTAgda.Auto.Convert
Move 
1 (Data Constructor)Agda.Auto.NarrowingSearch
2 (Type/Class)Agda.Auto.SearchControl
Move'Agda.Auto.NarrowingSearch
moveCostAgda.Auto.NarrowingSearch
moveNextAgda.Auto.NarrowingSearch
movePosAgda.Syntax.Position
movePosByStringAgda.Syntax.Position
mparensAgda.Utils.Pretty
mplusAgda.Utils.Monad
mpretAgda.Auto.NarrowingSearch
mprincipalpresentAgda.Auto.NarrowingSearch
mpSubstitutionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MRefineAgda.Auto.Options
mul 
1 (Function)Agda.Termination.Semiring
2 (Function)Agda.Termination.SparseMatrix
multiLineText 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
MultipleFixityDeclsAgda.Syntax.Concrete.Definitions
MultiplePolarityPragmasAgda.Syntax.Concrete.Definitions
munchAgda.Utils.Parser.ReadP
munch1Agda.Utils.Parser.ReadP
mustBeFiniteAgda.TypeChecking.SizedTypes.WarshallSolver
mustBePiAgda.TypeChecking.Telescope
MutIdAgda.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
mutualBlockOfAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mutualChecksAgda.TypeChecking.Rules.Decl
MutualIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MutualInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
mutualInfoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mutuallyRecursiveAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MutualNamesAgda.Termination.Monad
mutualNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mutualPositivityCheckAgda.Syntax.Info
mutualRangeAgda.Syntax.Info
mutualTermCheckAgda.Syntax.Info
mvFrozenAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvInfoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvInstantiationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvJudgementAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvListenersAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvPermutationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvPriorityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MyMBAgda.Auto.Syntax
MyPBAgda.Auto.Syntax
mzeroAgda.Utils.Monad