main | Agda.Main |
makeAbstract | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
makeAbstractClause | Agda.Interaction.MakeCase |
makeAbsurdClause | Agda.Interaction.MakeCase |
makeCase | Agda.Interaction.MakeCase |
makeClosed | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad |
makeConfiguration | Agda.TypeChecking.Test.Generators |
makeEnv | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
makeIncludeDirsAbsolute | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
makeOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad |
makeSubstitution | Agda.TypeChecking.Rules.LHS.Unify |
malonzoDir | Agda.Compiler.MAlonzo.Compiler |
many | Agda.Utils.ReadP |
many1 | Agda.Utils.ReadP |
manyTill | Agda.Utils.ReadP |
mapFlag | Agda.Interaction.Options |
mapMaybe | Agda.Utils.Maybe |
mapMaybeM | Agda.Utils.Monad |
mapNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
mapNameSpaceM | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
mapNodes | Agda.Utils.Warshall |
MapS | Agda.Auto.Convert |
mapScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
mapScopeM | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
mapScopeM_ | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
mapScope_ | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
mapSize | Agda.Utils.QuickCheck |
mapTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MArgList | Agda.Auto.Syntax |
Mat | Agda.Termination.CallGraph |
mat | Agda.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 |
matchCall | Agda.Utils.Trace |
matchCalls | Agda.Utils.Trace |
matchClause | Agda.TypeChecking.Coverage.Match |
matchCommand | Agda.Interaction.CommandLine.CommandLine |
matchDisplayForm | Agda.TypeChecking.DisplayForm |
matches | Agda.Interaction.Highlighting.Vim |
MatchLit | Agda.TypeChecking.Coverage.Match |
matchLits | Agda.TypeChecking.Coverage.Match |
matchPat | Agda.TypeChecking.Coverage.Match |
matchPats | Agda.TypeChecking.Coverage.Match |
matchPattern | Agda.TypeChecking.Patterns.Match |
matchPatterns | Agda.TypeChecking.Patterns.Match |
matchTrace | Agda.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 |
matrixInvariant | Agda.Termination.Matrix |
matrixUsingRowGen | Agda.Termination.Matrix |
Max | Agda.TypeChecking.Level |
maxDiscard | Agda.Utils.QuickCheck |
maxName | Agda.TypeChecking.Level |
maxSize | Agda.Utils.QuickCheck |
maxSuccess | Agda.Utils.QuickCheck |
Maybe | Agda.Utils.Maybe |
maybe | Agda.Utils.Maybe |
maybeCoGen | Agda.Utils.TestHelpers |
maybeGen | Agda.Utils.TestHelpers |
maybePrefixMatch | Agda.Utils.List |
maybePrimCon | Agda.TypeChecking.Level |
maybePrimDef | Agda.TypeChecking.Level |
maybeQualConName | Agda.Compiler.Alonzo.Main |
maybeQualDefName | Agda.Compiler.Alonzo.Main |
maybeQualName | Agda.Compiler.Alonzo.Main |
maybeToList | Agda.Utils.Maybe |
mazBoolToHBool | Agda.Compiler.MAlonzo.Primitives |
mazCharToInteger | Agda.Compiler.MAlonzo.Primitives |
mazCoerce | Agda.Compiler.MAlonzo.Misc |
mazerror | Agda.Compiler.MAlonzo.Misc |
mazHBoolToBool | Agda.Compiler.MAlonzo.Primitives |
mazHListToList | Agda.Compiler.MAlonzo.Primitives |
mazIntegerToNat | Agda.Compiler.MAlonzo.Primitives |
mazIntToNat | Agda.Compiler.MAlonzo.Primitives |
mazListToHList | Agda.Compiler.MAlonzo.Primitives |
mazListToString | Agda.Compiler.MAlonzo.Primitives |
mazMod | Agda.Compiler.MAlonzo.Misc |
mazMod' | Agda.Compiler.MAlonzo.Misc |
mazName | Agda.Compiler.MAlonzo.Misc |
mazNatToInt | Agda.Compiler.MAlonzo.Primitives |
mazNatToInteger | Agda.Compiler.MAlonzo.Primitives |
mazstr | Agda.Compiler.MAlonzo.Misc |
mazStringToList | Agda.Compiler.MAlonzo.Primitives |
MB | Agda.Auto.NarrowingSearch |
mbcase | Agda.Auto.NarrowingSearch |
mbfailed | Agda.Auto.NarrowingSearch |
mbind | Agda.Auto.NarrowingSearch |
mbpcase | Agda.Auto.NarrowingSearch |
mbret | Agda.Auto.NarrowingSearch |
mcompoint | Agda.Auto.NarrowingSearch |
mergeInterface | Agda.Interaction.Imports |
mergeNames | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
mergeScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
mergeScopes | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
Meta | Agda.Auto.NarrowingSearch |
MetaArg | Agda.TypeChecking.Positivity |
MetaCannotDependOn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MetaEnv | Agda.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 |
metaInstance | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
MetaInstantiation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MetaLevel | Agda.TypeChecking.Level |
metaNumber | Agda.Syntax.Info |
MetaOccursInItself | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
metaParseExpr | Agda.Interaction.CommandLine.CommandLine |
MetaPriority | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
metaRange | Agda.Syntax.Info |
MetaS | Agda.Syntax.Internal |
metaScope | Agda.Syntax.Info |
MetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MetaV | Agda.Syntax.Internal |
MetaVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Metavar | |
1 (Type/Class) | Agda.Auto.NarrowingSearch |
2 (Data Constructor) | Agda.Auto.NarrowingSearch |
MetaVariable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
metaVariable | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
MExp | Agda.Auto.Syntax |
MId | Agda.Auto.Syntax |
miInterface | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
minfoAsName | Agda.Syntax.Info |
minfoAsTo | Agda.Syntax.Info |
minfoRange | Agda.Syntax.Info |
MissingDefinition | Agda.Syntax.Concrete.Definitions |
MissingTypeSignature | Agda.Syntax.Concrete.Definitions |
MissingWithClauses | Agda.Syntax.Concrete.Definitions |
miTimeStamp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
miWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MIx | |
1 (Type/Class) | Agda.Termination.Matrix |
2 (Data Constructor) | Agda.Termination.Matrix |
mIxInvariant | Agda.Termination.Matrix |
mkAbsolute | Agda.Utils.FileName, Agda.Interaction.GhciTop |
mkBoundName_ | Agda.Syntax.Concrete |
mkContextEntry | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
mkDefInfo | Agda.Syntax.Info |
mkMatrix | Agda.Utils.Warshall |
mkName | Agda.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 |
mkPrimFun1 | Agda.TypeChecking.Primitive |
mkPrimFun2 | Agda.TypeChecking.Primitive |
mkPrimFun4 | Agda.TypeChecking.Primitive |
MkStr | Agda.Utils.QuickCheck |
mkType | Agda.Syntax.Internal |
MM | Agda.Auto.NarrowingSearch |
mmbpcase | Agda.Auto.NarrowingSearch |
mmcase | Agda.Auto.NarrowingSearch |
mmmcase | Agda.Auto.NarrowingSearch |
mmpcase | Agda.Auto.NarrowingSearch |
MName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
mnameFromList | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
mnameToConcrete | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
mnameToList | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
mobs | Agda.Auto.NarrowingSearch |
Mode | Agda.Utils.Pretty |
mode | Agda.Utils.Pretty |
modifyCurrentNameSpace | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
modifyCurrentScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
modifyCurrentScopeM | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
modifyImportedSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
modifyNamedScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
modifyNamedScopeM | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
modifyScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
modifyScopeInfo | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
modifyScopes | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
modifySignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
modSub | Agda.TypeChecking.Rules.LHS.Unify |
Module | |
1 (Type/Class) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Concrete |
3 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
ModuleArityMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ModuleDefinedInOtherFile | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ModuleDoesntExport | Agda.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 |
ModuleMacro | Agda.Syntax.Concrete |
ModuleName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
moduleName | Agda.Interaction.Imports |
moduleName' | Agda.Interaction.Imports |
ModuleNameDoesntMatchFileName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
moduleNameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
moduleNameToFileName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
moduleParser | |
1 (Function) | Agda.Syntax.Parser.Parser |
2 (Function) | Agda.Syntax.Parser, Agda.Interaction.GhciTop |
ModulesInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
moduleStr | Agda.Compiler.Alonzo.Names |
ModuleTag | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
ModuleToSource | Agda.Interaction.FindFile |
MonadException | Agda.TypeChecking.Monad.Exception |
MonadTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
movePos | Agda.Syntax.Position, Agda.Interaction.GhciTop |
movePosByString | Agda.Syntax.Position, Agda.Interaction.GhciTop |
mparen | Agda.Syntax.Concrete.Operators |
mparens | Agda.Utils.Pretty |
MPat | Agda.TypeChecking.Coverage.Match |
mpret | Agda.Auto.NarrowingSearch |
mprincipalpresent | Agda.Auto.NarrowingSearch |
msubs | Agda.Auto.Typecheck |
mul | |
1 (Function) | Agda.Termination.Semiring |
2 (Function) | Agda.Termination.Matrix |
MultipleFixityDecls | Agda.Syntax.Concrete.Definitions |
munch | Agda.Utils.ReadP |
munch1 | Agda.Utils.ReadP |
MutId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Mutual | Agda.Syntax.Concrete |
MutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
mvInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
mvInstantiation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
mvJudgement | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
mvListeners | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
mvPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MyMB | Agda.Auto.Syntax |
MyPB | Agda.Auto.Syntax |