| M | Agda.Auto.Options |
| Macro | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| MacroDef | Agda.Syntax.Common |
| MacroName | Agda.Syntax.Scope.Base |
| MainFunctionDef | |
| 1 (Type/Class) | Agda.Compiler.MAlonzo.Primitives |
| 2 (Data Constructor) | Agda.Compiler.MAlonzo.Primitives |
| mainFunctionDefs | Agda.Compiler.MAlonzo.Primitives |
| MainMode | Agda.Main |
| MainModePrintAgdaDir | Agda.Main |
| MainModePrintHelp | Agda.Main |
| MainModePrintVersion | Agda.Main |
| MainModeRun | Agda.Main |
| makeAbstract | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| makeAbstractClause | Agda.Interaction.MakeCase |
| makeAbsurdClause | Agda.Interaction.MakeCase |
| makeAll | Agda.Utils.IndexedList |
| makeCase | Agda.Interaction.MakeCase |
| MakeCaseVariant | Agda.Interaction.Response |
| makeInstance | Agda.Syntax.Common |
| makeInstance' | Agda.Syntax.Common |
| makeName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| makeOpen | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Open |
| makePatternVarsVisible | Agda.Interaction.MakeCase |
| makePi | Agda.Syntax.Concrete |
| makeProjection | Agda.TypeChecking.ProjectionLike |
| makeRHSEmptyRecord | Agda.Interaction.MakeCase |
| MakeStrict | Agda.Compiler.MAlonzo.Strict |
| makeStrict | Agda.Compiler.MAlonzo.Strict |
| makeSubstitution | Agda.TypeChecking.Rewriting.NonLinMatch |
| malformed | Agda.TypeChecking.Serialise.Base |
| ManyHoles | Agda.Utils.AffineHole |
| Map | Agda.Utils.TypeLevel |
| map | |
| 1 (Function) | Agda.Utils.List1 |
| 2 (Function) | Agda.Utils.Bag |
| 3 (Function) | Agda.Compiler.JS.Substitution |
| map' | Agda.Compiler.JS.Substitution |
| mapAbsNames | Agda.Syntax.Internal |
| mapAbsNamesM | Agda.Syntax.Internal |
| mapAbsoluteIncludePaths | Agda.Interaction.Options.Lenses |
| mapAbstraction | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| mapAnnotation | Agda.Syntax.Common |
| mapAPattern | Agda.Syntax.Abstract.Pattern |
| mapArgInfo | Agda.Syntax.Common |
| mapAwakeConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| mapBenchmarkOn | Agda.Utils.Benchmark |
| mapChangeT | Agda.Utils.Update |
| mapClosure | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Closure |
| mapCohesion | Agda.Syntax.Common |
| mapCohesionMod | Agda.Syntax.Common |
| mapCommandLineOptions | Agda.Interaction.Options.Lenses |
| mapConName | Agda.Syntax.Internal |
| mapCPattern | Agda.Syntax.Concrete.Pattern |
| mapCurrentAccount | Agda.Utils.Benchmark |
| mapEither3M | Agda.Utils.Three |
| mapExpr | |
| 1 (Function) | Agda.Syntax.Concrete.Generic |
| 2 (Function) | Agda.Syntax.Abstract.Views |
| mapFlag | Agda.Interaction.Options |
| mapFlexRigMap | Agda.TypeChecking.Free.Lazy |
| mapFreeVariables | Agda.Syntax.Common |
| mapFreeVariablesArgInfo | Agda.Syntax.Common |
| mapFst | Agda.Utils.Tuple |
| mapFstM | Agda.Utils.Tuple |
| mapHiding | Agda.Syntax.Common |
| mapHidingArgInfo | Agda.Syntax.Common |
| mapImportDir | Agda.Syntax.Scope.Monad |
| mapIncludePaths | Agda.Interaction.Options.Lenses |
| mapInScope | Agda.Syntax.Concrete, Agda.Syntax.Concrete.Name |
| mapKeysMonotonic | Agda.Utils.AssocList |
| mapLeft | Agda.Utils.Either |
| mapLHSCores | Agda.TypeChecking.Rules.Def |
| mapLHSHead | Agda.Syntax.Abstract.Pattern |
| mapLhsOriginalPattern | Agda.Syntax.Concrete.Pattern |
| mapLhsOriginalPatternM | Agda.Syntax.Concrete.Pattern |
| mapListT | Agda.Utils.ListT |
| mapLock | Agda.Syntax.Common |
| mapM' | Agda.Utils.Monad |
| mapMaybe | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| 3 (Function) | Agda.Utils.List1 |
| mapMaybeAndRest | Agda.Utils.List |
| mapMaybeM | Agda.Utils.Monad |
| mapMaybeMM | Agda.Utils.Monad |
| mapMembership | Agda.Utils.SmallSet |
| mapMListT | Agda.Utils.ListT |
| mapMListT_alt | Agda.Utils.ListT |
| mapMM | Agda.Utils.Monad |
| mapMM_ | Agda.Utils.Monad |
| mapModality | Agda.Syntax.Common |
| mapModalityArgInfo | Agda.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 |
| mapNameOf | Agda.Syntax.Common |
| mapNameSpace | Agda.Syntax.Scope.Base |
| mapNameSpaceM | Agda.Syntax.Scope.Base |
| mapOrigin | Agda.Syntax.Common |
| mapOriginArgInfo | Agda.Syntax.Common |
| mapPairM | Agda.Utils.Tuple |
| mapPersistentVerbosity | Agda.Interaction.Options.Lenses |
| mapPragmaOptions | Agda.Interaction.Options.Lenses |
| mapQuantity | Agda.Syntax.Common |
| mapQuantityMod | Agda.Syntax.Common |
| mapRedEnv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| mapRedEnvSt | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| mapRedSt | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| mapRelevance | Agda.Syntax.Common |
| mapRelevanceMod | Agda.Syntax.Common |
| mapRenaming | Agda.Syntax.Scope.Monad |
| mapRight | Agda.Utils.Either |
| MapS | Agda.Auto.Convert |
| mapSafeMode | Agda.Interaction.Options.Lenses |
| mapScope | Agda.Syntax.Scope.Base |
| mapScopeM | Agda.Syntax.Scope.Base |
| mapScopeM_ | Agda.Syntax.Scope.Base |
| mapScopeNS | Agda.Syntax.Scope.Base |
| mapScope_ | Agda.Syntax.Scope.Base |
| mapSleepingConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| mapSnd | Agda.Utils.Tuple |
| mapSndM | Agda.Utils.Tuple |
| mapSubTries | Agda.Utils.Trie |
| mapTCMT | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| mapTimings | Agda.Utils.Benchmark |
| mapUsing | Agda.Syntax.Common |
| mapVarMap | Agda.TypeChecking.Free.Lazy |
| mapVerbosity | Agda.Interaction.Options.Lenses |
| mapWithEdge | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| mapWithIndex | Agda.Utils.IndexedList |
| mapWithKey | |
| 1 (Function) | Agda.Utils.BiMap |
| 2 (Function) | Agda.Utils.AssocList |
| mapWithKeyFixedTags | Agda.Utils.BiMap |
| mapWithKeyFixedTagsPrecondition | Agda.Utils.BiMap |
| mapWithKeyM | Agda.Utils.AssocList |
| mapWithKeyPrecondition | Agda.Utils.BiMap |
| MArgList | Agda.Auto.Syntax |
| markInjective | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| markInline | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| markStatic | Agda.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 |
| masked | Agda.Termination.Monad |
| MaskedDeBruijnPatterns | Agda.Termination.Monad |
| Mat | Agda.Termination.Order |
| mat | Agda.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 |
| matchClause | Agda.TypeChecking.Coverage.Match |
| matchCompiled | Agda.TypeChecking.CompiledClause.Match |
| matchCompiledE | Agda.TypeChecking.CompiledClause.Match |
| matchCopattern | Agda.TypeChecking.Patterns.Match |
| matchCopatterns | Agda.TypeChecking.Patterns.Match |
| Matched | Agda.TypeChecking.Positivity.Occurrence |
| matchedArgs | Agda.TypeChecking.Patterns.Match |
| matchedArgs' | Agda.TypeChecking.Patterns.Match |
| matches | Agda.Interaction.Highlighting.Vim |
| matchingBlocked | Agda.TypeChecking.Rewriting.NonLinMatch |
| matchPattern | Agda.TypeChecking.Patterns.Match |
| matchPatternP | Agda.TypeChecking.Patterns.Match |
| matchPatterns | Agda.TypeChecking.Patterns.Match |
| matchPatternsP | Agda.TypeChecking.Patterns.Match |
| matchPatternSyn | Agda.Syntax.Abstract.PatternSynonyms |
| matchPatternSynP | Agda.Syntax.Abstract.PatternSynonyms |
| matchType | Agda.Auto.Convert |
| Matrix | |
| 1 (Type/Class) | Agda.Termination.SparseMatrix |
| 2 (Data Constructor) | Agda.Termination.SparseMatrix |
| 3 (Type/Class) | Agda.Utils.Warshall |
| matrix | Agda.Utils.Warshall |
| Max | Agda.Syntax.Internal |
| maxInstanceSearchDepth | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| maxInversionDepth | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| maxName | Agda.TypeChecking.Level |
| MaxNat | |
| 1 (Type/Class) | Agda.Utils.Monoid |
| 2 (Data Constructor) | Agda.Utils.Monoid |
| maxViewCons | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| maxViewMax | Agda.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 |
| maybeAbort | Agda.Interaction.InteractionTop |
| maybeFlexiblePattern | Agda.TypeChecking.Rules.LHS |
| MaybeFree | Agda.TypeChecking.Free.Reduce |
| maybeLeft | Agda.Utils.Either |
| maybeM | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| maybeor | Agda.Auto.Typecheck |
| MaybePlaceholder | Agda.Syntax.Common |
| maybePlaceholder | Agda.Syntax.Concrete.Operators.Parser |
| maybePrimCon | Agda.TypeChecking.Level |
| maybePrimDef | Agda.TypeChecking.Level |
| MaybeProjection | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| maybeProjTurnPostfix | Agda.Syntax.Abstract.Views |
| MaybeRed | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MaybeReduced | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MaybeReducedArgs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MaybeReducedElims | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| maybeRight | Agda.Utils.Either |
| maybeTimed | Agda.Interaction.InteractionTop |
| maybeToEither | Agda.Utils.Either |
| maybeToList | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| mayEraseType | Agda.Compiler.Backend |
| mazAccumlatedImports | Agda.Compiler.MAlonzo.Misc |
| mazAnyType | Agda.Compiler.MAlonzo.Misc |
| mazAnyTypeName | Agda.Compiler.MAlonzo.Misc |
| mazCoerce | Agda.Compiler.MAlonzo.Misc |
| mazCoerceName | Agda.Compiler.MAlonzo.Misc |
| mazErasedName | Agda.Compiler.MAlonzo.Misc |
| mazHole | Agda.Compiler.MAlonzo.Misc |
| mazIsMainModule | Agda.Compiler.MAlonzo.Misc |
| mazMod | Agda.Compiler.MAlonzo.Misc |
| mazMod' | Agda.Compiler.MAlonzo.Misc |
| mazModuleName | Agda.Compiler.MAlonzo.Misc |
| mazName | Agda.Compiler.MAlonzo.Misc |
| mazRTE | Agda.Compiler.MAlonzo.Misc |
| mazRTEFloat | Agda.Compiler.MAlonzo.Misc |
| mazRTEFloatImport | Agda.Compiler.MAlonzo.Compiler |
| mazstr | Agda.Compiler.MAlonzo.Misc |
| mazUnreachableError | Agda.Compiler.MAlonzo.Misc |
| MB | Agda.Auto.NarrowingSearch |
| mbcase | Agda.Auto.NarrowingSearch |
| mbfailed | Agda.Auto.NarrowingSearch |
| mbind | Agda.Auto.NarrowingSearch |
| mbpcase | Agda.Auto.NarrowingSearch |
| mbret | Agda.Auto.NarrowingSearch |
| MCaseSplit | Agda.Auto.Options |
| mcompoint | Agda.Auto.NarrowingSearch |
| mcons | Agda.Utils.List |
| MdFileType | Agda.Syntax.Common |
| Measure | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions |
| measureTime | Agda.Utils.Time |
| meet | Agda.TypeChecking.SizedTypes.Utils |
| MeetSemiLattice | Agda.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 |
| MemberIndex | Agda.Compiler.JS.Syntax |
| Memo | Agda.TypeChecking.Serialise.Base |
| memo | Agda.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 |
| MemoKey | Agda.Syntax.Concrete.Operators.Parser.Monad |
| memoModules | Agda.Syntax.Scope.Monad |
| memoNames | Agda.Syntax.Scope.Monad |
| memoRec | Agda.Utils.Memo |
| memoToScopeInfo | Agda.Syntax.Scope.Monad |
| memoUnsafe | Agda.Utils.Memo |
| memoUnsafeH | Agda.Utils.Memo |
| mentions | Agda.TypeChecking.SizedTypes.WarshallSolver |
| MentionsMeta | Agda.TypeChecking.MetaVars.Mention |
| mentionsMeta | Agda.TypeChecking.MetaVars.Mention |
| mentionsMetas | Agda.TypeChecking.MetaVars.Mention |
| mergeEdges | Agda.TypeChecking.Positivity |
| mergeElim | Agda.TypeChecking.Patterns.Match |
| mergeElims | Agda.TypeChecking.Patterns.Match |
| mergeHiding | Agda.Syntax.Common |
| mergeNames | Agda.Syntax.Scope.Base |
| mergeNamesMany | Agda.Syntax.Scope.Base |
| mergeNotations | Agda.Syntax.Notation |
| mergePatternSynDefs | Agda.Syntax.Abstract.PatternSynonyms |
| mergeScope | Agda.Syntax.Scope.Base |
| mergeScopes | Agda.Syntax.Scope.Base |
| mergeStrictlyOrderedBy | Agda.Utils.List |
| Meta | |
| 1 (Data Constructor) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Syntax.Reflected |
| MetaArg | Agda.TypeChecking.Positivity.Occurrence |
| MetaCannotDependOn | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| metaCheck | Agda.TypeChecking.MetaVars.Occurs |
| MetaEnv | Agda.Auto.NarrowingSearch |
| MetaErasedSolution | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| metaFrozen | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| metaHelperType | Agda.Interaction.BasicOps |
| MetaId | |
| 1 (Type/Class) | Agda.Syntax.Common, Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Common, Agda.Syntax.Internal |
| metaId | Agda.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 |
| MetaInstantiation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MetaIrrelevantSolution | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MetaKind | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| MetaliseOKH | Agda.Auto.Syntax |
| metaliseOKH | Agda.Auto.Syntax |
| metaliseokh | Agda.Auto.Syntax |
| metaModule | Agda.Syntax.Common, Agda.Syntax.Internal |
| MetaNameSuggestion | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| metaNameSuggestion | Agda.Syntax.Info |
| metaNumber | Agda.Syntax.Info |
| metaOccurs | Agda.TypeChecking.MetaVars.Occurs |
| MetaOccursInItself | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| metaOccursQName | Agda.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 |
| metaRange | Agda.Syntax.Info |
| MetaS | Agda.Syntax.Internal |
| Metas | Agda.Utils.ProfileOptions |
| metaScope | Agda.Syntax.Info |
| metasCreatedBy | Agda.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 |
| metaSetToBlocker | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| metasIn | Agda.Syntax.Internal.Names |
| metasIn' | Agda.Syntax.Internal.Names |
| metaToNat | Agda.TypeChecking.Primitive |
| metaType | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| MetaV | Agda.Syntax.Internal |
| MetaVar | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Metavar | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| MetaVariable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| meta_not_constructor | Agda.Auto.Typecheck |
| MExp | Agda.Auto.Syntax |
| mextrarefs | Agda.Auto.NarrowingSearch |
| miClosRange | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MId | Agda.Auto.Syntax |
| Middle | Agda.Syntax.Common |
| miGeneralizable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| miInterface | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| miMetaOccursCheck | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| mimicGHCi | Agda.Interaction.EmacsTop |
| miModality | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| miMode | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| miNameSuggestion | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| minfoAsName | Agda.Syntax.Info |
| minfoAsTo | Agda.Syntax.Info |
| minfoDirective | Agda.Syntax.Info |
| minfoOpenShort | Agda.Syntax.Info |
| minfoRange | Agda.Syntax.Info |
| minifiedCodeLinesLength | Agda.Compiler.JS.Pretty |
| minus | Agda.Interaction.Highlighting.Range |
| miPrimitive | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MissingClauses | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| MissingColonForField | Agda.Interaction.Library.Base |
| MissingDeclarations | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| MissingDeclarations_ | Agda.Interaction.Options.Warnings |
| MissingDefinition | Agda.Interaction.Highlighting.Precise |
| MissingDefinitions | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| MissingDefinitions_ | Agda.Interaction.Options.Warnings |
| MissingFieldName | Agda.Interaction.Library.Base |
| MissingFields | Agda.Interaction.Library.Base |
| MissingWithClauses | Agda.Syntax.Concrete.Definitions.Errors |
| miWarnings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MIx | |
| 1 (Type/Class) | Agda.Termination.SparseMatrix |
| 2 (Data Constructor) | Agda.Termination.SparseMatrix |
| Mixed | Agda.TypeChecking.Positivity.Occurrence |
| mkAbs | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| mkAbsolute | Agda.Utils.FileName |
| mkApp | Agda.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 |
| mkBindName | Agda.Syntax.Abstract |
| mkBoundName | Agda.Syntax.Concrete |
| mkBoundName_ | Agda.Syntax.Concrete |
| mkCall | Agda.Termination.CallGraph |
| mkCall' | Agda.Termination.CallGraph |
| mkComp | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| mkCompLazy | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| mkCon | Agda.TypeChecking.Records |
| mkDef | Agda.Syntax.Translation.ReflectedToAbstract |
| mkDefInfo | Agda.Syntax.Info |
| mkDefInfoInstance | Agda.Syntax.Info |
| mkDomainFree | Agda.Syntax.Abstract |
| mkGComp | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive.Cubical.Glue |
| mkIf | Agda.Compiler.MAlonzo.Compiler |
| mkInterfaceFile | Agda.Interaction.FindFile |
| mkIsSizeConstraint | Agda.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 |
| mkLibM | Agda.Interaction.Library |
| mkMatrix | Agda.Utils.Warshall |
| mkMetaInfo | Agda.Syntax.Translation.ReflectedToAbstract |
| MkName | Agda.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 |
| mkName_ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| mkNotation | Agda.Syntax.Notation |
| mkPi | |
| 1 (Function) | Agda.Syntax.Abstract |
| 2 (Function) | Agda.TypeChecking.Substitute |
| mkPiSort | Agda.TypeChecking.Substitute |
| mkPragma | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| mkPrimFun1 | Agda.TypeChecking.Primitive |
| mkPrimFun1TCM | Agda.TypeChecking.Primitive |
| mkPrimFun2 | Agda.TypeChecking.Primitive |
| mkPrimFun3 | Agda.TypeChecking.Primitive |
| mkPrimFun4 | Agda.TypeChecking.Primitive |
| mkPrimInjective | Agda.TypeChecking.Primitive |
| mkPrimLevelMax | Agda.TypeChecking.Primitive |
| mkPrimLevelSuc | Agda.TypeChecking.Primitive |
| mkPrimLevelZero | Agda.TypeChecking.Primitive |
| mkPrimSetOmega | Agda.TypeChecking.Primitive |
| mkProp | Agda.Syntax.Internal |
| mkRangeFile | Agda.Syntax.Position |
| mkSSet | Agda.Syntax.Internal |
| mkTApp | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| mkTBind | Agda.Syntax.Abstract |
| mkTLam | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| mkTLet | |
| 1 (Function) | Agda.Syntax.Concrete |
| 2 (Function) | Agda.Syntax.Abstract |
| mkType | Agda.Syntax.Internal |
| mkVar | Agda.Syntax.Translation.ReflectedToAbstract |
| mkVarName | Agda.Syntax.Translation.ReflectedToAbstract |
| mkWeakIORef | Agda.Utils.IORef |
| MM | Agda.Auto.NarrowingSearch |
| mmbpcase | Agda.Auto.NarrowingSearch |
| mmcase | Agda.Auto.NarrowingSearch |
| mmmcase | Agda.Auto.NarrowingSearch |
| mmpcase | Agda.Auto.NarrowingSearch |
| MName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| mnameFromList | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| mnameFromList1 | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| mnameToConcrete | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| mnameToList | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| mnameToList1 | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| mnameToQName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| MNormal | Agda.Auto.Options |
| mobs | Agda.Auto.NarrowingSearch |
| Mod | Agda.Syntax.Concrete |
| Modality | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| modalityAction | Agda.TypeChecking.CheckInternal |
| modalityOfConst | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| modCohesion | Agda.Syntax.Common |
| modDecls | Agda.Syntax.Concrete |
| Mode | |
| 1 (Type/Class) | Agda.Utils.Pretty |
| 2 (Type/Class) | Agda.Auto.Options |
| 3 (Type/Class) | Agda.Interaction.Imports |
| mode | Agda.Utils.Pretty |
| modFile | Agda.TypeChecking.Serialise.Base |
| modifyAbsoluteIncludePaths | Agda.Interaction.Options.Lenses |
| modifyAbstractClause | Agda.Auto.Convert |
| modifyAbstractExpr | Agda.Auto.Convert |
| modifyAllowedReductions | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| modifyArgOccurrences | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| modifyAwakeConstraints | Agda.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 |
| modifyCommandLineOptions | Agda.Interaction.Options.Lenses |
| modifyConcreteNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| modifyContext | Agda.Syntax.Parser.Monad |
| modifyContextInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| modifyCounter | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics |
| modifyCurrentNameSpace | Agda.Syntax.Scope.Monad |
| modifyCurrentScope | Agda.Syntax.Scope.Monad |
| modifyCurrentScopeM | Agda.Syntax.Scope.Monad |
| modifyFunClauses | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| modifyGlobalDefinition | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| modifyImportedSignature | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| modifyIncludePaths | Agda.Interaction.Options.Lenses |
| modifyInstanceDefs | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| modifyInteractionPoints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| modifyIORef | Agda.Utils.IORef |
| modifyIORef' | Agda.Utils.IORef |
| modifyLocalVars | Agda.Syntax.Scope.Monad |
| modifyNamedScope | Agda.Syntax.Scope.Monad |
| modifyNamedScopeM | Agda.Syntax.Scope.Monad |
| modifyNameSpace | Agda.Syntax.Scope.Base |
| modifyOccursCheckDefs | Agda.TypeChecking.MetaVars.Occurs |
| modifyOldInteractionScopes | Agda.Interaction.InteractionTop |
| modifyPatternSyns | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| modifyPersistentState | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| modifyPersistentVerbosity | Agda.Interaction.Options.Lenses |
| modifyPragmaOptions | Agda.Interaction.Options.Lenses |
| modifySafeMode | Agda.Interaction.Options.Lenses |
| modifyScope | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| modifyScopes | Agda.Syntax.Scope.Monad |
| modifyScope_ | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| modifySignature | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| modifySleepingConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| modifyStatistics | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics |
| modifySystem | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| modifyTC | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| modifyTC' | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| modifyTCLens | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| modifyTCLens' | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| modifyTCLensM | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| modifyTheInteractionPoints | Agda.Interaction.InteractionTop |
| modifyVerbosity | Agda.Interaction.Options.Lenses |
| modName | Agda.Compiler.JS.Syntax |
| modname | Agda.Compiler.JS.Pretty |
| modPragmas | Agda.Syntax.Concrete |
| modQuantity | Agda.Syntax.Common |
| modRelevance | Agda.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 |
| ModuleArityMismatch | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ModuleAssignment | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| ModuleCheckMode | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ModuleContents | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| moduleContents | Agda.Interaction.BasicOps |
| ModuleDefinedInOtherFile | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ModuleDoesntExport | Agda.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 |
| ModuleMacro | Agda.Syntax.Concrete |
| ModuleMap | Agda.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 |
| moduleName | Agda.Interaction.FindFile |
| ModuleNameDoesntMatchFileName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ModuleNameHash | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| moduleNameHash | Agda.Syntax.Common |
| moduleNameId | Agda.Syntax.TopLevelModuleName |
| moduleNameParser | |
| 1 (Function) | Agda.Syntax.Parser.Parser |
| 2 (Function) | Agda.Syntax.Parser |
| moduleNameParts | Agda.Syntax.TopLevelModuleName |
| moduleNameRange | Agda.Syntax.TopLevelModuleName |
| moduleNameToFileName | Agda.Syntax.TopLevelModuleName |
| ModuleNameUnexpected | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ModuleNotName | Agda.Syntax.Scope.Base |
| moduleParamsToApply | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| moduleParser | |
| 1 (Function) | Agda.Syntax.Parser.Parser |
| 2 (Function) | Agda.Syntax.Parser |
| ModulePragma | Agda.Utils.Haskell.Syntax |
| Modules | Agda.Utils.ProfileOptions |
| ModuleScopeChecked | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ModulesInScope | Agda.Syntax.Scope.Base |
| ModuleTag | Agda.Syntax.Scope.Base |
| ModuleToSource | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ModuleTypeChecked | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MonadAbsToCon | Agda.TypeChecking.Pretty, Agda.Syntax.Translation.AbstractToConcrete |
| MonadAddContext | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| MonadBench | Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| MonadBlock | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MonadChange | Agda.Utils.Update |
| MonadCheckInternal | Agda.TypeChecking.CheckInternal |
| MonadConstraint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| MonadConversion | Agda.TypeChecking.Conversion |
| MonadDebug | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MonadFixityError | Agda.Syntax.Concrete.Fixity |
| MonadFresh | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MonadGetDefs | Agda.Syntax.Internal.Defs |
| MonadGHCIO | Agda.Compiler.MAlonzo.Compiler |
| MonadInteractionPoints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| MonadMatch | Agda.TypeChecking.Patterns.Match |
| MonadMetaSolver | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| MonadPlus | Agda.Utils.Monad |
| MonadPretty | Agda.TypeChecking.Pretty |
| MonadReduce | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MonadReflectedToAbstract | Agda.Syntax.Translation.ReflectedToAbstract |
| MonadReify | Agda.Syntax.Translation.InternalToAbstract |
| MonadStatistics | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics |
| MonadStConcreteNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MonadTCEnv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MonadTCError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MonadTCM | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MonadTCState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MonadTer | Agda.Termination.Monad |
| MonadTrace | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace |
| MonadWarning | Agda.TypeChecking.Warnings |
| moreCohesion | Agda.Syntax.Common |
| moreQuantity | Agda.Syntax.Common |
| moreRelevant | Agda.Syntax.Common |
| moreUsableModality | Agda.Syntax.Common |
| MOT | Agda.Auto.Convert |
| Move | |
| 1 (Data Constructor) | Agda.Auto.NarrowingSearch |
| 2 (Type/Class) | Agda.Auto.SearchControl |
| Move' | Agda.Auto.NarrowingSearch |
| moveCost | Agda.Auto.NarrowingSearch |
| moveNext | Agda.Auto.NarrowingSearch |
| movePos | Agda.Syntax.Position |
| movePosByString | Agda.Syntax.Position |
| mparens | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Compiler.JS.Pretty |
| mplus | Agda.Utils.Monad |
| mpret | Agda.Auto.NarrowingSearch |
| mprincipalpresent | Agda.Auto.NarrowingSearch |
| MRefine | Agda.Auto.Options |
| mul | |
| 1 (Function) | Agda.Termination.Semiring |
| 2 (Function) | Agda.Termination.SparseMatrix |
| multiLineText | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| MultipleAttributes | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| MultipleAttributes_ | Agda.Interaction.Options.Warnings |
| MultipleEllipses | Agda.Syntax.Concrete.Definitions.Errors |
| MultipleFixityDecls | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MultiplePolarityPragmas | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| mustBeFinite | Agda.TypeChecking.SizedTypes.WarshallSolver |
| mustBePi | Agda.TypeChecking.Telescope |
| MutId | Agda.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 |
| mutualBlockOf | Agda.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 |
| mutualCoverage | Agda.Syntax.Concrete.Definitions.Types |
| mutualCoverageCheck | Agda.Syntax.Info |
| MutualId | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MutualInfo | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| mutualInfo | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| mutuallyRecursive | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| MutualNames | Agda.Termination.RecCheck |
| mutualNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| mutualPositivity | Agda.Syntax.Concrete.Definitions.Types |
| mutualPositivityCheck | Agda.Syntax.Info |
| mutualRange | Agda.Syntax.Info |
| MutualS | Agda.Syntax.Abstract |
| mutualTermination | Agda.Syntax.Concrete.Definitions.Types |
| mutualTerminationCheck | Agda.Syntax.Info |
| mvFrozen | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| mvInfo | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| mvInstantiation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| mvJudgement | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| mvListeners | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| mvPermutation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| mvPriority | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| mvTwin | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| MyMB | Agda.Auto.Syntax |
| MyPB | Agda.Auto.Syntax |
| mzero | Agda.Utils.Monad |