| machine_gen | Idris.Core.TT |
| machine_inf | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| make | Idris.Package |
| MakeCase | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| makeCase | Idris.Interactive |
| MakeCaseBlock | Idris.IdeMode |
| MakeDoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| makefile | Idris.Package.Common |
| MakeLemma | |
| 1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.IdeMode |
| makeLemma | Idris.Interactive |
| MakeWith | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| makeWith | Idris.Interactive |
| MakeWithBlock | Idris.IdeMode |
| Many | Idris.Core.Typecheck |
| ManyArgs | Idris.Help |
| mapCtxt | Idris.Core.TT |
| mapDefCtxt | Idris.Core.Evaluate |
| mapPDataFC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mapPDeclFC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mapPT | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mapPTermFC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mapRHS | Idris.Elab.Clause |
| mapRHSdecl | Idris.Elab.Clause |
| mapsnd | Idris.AbsSyntax |
| Match | Idris.Core.Unify |
| matchClause | Idris.AbsSyntax |
| matchClause' | Idris.AbsSyntax |
| MatchFill | Idris.Core.ProofState, Idris.Core.Elaborate |
| MatchProblems | Idris.Core.ProofState, Idris.Core.Elaborate |
| matchProblems | Idris.Core.Elaborate |
| MatchRefine | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| match_apply | Idris.Core.Elaborate |
| match_fill | Idris.Core.Elaborate |
| match_unify | Idris.Core.Unify |
| maxline | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| MaybeHoles | Idris.Core.TT |
| maybeWithNS | Idris.Parser.Helpers, Idris.Parser |
| mergeOptions | Idris.Package |
| MetaInformation | Idris.Core.Evaluate |
| MetaN | Idris.Core.TT |
| MetaVarArg | Idris.Help |
| Metavariables | Idris.IdeMode |
| metavarName | Idris.Elab.Term |
| MetavarOutput | Idris.Core.TT |
| Metavars | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| MethodN | Idris.Core.TT |
| Missing | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mkApp | Idris.Core.TT |
| mkApply | IRTS.Defunctionalise |
| mkApply2 | IRTS.Defunctionalise |
| mkApplyCase | IRTS.Defunctionalise |
| mkBigCase | IRTS.Defunctionalise |
| MKCON | IRTS.Bytecode |
| mkDirCmd | Idris.Package |
| mkEval | IRTS.Defunctionalise |
| mkFieldName | Idris.Erasure |
| mkFnCon | IRTS.Defunctionalise |
| mkForce | Idris.Core.CaseTree |
| mkList | Idris.Reflection |
| mkMultiPaths | Idris.Coverage |
| mkName | Idris.Parser.Helpers, Idris.Parser |
| mkPApp | Idris.AbsSyntax |
| mkPatTm | Idris.Coverage |
| mkPE_TermDecl | Idris.PartialEval |
| mkPE_TyDecl | Idris.PartialEval |
| mkProofTerm | Idris.Core.ProofTerm |
| mkStatic | Idris.Elab.Utils |
| mkStaticTy | Idris.Elab.Utils |
| mkTTName | Idris.DSL |
| mkType | Idris.Parser.Expr, Idris.Parser |
| mkUnderCon | IRTS.Defunctionalise |
| mkUniqueNames | Idris.AbsSyntax |
| mkWith | Idris.CaseSplit |
| MN | Idris.Core.TT |
| ModDoc | Idris.Docs |
| modDocName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| modifyConst | Idris.Parser.Expr, Idris.Parser |
| ModImport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ModuleArg | Idris.Help |
| moduleHeader | Idris.Parser |
| modules | Idris.Package.Common |
| ModuleTree | Idris.Chaser |
| module_aliases | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| mod_deps | Idris.Chaser |
| mod_needsRecheck | Idris.Chaser |
| mod_path | Idris.Chaser |
| mod_time | Idris.Chaser |
| MonadicParsing | Idris.Parser.Helpers, Idris.Parser |
| MoveLast | Idris.Core.ProofState, Idris.Core.Elaborate |
| movelast | Idris.Core.Elaborate |
| moveReg | IRTS.Bytecode |
| Msg | Idris.Core.TT |
| MTree | Idris.Chaser |
| multiLineComment | Idris.Parser.Helpers, Idris.Parser |
| MultiPath | Idris.Coverage |
| Mutual | Idris.Core.Evaluate |
| mutual | Idris.Parser |
| mutual_types | Idris.Core.TT |
| mut_nesting | Idris.AbsSyntaxTree, Idris.AbsSyntax |