Agda-2.6.2.2.20221106: 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
MainFunctionDef 
1 (Type/Class)Agda.Compiler.MAlonzo.Primitives
2 (Data Constructor)Agda.Compiler.MAlonzo.Primitives
mainFunctionDefsAgda.Compiler.MAlonzo.Primitives
MainModeAgda.Main
MainModePrintAgdaDirAgda.Main
MainModePrintHelpAgda.Main
MainModePrintVersionAgda.Main
MainModeRunAgda.Main
makeAbstractAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
makeAbstractClauseAgda.Interaction.MakeCase
makeAbsurdClauseAgda.Interaction.MakeCase
makeAllAgda.Utils.IndexedList
makeCaseAgda.Interaction.MakeCase
MakeCaseVariantAgda.Interaction.Response
makeInstanceAgda.Syntax.Common
makeInstance'Agda.Syntax.Common
makeNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
makeOpenAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Open
makePatternVarsVisibleAgda.Interaction.MakeCase
makePiAgda.Syntax.Concrete
makeProjectionAgda.TypeChecking.ProjectionLike
makeRHSEmptyRecordAgda.Interaction.MakeCase
MakeStrictAgda.Compiler.MAlonzo.Strict
makeStrictAgda.Compiler.MAlonzo.Strict
makeSubstitutionAgda.TypeChecking.Rewriting.NonLinMatch
malformedAgda.TypeChecking.Serialise.Base
ManyHolesAgda.Utils.AffineHole
MapAgda.Utils.TypeLevel
map 
1 (Function)Agda.Utils.List1
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
mapAbstractionAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
mapAnnotationAgda.Syntax.Common
mapAPatternAgda.Syntax.Abstract.Pattern
mapArgInfoAgda.Syntax.Common
mapAwakeConstraintsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
mapBenchmarkOnAgda.Utils.Benchmark
mapChangeTAgda.Utils.Update
mapClosureAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Closure
mapCohesionAgda.Syntax.Common
mapCohesionModAgda.Syntax.Common
mapCommandLineOptionsAgda.Interaction.Options.Lenses
mapConNameAgda.Syntax.Internal
mapCPatternAgda.Syntax.Concrete.Pattern
mapCurrentAccountAgda.Utils.Benchmark
mapEither3MAgda.Utils.Three
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, Agda.Syntax.Concrete.Name
mapKeysMonotonicAgda.Utils.AssocList
mapLeftAgda.Utils.Either
mapLHSCoresAgda.TypeChecking.Rules.Def
mapLHSHeadAgda.Syntax.Abstract.Pattern
mapLhsOriginalPatternAgda.Syntax.Concrete.Pattern
mapLhsOriginalPatternMAgda.Syntax.Concrete.Pattern
mapListTAgda.Utils.ListT
mapLockAgda.Syntax.Common
mapM'Agda.Utils.Monad
mapMaybe 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
3 (Function)Agda.Utils.List1
mapMaybeAndRestAgda.Utils.List
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
mapPragmaOptionsAgda.Interaction.Options.Lenses
mapQuantityAgda.Syntax.Common
mapQuantityModAgda.Syntax.Common
mapRedEnvAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mapRedEnvStAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mapRedStAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
mapSndAgda.Utils.Tuple
mapSndMAgda.Utils.Tuple
mapSubTriesAgda.Utils.Trie
mapTCMTAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mapTimingsAgda.Utils.Benchmark
mapUsingAgda.Syntax.Common
mapVarMapAgda.TypeChecking.Free.Lazy
mapVerbosityAgda.Interaction.Options.Lenses
mapWithEdgeAgda.Utils.Graph.AdjacencyMap.Unidirectional
mapWithIndexAgda.Utils.IndexedList
mapWithKey 
1 (Function)Agda.Utils.BiMap
2 (Function)Agda.Utils.AssocList
mapWithKeyFixedTagsAgda.Utils.BiMap
mapWithKeyFixedTagsPreconditionAgda.Utils.BiMap
mapWithKeyMAgda.Utils.AssocList
mapWithKeyPreconditionAgda.Utils.BiMap
MArgListAgda.Auto.Syntax
markInjectiveAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
markInlineAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
markStaticAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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.Coverage.Match
5 (Type/Class)Agda.TypeChecking.Rewriting.NonLinMatch
match 
1 (Function)Agda.Syntax.Parser.LookAhead
2 (Function)Agda.TypeChecking.Coverage.Match
3 (Function)Agda.TypeChecking.Rewriting.NonLinMatch
4 (Function)Agda.Interaction.Highlighting.Vim
match' 
1 (Function)Agda.Syntax.Parser.LookAhead
2 (Function)Agda.TypeChecking.CompiledClause.Match
matchClauseAgda.TypeChecking.Coverage.Match
matchCompiledAgda.TypeChecking.CompiledClause.Match
matchCompiledEAgda.TypeChecking.CompiledClause.Match
matchCopatternAgda.TypeChecking.Patterns.Match
matchCopatternsAgda.TypeChecking.Patterns.Match
MatchedAgda.TypeChecking.Positivity.Occurrence
matchedArgsAgda.TypeChecking.Patterns.Match
matchedArgs'Agda.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.Compiler.Backend, Agda.TypeChecking.Monad
maxInversionDepthAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
maxNameAgda.TypeChecking.Level
MaxNat 
1 (Type/Class)Agda.Utils.Monoid
2 (Data Constructor)Agda.Utils.Monoid
maxViewConsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
maxViewMaxAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
maxViewSuc_Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
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
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
MaybeProjectionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
maybeProjTurnPostfixAgda.Syntax.Abstract.Views
MaybeRedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MaybeReducedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MaybeReducedArgsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MaybeReducedElimsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
maybeRightAgda.Utils.Either
maybeTimedAgda.Interaction.InteractionTop
maybeToEitherAgda.Utils.Either
maybeToList 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
mayEraseTypeAgda.Compiler.Backend
mazAccumlatedImportsAgda.Compiler.MAlonzo.Misc
mazAnyTypeAgda.Compiler.MAlonzo.Misc
mazAnyTypeNameAgda.Compiler.MAlonzo.Misc
mazCoerceAgda.Compiler.MAlonzo.Misc
mazCoerceNameAgda.Compiler.MAlonzo.Misc
mazErasedNameAgda.Compiler.MAlonzo.Misc
mazHoleAgda.Compiler.MAlonzo.Misc
mazIsMainModuleAgda.Compiler.MAlonzo.Misc
mazModAgda.Compiler.MAlonzo.Misc
mazMod'Agda.Compiler.MAlonzo.Misc
mazModuleNameAgda.Compiler.MAlonzo.Misc
mazNameAgda.Compiler.MAlonzo.Misc
mazRTEAgda.Compiler.MAlonzo.Misc
mazRTEFloatAgda.Compiler.MAlonzo.Misc
mazRTEFloatImportAgda.Compiler.MAlonzo.Compiler
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.Types, Agda.Syntax.Concrete.Definitions
measureTimeAgda.Utils.Time
meetAgda.TypeChecking.SizedTypes.Utils
MeetSemiLatticeAgda.TypeChecking.SizedTypes.Utils
member 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.BoolSet
3 (Function)Agda.Utils.Bag
4 (Function)Agda.Utils.IntSet.Infinite
5 (Function)Agda.Utils.SmallSet
6 (Function)Agda.Utils.Trie
MemberId 
1 (Type/Class)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
MemberIndexAgda.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
mergeEdgesAgda.TypeChecking.Positivity
mergeElimAgda.TypeChecking.Patterns.Match
mergeElimsAgda.TypeChecking.Patterns.Match
mergeHidingAgda.Syntax.Common
mergeNamesAgda.Syntax.Scope.Base
mergeNamesManyAgda.Syntax.Scope.Base
mergeNotationsAgda.Syntax.Notation
mergePatternSynDefsAgda.Syntax.Abstract.PatternSynonyms
mergeScopeAgda.Syntax.Scope.Base
mergeScopesAgda.Syntax.Scope.Base
mergeStrictlyOrderedByAgda.Utils.List
Meta 
1 (Data Constructor)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Syntax.Reflected
MetaArgAgda.TypeChecking.Positivity.Occurrence
MetaCannotDependOnAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
metaCheckAgda.TypeChecking.MetaVars.Occurs
MetaEnvAgda.Auto.NarrowingSearch
MetaErasedSolutionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
metaFrozenAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
4 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MetaInstantiationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MetaIrrelevantSolutionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MetaKindAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
MetaliseOKHAgda.Auto.Syntax
metaliseOKHAgda.Auto.Syntax
metaliseokhAgda.Auto.Syntax
metaModuleAgda.Syntax.Common, Agda.Syntax.Internal
MetaNameSuggestionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
metaNameSuggestionAgda.Syntax.Info
metaNumberAgda.Syntax.Info
metaOccursAgda.TypeChecking.MetaVars.Occurs
MetaOccursInItselfAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
metaOccursQNameAgda.TypeChecking.MetaVars.Occurs
MetaPriority 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
metaRangeAgda.Syntax.Info
MetaSAgda.Syntax.Internal
MetasAgda.Utils.ProfileOptions
metaScopeAgda.Syntax.Info
metasCreatedByAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
MetaSet 
1 (Type/Class)Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
2 (Data Constructor)Agda.TypeChecking.Free.Lazy
metaSetToBlockerAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
metasInAgda.Syntax.Internal.Names
metasIn'Agda.Syntax.Internal.Names
metaToNatAgda.TypeChecking.Primitive
metaTypeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
MetaVAgda.Syntax.Internal
MetaVarAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Metavar 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
MetaVariableAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
meta_not_constructorAgda.Auto.Typecheck
MExpAgda.Auto.Syntax
mextrarefsAgda.Auto.NarrowingSearch
miClosRangeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MIdAgda.Auto.Syntax
MiddleAgda.Syntax.Common
miGeneralizableAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
miInterfaceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
miMetaOccursCheckAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mimicGHCiAgda.Interaction.EmacsTop
miModalityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
miModeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
miNameSuggestionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
minfoAsNameAgda.Syntax.Info
minfoAsToAgda.Syntax.Info
minfoDirectiveAgda.Syntax.Info
minfoOpenShortAgda.Syntax.Info
minfoRangeAgda.Syntax.Info
minifiedCodeLinesLengthAgda.Compiler.JS.Pretty
minusAgda.Interaction.Highlighting.Range
miPrimitiveAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MissingClausesAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
MissingColonForFieldAgda.Interaction.Library.Base
MissingDeclarationsAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
MissingDeclarations_Agda.Interaction.Options.Warnings
MissingDefinitionAgda.Interaction.Highlighting.Precise
MissingDefinitionsAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
MissingDefinitions_Agda.Interaction.Options.Warnings
MissingFieldNameAgda.Interaction.Library.Base
MissingFieldsAgda.Interaction.Library.Base
MissingWithClausesAgda.Syntax.Concrete.Definitions.Errors
miWarningsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
mkAppAgda.Syntax.Translation.ReflectedToAbstract
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
mkCompAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
mkCompLazyAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
mkConAgda.TypeChecking.Records
mkDefAgda.Syntax.Translation.ReflectedToAbstract
mkDefInfoAgda.Syntax.Info
mkDefInfoInstanceAgda.Syntax.Info
mkDomainFreeAgda.Syntax.Abstract
mkGCompAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive.Cubical.Glue
mkIfAgda.Compiler.MAlonzo.Compiler
mkInterfaceFileAgda.Interaction.FindFile
mkIsSizeConstraintAgda.TypeChecking.SizedTypes
mkLam 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.TypeChecking.Substitute
mkLet 
1 (Function)Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Function)Agda.Syntax.Concrete
3 (Function)Agda.Syntax.Abstract
mkLibMAgda.Interaction.Library
mkMatrixAgda.Utils.Warshall
mkMetaInfoAgda.Syntax.Translation.ReflectedToAbstract
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
mkPi 
1 (Function)Agda.Syntax.Abstract
2 (Function)Agda.TypeChecking.Substitute
mkPiSortAgda.TypeChecking.Substitute
mkPragmaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
mkPrimFun1Agda.TypeChecking.Primitive
mkPrimFun1TCMAgda.TypeChecking.Primitive
mkPrimFun2Agda.TypeChecking.Primitive
mkPrimFun3Agda.TypeChecking.Primitive
mkPrimFun4Agda.TypeChecking.Primitive
mkPrimInjectiveAgda.TypeChecking.Primitive
mkPrimLevelMaxAgda.TypeChecking.Primitive
mkPrimLevelSucAgda.TypeChecking.Primitive
mkPrimLevelZeroAgda.TypeChecking.Primitive
mkPrimSetOmegaAgda.TypeChecking.Primitive
mkPropAgda.Syntax.Internal
mkRangeFileAgda.Syntax.Position
mkSSetAgda.Syntax.Internal
mkTAppAgda.Syntax.Treeless, Agda.Compiler.Backend
mkTBindAgda.Syntax.Abstract
mkTLamAgda.Syntax.Treeless, Agda.Compiler.Backend
mkTLet 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
mkTypeAgda.Syntax.Internal
mkVarAgda.Syntax.Translation.ReflectedToAbstract
mkVarNameAgda.Syntax.Translation.ReflectedToAbstract
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
mnameFromList1Agda.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
mnameToList1Agda.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
ModAgda.Syntax.Concrete
Modality 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
modalityActionAgda.TypeChecking.CheckInternal
modalityOfConstAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
modCohesionAgda.Syntax.Common
modDeclsAgda.Syntax.Concrete
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
modifyArgOccurrencesAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
modifyAwakeConstraintsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
modifyBenchmark 
1 (Function)Agda.Utils.Benchmark
2 (Function)Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyCommandLineOptionsAgda.Interaction.Options.Lenses
modifyConcreteNamesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyContextAgda.Syntax.Parser.Monad
modifyContextInfoAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
modifyCounterAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics
modifyCurrentNameSpaceAgda.Syntax.Scope.Monad
modifyCurrentScopeAgda.Syntax.Scope.Monad
modifyCurrentScopeMAgda.Syntax.Scope.Monad
modifyFunClausesAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
modifyGlobalDefinitionAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyImportedSignatureAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyIncludePathsAgda.Interaction.Options.Lenses
modifyInstanceDefsAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyInteractionPointsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
modifyIORefAgda.Utils.IORef
modifyIORef'Agda.Utils.IORef
modifyLocalVarsAgda.Syntax.Scope.Monad
modifyNamedScopeAgda.Syntax.Scope.Monad
modifyNamedScopeMAgda.Syntax.Scope.Monad
modifyNameSpaceAgda.Syntax.Scope.Base
modifyOccursCheckDefsAgda.TypeChecking.MetaVars.Occurs
modifyOldInteractionScopesAgda.Interaction.InteractionTop
modifyPatternSynsAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyPersistentStateAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyPersistentVerbosityAgda.Interaction.Options.Lenses
modifyPragmaOptionsAgda.Interaction.Options.Lenses
modifySafeModeAgda.Interaction.Options.Lenses
modifyScopeAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyScopesAgda.Syntax.Scope.Monad
modifyScope_Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifySignatureAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifySleepingConstraintsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
modifyStatisticsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics
modifySystemAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyTCAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyTC'Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyTCLensAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyTCLens'Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyTCLensMAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyTheInteractionPointsAgda.Interaction.InteractionTop
modifyVerbosityAgda.Interaction.Options.Lenses
modNameAgda.Compiler.JS.Syntax
modnameAgda.Compiler.JS.Pretty
modPragmasAgda.Syntax.Concrete
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.Compiler.Backend, Agda.TypeChecking.Monad
ModuleAssignment 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
ModuleCheckModeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ModuleContentsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
moduleContentsAgda.Interaction.BasicOps
ModuleDefinedInOtherFileAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ModuleDoesntExportAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ModuleDoesntExport_Agda.Interaction.Options.Warnings
ModuleInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
3 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
4 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
ModuleNameHash 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
moduleNameHashAgda.Syntax.Common
moduleNameIdAgda.Syntax.TopLevelModuleName
moduleNameParser 
1 (Function)Agda.Syntax.Parser.Parser
2 (Function)Agda.Syntax.Parser
moduleNamePartsAgda.Syntax.TopLevelModuleName
moduleNameRangeAgda.Syntax.TopLevelModuleName
moduleNameToFileNameAgda.Syntax.TopLevelModuleName
ModuleNameUnexpectedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ModuleNotNameAgda.Syntax.Scope.Base
moduleParamsToApplyAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
moduleParser 
1 (Function)Agda.Syntax.Parser.Parser
2 (Function)Agda.Syntax.Parser
ModulePragmaAgda.Utils.Haskell.Syntax
ModulesAgda.Utils.ProfileOptions
ModuleScopeCheckedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ModulesInScopeAgda.Syntax.Scope.Base
ModuleTagAgda.Syntax.Scope.Base
ModuleToSourceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ModuleTypeCheckedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadAbsToConAgda.TypeChecking.Pretty, Agda.Syntax.Translation.AbstractToConcrete
MonadAddContextAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
MonadBenchAgda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
MonadBlockAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadChangeAgda.Utils.Update
MonadCheckInternalAgda.TypeChecking.CheckInternal
MonadConstraintAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
MonadConversionAgda.TypeChecking.Conversion
MonadDebugAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadFixityErrorAgda.Syntax.Concrete.Fixity
MonadFreshAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadGetDefsAgda.Syntax.Internal.Defs
MonadGHCIOAgda.Compiler.MAlonzo.Compiler
MonadInteractionPointsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
MonadMatchAgda.TypeChecking.Patterns.Match
MonadMetaSolverAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
MonadPlusAgda.Utils.Monad
MonadPrettyAgda.TypeChecking.Pretty
MonadReduceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadReflectedToAbstractAgda.Syntax.Translation.ReflectedToAbstract
MonadReifyAgda.Syntax.Translation.InternalToAbstract
MonadStatisticsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics
MonadStConcreteNamesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadTCEnvAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadTCErrorAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadTCMAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadTCStateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadTerAgda.Termination.Monad
MonadTraceAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace
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
mparens 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.JS.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
MultipleAttributesAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
MultipleAttributes_Agda.Interaction.Options.Warnings
MultipleEllipsesAgda.Syntax.Concrete.Definitions.Errors
MultipleFixityDeclsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MultiplePolarityPragmasAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mustBeFiniteAgda.TypeChecking.SizedTypes.WarshallSolver
mustBePiAgda.TypeChecking.Telescope
MutIdAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Mutual 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
MutualBlock 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mutualBlockOfAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual
MutualChecks 
1 (Type/Class)Agda.Syntax.Concrete.Definitions.Types
2 (Data Constructor)Agda.Syntax.Concrete.Definitions.Types
mutualChecks 
1 (Function)Agda.Syntax.Concrete.Definitions.Types
2 (Function)Agda.TypeChecking.Rules.Decl
mutualCoverageAgda.Syntax.Concrete.Definitions.Types
mutualCoverageCheckAgda.Syntax.Info
MutualIdAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MutualInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
mutualInfoAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mutuallyRecursiveAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
MutualNamesAgda.Termination.RecCheck
mutualNamesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mutualPositivityAgda.Syntax.Concrete.Definitions.Types
mutualPositivityCheckAgda.Syntax.Info
mutualRangeAgda.Syntax.Info
MutualSAgda.Syntax.Abstract
mutualTerminationAgda.Syntax.Concrete.Definitions.Types
mutualTerminationCheckAgda.Syntax.Info
mvFrozenAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mvInfoAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mvInstantiationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mvJudgementAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mvListenersAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mvPermutationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mvPriorityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mvTwinAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MyMBAgda.Auto.Syntax
MyPBAgda.Auto.Syntax
mzeroAgda.Utils.Monad