Agda-2.6.1.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
makeConHeadAgda.TypeChecking.Datatypes
makeInstanceAgda.Syntax.Common
makeInstance'Agda.Syntax.Common
makeOpenAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend
makePatternVarsVisibleAgda.Interaction.MakeCase
makePiAgda.Syntax.Concrete
makeProjectionAgda.TypeChecking.ProjectionLike
makeSubstitutionAgda.TypeChecking.Rewriting.NonLinMatch
malformedAgda.TypeChecking.Serialise.Base
ManyHolesAgda.Utils.AffineHole
MapAgda.Utils.TypeLevel
map 
1 (Function)Agda.Utils.Bag
2 (Function)Agda.Compiler.JS.Substitution
map'Agda.Compiler.JS.Substitution
mapAbsNamesAgda.Syntax.Internal
mapAbsNamesMAgda.Syntax.Internal
mapAbsoluteIncludePathsAgda.Interaction.Options.Lenses
mapAbstractionAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapAPatternAgda.Syntax.Abstract.Pattern
mapArgInfoAgda.Syntax.Common
mapAwakeConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapBenchmarkOnAgda.Utils.Benchmark
mapChangeTAgda.Utils.Update
mapClosureAgda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapCohesionAgda.Syntax.Common
mapCohesionModAgda.Syntax.Common
mapCommandLineOptionsAgda.Interaction.Options.Lenses
mapConNameAgda.Syntax.Internal
mapCPatternAgda.Syntax.Concrete.Pattern
mapCurrentAccountAgda.Utils.Benchmark
mapEither3MAgda.Utils.Three
mapExceptTAgda.Utils.Except
mapExpr 
1 (Function)Agda.Syntax.Concrete.Generic
2 (Function)Agda.Syntax.Abstract.Views
mapFlagAgda.Interaction.Options
mapFlexRigMapAgda.TypeChecking.Free.Lazy
mapFreeVariablesAgda.Syntax.Common
mapFreeVariablesArgInfoAgda.Syntax.Common
mapFstAgda.Utils.Tuple
mapFstMAgda.Utils.Tuple
mapHidingAgda.Syntax.Common
mapHidingArgInfoAgda.Syntax.Common
mapImportDirAgda.Syntax.Scope.Monad
mapIncludePathsAgda.Interaction.Options.Lenses
mapInScopeAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
mapKeysMonotonicAgda.Utils.AssocList
mapLeftAgda.Utils.Either
mapLHSHeadAgda.Syntax.Abstract.Pattern
mapLhsOriginalPatternAgda.Syntax.Concrete.Pattern
mapLhsOriginalPatternMAgda.Syntax.Concrete.Pattern
mapListTAgda.Utils.ListT
mapM'Agda.Utils.Monad
mapMaybe 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
mapMaybeAndRestAgda.Utils.List
mapMaybeKeysAgda.Utils.Map
mapMaybeMAgda.Utils.Monad
mapMaybeMMAgda.Utils.Monad
mapMemberShipAgda.Utils.SmallSet
mapMListTAgda.Utils.ListT
mapMListT_altAgda.Utils.ListT
mapMMAgda.Utils.Monad
mapMM_Agda.Utils.Monad
mapModalityAgda.Syntax.Common
mapModalityArgInfoAgda.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
mapNameOfAgda.Syntax.Common
mapNameSpaceAgda.Syntax.Scope.Base
mapNameSpaceMAgda.Syntax.Scope.Base
mapOriginAgda.Syntax.Common
mapOriginArgInfoAgda.Syntax.Common
mapPairMAgda.Utils.Tuple
mapPersistentVerbosityAgda.Interaction.Options.Lenses
mappingAgda.Interaction.Highlighting.Precise
mapPragmaOptionsAgda.Interaction.Options.Lenses
mapQuantityAgda.Syntax.Common
mapQuantityModAgda.Syntax.Common
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
mapRelevanceModAgda.Syntax.Common
mapRenamingAgda.Syntax.Scope.Monad
mapRightAgda.Utils.Either
MapSAgda.Auto.Convert
mapSafeModeAgda.Interaction.Options.Lenses
mapScopeAgda.Syntax.Scope.Base
mapScopeMAgda.Syntax.Scope.Base
mapScopeM_Agda.Syntax.Scope.Base
mapScopeNSAgda.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.Common
mapVarMapAgda.TypeChecking.Free.Lazy
mapVerbosityAgda.Interaction.Options.Lenses
mapVisitedModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapWithEdgeAgda.Utils.Graph.AdjacencyMap.Unidirectional
mapWithIndexAgda.Utils.IndexedList
mapWithKeyAgda.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
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
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.Coverage.Match
6 (Type/Class)Agda.TypeChecking.Rewriting.NonLinMatch
match 
1 (Function)Agda.Syntax.Parser.LookAhead
2 (Function)Agda.TypeChecking.DisplayForm
3 (Function)Agda.TypeChecking.Coverage.Match
4 (Function)Agda.TypeChecking.Rewriting.NonLinMatch
5 (Function)Agda.Interaction.Highlighting.Vim
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
matchPatternAgda.TypeChecking.Patterns.Match
matchPatternPAgda.TypeChecking.Patterns.Match
matchPatternsAgda.TypeChecking.Patterns.Match
matchPatternsPAgda.TypeChecking.Patterns.Match
matchPatternSynAgda.Syntax.Abstract.PatternSynonyms
matchPatternSynPAgda.Syntax.Abstract.PatternSynonyms
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
maxInversionDepthAgda.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
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
maybe 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
maybeAbortAgda.Interaction.InteractionTop
maybeFastReduceTermAgda.TypeChecking.Reduce
maybeFlexiblePatternAgda.TypeChecking.Rules.LHS
MaybeFreeAgda.TypeChecking.Free.Reduce
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
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
mayEraseTypeAgda.Compiler.Backend
mazAnyTypeAgda.Compiler.MAlonzo.Misc
mazAnyTypeNameAgda.Compiler.MAlonzo.Misc
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
MdFileTypeAgda.Syntax.Common
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.Bag
3 (Function)Agda.Utils.IntSet.Infinite
4 (Function)Agda.Utils.SmallSet
5 (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
mentionsMetasAgda.TypeChecking.MetaVars.Mention
mergeAgda.Interaction.Highlighting.Precise
mergeCAgda.Interaction.Highlighting.Precise
mergeEdgesAgda.TypeChecking.Positivity
mergeElimAgda.TypeChecking.Patterns.Match
mergeElimsAgda.TypeChecking.Patterns.Match
mergeHidingAgda.Syntax.Common
mergeInterfaceAgda.Interaction.Imports
mergeNamesAgda.Syntax.Scope.Base
mergeNamesManyAgda.Syntax.Scope.Base
mergeNotationsAgda.Syntax.Notation
mergePatternSynDefsAgda.Syntax.Abstract.PatternSynonyms
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
MetaErasedSolutionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
metaFrozenAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
MetaIrrelevantSolutionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaKindAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
metaOccursQNameAgda.TypeChecking.MetaVars.Occurs
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
MetaSAgda.Syntax.Internal
metaScopeAgda.Syntax.Info
metasCreatedByAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaSet 
1 (Type/Class)Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
2 (Data Constructor)Agda.TypeChecking.Free.Lazy
MetaStoreAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
metaTypeAgda.TypeChecking.Monad.MetaVars, 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
miGeneralizableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
miPrimitiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MissingClausesAgda.Syntax.Internal
MissingDefinitionAgda.Interaction.Highlighting.Precise
MissingDefinitionsAgda.Syntax.Concrete.Definitions
MissingDefinitions_Agda.Interaction.Options.Warnings
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
mkBinder 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
mkBinder_ 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
mkBindNameAgda.Syntax.Abstract
mkBoundNameAgda.Syntax.Concrete
mkBoundName_Agda.Syntax.Concrete
mkCallAgda.Termination.CallGraph
mkCall'Agda.Termination.CallGraph
mkConAgda.TypeChecking.Records
mkDefAgda.Syntax.Translation.ReflectedToAbstract
mkDefInfoAgda.Syntax.Info
mkDefInfoInstanceAgda.Syntax.Info
mkDomainFreeAgda.Syntax.Abstract
mkExceptTAgda.Utils.Except
mkGCompAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
mkIfAgda.Compiler.MAlonzo.Compiler
mkInterfaceFileAgda.Interaction.FindFile
mkIsSizeConstraintAgda.TypeChecking.SizedTypes
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
mkPrimInjectiveAgda.TypeChecking.Primitive
mkPrimLevelMaxAgda.TypeChecking.Primitive
mkPrimLevelSucAgda.TypeChecking.Primitive
mkPrimLevelZeroAgda.TypeChecking.Primitive
mkPrimSetOmegaAgda.TypeChecking.Primitive
mkPropAgda.Syntax.Internal
mkSetAgda.Syntax.Translation.ReflectedToAbstract
mkTAppAgda.Syntax.Treeless, Agda.Compiler.Backend
mkTBindAgda.Syntax.Abstract
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
Modality 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
modalityOfConstAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modCohesionAgda.Syntax.Common
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
modifyConcreteNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyContextInfoAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyCounterAgda.TypeChecking.Monad.Statistics, 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
modifySystemAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTCAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTC'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTCLensAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTCLensMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTheInteractionPointsAgda.Interaction.InteractionTop
modifyVerbosityAgda.Interaction.Options.Lenses
modNameAgda.Compiler.JS.Syntax
modnameAgda.Compiler.JS.Pretty
modQuantityAgda.Syntax.Common
modRelevanceAgda.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
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
ModuleDoesntExport_Agda.Interaction.Options.Warnings
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
ModuleMapAgda.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
moduleNameAgda.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
ModuleNotNameAgda.Syntax.Scope.Base
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
MonadAbsToConAgda.Syntax.Translation.AbstractToConcrete
MonadAddContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadBenchAgda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
MonadChangeAgda.Utils.Update
MonadCheckInternalAgda.TypeChecking.CheckInternal
MonadConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadConversionAgda.TypeChecking.Conversion
MonadDebugAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadDisplayFormAgda.TypeChecking.DisplayForm
MonadErrorAgda.Utils.Except
MonadFixityErrorAgda.Syntax.Concrete.Fixity
MonadFreshAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadGetDefsAgda.Syntax.Internal.Defs
MonadInteractionPointsAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadMetaSolverAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadPlusAgda.Utils.Monad
MonadPrettyAgda.TypeChecking.Pretty
MonadReduceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadReflectedToAbstractAgda.Syntax.Translation.ReflectedToAbstract
MonadReifyAgda.Syntax.Translation.InternalToAbstract
MonadStatisticsAgda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadStConcreteNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTCEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTCStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTerAgda.Termination.Monad
MonadWarningAgda.TypeChecking.Warnings
moreCohesionAgda.Syntax.Common
moreQuantityAgda.Syntax.Common
moreRelevantAgda.Syntax.Common
moreUsableModalityAgda.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
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
MultipleEllipsesAgda.Syntax.Concrete.Definitions
MultipleFixityDeclsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MultiplePolarityPragmasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
mutualCoverageCheckAgda.Syntax.Info
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
mutualTerminationCheckAgda.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
mvTwinAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MyMBAgda.Auto.Syntax
MyPBAgda.Auto.Syntax
mzeroAgda.Utils.Monad