Agda-2.2.6: A dependently typed functional programming language and proof assistant

Index - M

mainAgda.Main
makeAbstractAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
makeAbstractClauseAgda.Interaction.MakeCase
makeAbsurdClauseAgda.Interaction.MakeCase
makeCaseAgda.Interaction.MakeCase
makeClosedAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
makeConfigurationAgda.TypeChecking.Test.Generators
makeEnvAgda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
makeIncludeDirsAbsoluteAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
makeOpenAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
makeSubstitutionAgda.TypeChecking.Rules.LHS.Unify
malonzoDirAgda.Compiler.MAlonzo.Compiler
manyAgda.Utils.ReadP
many1Agda.Utils.ReadP
manyTillAgda.Utils.ReadP
mapFlagAgda.Interaction.Options
mapMaybeAgda.Utils.Maybe
mapMaybeMAgda.Utils.Monad
mapNameSpaceAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapNameSpaceMAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapNodesAgda.Utils.Warshall
MapSAgda.Auto.Convert
mapScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapScopeMAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapScopeM_Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapScope_Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapSizeAgda.Utils.QuickCheck
mapTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MArgListAgda.Auto.Syntax
MatAgda.Termination.CallGraph
matAgda.Termination.CallGraph
Match 
1 (Type/Class)Agda.TypeChecking.Coverage.Match
2 (Type/Class)Agda.TypeChecking.Patterns.Match
3 (Type/Class)Agda.TypeChecking.DisplayForm
match 
1 (Function)Agda.TypeChecking.Coverage.Match
2 (Function)Agda.Syntax.Parser.LookAhead
3 (Function)Agda.Interaction.Highlighting.Vim
4 (Function)Agda.TypeChecking.DisplayForm
match'Agda.Syntax.Parser.LookAhead
matchCallAgda.Utils.Trace
matchCallsAgda.Utils.Trace
matchClauseAgda.TypeChecking.Coverage.Match
matchCommandAgda.Interaction.CommandLine.CommandLine
matchDisplayFormAgda.TypeChecking.DisplayForm
matchesAgda.Interaction.Highlighting.Vim
MatchLitAgda.TypeChecking.Coverage.Match
matchLitsAgda.TypeChecking.Coverage.Match
matchPatAgda.TypeChecking.Coverage.Match
matchPatsAgda.TypeChecking.Coverage.Match
matchPatternAgda.TypeChecking.Patterns.Match
matchPatternsAgda.TypeChecking.Patterns.Match
matchTraceAgda.Utils.Trace
Matrix 
1 (Type/Class)Agda.Termination.Matrix
2 (Type/Class)Agda.Utils.Warshall
matrix 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Utils.Warshall
matrixInvariantAgda.Termination.Matrix
matrixUsingRowGenAgda.Termination.Matrix
MaxAgda.TypeChecking.Level
maxDiscardAgda.Utils.QuickCheck
maxNameAgda.TypeChecking.Level
maxSizeAgda.Utils.QuickCheck
maxSuccessAgda.Utils.QuickCheck
MaybeAgda.Utils.Maybe
maybeAgda.Utils.Maybe
maybeCoGenAgda.Utils.TestHelpers
maybeGenAgda.Utils.TestHelpers
maybePrefixMatchAgda.Utils.List
maybePrimConAgda.TypeChecking.Level
maybePrimDefAgda.TypeChecking.Level
maybeQualConNameAgda.Compiler.Alonzo.Main
maybeQualDefNameAgda.Compiler.Alonzo.Main
maybeQualNameAgda.Compiler.Alonzo.Main
maybeToListAgda.Utils.Maybe
mazBoolToHBoolAgda.Compiler.MAlonzo.Primitives
mazCharToIntegerAgda.Compiler.MAlonzo.Primitives
mazCoerceAgda.Compiler.MAlonzo.Misc
mazerrorAgda.Compiler.MAlonzo.Misc
mazHBoolToBoolAgda.Compiler.MAlonzo.Primitives
mazHListToListAgda.Compiler.MAlonzo.Primitives
mazIntegerToNatAgda.Compiler.MAlonzo.Primitives
mazIntToNatAgda.Compiler.MAlonzo.Primitives
mazListToHListAgda.Compiler.MAlonzo.Primitives
mazListToStringAgda.Compiler.MAlonzo.Primitives
mazModAgda.Compiler.MAlonzo.Misc
mazMod'Agda.Compiler.MAlonzo.Misc
mazNameAgda.Compiler.MAlonzo.Misc
mazNatToIntAgda.Compiler.MAlonzo.Primitives
mazNatToIntegerAgda.Compiler.MAlonzo.Primitives
mazstrAgda.Compiler.MAlonzo.Misc
mazStringToListAgda.Compiler.MAlonzo.Primitives
MBAgda.Auto.NarrowingSearch
mbcaseAgda.Auto.NarrowingSearch
mbfailedAgda.Auto.NarrowingSearch
mbindAgda.Auto.NarrowingSearch
mbpcaseAgda.Auto.NarrowingSearch
mbretAgda.Auto.NarrowingSearch
mcompointAgda.Auto.NarrowingSearch
mergeInterfaceAgda.Interaction.Imports
mergeNamesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mergeScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mergeScopesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
MetaAgda.Auto.NarrowingSearch
MetaArgAgda.TypeChecking.Positivity
MetaCannotDependOnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaEnvAgda.Auto.NarrowingSearch
MetaId 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
MetaInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
3 (Type/Class)Agda.Interaction.Highlighting.Precise
4 (Data Constructor)Agda.Interaction.Highlighting.Precise
5 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
metaInstanceAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
MetaInstantiationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaLevelAgda.TypeChecking.Level
metaNumberAgda.Syntax.Info
MetaOccursInItselfAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
metaParseExprAgda.Interaction.CommandLine.CommandLine
MetaPriority 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
metaRangeAgda.Syntax.Info
MetaSAgda.Syntax.Internal
metaScopeAgda.Syntax.Info
MetaStoreAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaVAgda.Syntax.Internal
MetaVarAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Metavar 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
MetaVariableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
metaVariableAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
MExpAgda.Auto.Syntax
MIdAgda.Auto.Syntax
miInterfaceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
minfoAsNameAgda.Syntax.Info
minfoAsToAgda.Syntax.Info
minfoRangeAgda.Syntax.Info
MissingDefinitionAgda.Syntax.Concrete.Definitions
MissingTypeSignatureAgda.Syntax.Concrete.Definitions
MissingWithClausesAgda.Syntax.Concrete.Definitions
miTimeStampAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
miWarningsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MIx 
1 (Type/Class)Agda.Termination.Matrix
2 (Data Constructor)Agda.Termination.Matrix
mIxInvariantAgda.Termination.Matrix
mkAbsoluteAgda.Utils.FileName, Agda.Interaction.GhciTop
mkBoundName_Agda.Syntax.Concrete
mkContextEntryAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
mkDefInfoAgda.Syntax.Info
mkMatrixAgda.Utils.Warshall
mkNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mkName_Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mkPrimFun1Agda.TypeChecking.Primitive
mkPrimFun2Agda.TypeChecking.Primitive
mkPrimFun4Agda.TypeChecking.Primitive
MkStrAgda.Utils.QuickCheck
mkTypeAgda.Syntax.Internal
MMAgda.Auto.NarrowingSearch
mmbpcaseAgda.Auto.NarrowingSearch
mmcaseAgda.Auto.NarrowingSearch
mmmcaseAgda.Auto.NarrowingSearch
mmpcaseAgda.Auto.NarrowingSearch
MNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mnameFromListAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mnameToConcreteAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mnameToListAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mobsAgda.Auto.NarrowingSearch
ModeAgda.Utils.Pretty
modeAgda.Utils.Pretty
modifyCurrentNameSpaceAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyCurrentScopeAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyCurrentScopeMAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyImportedSignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
modifyNamedScopeAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyNamedScopeMAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
modifyScopeInfoAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyScopesAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifySignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
modSubAgda.TypeChecking.Rules.LHS.Unify
Module 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Interaction.Highlighting.Precise
ModuleArityMismatchAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ModuleDefinedInOtherFileAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ModuleDoesntExportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
ModuleMacroAgda.Syntax.Concrete
ModuleNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
moduleNameAgda.Interaction.Imports
moduleName'Agda.Interaction.Imports
ModuleNameDoesntMatchFileNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
moduleNamePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
moduleNameToFileNameAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
moduleParser 
1 (Function)Agda.Syntax.Parser.Parser
2 (Function)Agda.Syntax.Parser, Agda.Interaction.GhciTop
ModulesInScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
moduleStrAgda.Compiler.Alonzo.Names
ModuleTagAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ModuleToSourceAgda.Interaction.FindFile
MonadExceptionAgda.TypeChecking.Monad.Exception
MonadTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
movePosAgda.Syntax.Position, Agda.Interaction.GhciTop
movePosByStringAgda.Syntax.Position, Agda.Interaction.GhciTop
mparenAgda.Syntax.Concrete.Operators
mparensAgda.Utils.Pretty
MPatAgda.TypeChecking.Coverage.Match
mpretAgda.Auto.NarrowingSearch
mprincipalpresentAgda.Auto.NarrowingSearch
msubsAgda.Auto.Typecheck
mul 
1 (Function)Agda.Termination.Semiring
2 (Function)Agda.Termination.Matrix
MultipleFixityDeclsAgda.Syntax.Concrete.Definitions
munchAgda.Utils.ReadP
munch1Agda.Utils.ReadP
MutIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MutualAgda.Syntax.Concrete
MutualIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvInfoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvInstantiationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvJudgementAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvListenersAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvPriorityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MyMBAgda.Auto.Syntax
MyPBAgda.Auto.Syntax