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

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- #
- $
- %
- &
- +
- .
- /
- <
- =
- >
- ?
- @
- \
- ^
- |
- -
- _
- All

Index - M

M | Agda.Mimer.Options
Macro |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Abstract
MacroBound | Agda.Syntax.Scope.Base
MacroDef | Agda.Syntax.Common
MacroInLetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MacroInLetBindings_ | Agda.Interaction.Options.Warnings
MacroName | Agda.Syntax.Scope.Base
MacroResultTypeMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MacroResultTypeMismatch_ | Agda.Interaction.Options.Errors
MainFunctionDef |
1 (Type/Class) | Agda.Compiler.MAlonzo.Primitives
2 (Data Constructor) | Agda.Compiler.MAlonzo.Primitives
mainFunctionDefs | Agda.Compiler.MAlonzo.Primitives
makeAbstractClause | Agda.Interaction.MakeCase
makeAbsurdClause | Agda.Interaction.MakeCase
makeAbsurdLambda | Agda.TypeChecking.Rules.Term
makeAll | Agda.Utils.IndexedList
makeCase | Agda.Interaction.MakeCase
MakeCaseVariant | Agda.Interaction.Response.Base, Agda.Interaction.Response
makeCaseVariant | Agda.Interaction.InteractionTop
makeInstance | Agda.Syntax.Common
makeInstance' | Agda.Syntax.Common
makeIrrelevant | Agda.Syntax.Parser.Helpers
makeIrrelevantM | Agda.Syntax.Parser.Helpers
makeName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
makeOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend
makePatternVarsVisible | Agda.Interaction.MakeCase
makePi | Agda.Syntax.Concrete
makeProjection | Agda.TypeChecking.ProjectionLike
makeRelativeCanonical | Agda.Utils.FileName
makeRHSEmptyRecord | Agda.Interaction.MakeCase
makeShapeIrrelevant | Agda.Syntax.Parser.Helpers
makeShapeIrrelevantM | Agda.Syntax.Parser.Helpers
MakeStrict | Agda.Compiler.MAlonzo.Strict
makeStrict | Agda.Compiler.MAlonzo.Strict
makeSubstitution | Agda.TypeChecking.Rewriting.NonLinMatch
malformed | Agda.TypeChecking.Serialise.Base
ManyHoles | Agda.Utils.AffineHole
Map | Agda.Utils.TypeLevel
map |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.Utils.Map1
3 (Function) | Agda.Utils.Set1
4 (Function) | Agda.Utils.Bag
5 (Function) | Agda.Compiler.JS.Substitution
map' | Agda.Compiler.JS.Substitution
Map1 | Agda.Utils.Map1
mapAbsNames | Agda.Syntax.Internal
mapAbsNamesM | Agda.Syntax.Internal
mapAbsoluteIncludePaths | Agda.Interaction.Options.Lenses
mapAbstraction | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapAbstraction_ | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapAccum | Agda.Utils.Map1
mapAccumRWithKey | Agda.Utils.Map1
mapAccumWithKey | Agda.Utils.Map1
mapAnnotation | Agda.Syntax.Common
mapAPattern | Agda.Syntax.Abstract.Pattern
mapArgInfo | Agda.Syntax.Common
mapAwakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapBenchmarkOn | Agda.Utils.Benchmark
mapChangeT | Agda.Utils.Update
mapClosure | Agda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapCohesion | Agda.Syntax.Common
mapCohesionMod | Agda.Syntax.Common
mapCommandLineOptions | Agda.Interaction.Options.Lenses
mapConName | Agda.Syntax.Internal
mapCPattern | Agda.Syntax.Concrete.Pattern
mapCurrentAccount | Agda.Utils.Benchmark
mapEither | Agda.Utils.Map1
mapEither3M | Agda.Utils.Three
mapEitherWithKey | Agda.Utils.Map1
mapExpr |
1 (Function) | Agda.Syntax.Concrete.Generic
2 (Function) | Agda.Syntax.Abstract.Views
mapFlag | Agda.Interaction.Options
mapFlexRigMap | Agda.TypeChecking.Free.Lazy
mapFreeVariables | Agda.Syntax.Common
mapFreeVariablesArgInfo | Agda.Syntax.Common
mapFst | Agda.Utils.Tuple
mapFstM | Agda.Utils.Tuple
mapHiding | Agda.Syntax.Common
mapHidingArgInfo | Agda.Syntax.Common
mapImportDir | Agda.Syntax.Scope.Monad
mapIncludePaths | Agda.Interaction.Options.Lenses
mapInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
mapKeys | Agda.Utils.Map1
mapKeysMonotonic |
1 (Function) | Agda.Utils.Map1
2 (Function) | Agda.Utils.AssocList
mapKeysWith | Agda.Utils.Map1
mapLeft | Agda.Utils.Either
mapLHSCores | Agda.TypeChecking.Rules.Def
mapLHSHead | Agda.Syntax.Abstract.Pattern
mapLhsOriginalPattern | Agda.Syntax.Concrete.Pattern
mapLhsOriginalPatternM | Agda.Syntax.Concrete.Pattern
mapListT | Agda.Utils.ListT
mapLock | Agda.Syntax.Common
mapM' | Agda.Utils.Monad
mapMaybe |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Map1
3 (Function) | Agda.Utils.Maybe.Strict
4 (Function) | Agda.Utils.List1
mapMaybeAndRest | Agda.Utils.List
mapMaybeM | Agda.Utils.Monad
mapMaybeMM | Agda.Utils.Monad
mapMaybeWithKey | Agda.Utils.Map1
mapMListT | Agda.Utils.ListT
mapMListT_alt | Agda.Utils.ListT
mapMM | Agda.Utils.Monad
mapMM_ | Agda.Utils.Monad
mapModality | Agda.Syntax.Common
mapModalityArgInfo | Agda.Syntax.Common
mapModalPolarity | Agda.Syntax.Common
mapMonotonic |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.Set1
MapNamedArgPattern |
1 (Type/Class) | Agda.Syntax.Internal.Pattern
2 (Type/Class) | Agda.Syntax.Abstract.Pattern
mapNamedArgPattern |
1 (Function) | Agda.Syntax.Internal.Pattern
2 (Function) | Agda.Syntax.Abstract.Pattern
mapNameOf | Agda.Syntax.Common
mapNameSpace | Agda.Syntax.Scope.Base
mapNameSpaceM | Agda.Syntax.Scope.Base
mapOrigin | Agda.Syntax.Common
mapOriginArgInfo | Agda.Syntax.Common
mapPairM | Agda.Utils.Tuple
mapPersistentVerbosity | Agda.Interaction.Options.Lenses
mapPolarityMod | Agda.Syntax.Common
mapPragmaOptions | Agda.Interaction.Options
mapQuantity | Agda.Syntax.Common
mapQuantityMod | Agda.Syntax.Common
mapRedEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapRedEnvSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapRedSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapRelevance | Agda.Syntax.Common
mapRelevanceMod | Agda.Syntax.Common
mapRenaming | Agda.Syntax.Scope.Monad
mapRight | Agda.Utils.Either
mapSafeMode | Agda.Interaction.Options.Lenses
mapScope | Agda.Syntax.Scope.Base
mapScopeM | Agda.Syntax.Scope.Base
mapScopeM_ | Agda.Syntax.Scope.Base
mapScopeNS | Agda.Syntax.Scope.Base
mapScope_ | Agda.Syntax.Scope.Base
mapSleepingConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapSnd | Agda.Utils.Tuple
mapSndM | Agda.Utils.Tuple
mapSubTries | Agda.Utils.Trie
mapTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapTimings | Agda.Utils.Benchmark
mapUsing | Agda.Syntax.Common
mapValue | Agda.Utils.WithDefault
mapVarMap | Agda.TypeChecking.Free.Lazy
mapVerbosity | Agda.Interaction.Options.Lenses
mapWithEdge | Agda.Utils.Graph.AdjacencyMap.Unidirectional
mapWithIndex | Agda.Utils.IndexedList
mapWithKey |
1 (Function) | Agda.Utils.Map1
2 (Function) | Agda.Utils.AssocList
3 (Function) | Agda.Utils.BiMap
mapWithKeyFixedTags | Agda.Utils.BiMap
mapWithKeyFixedTagsPrecondition | Agda.Utils.BiMap
mapWithKeyM | Agda.Utils.AssocList
mapWithKeyPrecondition | Agda.Utils.BiMap
markFirstOrder | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
markInjective | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
markInline | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
markStatic | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Markup |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.Syntax.Parser.Literate
Masked |
1 (Type/Class) | Agda.Termination.Monad
2 (Data Constructor) | Agda.Termination.Monad
masked | Agda.Termination.Monad
MaskedDeBruijnPatterns | Agda.Termination.Monad
Mat | Agda.Termination.Order
mat | Agda.Termination.CallMatrix
Match |
1 (Type/Class) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Utils.Haskell.Syntax
3 (Type/Class) | Agda.TypeChecking.Patterns.Match
4 (Type/Class) | Agda.TypeChecking.Coverage.Match
5 (Type/Class) | Agda.TypeChecking.Rewriting.NonLinMatch
match |
1 (Function) | Agda.Syntax.Parser.LookAhead
2 (Function) | Agda.Interaction.Highlighting.Vim
3 (Function) | Agda.TypeChecking.Coverage.Match
4 (Function) | Agda.TypeChecking.Rewriting.NonLinMatch
match' |
1 (Function) | Agda.Syntax.Parser.LookAhead
2 (Function) | Agda.TypeChecking.CompiledClause.Match
matchClause | Agda.TypeChecking.Coverage.Match
matchCompiled | Agda.TypeChecking.CompiledClause.Match
matchCompiledE | Agda.TypeChecking.CompiledClause.Match
matchCopattern | Agda.TypeChecking.Patterns.Match
matchCopatterns | Agda.TypeChecking.Patterns.Match
Matched | Agda.TypeChecking.Positivity.Occurrence
matchedArgs | Agda.TypeChecking.Patterns.Match
matchedArgs' | Agda.TypeChecking.Patterns.Match
matches | Agda.Interaction.Highlighting.Vim
matchingBlocked | Agda.TypeChecking.Rewriting.NonLinMatch
matchPattern | Agda.TypeChecking.Patterns.Match
matchPatternP | Agda.TypeChecking.Patterns.Match
matchPatterns | Agda.TypeChecking.Patterns.Match
matchPatternsP | Agda.TypeChecking.Patterns.Match
matchPatternSyn | Agda.Syntax.Abstract.PatternSynonyms
matchPatternSynP | Agda.Syntax.Abstract.PatternSynonyms
Matrix |
1 (Type/Class) | Agda.Termination.SparseMatrix
2 (Data Constructor) | Agda.Termination.SparseMatrix
Max | Agda.Syntax.Internal
maxInstanceSearchDepth | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
maxInversionDepth | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
maxName | Agda.TypeChecking.Level
MaxNat |
1 (Type/Class) | Agda.Utils.Monoid
2 (Data Constructor) | Agda.Utils.Monoid
maxView | Agda.Utils.Map1
maxViewCons | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
maxViewMax | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
maxViewSuc_ | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Interaction.InteractionTop
maybeFlexiblePattern | Agda.TypeChecking.Rules.LHS
MaybeFree | Agda.TypeChecking.Free.Reduce
maybeLeft | Agda.Utils.Either
maybeM |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
maybeNamed | Agda.Syntax.Parser.Helpers
MaybePlaceholder | Agda.Syntax.Common
maybePlaceholder | Agda.Syntax.Concrete.Operators.Parser
MaybeProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
maybeProjTurnPostfix | Agda.Syntax.Abstract.Views
MaybeRed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MaybeReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MaybeReducedArgs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MaybeReducedElims | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
maybeRight | Agda.Utils.Either
maybeTimed | Agda.Interaction.InteractionTop
maybeToEither | Agda.Utils.Either
maybeToList |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
mayEraseType | Agda.Compiler.Backend.Base, Agda.Compiler.Backend
mazAccumlatedImports | Agda.Compiler.MAlonzo.Misc
mazAnyType | Agda.Compiler.MAlonzo.Misc
mazAnyTypeName | Agda.Compiler.MAlonzo.Misc
mazCoerce | Agda.Compiler.MAlonzo.Misc
mazCoerceName | Agda.Compiler.MAlonzo.Misc
mazErasedName | Agda.Compiler.MAlonzo.Misc
mazHole | Agda.Compiler.MAlonzo.Misc
mazIsMainModule | Agda.Compiler.MAlonzo.Misc
mazMod | Agda.Compiler.MAlonzo.Misc
mazMod' | Agda.Compiler.MAlonzo.Misc
mazModuleName | Agda.Compiler.MAlonzo.Misc
mazName | Agda.Compiler.MAlonzo.Misc
mazRTE | Agda.Compiler.MAlonzo.Misc
mazRTEFloat | Agda.Compiler.MAlonzo.Misc
mazstr | Agda.Compiler.MAlonzo.Misc
mazUnreachableError | Agda.Compiler.MAlonzo.Misc
mcons | Agda.Utils.List
MdFileType | Agda.Syntax.Common
Measure | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
measureTime | Agda.Utils.Time
MECons | Agda.TypeChecking.Serialise.Base
MEEmpty | Agda.TypeChecking.Serialise.Base
meet | Agda.TypeChecking.SizedTypes.Utils
MeetSemiLattice | Agda.TypeChecking.SizedTypes.Utils
member |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.Set1
3 (Function) | Agda.Utils.Map1
4 (Function) | Agda.Utils.Bag
5 (Function) | Agda.Utils.BoolSet
6 (Function) | Agda.Utils.IntSet.Infinite
7 (Function) | Agda.Utils.SmallSet
8 (Function) | Agda.Utils.Trie
MemberId |
1 (Type/Class) | Agda.Compiler.JS.Syntax
2 (Data Constructor) | Agda.Compiler.JS.Syntax
MemberIndex | Agda.Compiler.JS.Syntax
Memo | Agda.TypeChecking.Serialise.Base
memo | Agda.Utils.Memo
MemoEntry | Agda.TypeChecking.Serialise.Base
memoise |
1 (Function) | Agda.Utils.Parser.MemoisedCPS
2 (Function) | Agda.Syntax.Concrete.Operators.Parser.Monad
memoiseIfPrinting |
1 (Function) | Agda.Utils.Parser.MemoisedCPS
2 (Function) | Agda.Syntax.Concrete.Operators.Parser.Monad
MemoKey | Agda.Syntax.Concrete.Operators.Parser.Monad
memoModules | Agda.Syntax.Scope.Monad
memoNames | Agda.Syntax.Scope.Monad
memoRec | Agda.Utils.Memo
memoToScopeInfo | Agda.Syntax.Scope.Monad
memoUnsafe | Agda.Utils.Memo
memoUnsafeH | Agda.Utils.Memo
mentions | Agda.TypeChecking.SizedTypes.WarshallSolver
MentionsMeta | Agda.TypeChecking.MetaVars.Mention
mentionsMeta | Agda.TypeChecking.MetaVars.Mention
mentionsMetas | Agda.TypeChecking.MetaVars.Mention
mergeDT | Agda.TypeChecking.DiscrimTree.Types
mergeEdges | Agda.TypeChecking.Positivity
mergeElim | Agda.TypeChecking.Patterns.Match
mergeElims | Agda.TypeChecking.Patterns.Match
mergeHiding | Agda.Syntax.Common
mergeNames | Agda.Syntax.Scope.Base
mergeNamesMany | Agda.Syntax.Scope.Base
mergeNotations | Agda.Syntax.Notation
mergePatternSynDefs | Agda.Syntax.Abstract.PatternSynonyms
mergeScope | Agda.Syntax.Scope.Base
mergeScopes | Agda.Syntax.Scope.Base
mergeStrictlyOrderedBy | Agda.Utils.List
Meta | Agda.Syntax.Reflected
MetaArg | Agda.TypeChecking.Positivity.Occurrence
MetaCannotDependOn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaCannotDependOn_ | Agda.Interaction.Options.Errors
metaCheck | Agda.TypeChecking.MetaVars.Occurs
MetaClass | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaErasedSolution | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaErasedSolution_ | Agda.Interaction.Options.Errors
metaFrozen | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
metaHelperType | Agda.Interaction.BasicOps
MetaId |
1 (Type/Class) | Agda.Syntax.Common, Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Common, Agda.Syntax.Internal
metaId | Agda.Syntax.Common, 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, Agda.Compiler.Backend
4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaInstantiation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
metaInstantiationToMetaKind | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaIrrelevantSolution | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaIrrelevantSolution_ | Agda.Interaction.Options.Errors
MetaKind | Agda.Syntax.Info
metaKind | Agda.Syntax.Info
metaModule | Agda.Syntax.Common, Agda.Syntax.Internal
MetaNameSuggestion | Agda.Syntax.Info
metaNameSuggestion | Agda.Syntax.Info
metaNumber | Agda.Syntax.Info
metaOccurs | Agda.TypeChecking.MetaVars.Occurs
metaOccurs2 | Agda.TypeChecking.MetaVars.Occurs
metaOccurs3 | Agda.TypeChecking.MetaVars.Occurs
metaOccursQName | Agda.TypeChecking.MetaVars.Occurs
MetaPriority |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
metaRange | Agda.Syntax.Info
MetaS | Agda.Syntax.Internal
Metas | Agda.Utils.ProfileOptions
metaScope | Agda.Syntax.Info
metasCreatedBy | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaSet |
1 (Type/Class) | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
2 (Data Constructor) | Agda.TypeChecking.Free.Lazy
metaSetToBlocker | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
metasIn | Agda.Syntax.Internal.Names
metasIn' | Agda.Syntax.Internal.Names
metaToNat | Agda.TypeChecking.Primitive
metaType | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaV | Agda.Syntax.Internal
MetaVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaVariable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
miClosRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Middle | Agda.Syntax.Common
miGeneralizable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
miInterface | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MilliSeconds | Agda.Mimer.Options
mimer | Agda.Mimer.Mimer
MimerClauses | Agda.Mimer.Mimer
MimerExpr | Agda.Mimer.Mimer
MimerList | Agda.Mimer.Mimer
MimerNoResult | Agda.Mimer.Mimer
MimerResult | Agda.Mimer.Mimer
miMetaOccursCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mimicGHCi | Agda.Interaction.EmacsTop
miModality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
miMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
miNameSuggestion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
minfoAsName | Agda.Syntax.Info
minfoAsTo | Agda.Syntax.Info
minfoDirective | Agda.Syntax.Info
minfoOpenShort | Agda.Syntax.Info
minfoRange | Agda.Syntax.Info
minifiedCodeLinesLength | Agda.Compiler.JS.Pretty
minus | Agda.Interaction.Highlighting.Range
minView | Agda.Utils.Map1
miPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MismatchedProjectionsError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MismatchedProjectionsError_ | Agda.Interaction.Options.Errors
MisplacedAttributes | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
MisplacedAttributes_ | Agda.Interaction.Options.Warnings
MissingBody | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MissingClauses | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
MissingColonForField | Agda.Interaction.Library.Base
MissingDataDeclaration | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
MissingDataDeclaration_ | Agda.Interaction.Options.Warnings
MissingDataSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MissingDeclaration | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MissingDeclaration_ | Agda.Interaction.Options.Errors
MissingDefinition |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MissingDefinitions | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
MissingDefinitions_ | Agda.Interaction.Options.Warnings
MissingDefinition_ | Agda.Interaction.Options.Errors
MissingFieldName | Agda.Interaction.Library.Base
MissingFields | Agda.Interaction.Library.Base
MissingFunctionSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MissingRecordSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MissingRHS | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MissingTypeSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MissingTypeSignatureForOpaque | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MissingTypeSignatureForOpaque_ | Agda.Interaction.Options.Warnings
MissingTypeSignatureInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
missingTypeSignatureInfoName | Agda.TypeChecking.Errors.Names
MissingTypeSignature_ | Agda.Interaction.Options.Errors
MissingWithClauses | Agda.Syntax.Concrete.Definitions.Errors
MissingWithClauses_ | Agda.Interaction.Options.Errors
miWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MIx |
1 (Type/Class) | Agda.Termination.SparseMatrix
2 (Data Constructor) | Agda.Termination.SparseMatrix
Mixed | Agda.TypeChecking.Positivity.Occurrence
MixedPolarity | Agda.Syntax.Common
mixedPolarity | Agda.Syntax.Common
mkAbs | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
mkAbsolute | Agda.Utils.FileName
mkAbsurdBinding | Agda.Syntax.Parser.Helpers
mkAbsurdLamClause | Agda.Syntax.Parser.Helpers
mkApp | Agda.Syntax.Translation.ReflectedToAbstract
mkBinder |
1 (Function) | Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Abstract
mkBinder_ |
1 (Function) | Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Abstract
mkBindName | Agda.Syntax.Abstract
mkBoundName | Agda.Syntax.Concrete
mkBoundName_ | Agda.Syntax.Concrete
mkCall | Agda.Termination.CallGraph
mkCall' | Agda.Termination.CallGraph
mkComp | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
mkCompLazy | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
mkCon | Agda.TypeChecking.Records
mkDef | Agda.Syntax.Translation.ReflectedToAbstract
mkDefInfo | Agda.Syntax.Info
mkDefInfoInstance | Agda.Syntax.Info
mkDomainFree | Agda.Syntax.Abstract
mkDomainFree_ | Agda.Syntax.Parser.Helpers
mkGComp | Agda.TypeChecking.Primitive.Cubical.Glue, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
mkInterfaceFile | Agda.Interaction.FindFile
mkIsSizeConstraint | Agda.TypeChecking.SizedTypes
mkLam |
1 (Function) | Agda.Syntax.Concrete
2 (Function) | Agda.TypeChecking.Substitute
mkLamBinds | Agda.Syntax.Parser.Helpers
mkLamClause | Agda.Syntax.Parser.Helpers
mkLet |
1 (Function) | Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Function) | Agda.Syntax.Concrete
3 (Function) | Agda.Syntax.Abstract
mkLibM | Agda.Interaction.Library
mkMetaInfo | Agda.Syntax.Translation.ReflectedToAbstract
MkName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mkName |
1 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
2 (Function) | Agda.Syntax.Parser.Helpers
mkName' | Agda.Syntax.Parser.Helpers
mkNamedArg | Agda.Syntax.Parser.Helpers
mkName_ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mkNotation | Agda.Syntax.Notation
mkPi |
1 (Function) | Agda.Syntax.Abstract
2 (Function) | Agda.TypeChecking.Substitute
mkPiSort | Agda.TypeChecking.Substitute
mkPragma | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mkPrimFun1 | Agda.TypeChecking.Primitive
mkPrimFun1TCM | Agda.TypeChecking.Primitive
mkPrimFun2 | Agda.TypeChecking.Primitive
mkPrimFun3 | Agda.TypeChecking.Primitive
mkPrimFun4 | Agda.TypeChecking.Primitive
mkPrimInjective | Agda.TypeChecking.Primitive
mkPrimLevelMax | Agda.TypeChecking.Primitive
mkPrimLevelSuc | Agda.TypeChecking.Primitive
mkPrimLevelZero | Agda.TypeChecking.Primitive
mkProp | Agda.Syntax.Internal
mkQName | Agda.Syntax.Parser.Helpers
mkRangeFile | Agda.Syntax.Position
mkRString | Agda.Syntax.Parser.Helpers
mkRText | Agda.Syntax.Parser.Helpers
mkSortKit | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mkSSet | Agda.Syntax.Internal
mkTApp | Agda.Syntax.Treeless, Agda.Compiler.Backend
mkTBind | Agda.Syntax.Abstract
mkTLam | Agda.Syntax.Treeless, Agda.Compiler.Backend
mkTLet |
1 (Function) | Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Abstract
mkType | Agda.Syntax.Internal
mkValidName | Agda.Syntax.Parser.Helpers
mkVar | Agda.Syntax.Translation.ReflectedToAbstract
mkVarName | Agda.Syntax.Translation.ReflectedToAbstract
mkWeakIORef | Agda.Utils.IORef
MName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mnameFromList | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mnameFromList1 | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mnameToConcrete | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mnameToList | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mnameToList1 | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mnameToQName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
Mod | Agda.Syntax.Concrete
Modality |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
modalityAction | Agda.TypeChecking.CheckInternal
modalityOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModalPolarity | Agda.Syntax.Common
modalPolarityToOccurrence | Agda.TypeChecking.Positivity.Occurrence
modCohesion | Agda.Syntax.Common
modDecls | Agda.Syntax.Concrete
Mode |
1 (Type/Class) | Agda.Syntax.Common.Pretty
2 (Type/Class) | Agda.Interaction.Imports
mode | Agda.Syntax.Common.Pretty
modFile | Agda.TypeChecking.Serialise.Base
modifyAbsoluteIncludePaths | Agda.Interaction.Options.Lenses
modifyAllowedReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyArgOccurrences | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyAwakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyBenchmark | Agda.Utils.Benchmark
modifyCommandLineOptions | Agda.Interaction.Options.Lenses
modifyConcreteNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyContext | Agda.Syntax.Parser.Monad
modifyContextInfo | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyCounter | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyCurrentNameSpace | Agda.Syntax.Scope.Monad
modifyCurrentScope | Agda.Syntax.Scope.Monad
modifyCurrentScopeM | Agda.Syntax.Scope.Monad
modifyFunClauses | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyGlobalDefinition | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyImportedSignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyIncludePaths | Agda.Interaction.Options.Lenses
modifyInstanceDefs | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyInteractionPoints | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyIORef | Agda.Utils.IORef
modifyIORef' | Agda.Utils.IORef
modifyLocalVars | Agda.Syntax.Scope.Monad
modifyNamedScope | Agda.Syntax.Scope.Monad
modifyNamedScopeM | Agda.Syntax.Scope.Monad
modifyNameSpace | Agda.Syntax.Scope.Base
modifyOccursCheckDefs | Agda.TypeChecking.MetaVars.Occurs
modifyOldInteractionScopes | Agda.Interaction.InteractionTop
modifyPatternSyns | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyPersistentState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyPersistentVerbosity | Agda.Interaction.Options.Lenses
modifyPragmaOptions | Agda.Interaction.Options.Lenses
modifyRecEta | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifySafeMode | Agda.Interaction.Options.Lenses
modifyScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyScopes | Agda.Syntax.Scope.Monad
modifyScope_ | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifySignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifySleepingConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyStatistics | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifySystem | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTC' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTCLens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTCLens' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTCLensM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyTheInteractionPoints | Agda.Interaction.InteractionTop
modifyVerbosity | Agda.Interaction.Options.Lenses
modName | Agda.Compiler.JS.Syntax
modname | Agda.Compiler.JS.Pretty
modPolarity | Agda.Syntax.Common
modPolarityAnn | Agda.Syntax.Common
modPolarityLock | Agda.Syntax.Common
modPolarityOrigin | Agda.Syntax.Common
modPragmas | Agda.Syntax.Concrete
modQuantity | Agda.Syntax.Common
modRelevance | Agda.Syntax.Common
Module |
1 (Type/Class) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Utils.Haskell.Syntax
3 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
4 (Type/Class) | Agda.Compiler.JS.Syntax
5 (Data Constructor) | Agda.Compiler.JS.Syntax
6 (Type/Class) | Agda.Syntax.Concrete
7 (Data Constructor) | Agda.Syntax.Concrete
8 (Data Constructor) | Agda.Mimer.Options
ModuleApplication |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
ModuleArityMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleArityMismatch_ | Agda.Interaction.Options.Errors
ModuleAssignment |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
ModuleCheckMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleContents | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
moduleContents | Agda.Interaction.BasicOps
ModuleDefinedInOtherFile | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleDefinedInOtherFile_ | Agda.Interaction.Options.Errors
ModuleDoesntExport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleDoesntExport_ | Agda.Interaction.Options.Warnings
ModuleInfo |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleMacro | Agda.Syntax.Concrete
ModuleMap | Agda.Syntax.Scope.Base
ModuleName |
1 (Type/Class) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Utils.Haskell.Syntax
3 (Type/Class) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
4 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
ModuleNameDoesntMatchFileName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleNameDoesntMatchFileName_ | Agda.Interaction.Options.Errors
ModuleNameHash |
1 (Type/Class) | Agda.Syntax.TopLevelModuleName.Boot, Agda.Syntax.Common, Agda.Syntax.TopLevelModuleName
2 (Data Constructor) | Agda.Syntax.TopLevelModuleName.Boot, Agda.Syntax.Common, Agda.Syntax.TopLevelModuleName
moduleNameHash | Agda.Syntax.TopLevelModuleName.Boot, Agda.Syntax.Common, Agda.Syntax.TopLevelModuleName
ModuleNameHashCollision | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleNameHashCollision_ | Agda.Interaction.Options.Errors
moduleNameId | Agda.Syntax.TopLevelModuleName.Boot, Agda.Syntax.Common, Agda.Syntax.TopLevelModuleName
moduleNameInferred | Agda.Syntax.TopLevelModuleName.Boot, Agda.Syntax.Common, Agda.Syntax.TopLevelModuleName
moduleNameParser |
1 (Function) | Agda.Syntax.Parser.Parser
2 (Function) | Agda.Syntax.Parser
moduleNameParts | Agda.Syntax.TopLevelModuleName.Boot, Agda.Syntax.Common, Agda.Syntax.TopLevelModuleName
moduleNameRange | Agda.Syntax.TopLevelModuleName.Boot, Agda.Syntax.Common, Agda.Syntax.TopLevelModuleName
moduleNameToFileName | Agda.Syntax.TopLevelModuleName
ModuleNameUnexpected | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleNameUnexpected_ | Agda.Interaction.Options.Errors
ModuleNotName | Agda.Syntax.Scope.Base
moduleParamsToApply | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
moduleParser |
1 (Function) | Agda.Syntax.Parser.Parser
2 (Function) | Agda.Syntax.Parser
ModulePragma | Agda.Utils.Haskell.Syntax
Modules | Agda.Utils.ProfileOptions
ModuleScopeChecked | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModulesInScope | Agda.Syntax.Scope.Base
ModuleTag | Agda.Syntax.Scope.Base
ModuleToSource |
1 (Type/Class) | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleToSourceId | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
moduleToSourceId | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleTypeChecked | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadAbsToCon | Agda.Syntax.Translation.AbstractToConcrete, Agda.TypeChecking.Pretty
MonadAddContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadBench | Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
MonadBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadChange | Agda.Utils.Update
MonadCheckInternal | Agda.TypeChecking.CheckInternal
MonadConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadConversion | Agda.TypeChecking.Conversion
MonadDebug | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadFileId | Agda.Utils.FileId, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadFixityError | Agda.Syntax.Concrete.Fixity
MonadFresh | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadGetDefs | Agda.Syntax.Internal.Defs
MonadInteractionPoints | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadLogHtml | Agda.Interaction.Highlighting.HTML.Base
MonadLogLaTeX | Agda.Interaction.Highlighting.LaTeX.Base
MonadMatch | Agda.TypeChecking.Patterns.Match
MonadMetaSolver | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadPlus | Agda.Utils.Monad
MonadPretty | Agda.TypeChecking.Pretty
MonadReduce | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadReflectedToAbstract | Agda.Syntax.Translation.ReflectedToAbstract
MonadReify | Agda.Syntax.Translation.InternalToAbstract
MonadStatistics | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadStConcreteNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTCEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTCError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTer | Agda.Termination.Monad
MonadTrace | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTrans | Agda.Utils.Monad
MonadWarning | Agda.TypeChecking.Warnings
moreCohesion | Agda.Syntax.Common
morePolarity | Agda.Syntax.Common
morePolarity' | Agda.Syntax.Common
moreQuantity | Agda.Syntax.Common
moreRelevant | Agda.Syntax.Common
moreUsableModality | Agda.Syntax.Common
movePos | Agda.Syntax.Position
movePosByString | Agda.Syntax.Position
mparens |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.Compiler.JS.Pretty
mplus | Agda.Utils.Monad
msum | Agda.Utils.Monad
mul |
1 (Function) | Agda.Termination.Semiring
2 (Function) | Agda.Termination.SparseMatrix
multiLineText |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.TypeChecking.Pretty
MultipleAttributes | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
MultipleAttributes_ | Agda.Interaction.Options.Warnings
MultipleEllipses | Agda.Syntax.Concrete.Definitions.Errors
MultipleEllipses_ | Agda.Interaction.Options.Errors
MultipleFixityDecls | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MultipleFixityDecls_ | Agda.Interaction.Options.Errors
MultiplePolarityPragmas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MultiplePolarityPragmas_ | Agda.Interaction.Options.Errors
mustBeFinite | Agda.TypeChecking.SizedTypes.WarshallSolver
mustBePi | Agda.TypeChecking.Telescope
Mutual |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
MutualBlock |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MutualBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MutualChecks |
1 (Type/Class) | Agda.Syntax.Concrete.Definitions.Types
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types
mutualChecks |
1 (Function) | Agda.Syntax.Concrete.Definitions.Types
2 (Function) | Agda.TypeChecking.Rules.Decl
mutualCoverage | Agda.Syntax.Concrete.Definitions.Types
mutualCoverageCheck | Agda.Syntax.Info
MutualId |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MutualInfo |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
mutualInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mutuallyRecursive | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MutualNames | Agda.Termination.RecCheck
mutualNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mutualPositivity | Agda.Syntax.Concrete.Definitions.Types
mutualPositivityCheck | Agda.Syntax.Info
mutualRange | Agda.Syntax.Info
MutualS | Agda.Syntax.Abstract
mutualTermination | Agda.Syntax.Concrete.Definitions.Types
mutualTerminationCheck | Agda.Syntax.Info
mvFrozen | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvInstantiation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvJudgement | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvListeners | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvPermutation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mvTwin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mzero | Agda.Utils.Monad