| 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 |
| main | Agda.Main |
| MainInterface | |
| 1 (Type/Class) | Agda.Interaction.Imports |
| 2 (Data Constructor) | Agda.Interaction.Imports |
| makeAbstract | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| makeAbstractClause | Agda.Interaction.MakeCase |
| makeAbsurdClause | Agda.Interaction.MakeCase |
| makeAll | Agda.Utils.IndexedList |
| makeCase | Agda.Interaction.MakeCase |
| MakeCaseVariant | Agda.Interaction.Response |
| makeConHead | Agda.TypeChecking.Datatypes |
| makeInstance | Agda.Syntax.Common |
| makeInstance' | Agda.Syntax.Common |
| makeOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| makePatternVarsVisible | Agda.Interaction.MakeCase |
| makePi | Agda.Syntax.Concrete |
| makeProjection | Agda.TypeChecking.ProjectionLike |
| makeSubstitution | Agda.TypeChecking.Rewriting.NonLinMatch |
| malformed | Agda.TypeChecking.Serialise.Base |
| ManyHoles | Agda.Utils.AffineHole |
| Map | Agda.Utils.TypeLevel |
| map | |
| 1 (Function) | Agda.Utils.Bag |
| 2 (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.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mapAPattern | Agda.Syntax.Abstract.Pattern |
| mapArgInfo | Agda.Syntax.Common |
| mapAwakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mapBenchmarkOn | Agda.Utils.Benchmark |
| mapChangeT | Agda.Utils.Update |
| mapClosure | Agda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| mapExceptT | Agda.Utils.Except |
| 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.Name, Agda.Syntax.Concrete |
| mapKeysMonotonic | Agda.Utils.AssocList |
| mapLeft | Agda.Utils.Either |
| mapLHSHead | Agda.Syntax.Abstract.Pattern |
| mapLhsOriginalPattern | Agda.Syntax.Concrete.Pattern |
| mapLhsOriginalPatternM | Agda.Syntax.Concrete.Pattern |
| mapListT | Agda.Utils.ListT |
| mapM' | Agda.Utils.Monad |
| mapMaybe | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| mapMaybeAndRest | Agda.Utils.List |
| mapMaybeKeys | Agda.Utils.Map |
| 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 |
| mapping | Agda.Interaction.Highlighting.Precise |
| mapPragmaOptions | Agda.Interaction.Options.Lenses |
| mapQuantity | Agda.Syntax.Common |
| mapQuantityMod | Agda.Syntax.Common |
| mapRedEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mapRedEnvSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mapRedSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mapSnd | Agda.Utils.Tuple |
| mapSndM | Agda.Utils.Tuple |
| mapSubTries | Agda.Utils.Trie |
| mapTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mapTimings | Agda.Utils.Benchmark |
| mapUsing | Agda.Syntax.Common |
| mapVarMap | Agda.TypeChecking.Free.Lazy |
| mapVerbosity | Agda.Interaction.Options.Lenses |
| mapVisitedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mapWithEdge | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| mapWithIndex | Agda.Utils.IndexedList |
| mapWithKey | Agda.Utils.AssocList |
| mapWithKeyM | Agda.Utils.AssocList |
| MArgList | Agda.Auto.Syntax |
| markInjective | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| markInline | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| markStatic | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Markup | |
| 1 (Data Constructor) | Agda.Syntax.Parser.Literate |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| Masked | |
| 1 (Type/Class) | Agda.Termination.Monad |
| 2 (Data Constructor) | Agda.Termination.Monad |
| 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.DisplayForm |
| 5 (Type/Class) | Agda.TypeChecking.Coverage.Match |
| 6 (Type/Class) | Agda.TypeChecking.Rewriting.NonLinMatch |
| match | |
| 1 (Function) | Agda.Syntax.Parser.LookAhead |
| 2 (Function) | Agda.TypeChecking.DisplayForm |
| 3 (Function) | Agda.TypeChecking.Coverage.Match |
| 4 (Function) | Agda.TypeChecking.Rewriting.NonLinMatch |
| 5 (Function) | Agda.Interaction.Highlighting.Vim |
| match' | |
| 1 (Function) | Agda.Syntax.Parser.LookAhead |
| 2 (Function) | Agda.TypeChecking.CompiledClause.Match |
| matchClause | Agda.TypeChecking.Coverage.Match |
| matchCommand | Agda.Interaction.CommandLine |
| matchCompiled | Agda.TypeChecking.CompiledClause.Match |
| matchCompiledE | Agda.TypeChecking.CompiledClause.Match |
| matchCopattern | Agda.TypeChecking.Patterns.Match |
| matchCopatterns | Agda.TypeChecking.Patterns.Match |
| matchDisplayForm | Agda.TypeChecking.DisplayForm |
| Matched | Agda.TypeChecking.Positivity.Occurrence |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| maxInversionDepth | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| maxName | Agda.TypeChecking.Level |
| MaxNat | |
| 1 (Type/Class) | Agda.Utils.Monoid |
| 2 (Data Constructor) | Agda.Utils.Monoid |
| maxViewCons | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| maxViewMax | Agda.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 |
| maybeAbort | Agda.Interaction.InteractionTop |
| maybeFastReduceTerm | Agda.TypeChecking.Reduce |
| 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 |
| maybeProjTurnPostfix | Agda.Syntax.Abstract.Views |
| MaybeRed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MaybeReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MaybeReducedArgs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MaybeReducedElims | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| maybeRight | Agda.Utils.Either |
| maybeTimed | Agda.Interaction.InteractionTop |
| maybeToEither | Agda.Utils.Either |
| maybeToList | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| MaybeWarnings | Agda.Interaction.Imports |
| MaybeWarnings' | Agda.Interaction.Imports |
| mayEraseType | Agda.Compiler.Backend |
| 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 |
| mazerror | Agda.Compiler.MAlonzo.Misc |
| mazIncompleteMatch | Agda.Compiler.MAlonzo.Misc |
| mazMod | Agda.Compiler.MAlonzo.Misc |
| mazMod' | Agda.Compiler.MAlonzo.Misc |
| mazName | Agda.Compiler.MAlonzo.Misc |
| mazRTE | Agda.Compiler.MAlonzo.Misc |
| 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 |
| measureTime | Agda.Utils.Time |
| meet | Agda.TypeChecking.SizedTypes.Utils |
| MeetSemiLattice | Agda.TypeChecking.SizedTypes.Utils |
| member | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.Bag |
| 3 (Function) | Agda.Utils.IntSet.Infinite |
| 4 (Function) | Agda.Utils.SmallSet |
| 5 (Function) | Agda.Utils.Trie |
| MemberId | |
| 1 (Type/Class) | Agda.Compiler.JS.Syntax |
| 2 (Data Constructor) | Agda.Compiler.JS.Syntax |
| 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 |
| merge | Agda.Interaction.Highlighting.Precise |
| mergeC | Agda.Interaction.Highlighting.Precise |
| mergeEdges | Agda.TypeChecking.Positivity |
| mergeElim | Agda.TypeChecking.Patterns.Match |
| mergeElims | Agda.TypeChecking.Patterns.Match |
| mergeHiding | Agda.Syntax.Common |
| mergeInterface | Agda.Interaction.Imports |
| 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 |
| Meta | |
| 1 (Data Constructor) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Syntax.Reflected |
| MetaArg | Agda.TypeChecking.Positivity.Occurrence |
| MetaCannotDependOn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MetaEnv | Agda.Auto.NarrowingSearch |
| MetaErasedSolution | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| metaFrozen | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| 4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MetaInstantiation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MetaIrrelevantSolution | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MetaKind | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MetaLevel | Agda.Syntax.Internal |
| MetaliseOKH | Agda.Auto.Syntax |
| metaliseOKH | Agda.Auto.Syntax |
| metaliseokh | Agda.Auto.Syntax |
| MetaNameSuggestion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| metaNameSuggestion | Agda.Syntax.Info |
| metaNumber | Agda.Syntax.Info |
| metaOccurs | Agda.TypeChecking.MetaVars.Occurs |
| MetaOccursInItself | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| metaOccursQName | Agda.TypeChecking.MetaVars.Occurs |
| metaParseExpr | Agda.Interaction.CommandLine |
| MetaPriority | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| metaRange | Agda.Syntax.Info |
| MetaS | Agda.Syntax.Internal |
| metaScope | Agda.Syntax.Info |
| metasCreatedBy | Agda.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 |
| MetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| metaType | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MetaV | Agda.Syntax.Internal |
| MetaVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Metavar | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| MetaVariable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| meta_not_constructor | Agda.Auto.Typecheck |
| MExp | Agda.Auto.Syntax |
| mextrarefs | Agda.Auto.NarrowingSearch |
| miClosRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MId | Agda.Auto.Syntax |
| Middle | Agda.Syntax.Common |
| miGeneralizable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| miInterface | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| miMetaOccursCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mimicGHCi | Agda.Interaction.EmacsTop |
| miNameSuggestion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| minfoAsName | Agda.Syntax.Info |
| minfoAsTo | Agda.Syntax.Info |
| minfoDirective | Agda.Syntax.Info |
| minfoOpenShort | Agda.Syntax.Info |
| minfoRange | Agda.Syntax.Info |
| minus | Agda.Interaction.Highlighting.Range |
| miPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MissingClauses | Agda.Syntax.Internal |
| MissingDefinition | Agda.Interaction.Highlighting.Precise |
| MissingDefinitions | Agda.Syntax.Concrete.Definitions |
| MissingDefinitions_ | Agda.Interaction.Options.Warnings |
| MissingWithClauses | Agda.Syntax.Concrete.Definitions |
| miWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| 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 |
| mkCon | Agda.TypeChecking.Records |
| mkDef | Agda.Syntax.Translation.ReflectedToAbstract |
| mkDefInfo | Agda.Syntax.Info |
| mkDefInfoInstance | Agda.Syntax.Info |
| mkDomainFree | Agda.Syntax.Abstract |
| mkExceptT | Agda.Utils.Except |
| mkGComp | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| mkIf | Agda.Compiler.MAlonzo.Compiler |
| mkInterfaceFile | Agda.Interaction.FindFile |
| mkIsSizeConstraint | Agda.TypeChecking.SizedTypes |
| mkLam | Agda.TypeChecking.Substitute |
| mkLet | |
| 1 (Function) | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| 2 (Function) | Agda.Syntax.Abstract |
| mkMatrix | Agda.Utils.Warshall |
| 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 | Agda.TypeChecking.Substitute |
| mkPragma | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mkPrimFun1 | Agda.TypeChecking.Primitive |
| mkPrimFun1TCM | Agda.TypeChecking.Primitive |
| mkPrimFun2 | 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 |
| mkSet | Agda.Syntax.Translation.ReflectedToAbstract |
| mkTApp | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| mkTBind | Agda.Syntax.Abstract |
| mkTLam | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| mkType | Agda.Syntax.Internal |
| 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 |
| 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 |
| 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 |
| Modality | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| modalityOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modCohesion | Agda.Syntax.Common |
| 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.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyArgOccurrences | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyAwakeConstraints | Agda.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 |
| modifyCommandLineOptions | Agda.Interaction.Options.Lenses |
| modifyConcreteNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyContextInfo | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyCounter | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyCurrentNameSpace | Agda.Syntax.Scope.Monad |
| modifyCurrentScope | Agda.Syntax.Scope.Monad |
| modifyCurrentScopeM | Agda.Syntax.Scope.Monad |
| modifyFunClauses | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyGlobalDefinition | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyImportedSignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyIncludePaths | Agda.Interaction.Options.Lenses |
| modifyInstanceDefs | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyInteractionPoints | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyIORef | Agda.Utils.IORef |
| modifyIORef' | Agda.Utils.IORef |
| modifyLocalVars | Agda.Syntax.Scope.Monad |
| modifyMetaStore | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyPersistentState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyPersistentVerbosity | Agda.Interaction.Options.Lenses |
| modifyPragmaOptions | Agda.Interaction.Options.Lenses |
| modifySafeMode | Agda.Interaction.Options.Lenses |
| modifyScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyScopes | Agda.Syntax.Scope.Monad |
| modifyScope_ | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifySignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifySleepingConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyStatistics | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifySystem | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyTC' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyTCLens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyTCLensM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| modifyTheInteractionPoints | Agda.Interaction.InteractionTop |
| modifyVerbosity | Agda.Interaction.Options.Lenses |
| modName | Agda.Compiler.JS.Syntax |
| modname | Agda.Compiler.JS.Pretty |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| ModuleAssignment | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| ModuleContents | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| moduleContents | Agda.Interaction.BasicOps |
| ModuleDefinedInOtherFile | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ModuleDoesntExport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ModuleDoesntExport_ | Agda.Interaction.Options.Warnings |
| moduleHash | Agda.Interaction.Imports |
| ModuleId | Agda.Interaction.Highlighting.Dot |
| ModuleInfo | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| 3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| moduleNameParser | |
| 1 (Function) | Agda.Syntax.Parser.Parser |
| 2 (Function) | Agda.Syntax.Parser |
| moduleNameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| moduleNameRange | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| moduleNameToFileName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| ModuleNameUnexpected | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ModuleNotName | Agda.Syntax.Scope.Base |
| moduleParamsToApply | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| moduleParser | |
| 1 (Function) | Agda.Syntax.Parser.Parser |
| 2 (Function) | Agda.Syntax.Parser |
| ModulePragma | Agda.Utils.Haskell.Syntax |
| ModulesInScope | Agda.Syntax.Scope.Base |
| ModuleTag | Agda.Syntax.Scope.Base |
| ModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MonadAbsToCon | Agda.Syntax.Translation.AbstractToConcrete |
| MonadAddContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MonadBench | Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| MonadChange | Agda.Utils.Update |
| MonadCheckInternal | Agda.TypeChecking.CheckInternal |
| MonadConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MonadConversion | Agda.TypeChecking.Conversion |
| MonadDebug | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MonadDisplayForm | Agda.TypeChecking.DisplayForm |
| MonadError | Agda.Utils.Except |
| MonadFixityError | Agda.Syntax.Concrete.Fixity |
| MonadFresh | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MonadGetDefs | Agda.Syntax.Internal.Defs |
| MonadInteractionPoints | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MonadMetaSolver | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MonadPlus | Agda.Utils.Monad |
| MonadPretty | Agda.TypeChecking.Pretty |
| MonadReduce | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MonadReflectedToAbstract | Agda.Syntax.Translation.ReflectedToAbstract |
| MonadReify | Agda.Syntax.Translation.InternalToAbstract |
| MonadStatistics | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MonadStConcreteNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MonadTCEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MonadTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MonadTCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MonadTer | Agda.Termination.Monad |
| 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 | Agda.Utils.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 |
| MultipleEllipses | Agda.Syntax.Concrete.Definitions |
| MultipleFixityDecls | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MultiplePolarityPragmas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mustBeFinite | Agda.TypeChecking.SizedTypes.WarshallSolver |
| mustBePi | Agda.TypeChecking.Telescope |
| MutId | Agda.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 |
| mutualBlockOf | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mutualChecks | Agda.TypeChecking.Rules.Decl |
| mutualCoverageCheck | Agda.Syntax.Info |
| MutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MutualInfo | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| mutualInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mutuallyRecursive | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MutualNames | Agda.Termination.Monad |
| mutualNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mutualPositivityCheck | Agda.Syntax.Info |
| mutualRange | Agda.Syntax.Info |
| mutualTerminationCheck | Agda.Syntax.Info |
| mvFrozen | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mvInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mvInstantiation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mvJudgement | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mvListeners | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mvPermutation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mvPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| mvTwin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| MyMB | Agda.Auto.Syntax |
| MyPB | Agda.Auto.Syntax |
| mzero | Agda.Utils.Monad |