machine_gen | Idris.Core.TT |
machine_inf | Idris.AbsSyntaxTree, Idris.AbsSyntax |
make | Idris.Package |
MakeCase | Idris.REPL.Commands |
makeCase | Idris.Interactive |
MakeCaseBlock | Idris.IdeMode |
MakeDoc | Idris.REPL.Commands |
makefile | Idris.Package.Common |
makeFn | IRTS.Lang, IRTS.Defunctionalise |
MakeLemma | |
1 (Data Constructor) | Idris.IdeMode |
2 (Data Constructor) | Idris.REPL.Commands |
makeLemma | Idris.Interactive |
makeTarget | Idris.Package |
MakeWith | Idris.REPL.Commands |
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 |
Mark | Idris.Parser.Stack, Idris.Parser.Helpers |
mark | Idris.Parser.Stack, Idris.Parser.Helpers |
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 |
mergeOptions | Idris.Package |
Message | Idris.Output |
messageExtent | Idris.Output |
messageSource | Idris.Output |
messageText | Idris.Output |
MetaInformation | Idris.Core.Evaluate |
MetaN | Idris.Core.TT |
MetaVarArg | Idris.Help |
Metavariables | Idris.IdeMode |
metavarName | Idris.Elab.Term |
MetavarOutput | Idris.Core.TT |
Metavars | Idris.REPL.Commands |
MethodN | Idris.Core.TT |
Missing | Idris.REPL.Commands |
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 |
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 |
mkType | Idris.Parser.Expr |
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 |
ModImport | Idris.REPL.Commands |
ModuleArg | Idris.Help |
moduleName | 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 |
MoveLast | Idris.Core.ProofState, Idris.Core.Elaborate |
movelast | Idris.Core.Elaborate |
moveReg | IRTS.Bytecode |
Msg | Idris.Core.TT |
MTree | Idris.Chaser |
Mutual | Idris.Core.Evaluate |
mutual_types | Idris.Core.TT |
mut_nesting | Idris.AbsSyntaxTree, Idris.AbsSyntax |