Agda-2.2.6: A dependently typed functional programming language and proof assistantContentsIndex
ABCDEFGHIJKLMNOPQRSTUVWXYZ!$+./<=>|-
Index (M)
main
makeAbstract
makeAbstractClause
makeAbsurdClause
makeCase
makeClosed
makeConfiguration
makeEnv
makeIncludeDirsAbsolute
makeOpen
makeSubstitution
malonzoDir
many
many1
manyTill
mapFlag
mapMaybe
mapMaybeM
mapNameSpace
mapNameSpaceM
mapNodes
MapS
mapScope
mapScopeM
mapScopeM_
mapScope_
mapSize
mapTCMT
MArgList
Mat
mat
Match
1 (Type/Class)
2 (Type/Class)
3 (Type/Class)
match
1 (Function)
2 (Function)
3 (Function)
4 (Function)
match'
matchCall
matchCalls
matchClause
matchCommand
matchDisplayForm
matches
MatchLit
matchLits
matchPat
matchPats
matchPattern
matchPatterns
matchTrace
Matrix
1 (Type/Class)
2 (Type/Class)
matrix
1 (Function)
2 (Function)
matrixInvariant
matrixUsingRowGen
Max
maxDiscard
maxName
maxSize
maxSuccess
Maybe
maybe
maybeCoGen
maybeGen
maybePrefixMatch
maybePrimCon
maybePrimDef
maybeQualConName
maybeQualDefName
maybeQualName
maybeToList
mazBoolToHBool
mazCharToInteger
mazCoerce
mazerror
mazHBoolToBool
mazHListToList
mazIntegerToNat
mazIntToNat
mazListToHList
mazListToString
mazMod
mazMod'
mazName
mazNatToInt
mazNatToInteger
mazstr
mazStringToList
MB
mbcase
mbfailed
mbind
mbpcase
mbret
mcompoint
mergeInterface
mergeNames
mergeScope
mergeScopes
Meta
MetaArg
MetaCannotDependOn
MetaEnv
MetaId
1 (Type/Class)
2 (Data Constructor)
MetaInfo
1 (Type/Class)
2 (Data Constructor)
3 (Type/Class)
4 (Data Constructor)
5 (Type/Class)
metaInstance
MetaInstantiation
MetaLevel
metaNumber
MetaOccursInItself
metaParseExpr
MetaPriority
1 (Type/Class)
2 (Data Constructor)
metaRange
MetaS
metaScope
MetaStore
MetaV
MetaVar
Metavar
1 (Type/Class)
2 (Data Constructor)
MetaVariable
metaVariable
MExp
MId
miInterface
minfoAsName
minfoAsTo
minfoRange
MissingDefinition
MissingTypeSignature
MissingWithClauses
miTimeStamp
miWarnings
MIx
1 (Type/Class)
2 (Data Constructor)
mIxInvariant
mkAbsolute
mkBoundName_
mkContextEntry
mkDefInfo
mkMatrix
mkName
mkName_
mkPrimFun1
mkPrimFun2
mkPrimFun4
MkStr
mkType
MM
mmbpcase
mmcase
mmmcase
mmpcase
MName
mnameFromList
mnameToConcrete
mnameToList
mobs
Mode
mode
modifyCurrentNameSpace
modifyCurrentScope
modifyCurrentScopeM
modifyImportedSignature
modifyNamedScope
modifyNamedScopeM
modifyScope
modifyScopeInfo
modifyScopes
modifySignature
modSub
Module
1 (Type/Class)
2 (Data Constructor)
3 (Data Constructor)
ModuleArityMismatch
ModuleDefinedInOtherFile
ModuleDoesntExport
ModuleInfo
1 (Type/Class)
2 (Data Constructor)
3 (Type/Class)
4 (Data Constructor)
ModuleMacro
ModuleName
moduleName
moduleName'
ModuleNameDoesntMatchFileName
moduleNameParts
moduleNameToFileName
moduleParser
1 (Function)
2 (Function)
ModulesInScope
moduleStr
ModuleTag
ModuleToSource
MonadException
MonadTCM
movePos
movePosByString
mparen
mparens
MPat
mpret
mprincipalpresent
msubs
mul
1 (Function)
2 (Function)
MultipleFixityDecls
munch
munch1
MutId
Mutual
MutualId
mvInfo
mvInstantiation
mvJudgement
mvListeners
mvPriority
MyMB
MyPB