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

Index - M

MAgda.Auto.Options
Macro 
1 (Data Constructor)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Syntax.Concrete
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
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.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapAbstraction_Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapAnnotationAgda.Syntax.Common
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
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
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
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.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
mapValueAgda.Utils.WithDefault
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.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.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.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.Coverage.Match
5 (Type/Class)Agda.TypeChecking.Rewriting.NonLinMatch
match 
1 (Function)Agda.Syntax.Parser.LookAhead
2 (Function)Agda.Interaction.Highlighting.Vim
3 (Function)Agda.TypeChecking.Coverage.Match
4 (Function)Agda.TypeChecking.Rewriting.NonLinMatch
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.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
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.TypeChecking.Monad, Agda.Compiler.Backend
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
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
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.TypeChecking.Monad, Agda.Compiler.Backend
metaCheckAgda.TypeChecking.MetaVars.Occurs
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
MetaliseOKHAgda.Auto.Syntax
metaliseOKHAgda.Auto.Syntax
metaliseokhAgda.Auto.Syntax
metaModuleAgda.Syntax.Common, Agda.Syntax.Internal
MetaNameSuggestionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
metaNameSuggestionAgda.Syntax.Info
metaNumberAgda.Syntax.Info
metaOccursAgda.TypeChecking.MetaVars.Occurs
metaOccurs2Agda.TypeChecking.MetaVars.Occurs
metaOccurs3Agda.TypeChecking.MetaVars.Occurs
MetaOccursInItselfAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
metaOccursQNameAgda.TypeChecking.MetaVars.Occurs
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
MetasAgda.Utils.ProfileOptions
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
metaSetToBlockerAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
metasInAgda.Syntax.Internal.Names
metasIn'Agda.Syntax.Internal.Names
metaToNatAgda.TypeChecking.Primitive
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
miModalityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
miModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
minifiedCodeLinesLengthAgda.Compiler.JS.Pretty
minusAgda.Interaction.Highlighting.Range
miPrimitiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MismatchedProjectionsErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Syntax.Common.Aspect, Agda.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.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
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.Cubical, Agda.TypeChecking.Primitive
mkCompLazyAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
mkConAgda.TypeChecking.Records
mkDefAgda.Syntax.Translation.ReflectedToAbstract
mkDefInfoAgda.Syntax.Info
mkDefInfoInstanceAgda.Syntax.Info
mkDomainFreeAgda.Syntax.Abstract
mkGCompAgda.TypeChecking.Primitive.Cubical.Glue, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
mkInterfaceFileAgda.Interaction.FindFile
mkIsSizeConstraintAgda.TypeChecking.SizedTypes
mkLam 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.TypeChecking.Substitute
mkLet 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Treeless, Agda.Compiler.Backend
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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
mkPropAgda.Syntax.Internal
mkRangeFileAgda.Syntax.Position
mkSortKitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modCohesionAgda.Syntax.Common
modDeclsAgda.Syntax.Concrete
Mode 
1 (Type/Class)Agda.Syntax.Common.Pretty
2 (Type/Class)Agda.Auto.Options
3 (Type/Class)Agda.Interaction.Imports
modeAgda.Syntax.Common.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
modifyContextAgda.Syntax.Parser.Monad
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
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
modifyTCLens'Agda.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
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 (Data Constructor)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
4 (Type/Class)Agda.Syntax.Concrete
5 (Data Constructor)Agda.Syntax.Concrete
6 (Type/Class)Agda.Compiler.JS.Syntax
7 (Data Constructor)Agda.Compiler.JS.Syntax
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
ModuleCheckModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
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.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
ModulesAgda.Utils.ProfileOptions
ModuleScopeCheckedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModulesInScopeAgda.Syntax.Scope.Base
ModuleTagAgda.Syntax.Scope.Base
ModuleToSourceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleTypeCheckedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadAbsToConAgda.Syntax.Translation.AbstractToConcrete, Agda.TypeChecking.Pretty
MonadAddContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadBenchAgda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
MonadBlockAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
MonadMatchAgda.TypeChecking.Patterns.Match
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
MonadTCErrorAgda.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
MonadTraceAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Syntax.Common.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.Syntax.Common.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.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
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.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.RecCheck
mutualNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.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