main | Agda.Main |
MainInterface | |
1 (Type/Class) | Agda.Interaction.Imports |
2 (Data Constructor) | Agda.Interaction.Imports |
mainName | Agda.Compiler.Epic.Interface |
makeAbstract | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
makeAbstractClause | Agda.Interaction.MakeCase |
makeAbsurdClause | Agda.Interaction.MakeCase |
makeCase | Agda.Interaction.MakeCase |
MakeCaseVariant | Agda.Interaction.Response |
makeClosed | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad |
makeConfiguration | Agda.TypeChecking.Test.Generators |
makeEnv | Agda.Syntax.Translation.AbstractToConcrete |
makeForcedArgs | Agda.Compiler.Epic.ForceConstrs |
makeHom | Agda.TypeChecking.Rules.LHS.Unify |
makeInstance | Agda.Syntax.Common |
makeOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad |
makeProjection | Agda.TypeChecking.ProjectionLike |
makeSubstitution | |
1 (Function) | Agda.TypeChecking.Rewriting.NonLinMatch |
2 (Function) | Agda.TypeChecking.Rules.LHS.Unify |
MAlonzo | Agda.Interaction.InteractionTop |
MAlonzoNoMain | Agda.Interaction.InteractionTop |
many | Agda.Utils.ReadP |
many1 | Agda.Utils.ReadP |
manyTill | Agda.Utils.ReadP |
map | |
1 (Function) | Agda.Utils.HashMap |
2 (Function) | Agda.Utils.Bag |
3 (Function) | Agda.Compiler.JS.Substitution |
map' | Agda.Compiler.JS.Substitution |
mapAbsNames | Agda.Syntax.Internal |
mapAbsNamesM | Agda.Syntax.Internal |
mapAndUnzipM | Agda.Utils.Monad |
mapArgColors | Agda.Syntax.Common |
mapArgInfo | Agda.Syntax.Common |
mapArgInfoColors | Agda.Syntax.Common |
mapAwakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
mapBlockingVarCons | Agda.TypeChecking.Coverage.Match |
mapCommandLineOptions | Agda.Interaction.Options.Lenses |
mapCon | Agda.Compiler.Epic.Primitive |
mapConName | Agda.Syntax.Internal |
mapDomInfo | Agda.Syntax.Common |
mapEither | |
1 (Function) | Agda.Utils.Either |
2 (Function) | Agda.Utils.List |
mapExpr | |
1 (Function) | Agda.Syntax.Concrete.Generic |
2 (Function) | Agda.Syntax.Abstract.Views |
mapFlag | Agda.Interaction.Options |
mapFst | Agda.Utils.Tuple |
mapFstM | Agda.Utils.Tuple |
mapHiding | Agda.Syntax.Common |
mapIncludeDirs | Agda.Interaction.Options.Lenses |
mapKeysMonotonic | Agda.Utils.AssocList |
mapLeft | Agda.Utils.Either |
mapLHSHead | Agda.Syntax.Abstract |
mapLhsOriginalPattern | Agda.Syntax.Concrete |
mapM' | Agda.Utils.Monad |
mapMaybe | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
3 (Function) | Agda.Utils.HashMap |
mapMaybeM | Agda.Utils.Monad |
mapMaybeWithKey | Agda.Utils.HashMap |
mapM_ | Agda.Utils.Monad |
mapNameSpace | Agda.Syntax.Scope.Base |
mapNameSpaceM | Agda.Syntax.Scope.Base |
mapNodes | Agda.Utils.Warshall |
mapPairM | Agda.Utils.Tuple |
mapPersistentVerbosity | Agda.Interaction.Options.Lenses |
mapping | Agda.Compiler.JS.Compiler |
mapping' | Agda.Compiler.JS.Compiler |
mapPragmaOptions | Agda.Interaction.Options.Lenses |
mapRedEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
mapRedEnvSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
mapRedSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
mapRelevance | Agda.Syntax.Common |
mapRight | Agda.Utils.Either |
MapS | Agda.Auto.Convert |
mapSafeMode | Agda.Interaction.Options.Lenses |
mapScope | Agda.Syntax.Scope.Base |
mapScopeM | Agda.Syntax.Scope.Base |
mapScopeM_ | Agda.Syntax.Scope.Base |
mapScope_ | Agda.Syntax.Scope.Base |
mapSize | Agda.Utils.QuickCheck |
mapSleepingConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
mapSnd | Agda.Utils.Tuple |
mapSndM | Agda.Utils.Tuple |
mapTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
mapVerbosity | Agda.Interaction.Options.Lenses |
mapWithKey | |
1 (Function) | Agda.Utils.HashMap |
2 (Function) | Agda.Utils.AssocList |
mapWithKeyM | Agda.Utils.AssocList |
MArgList | Agda.Auto.Syntax |
markStatic | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
Masked | |
1 (Type/Class) | Agda.Termination.Monad |
2 (Data Constructor) | Agda.Termination.Monad |
masked | Agda.Termination.Monad |
MaskedDeBruijnPats | Agda.Termination.Monad |
Mat | Agda.Termination.Order |
mat | Agda.Termination.CallMatrix |
Match | |
1 (Type/Class) | Agda.TypeChecking.Patterns.Match |
2 (Type/Class) | Agda.TypeChecking.DisplayForm |
3 (Type/Class) | Agda.TypeChecking.Coverage.Match |
match | |
1 (Function) | Agda.Compiler.JS.Case |
2 (Function) | Agda.Syntax.Parser.LookAhead |
3 (Function) | Agda.Interaction.Highlighting.Vim |
4 (Function) | Agda.TypeChecking.DisplayForm |
5 (Function) | Agda.TypeChecking.Coverage.Match |
match' | |
1 (Function) | Agda.Syntax.Parser.LookAhead |
2 (Function) | Agda.TypeChecking.CompiledClause.Match |
matchClause | Agda.TypeChecking.Coverage.Match |
matchCommand | Agda.Interaction.CommandLine |
matchCompiled | Agda.TypeChecking.CompiledClause.Match |
matchCompiledE | Agda.TypeChecking.CompiledClause.Match |
matchCopattern | Agda.TypeChecking.Patterns.Match |
matchCopatterns | Agda.TypeChecking.Patterns.Match |
matchDisplayForm | Agda.TypeChecking.DisplayForm |
Matched | Agda.TypeChecking.Positivity |
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 |
matchType | Agda.Auto.Convert |
Matrix | |
1 (Type/Class) | Agda.Termination.SparseMatrix |
2 (Type/Class) | Agda.Utils.Warshall |
matrix | |
1 (Function) | Agda.Termination.SparseMatrix |
2 (Function) | Agda.Utils.Warshall |
matrixInvariant | Agda.Termination.SparseMatrix |
matrixUsingRowGen | Agda.Termination.SparseMatrix |
Max | Agda.Syntax.Internal |
maxDiscardRatio | Agda.Utils.QuickCheck |
maxName | Agda.TypeChecking.Level |
maxSize | Agda.Utils.QuickCheck |
maxSuccess | Agda.Utils.QuickCheck |
maxViewCons | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
maxViewMax | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
maxViewSuc_ | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
Maybe | |
1 (Type/Class) | Agda.Utils.Maybe |
2 (Type/Class) | Agda.Utils.Maybe.Strict |
maybe | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
MaybeAbort | Agda.TypeChecking.Injectivity |
maybeCoGen | Agda.Utils.TestHelpers |
maybeGen | Agda.Utils.TestHelpers |
maybeM | |
1 (Function) | Agda.Utils.Maybe.Strict |
2 (Function) | Agda.Utils.Maybe |
maybeor | Agda.Auto.Typecheck |
maybePrefixMatch | Agda.Utils.List |
maybePrimCon | Agda.TypeChecking.Level |
maybePrimDef | Agda.TypeChecking.Level |
MaybeRed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MaybeReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MaybeReducedArgs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MaybeReducedElims | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
maybeToList | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
MaybeWarnings | Agda.Interaction.Imports |
MayNotPostpone | Agda.TypeChecking.Rules.LHS.Unify |
MayPostpone | Agda.TypeChecking.Rules.LHS.Unify |
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 |
mazIncompleteMatch | Agda.Compiler.MAlonzo.Misc |
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 |
mazRTE | Agda.Compiler.MAlonzo.Misc |
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 |
mcons | Agda.Utils.List |
Measure | Agda.Syntax.Concrete.Definitions |
measureTime | Agda.Utils.Time |
meet | Agda.TypeChecking.SizedTypes.Utils |
MeetSemiLattice | Agda.TypeChecking.SizedTypes.Utils |
member | |
1 (Function) | Agda.Utils.VarSet |
2 (Function) | Agda.Utils.HashMap |
3 (Function) | Agda.Utils.Bag |
MemberId | |
1 (Type/Class) | Agda.Compiler.JS.Syntax |
2 (Data Constructor) | Agda.Compiler.JS.Syntax |
mentions | Agda.TypeChecking.SizedTypes.WarshallSolver |
MentionsMeta | Agda.TypeChecking.MetaVars.Mention |
mentionsMeta | Agda.TypeChecking.MetaVars.Mention |
mergeGroups | Agda.Compiler.Epic.Injection |
mergeHiding | Agda.Syntax.Common |
mergeInterface | Agda.Interaction.Imports |
mergeNames | Agda.Syntax.Scope.Base |
mergeNotations | Agda.Syntax.Fixity |
mergeScope | Agda.Syntax.Scope.Base |
mergeScopes | Agda.Syntax.Scope.Base |
Meta | Agda.Auto.NarrowingSearch |
MetaArg | Agda.TypeChecking.Positivity |
MetaCannotDependOn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MetaEnv | Agda.Auto.NarrowingSearch |
metaHelperType | Agda.Interaction.BasicOps |
MetaId | |
1 (Type/Class) | Agda.Syntax.Internal |
2 (Data Constructor) | Agda.Syntax.Internal |
metaId | Agda.Syntax.Internal |
MetaInfo | |
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 |
MetaInstantiation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MetaKind | Agda.TypeChecking.MetaVars |
MetaLevel | Agda.Syntax.Internal |
metaliseokh | Agda.Auto.Syntax |
MetaNameSuggestion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
metaNameSuggestion | Agda.Syntax.Info |
metaNumber | Agda.Syntax.Info |
metaOccurs | Agda.TypeChecking.MetaVars.Occurs |
MetaOccursInItself | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
metaParseExpr | Agda.Interaction.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 |
metaScope | Agda.Syntax.Info |
MetaSh | Agda.TypeChecking.Rules.LHS.Unify |
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 |
meta_not_constructor | Agda.Auto.Typecheck |
MExp | Agda.Auto.Syntax |
mextrarefs | Agda.Auto.NarrowingSearch |
mfilter | Agda.Utils.Monad |
miClosRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MId | Agda.Auto.Syntax |
miInterface | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
miMetaOccursCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
mimicGHCi | Agda.Interaction.EmacsTop |
miNameSuggestion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
minfoAsName | Agda.Syntax.Info |
minfoAsTo | Agda.Syntax.Info |
minfoDirective | Agda.Syntax.Info |
minfoOpenShort | Agda.Syntax.Info |
minfoRange | Agda.Syntax.Info |
minus | Agda.Interaction.Highlighting.Range |
MissingClauses | Agda.Syntax.Internal |
MissingDataSignature | Agda.Syntax.Concrete.Definitions |
MissingDefinition | Agda.Syntax.Concrete.Definitions |
MissingTypeSignature | Agda.Syntax.Concrete.Definitions |
MissingWithClauses | Agda.Syntax.Concrete.Definitions |
miWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MIx | |
1 (Type/Class) | Agda.Termination.SparseMatrix |
2 (Data Constructor) | Agda.Termination.SparseMatrix |
Mixed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
mIxInvariant | Agda.Termination.SparseMatrix |
mkAbs | Agda.TypeChecking.Substitute |
mkAbsolute | Agda.Utils.FileName |
mkBoundName | Agda.Syntax.Concrete |
mkBoundName_ | Agda.Syntax.Concrete |
mkCall | Agda.Termination.CallGraph |
mkCall' | Agda.Termination.CallGraph |
mkCon | Agda.Compiler.Epic.Forcing |
mkContextEntry | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
mkDefInfo | Agda.Syntax.Info |
mkDefInfoInstance | Agda.Syntax.Info |
mkExceptT | Agda.Utils.Except |
mkLam | Agda.TypeChecking.Substitute |
mkMatrix | Agda.Utils.Warshall |
MkName | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
mkName | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
mkName_ | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
mkNotation | Agda.Syntax.Notation |
mkPi | Agda.TypeChecking.Substitute |
mkPrimFun1 | Agda.TypeChecking.Primitive |
mkPrimFun1TCM | Agda.TypeChecking.Primitive |
mkPrimFun2 | Agda.TypeChecking.Primitive |
mkPrimFun4 | Agda.TypeChecking.Primitive |
mkPrimLevelMax | Agda.TypeChecking.Primitive |
mkPrimLevelSuc | Agda.TypeChecking.Primitive |
mkPrimLevelZero | Agda.TypeChecking.Primitive |
mkType | Agda.Syntax.Internal |
mkUnused | Agda.TypeChecking.Polarity |
mkWeakIORef | Agda.Utils.IORef |
mlevel | Agda.TypeChecking.Level |
MM | Agda.Auto.NarrowingSearch |
mm | Agda.Auto.CaseSplit |
mmbpcase | Agda.Auto.NarrowingSearch |
mmcase | Agda.Auto.NarrowingSearch |
mmmcase | Agda.Auto.NarrowingSearch |
mmpcase | Agda.Auto.NarrowingSearch |
MName | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
mnameFromList | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
mnameToConcrete | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
mnameToList | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
mnameToQName | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
mobs | Agda.Auto.NarrowingSearch |
Mode | Agda.Utils.Pretty |
mode | Agda.Utils.Pretty |
modify' | Agda.Utils.Monad |
modifyAbstractClause | Agda.Auto.Convert |
modifyAbstractExpr | Agda.Auto.Convert |
modifyAllowedReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
modifyAwakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
modifyBenchmark | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
modifyCommandLineOptions | Agda.Interaction.Options.Lenses |
modifyContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
modifyContextEntries | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
modifyContextEntry | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
modifyCurrentAccount | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
modifyCurrentNameSpace | Agda.Syntax.Scope.Monad |
modifyCurrentScope | Agda.Syntax.Scope.Monad |
modifyCurrentScopeM | Agda.Syntax.Scope.Monad |
modifyEI | Agda.Compiler.Epic.CompileState |
modifyFunClauses | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
modifyImportedSignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
modifyIncludeDirs | Agda.Interaction.Options.Lenses |
modifyInstanceDefs | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
modifyInteractionPoints | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
modifyIORef | Agda.Utils.IORef |
modifyIORef' | Agda.Utils.IORef |
modifyLocalVars | Agda.Syntax.Scope.Monad |
modifyMetaStore | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
modifyNamedScope | Agda.Syntax.Scope.Monad |
modifyNamedScopeM | Agda.Syntax.Scope.Monad |
modifyOccursCheckDefs | Agda.TypeChecking.MetaVars.Occurs |
modifyOldInteractionScopes | Agda.Interaction.InteractionTop |
modifyPatternSyns | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
modifyPersistentState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
modifyPersistentVerbosity | Agda.Interaction.Options.Lenses |
modifyPragmaOptions | Agda.Interaction.Options.Lenses |
modifySafeMode | Agda.Interaction.Options.Lenses |
modifyScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
modifyScopeInfo | Agda.Syntax.Scope.Monad |
modifyScopes | Agda.Syntax.Scope.Monad |
modifySignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
modifySleepingConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
modifyStatistics | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad |
modifyTheInteractionPoints | Agda.Interaction.InteractionTop |
modifyTimings | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
modifyVerbosity | Agda.Interaction.Options.Lenses |
modName | Agda.Compiler.JS.Syntax |
modname | Agda.Compiler.JS.Pretty |
modSub | Agda.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 |
ModuleArityMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
moduleContents | Agda.Interaction.BasicOps |
ModuleDefinedInOtherFile | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ModuleDoesntExport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
moduleHash | Agda.Interaction.Imports |
ModuleId | Agda.Interaction.Highlighting.Dot |
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 | |
1 (Data Constructor) | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
2 (Type/Class) | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
moduleName | Agda.Interaction.FindFile |
moduleName' | Agda.Interaction.FindFile |
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 |
ModulesInScope | Agda.Syntax.Scope.Base |
ModuleTag | Agda.Syntax.Scope.Base |
ModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Monad | Agda.Utils.Monad |
MonadChange | Agda.Utils.Update |
MonadError | Agda.Utils.Except |
MonadException | Agda.TypeChecking.Monad.Exception |
MonadGetDefs | Agda.Syntax.Internal.Defs |
MonadPlus | Agda.Utils.Monad |
MonadTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MonadTer | Agda.Termination.Monad |
monomorphic | Agda.Utils.QuickCheck |
moreRelevant | Agda.Syntax.Common |
movePos | Agda.Syntax.Position |
movePosByString | Agda.Syntax.Position |
mparens | Agda.Utils.Pretty |
MPat | Agda.TypeChecking.Coverage.Match |
mplus | Agda.Utils.Monad |
mpret | Agda.Auto.NarrowingSearch |
mprincipalpresent | Agda.Auto.NarrowingSearch |
msum | Agda.Utils.Monad |
mul | |
1 (Function) | Agda.Termination.Semiring |
2 (Function) | Agda.Termination.SparseMatrix |
MultipleFixityDecls | Agda.Syntax.Concrete.Definitions |
multiply | Agda.Termination.Semiring |
munch | Agda.Utils.ReadP |
munch1 | Agda.Utils.ReadP |
mustBeFinite | Agda.TypeChecking.SizedTypes.WarshallSolver |
mustBePi | Agda.TypeChecking.Telescope |
MutId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Mutual | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
mutualChecks | Agda.TypeChecking.Rules.Decl |
MutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MutualInfo | |
1 (Type/Class) | Agda.Syntax.Info |
2 (Data Constructor) | Agda.Syntax.Info |
mutuallyRecursive | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
MutualNames | Agda.Termination.Monad |
mutualRange | Agda.Syntax.Info |
mutualTermCheck | Agda.Syntax.Info |
mvFrozen | 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 |
mvPermutation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
mvPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
MyMB | Agda.Auto.Syntax |
MyPB | Agda.Auto.Syntax |
mzero | Agda.Utils.Monad |