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

Index - M

mainAgda.Main
mainNameAgda.Compiler.Epic.Interface
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
makeForcedArgsAgda.Compiler.Epic.ForceConstrs
makeInstanceAgda.Syntax.Common
makeOpenAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
makeProjectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
makeSilentAgda.Interaction.GhciTop
makeSubstitutionAgda.TypeChecking.Rules.LHS.Unify
MAlonzoAgda.Interaction.GhciTop
manyAgda.Utils.ReadP
many1Agda.Utils.ReadP
manyTillAgda.Utils.ReadP
mapAgda.Compiler.JS.Substitution
map'Agda.Compiler.JS.Substitution
mapConAgda.Compiler.Epic.Primitive
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
mappingAgda.Compiler.JS.Compiler
mapping'Agda.Compiler.JS.Compiler
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
markStaticAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
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.Compiler.JS.Case
2 (Function)Agda.TypeChecking.Coverage.Match
3 (Function)Agda.Syntax.Parser.LookAhead
4 (Function)Agda.Interaction.Highlighting.Vim
5 (Function)Agda.TypeChecking.DisplayForm
6 (Function)Agda.TypeChecking.CompiledClause.Match
match' 
1 (Function)Agda.Syntax.Parser.LookAhead
2 (Function)Agda.TypeChecking.CompiledClause.Match
matchClauseAgda.TypeChecking.Coverage.Match
matchCommandAgda.Interaction.CommandLine.CommandLine
matchCompiledAgda.TypeChecking.CompiledClause.Match
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
matchTypeAgda.Auto.Convert
Matrix 
1 (Type/Class)Agda.Termination.SparseMatrix
2 (Type/Class)Agda.Termination.Matrix
3 (Type/Class)Agda.Utils.Warshall
matrix 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
3 (Function)Agda.Utils.Warshall
matrixInvariant 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
matrixUsingRowGen 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
MaxAgda.Syntax.Internal
maxDiscardAgda.Utils.QuickCheck
maxNameAgda.TypeChecking.Level
maxSizeAgda.Utils.QuickCheck
maxSuccessAgda.Utils.QuickCheck
MaybeAgda.Utils.Maybe
maybeAgda.Utils.Maybe
maybeCoGenAgda.Utils.TestHelpers
maybeGenAgda.Utils.TestHelpers
maybeorAgda.Auto.Typecheck
maybePrefixMatchAgda.Utils.List
maybePrimConAgda.TypeChecking.Level
maybePrimDefAgda.TypeChecking.Level
MaybeRedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MaybeReducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MaybeReducedArgsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
maybeToListAgda.Utils.Maybe
MayNotPostponeAgda.TypeChecking.Rules.LHS.Unify
MayPostponeAgda.TypeChecking.Rules.LHS.Unify
mazBoolToHBoolAgda.Compiler.MAlonzo.Primitives
mazCharToIntegerAgda.Compiler.MAlonzo.Primitives
mazCoerceAgda.Compiler.MAlonzo.Misc
mazerrorAgda.Compiler.MAlonzo.Misc
mazHBoolToBoolAgda.Compiler.MAlonzo.Primitives
mazHListToListAgda.Compiler.MAlonzo.Primitives
mazIncompleteMatchAgda.Compiler.MAlonzo.Misc
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
mazRTEAgda.Compiler.MAlonzo.Misc
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
memberAgda.Utils.VarSet
MemberId 
1 (Type/Class)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
MentionsMetaAgda.TypeChecking.MetaVars.Mention
mentionsMetaAgda.TypeChecking.MetaVars.Mention
mergeGroupsAgda.Compiler.Epic.Injection
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
MetaElimAgda.TypeChecking.Eliminators
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
MetaInstantiationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaKindAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
MetaLevelAgda.Syntax.Internal
metaliseokhAgda.Auto.Syntax
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
metaScopeAgda.Syntax.Info
MetaShAgda.TypeChecking.Rules.LHS.Unify
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
meta_not_constructorAgda.Auto.Typecheck
MExpAgda.Auto.Syntax
mextrarefsAgda.Auto.NarrowingSearch
mheadAgda.Utils.List
MIdAgda.Auto.Syntax
miInterfaceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
minfoAsNameAgda.Syntax.Info
minfoAsToAgda.Syntax.Info
minfoDirectiveAgda.Syntax.Info
minfoOpenShortAgda.Syntax.Info
minfoRangeAgda.Syntax.Info
MissingDataSignatureAgda.Syntax.Concrete.Definitions
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.SparseMatrix
2 (Data Constructor)Agda.Termination.SparseMatrix
3 (Type/Class)Agda.Termination.Matrix
4 (Data Constructor)Agda.Termination.Matrix
mIxInvariant 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
mkAbsAgda.TypeChecking.Substitute
mkAbsoluteAgda.Utils.FileName, Agda.Interaction.GhciTop
mkBoundName_Agda.Syntax.Concrete
mkConAgda.Compiler.Epic.Forcing
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
mkNotationAgda.Syntax.Notation
mkPrimFun1Agda.TypeChecking.Primitive
mkPrimFun1TCMAgda.TypeChecking.Primitive
mkPrimFun2Agda.TypeChecking.Primitive
mkPrimFun4Agda.TypeChecking.Primitive
mkPrimLevelMaxAgda.TypeChecking.Primitive
mkPrimLevelSucAgda.TypeChecking.Primitive
mkPrimLevelZeroAgda.TypeChecking.Primitive
mkQAgda.Utils.Generics
MkStrAgda.Utils.QuickCheck
mkTypeAgda.Syntax.Internal
mlevelAgda.TypeChecking.Conversion
MMAgda.Auto.NarrowingSearch
mmAgda.Auto.CaseSplit
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
mnameToQNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mobsAgda.Auto.NarrowingSearch
ModeAgda.Utils.Pretty
modeAgda.Utils.Pretty
modifyAbstractClauseAgda.Auto.Convert
modifyAbstractExprAgda.Auto.Convert
modifyArgRelevanceAgda.TypeChecking.Irrelevance
modifyContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
modifyContextEntriesAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
modifyContextEntryAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
modifyCurrentNameSpaceAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyCurrentScopeAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyCurrentScopeMAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyEIAgda.Compiler.Epic.CompileState
modifyImportedSignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
modifyMetaStoreAgda.TypeChecking.Monad.MetaVars, 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
modNameAgda.Compiler.JS.Syntax
modnameAgda.Compiler.JS.Pretty
modSubAgda.TypeChecking.Rules.LHS.Unify
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
ModuleArityMismatchAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
moduleContentsAgda.Interaction.BasicOps
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.FindFile
moduleName'Agda.Interaction.FindFile
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
ModuleTagAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ModuleToSourceAgda.Interaction.FindFile
MonadExceptionAgda.TypeChecking.Monad.Exception
MonadTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
moreRelevantAgda.Syntax.Common
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
mul 
1 (Function)Agda.Termination.Semiring
2 (Function)Agda.Termination.SparseMatrix
3 (Function)Agda.Termination.Matrix
MultipleFixityDeclsAgda.Syntax.Concrete.Definitions
multiplyAgda.Termination.Semiring
munchAgda.Utils.ReadP
munch1Agda.Utils.ReadP
MutIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Mutual 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
MutualIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvFrozenAgda.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
mvPermutationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvPriorityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MyMBAgda.Auto.Syntax
MyPBAgda.Auto.Syntax