| 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 |
| MagicConstrInfo | Agda.Compiler.UHC.MagicTypes |
| MagicName | Agda.Compiler.UHC.MagicTypes |
| MagicTypeInfo | Agda.Compiler.UHC.MagicTypes |
| main | Agda.Main |
| MainInterface | |
| 1 (Type/Class) | Agda.Interaction.Imports |
| 2 (Data Constructor) | Agda.Interaction.Imports |
| mainName | Agda.Compiler.Epic.Interface |
| makeAbstract | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| makeAbstractClause | Agda.Interaction.MakeCase |
| makeAbsurdClause | Agda.Interaction.MakeCase |
| makeCase | Agda.Interaction.MakeCase |
| MakeCaseVariant | Agda.Interaction.Response |
| makeClosed | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad |
| makeConAlt | Agda.Compiler.UHC.FromAgda |
| makeConfiguration | Agda.TypeChecking.Test.Generators |
| makeEnv | Agda.Syntax.Translation.AbstractToConcrete |
| makeForcedArgs | Agda.Compiler.Epic.ForceConstrs |
| makeInstance | Agda.Syntax.Common |
| makeOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad |
| makeProjection | Agda.TypeChecking.ProjectionLike |
| makeSubstitution | Agda.TypeChecking.Rewriting.NonLinMatch |
| malformed | Agda.TypeChecking.Serialise.Base |
| MAlonzo | Agda.Interaction.InteractionTop |
| MAlonzoNoMain | Agda.Interaction.InteractionTop |
| many | Agda.Utils.Parser.ReadP |
| many1 | Agda.Utils.Parser.ReadP |
| manyTill | Agda.Utils.Parser.ReadP |
| map | |
| 1 (Function) | Agda.Utils.HashMap |
| 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 |
| mapArgInfo | Agda.Syntax.Common |
| mapAwakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| mapBenchmarkOn | Agda.Utils.Benchmark |
| mapBlockingVarCons | Agda.TypeChecking.Coverage.Match |
| mapCommandLineOptions | Agda.Interaction.Options.Lenses |
| mapCon | Agda.Compiler.Epic.Primitive |
| mapConName | Agda.Syntax.Internal |
| mapContext | Agda.Compiler.MAlonzo.Compiler |
| mapCurrentAccount | Agda.Utils.Benchmark |
| mapEither | |
| 1 (Function) | Agda.Utils.Either |
| 2 (Function) | Agda.Utils.List |
| mapExceptT | Agda.Utils.Except |
| mapExpr | |
| 1 (Function) | Agda.Syntax.Concrete.Generic |
| 2 (Function) | Agda.Syntax.Abstract.Views |
| mapFlag | Agda.Interaction.Options |
| mapFst | Agda.Utils.Tuple |
| mapFstM | Agda.Utils.Tuple |
| mapHiding | Agda.Syntax.Common |
| mapImportDir | Agda.Syntax.Scope.Monad |
| mapIncludePaths | Agda.Interaction.Options.Lenses |
| mapKeysMonotonic | Agda.Utils.AssocList |
| mapLeft | Agda.Utils.Either |
| mapLHSHead | Agda.Syntax.Abstract |
| mapLhsOriginalPattern | Agda.Syntax.Concrete |
| mapM' | Agda.Utils.Monad |
| mapMaybe | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.HashMap |
| 3 (Function) | Agda.Utils.Maybe.Strict |
| mapMaybeM | Agda.Utils.Monad |
| mapMaybeWithKey | Agda.Utils.HashMap |
| mapMListT | Agda.Utils.ListT |
| mapMListT_alt | Agda.Utils.ListT |
| mapNameSpace | Agda.Syntax.Scope.Base |
| mapNameSpaceM | Agda.Syntax.Scope.Base |
| mapNameSupply | Agda.Compiler.MAlonzo.Compiler |
| mapNodes | Agda.Utils.Warshall |
| mapPairM | Agda.Utils.Tuple |
| mapPersistentVerbosity | Agda.Interaction.Options.Lenses |
| mapping | Agda.Compiler.JS.Compiler |
| mapping' | Agda.Compiler.JS.Compiler |
| mapPragmaOptions | Agda.Interaction.Options.Lenses |
| mapRedEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mapRedEnvSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mapRedSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mapRelevance | 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 |
| mapScope' | Agda.Syntax.Scope.Base |
| mapScopeInfo | Agda.Syntax.Scope.Base |
| mapScopeM | Agda.Syntax.Scope.Base |
| mapScopeM_ | Agda.Syntax.Scope.Base |
| mapScope_ | Agda.Syntax.Scope.Base |
| mapSize | Agda.Utils.QuickCheck |
| mapSleepingConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| mapSnd | Agda.Utils.Tuple |
| mapSndM | Agda.Utils.Tuple |
| mapTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mapTimings | Agda.Utils.Benchmark |
| mapUsing | Agda.Syntax.Scope.Monad |
| mapVerbosity | Agda.Interaction.Options.Lenses |
| mapWithEdge | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| mapWithKey | |
| 1 (Function) | Agda.Utils.HashMap |
| 2 (Function) | Agda.Utils.AssocList |
| mapWithKeyM | Agda.Utils.AssocList |
| MArgList | Agda.Auto.Syntax |
| markInline | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| markNoSmashing | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| markStatic | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| Masked | |
| 1 (Type/Class) | Agda.Termination.Monad |
| 2 (Data Constructor) | Agda.Termination.Monad |
| masked | Agda.Termination.Monad |
| MaskedDeBruijnPats | Agda.Termination.Monad |
| Mat | Agda.Termination.Order |
| mat | Agda.Termination.CallMatrix |
| Match | |
| 1 (Type/Class) | Agda.TypeChecking.Patterns.Match |
| 2 (Type/Class) | Agda.TypeChecking.DisplayForm |
| 3 (Type/Class) | Agda.TypeChecking.Rewriting.NonLinMatch |
| 4 (Type/Class) | Agda.TypeChecking.Coverage.Match |
| match | |
| 1 (Function) | Agda.Compiler.JS.Case |
| 2 (Function) | Agda.Syntax.Parser.LookAhead |
| 3 (Function) | Agda.Interaction.Highlighting.Vim |
| 4 (Function) | Agda.TypeChecking.DisplayForm |
| 5 (Function) | Agda.TypeChecking.Rewriting.NonLinMatch |
| 6 (Function) | Agda.TypeChecking.Coverage.Match |
| 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 |
| matches | Agda.Interaction.Highlighting.Vim |
| matchingBlocked | Agda.TypeChecking.Rewriting.NonLinMatch |
| MatchLit | Agda.TypeChecking.Coverage.Match |
| matchLits | Agda.TypeChecking.Coverage.Match |
| matchPat | Agda.TypeChecking.Coverage.Match |
| matchPats | Agda.TypeChecking.Coverage.Match |
| matchPattern | Agda.TypeChecking.Patterns.Match |
| matchPatterns | Agda.TypeChecking.Patterns.Match |
| matchType | Agda.Auto.Convert |
| Matrix | |
| 1 (Type/Class) | Agda.Termination.SparseMatrix |
| 2 (Type/Class) | Agda.Utils.Warshall |
| matrix | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Utils.Warshall |
| matrixInvariant | Agda.Termination.SparseMatrix |
| matrixUsingRowGen | Agda.Termination.SparseMatrix |
| Max | Agda.Syntax.Internal |
| maxDiscardRatio | Agda.Utils.QuickCheck |
| maxName | Agda.TypeChecking.Level |
| maxSize | Agda.Utils.QuickCheck |
| maxSuccess | Agda.Utils.QuickCheck |
| maxVarOcc | Agda.TypeChecking.Free.Lazy |
| maxViewCons | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| maxViewMax | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| maxViewSuc_ | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| Maybe | |
| 1 (Type/Class) | Agda.Utils.Maybe |
| 2 (Type/Class) | Agda.Utils.Maybe.Strict |
| 3 (Data Constructor) | Agda.TypeChecking.InstanceArguments |
| maybe | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| MaybeAbort | Agda.TypeChecking.Injectivity |
| maybeCoGen | Agda.Utils.TestHelpers |
| maybeFlexiblePattern | Agda.TypeChecking.Rules.LHS |
| maybeGen | Agda.Utils.TestHelpers |
| 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 |
| maybePrefixMatch | Agda.Utils.List |
| maybePrimCon | Agda.TypeChecking.Level |
| maybePrimDef | Agda.TypeChecking.Level |
| MaybeRed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MaybeReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MaybeReducedArgs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MaybeReducedElims | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| maybeRight | Agda.Utils.Either |
| maybeTimed | Agda.Interaction.InteractionTop |
| maybeToList | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| MaybeWarnings | Agda.Interaction.Imports |
| 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 |
| mcompoint | Agda.Auto.NarrowingSearch |
| mcons | Agda.Utils.List |
| 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.HashMap |
| 3 (Function) | Agda.Utils.Bag |
| 4 (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 | Agda.Utils.Parser.MemoisedCPS |
| MemoKey | Agda.Syntax.Concrete.Operators.Parser |
| memoRec | Agda.Utils.Memo |
| mentions | Agda.TypeChecking.SizedTypes.WarshallSolver |
| MentionsMeta | Agda.TypeChecking.MetaVars.Mention |
| mentionsMeta | Agda.TypeChecking.MetaVars.Mention |
| mergeGroups | Agda.Compiler.Epic.Injection |
| mergeHiding | Agda.Syntax.Common |
| mergeInterface | Agda.Interaction.Imports |
| mergeNames | Agda.Syntax.Scope.Base |
| mergeNotations | Agda.Syntax.Fixity |
| 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 |
| MetaCannotDependOn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MetaEnv | Agda.Auto.NarrowingSearch |
| 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 |
| 4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MetaInstantiation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MetaKind | Agda.TypeChecking.MetaVars |
| MetaLevel | Agda.Syntax.Internal |
| metaliseokh | Agda.Auto.Syntax |
| MetaNameSuggestion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| metaNameSuggestion | Agda.Syntax.Info |
| metaNumber | Agda.Syntax.Info |
| metaOccurs | Agda.TypeChecking.MetaVars.Occurs |
| MetaOccursInItself | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| metaParseExpr | Agda.Interaction.CommandLine |
| MetaPriority | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| metaRange | Agda.Syntax.Info |
| metaScope | Agda.Syntax.Info |
| MetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MetaV | Agda.Syntax.Internal |
| MetaVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Metavar | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| MetaVariable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| meta_not_constructor | Agda.Auto.Typecheck |
| MExp | Agda.Auto.Syntax |
| mextrarefs | Agda.Auto.NarrowingSearch |
| miClosRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MId | Agda.Auto.Syntax |
| Middle | Agda.Syntax.Common |
| miInterface | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| miMetaOccursCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mimicGHCi | Agda.Interaction.EmacsTop |
| miNameSuggestion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 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 |
| MissingClauses | Agda.Syntax.Internal |
| MissingDataSignature | Agda.Syntax.Concrete.Definitions |
| MissingDefinition | Agda.Syntax.Concrete.Definitions |
| MissingTypeSignature | Agda.Syntax.Concrete.Definitions |
| MissingWithClauses | Agda.Syntax.Concrete.Definitions |
| miWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MIx | |
| 1 (Type/Class) | Agda.Termination.SparseMatrix |
| 2 (Data Constructor) | Agda.Termination.SparseMatrix |
| Mixed | Agda.TypeChecking.Positivity.Occurrence |
| mIxInvariant | Agda.Termination.SparseMatrix |
| mkAbs | Agda.TypeChecking.Substitute |
| mkAbsolute | Agda.Utils.FileName |
| mkAlt | Agda.Compiler.UHC.Bridge |
| mkApp | Agda.Compiler.UHC.Bridge |
| mkBind1 | Agda.Compiler.UHC.Bridge |
| mkBind1Nm1 | Agda.Compiler.UHC.Bridge |
| mkBody | Agda.TypeChecking.Rules.Def |
| mkBoundName | Agda.Syntax.Concrete |
| mkBoundName_ | Agda.Syntax.Concrete |
| mkCall | Agda.Termination.CallGraph |
| mkCall' | Agda.Termination.CallGraph |
| mkCase | Agda.Compiler.UHC.Bridge |
| mkChar | Agda.Compiler.UHC.Bridge |
| mkCon | Agda.Compiler.Epic.Forcing |
| mkContextEntry | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| mkCTag | Agda.Compiler.UHC.Bridge |
| mkDefInfo | Agda.Syntax.Info |
| mkDefInfoInstance | Agda.Syntax.Info |
| mkError | Agda.Compiler.UHC.Bridge |
| mkExceptT | Agda.Utils.Except |
| mkExport | Agda.Compiler.UHC.Bridge |
| mkHsName | Agda.Compiler.UHC.Bridge |
| mkHsName1 | Agda.Compiler.UHC.Bridge |
| mkIfThenElse | Agda.Compiler.UHC.FromAgda |
| mkImport | Agda.Compiler.UHC.Bridge |
| mkInt | Agda.Compiler.UHC.Bridge |
| mkInteger | Agda.Compiler.UHC.Bridge |
| mkLam | |
| 1 (Function) | Agda.Compiler.UHC.Bridge |
| 2 (Function) | Agda.TypeChecking.Substitute |
| mkLet | |
| 1 (Function) | Agda.Syntax.Treeless |
| 2 (Function) | Agda.Syntax.Abstract |
| mkLet1Plain | Agda.Compiler.UHC.Bridge |
| mkLet1Strict | Agda.Compiler.UHC.Bridge |
| mkLetRec | Agda.Compiler.UHC.Bridge |
| mkMain | Agda.Compiler.UHC.Bridge |
| mkMatrix | Agda.Utils.Warshall |
| mkMetaData | Agda.Compiler.UHC.Bridge |
| mkMetaDataCon | Agda.Compiler.UHC.Bridge |
| mkMetaDataConFromCTag | Agda.Compiler.UHC.Bridge |
| mkModule | Agda.Compiler.UHC.Bridge |
| MkName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| mkName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| mkName_ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| mkNotation | Agda.Syntax.Notation |
| mkPatCon | Agda.Compiler.UHC.Bridge |
| mkPatFldBind | Agda.Compiler.UHC.Bridge |
| mkPatRestEmpty | Agda.Compiler.UHC.Bridge |
| mkPi | Agda.TypeChecking.Substitute |
| mkPrimFun1 | Agda.TypeChecking.Primitive |
| mkPrimFun1TCM | Agda.TypeChecking.Primitive |
| mkPrimFun2 | Agda.TypeChecking.Primitive |
| mkPrimFun4 | Agda.TypeChecking.Primitive |
| mkPrimLevelMax | Agda.TypeChecking.Primitive |
| mkPrimLevelSuc | Agda.TypeChecking.Primitive |
| mkPrimLevelZero | Agda.TypeChecking.Primitive |
| mkSet | Agda.Syntax.Translation.ReflectedToAbstract |
| mkShared | Agda.TypeChecking.Serialise.Base |
| mkString | Agda.Compiler.UHC.Bridge |
| mkTagTup | Agda.Compiler.UHC.Bridge |
| mkTApp | Agda.Syntax.Treeless |
| mkType | Agda.Syntax.Internal |
| mkUndefined | Agda.Compiler.UHC.Bridge |
| mkUniqueHsName | Agda.Compiler.UHC.Bridge |
| mkUnit | Agda.Compiler.UHC.Bridge |
| mkUnused | Agda.TypeChecking.Polarity |
| mkVar | Agda.Compiler.UHC.Bridge |
| mkWeakIORef | Agda.Utils.IORef |
| mlevel | Agda.TypeChecking.Level |
| MM | Agda.Auto.NarrowingSearch |
| mm | Agda.Auto.CaseSplit |
| 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.Abstract, Agda.Syntax.Internal |
| mnameFromList | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| mnameToConcrete | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| mnameToList | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| mnameToQName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| mobs | Agda.Auto.NarrowingSearch |
| Mode | Agda.Utils.Pretty |
| mode | Agda.Utils.Pretty |
| modFile | Agda.TypeChecking.Serialise.Base |
| modify' | Agda.Utils.Monad |
| modifyAbsoluteIncludePaths | Agda.Interaction.Options.Lenses |
| modifyAbstractClause | Agda.Auto.Convert |
| modifyAbstractExpr | Agda.Auto.Convert |
| modifyAllowedReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| modifyArgOccurrences | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| modifyAwakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| modifyBenchmark | |
| 1 (Function) | Agda.Utils.Benchmark |
| 2 (Function) | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| modifyCommandLineOptions | Agda.Interaction.Options.Lenses |
| modifyContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| modifyContextEntries | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| modifyContextEntry | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| modifyCurrentNameSpace | Agda.Syntax.Scope.Monad |
| modifyCurrentScope | Agda.Syntax.Scope.Monad |
| modifyCurrentScopeM | Agda.Syntax.Scope.Monad |
| modifyEI | Agda.Compiler.Epic.CompileState |
| modifyFunClauses | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| modifyGlobalDefinition | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| modifyImportedSignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| modifyIncludePaths | Agda.Interaction.Options.Lenses |
| modifyInstanceDefs | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| modifyInteractionPoints | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| modifyIORef | Agda.Utils.IORef |
| modifyIORef' | Agda.Utils.IORef |
| modifyLocalVars | Agda.Syntax.Scope.Monad |
| modifyMetaStore | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.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.TypeChecking.Monad |
| modifyPersistentState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| modifyPersistentVerbosity | Agda.Interaction.Options.Lenses |
| modifyPragmaOptions | Agda.Interaction.Options.Lenses |
| modifySafeMode | Agda.Interaction.Options.Lenses |
| modifyScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| modifyScopes | Agda.Syntax.Scope.Monad |
| modifyScope_ | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| modifySignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| modifySleepingConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| modifyStatistics | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad |
| modifyTheInteractionPoints | Agda.Interaction.InteractionTop |
| modifyVerbosity | Agda.Interaction.Options.Lenses |
| modName | Agda.Compiler.JS.Syntax |
| modname | Agda.Compiler.JS.Pretty |
| Module | |
| 1 (Type/Class) | Agda.Compiler.JS.Syntax |
| 2 (Data Constructor) | Agda.Compiler.JS.Syntax |
| 3 (Type/Class) | Agda.Syntax.Concrete |
| 4 (Data Constructor) | Agda.Syntax.Concrete |
| 5 (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 |
| ModuleAssignment | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| ModuleContents | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| moduleContents | Agda.Interaction.BasicOps |
| ModuleDefinedInOtherFile | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ModuleDoesntExport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 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 |
| 4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ModuleMacro | Agda.Syntax.Concrete |
| ModuleName | |
| 1 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| 2 (Type/Class) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| moduleName | Agda.Interaction.FindFile |
| moduleName' | Agda.Interaction.FindFile |
| ModuleNameDoesntMatchFileName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| moduleNameParser | |
| 1 (Function) | Agda.Syntax.Parser.Parser |
| 2 (Function) | Agda.Syntax.Parser |
| moduleNameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| moduleNameToCoreName | Agda.Compiler.UHC.CompileState |
| moduleNameToCoreNameParts | Agda.Compiler.UHC.CompileState |
| moduleNameToFileName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| moduleParser | |
| 1 (Function) | Agda.Syntax.Parser.Parser |
| 2 (Function) | Agda.Syntax.Parser |
| ModulesInScope | Agda.Syntax.Scope.Base |
| ModuleTag | Agda.Syntax.Scope.Base |
| ModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MonadBench | Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| MonadChange | Agda.Utils.Update |
| MonadError | Agda.Utils.Except |
| MonadException | Agda.TypeChecking.Monad.Exception |
| MonadGetDefs | Agda.Syntax.Internal.Defs |
| MonadPlus | Agda.Utils.Monad |
| MonadTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MonadTer | Agda.Termination.Monad |
| monomorphic | Agda.Utils.QuickCheck |
| moreRelevant | Agda.Syntax.Common |
| movePos | Agda.Syntax.Position |
| movePosByString | Agda.Syntax.Position |
| mparens | Agda.Utils.Pretty |
| MPat | Agda.TypeChecking.Coverage.Match |
| mplus | Agda.Utils.Monad |
| mpret | Agda.Auto.NarrowingSearch |
| mprincipalpresent | Agda.Auto.NarrowingSearch |
| mul | |
| 1 (Function) | Agda.Termination.Semiring |
| 2 (Function) | Agda.Termination.SparseMatrix |
| MultipleFixityDecls | Agda.Syntax.Concrete.Definitions |
| multiply | Agda.Termination.Semiring |
| munch | Agda.Utils.Parser.ReadP |
| munch1 | Agda.Utils.Parser.ReadP |
| mustBeFinite | Agda.TypeChecking.SizedTypes.WarshallSolver |
| mustBePi | Agda.TypeChecking.Telescope |
| MutId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Mutual | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| mutualBlockOf | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| mutualChecks | Agda.TypeChecking.Rules.Decl |
| MutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MutualInfo | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| mutuallyRecursive | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| MutualNames | Agda.Termination.Monad |
| mutualPositivityCheck | Agda.Syntax.Info |
| mutualRange | Agda.Syntax.Info |
| mutualTermCheck | Agda.Syntax.Info |
| mvFrozen | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mvInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mvInstantiation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mvJudgement | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mvListeners | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mvPermutation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mvPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MyMB | Agda.Auto.Syntax |
| MyPB | Agda.Auto.Syntax |
| mzero | Agda.Utils.Monad |