Agda-2.6.0.1: 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.Auto.Options
Macro |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
3 (Data Constructor) | Agda.Syntax.Abstract
MacroDef | Agda.Syntax.Common
MacroName | Agda.Syntax.Scope.Base
main | Agda.Main
MainInterface |
1 (Type/Class) | Agda.Interaction.Imports
2 (Data Constructor) | Agda.Interaction.Imports
makeAbstract | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
makeAbstractClause | Agda.Interaction.MakeCase
makeAbsurdClause | Agda.Interaction.MakeCase
makeAll | Agda.Utils.IndexedList
makeCase | Agda.Interaction.MakeCase
MakeCaseVariant | Agda.Interaction.Response
makeInstance | Agda.Syntax.Common
makeInstance' | Agda.Syntax.Common
makeOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend
makePatternVarsVisible | Agda.Interaction.MakeCase
makePi | Agda.Syntax.Concrete
makeProjection | Agda.TypeChecking.ProjectionLike
makeSubstitution | Agda.TypeChecking.Rewriting.NonLinMatch
malformed | Agda.TypeChecking.Serialise.Base
many | Agda.Utils.Parser.ReadP
many1 | Agda.Utils.Parser.ReadP
ManyHoles | Agda.Utils.AffineHole
manyTill | Agda.Utils.Parser.ReadP
Map | Agda.Utils.TypeLevel
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
mapAbsoluteIncludePaths | Agda.Interaction.Options.Lenses
mapAPattern | Agda.Syntax.Abstract.Pattern
mapArgInfo | Agda.Syntax.Common
mapAwakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapBenchmarkOn | Agda.Utils.Benchmark
mapClosure | Agda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapCommandLineOptions | Agda.Interaction.Options.Lenses
mapConName | Agda.Syntax.Internal
mapCPattern | Agda.Syntax.Concrete.Pattern
mapCurrentAccount | Agda.Utils.Benchmark
mapEither |
1 (Function) | Agda.Utils.Either
2 (Function) | Agda.Utils.List
mapEither3M | Agda.Utils.Three
mapExceptT | Agda.Utils.Except
mapExpr |
1 (Function) | Agda.Syntax.Concrete.Generic
2 (Function) | Agda.Syntax.Abstract.Views
mapFlag | Agda.Interaction.Options
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
mapKeysMonotonic | Agda.Utils.AssocList
mapLeft | Agda.Utils.Either
mapLHSHead | Agda.Syntax.Abstract.Pattern
mapLhsOriginalPattern | Agda.Syntax.Concrete.Pattern
mapLhsOriginalPatternM | Agda.Syntax.Concrete.Pattern
mapListT | Agda.Utils.ListT
mapM' | Agda.Utils.Monad
mapMaybe |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.HashMap
3 (Function) | Agda.Utils.Maybe.Strict
mapMaybeAndRest | Agda.Utils.List
mapMaybeM | Agda.Utils.Monad
mapMaybeWithKey | Agda.Utils.HashMap
mapMListT | Agda.Utils.ListT
mapMListT_alt | Agda.Utils.ListT
mapMM | Agda.Utils.Monad
mapModality | Agda.Syntax.Common
mapModalityArgInfo | Agda.Syntax.Common
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
mapping | Agda.Interaction.Highlighting.Precise
mapPragmaOptions | Agda.Interaction.Options.Lenses
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
MapS | Agda.Auto.Convert
mapSafeMode | Agda.Interaction.Options.Lenses
mapScope | Agda.Syntax.Scope.Base
mapScope' | Agda.Syntax.Scope.Base
mapScopeInfo | Agda.Syntax.Scope.Base
mapScopeM | Agda.Syntax.Scope.Base
mapScopeM_ | 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.Scope.Monad
mapVarMap | Agda.TypeChecking.Free.Lazy
mapVerbosity | Agda.Interaction.Options.Lenses
mapVisitedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mapWithEdge | Agda.Utils.Graph.AdjacencyMap.Unidirectional
mapWithIndex | Agda.Utils.IndexedList
mapWithKey |
1 (Function) | Agda.Utils.HashMap
2 (Function) | Agda.Utils.AssocList
mapWithKeyM | Agda.Utils.AssocList
MArgList | Agda.Auto.Syntax
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.Parser.Literate
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
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.DisplayForm
5 (Type/Class) | Agda.TypeChecking.Rewriting.NonLinMatch
6 (Type/Class) | Agda.TypeChecking.Coverage.Match
match |
1 (Function) | Agda.Syntax.Parser.LookAhead
2 (Function) | Agda.TypeChecking.DisplayForm
3 (Function) | Agda.Interaction.Highlighting.Vim
4 (Function) | Agda.TypeChecking.Rewriting.NonLinMatch
5 (Function) | Agda.TypeChecking.Coverage.Match
match' |
1 (Function) | Agda.Syntax.Parser.LookAhead
2 (Function) | Agda.TypeChecking.CompiledClause.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.Occurrence
matchedArgs | Agda.TypeChecking.Patterns.Match
matches | Agda.Interaction.Highlighting.Vim
matchingBlocked | Agda.TypeChecking.Rewriting.NonLinMatch
matchPattern | Agda.TypeChecking.Patterns.Match
matchPatterns | Agda.TypeChecking.Patterns.Match
matchPatternSyn | Agda.Syntax.Abstract.PatternSynonyms
matchPatternSynP | Agda.Syntax.Abstract.PatternSynonyms
matchType | Agda.Auto.Convert
Matrix |
1 (Type/Class) | Agda.Termination.SparseMatrix
2 (Data Constructor) | Agda.Termination.SparseMatrix
3 (Type/Class) | Agda.Utils.Warshall
matrix | Agda.Utils.Warshall
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
maxVarOcc | Agda.TypeChecking.Free.Lazy
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.TypeChecking.Injectivity
maybeAbort | Agda.Interaction.InteractionTop
maybeFastReduceTerm | Agda.TypeChecking.Reduce
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
maybeor | Agda.Auto.Typecheck
MaybePlaceholder | Agda.Syntax.Common
maybePlaceholder | Agda.Syntax.Concrete.Operators.Parser
maybePrimCon | Agda.TypeChecking.Level
maybePrimDef | Agda.TypeChecking.Level
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
MaybeWarnings | Agda.Interaction.Imports
MaybeWarnings' | Agda.Interaction.Imports
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
mazerror | Agda.Compiler.MAlonzo.Misc
mazIncompleteMatch | Agda.Compiler.MAlonzo.Misc
mazMod | Agda.Compiler.MAlonzo.Misc
mazMod' | Agda.Compiler.MAlonzo.Misc
mazName | Agda.Compiler.MAlonzo.Misc
mazRTE | Agda.Compiler.MAlonzo.Misc
mazstr | Agda.Compiler.MAlonzo.Misc
mazUnreachableError | Agda.Compiler.MAlonzo.Misc
MB | Agda.Auto.NarrowingSearch
mbcase | Agda.Auto.NarrowingSearch
mbfailed | Agda.Auto.NarrowingSearch
mbind | Agda.Auto.NarrowingSearch
mbpcase | Agda.Auto.NarrowingSearch
mbret | Agda.Auto.NarrowingSearch
MCaseSplit | Agda.Auto.Options
mcompoint | Agda.Auto.NarrowingSearch
mcons | Agda.Utils.List
MdFileType | Agda.Syntax.Common
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
4 (Function) | Agda.Utils.IntSet.Infinite
5 (Function) | Agda.Utils.Trie
MemberId |
1 (Type/Class) | Agda.Compiler.JS.Syntax
2 (Data Constructor) | Agda.Compiler.JS.Syntax
Memo | Agda.TypeChecking.Serialise.Base
memo | Agda.Utils.Memo
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
merge | Agda.Interaction.Highlighting.Precise
mergeC | Agda.Interaction.Highlighting.Precise
mergeEdges | Agda.TypeChecking.Positivity
mergeElim | Agda.TypeChecking.Patterns.Match
mergeElims | Agda.TypeChecking.Patterns.Match
mergeHiding | Agda.Syntax.Common
mergeInterface | Agda.Interaction.Imports
mergeNames | Agda.Syntax.Scope.Base
mergeNotations | Agda.Syntax.Fixity
mergePatternSynDefs | Agda.Syntax.Abstract.PatternSynonyms
mergeScope | Agda.Syntax.Scope.Base
mergeScopes | Agda.Syntax.Scope.Base
Meta |
1 (Data Constructor) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Syntax.Reflected
MetaArg | Agda.TypeChecking.Positivity.Occurrence
MetaCannotDependOn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaEnv | Agda.Auto.NarrowingSearch
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
MetaIrrelevantSolution | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaKind | Agda.TypeChecking.MetaVars
MetaLevel | Agda.Syntax.Internal
MetaliseOKH | Agda.Auto.Syntax
metaliseOKH | Agda.Auto.Syntax
metaliseokh | Agda.Auto.Syntax
MetaNameSuggestion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
metaNameSuggestion | Agda.Syntax.Info
metaNumber | Agda.Syntax.Info
metaOccurs | Agda.TypeChecking.MetaVars.Occurs
MetaOccursInItself | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
metaOccursQName | Agda.TypeChecking.MetaVars.Occurs
metaParseExpr | Agda.Interaction.CommandLine
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
metaScope | Agda.Syntax.Info
metasCreatedBy | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaSet | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
MetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MetaV | Agda.Syntax.Internal
MetaVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Metavar |
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
MetaVariable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
meta_not_constructor | Agda.Auto.Typecheck
MExp | Agda.Auto.Syntax
mextrarefs | Agda.Auto.NarrowingSearch
miClosRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MId | Agda.Auto.Syntax
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
miMetaOccursCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mimicGHCi | Agda.Interaction.EmacsTop
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
minus | Agda.Interaction.Highlighting.Range
miPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MissingClauses | Agda.Syntax.Internal
MissingDefinitions | Agda.Syntax.Concrete.Definitions
MissingDefinitions_ | Agda.Interaction.Options.Warnings
MissingWithClauses | Agda.Syntax.Concrete.Definitions
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
mkAbs | Agda.TypeChecking.Substitute.Class, 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.TypeChecking.Records
mkDef | Agda.Syntax.Translation.ReflectedToAbstract
mkDefInfo | Agda.Syntax.Info
mkDefInfoInstance | Agda.Syntax.Info
mkExceptT | Agda.Utils.Except
mkIf | Agda.Compiler.MAlonzo.Compiler
mkLam | Agda.TypeChecking.Substitute
mkLet |
1 (Function) | Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Function) | Agda.Syntax.Abstract
mkMatrix | Agda.Utils.Warshall
MkName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mkName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mkName_ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
mkNotation | Agda.Syntax.Notation
mkPi | 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
mkPrimFun4 | Agda.TypeChecking.Primitive
mkPrimInjective | Agda.TypeChecking.Primitive
mkPrimLevelMax | Agda.TypeChecking.Primitive
mkPrimLevelSuc | Agda.TypeChecking.Primitive
mkPrimLevelZero | Agda.TypeChecking.Primitive
mkPrimSetOmega | Agda.TypeChecking.Primitive
mkProp | Agda.Syntax.Internal
mkSet | Agda.Syntax.Translation.ReflectedToAbstract
mkTApp | Agda.Syntax.Treeless, Agda.Compiler.Backend
mkTLam | Agda.Syntax.Treeless, Agda.Compiler.Backend
mkType | Agda.Syntax.Internal
mkWeakIORef | Agda.Utils.IORef
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.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
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
mnameToQName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
MNormal | Agda.Auto.Options
mobs | Agda.Auto.NarrowingSearch
Modality |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
modalityOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Mode |
1 (Type/Class) | Agda.Utils.Pretty
2 (Type/Class) | Agda.Auto.Options
3 (Type/Class) | Agda.Interaction.Imports
mode | Agda.Utils.Pretty
modFile | Agda.TypeChecking.Serialise.Base
modifyAbsoluteIncludePaths | Agda.Interaction.Options.Lenses
modifyAbstractClause | Agda.Auto.Convert
modifyAbstractExpr | Agda.Auto.Convert
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 |
1 (Function) | Agda.Utils.Benchmark
2 (Function) | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
modifyCommandLineOptions | Agda.Interaction.Options.Lenses
modifyContext | Agda.TypeChecking.Monad.Context, 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
modifyMetaStore | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
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
modQuantity | Agda.Syntax.Common
modRelevance | Agda.Syntax.Common
Module |
1 (Type/Class) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Utils.Haskell.Syntax
3 (Type/Class) | Agda.Compiler.JS.Syntax
4 (Data Constructor) | Agda.Compiler.JS.Syntax
5 (Type/Class) | Agda.Syntax.Concrete
6 (Data Constructor) | Agda.Syntax.Concrete
7 (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, Agda.Compiler.Backend
ModuleAssignment |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
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
ModuleDoesntExport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ModuleDoesntExport_ | Agda.Interaction.Options.Warnings
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, 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
moduleName | Agda.Interaction.FindFile
ModuleNameDoesntMatchFileName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
moduleNameParser |
1 (Function) | Agda.Syntax.Parser.Parser
2 (Function) | Agda.Syntax.Parser
moduleNameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
moduleNameRange | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
moduleNameToFileName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
ModuleNameUnexpected | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
ModulesInScope | Agda.Syntax.Scope.Base
ModuleTag | Agda.Syntax.Scope.Base
ModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadBench | Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
MonadChange | Agda.Utils.Update
MonadDebug | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadError | Agda.Utils.Except
MonadFixityError | Agda.Syntax.Concrete.Fixity
MonadGetDefs | Agda.Syntax.Internal.Defs
MonadPlus | Agda.Utils.Monad
MonadReduce | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MonadTCEnv | 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
moreQuantity | Agda.Syntax.Common
moreRelevant | Agda.Syntax.Common
moreUsableModality | Agda.Syntax.Common
MOT | Agda.Auto.Convert
Move |
1 (Data Constructor) | Agda.Auto.NarrowingSearch
2 (Type/Class) | Agda.Auto.SearchControl
Move' | Agda.Auto.NarrowingSearch
moveCost | Agda.Auto.NarrowingSearch
moveNext | Agda.Auto.NarrowingSearch
movePos | Agda.Syntax.Position
movePosByString | Agda.Syntax.Position
mparens | Agda.Utils.Pretty
mplus | Agda.Utils.Monad
mpret | Agda.Auto.NarrowingSearch
mprincipalpresent | Agda.Auto.NarrowingSearch
MRefine | Agda.Auto.Options
mul |
1 (Function) | Agda.Termination.Semiring
2 (Function) | Agda.Termination.SparseMatrix
multiLineText |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
MultipleEllipses | Agda.Syntax.Concrete.Definitions
MultipleFixityDecls | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
MultiplePolarityPragmas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
munch | Agda.Utils.Parser.ReadP
munch1 | Agda.Utils.Parser.ReadP
mustBeFinite | Agda.TypeChecking.SizedTypes.WarshallSolver
mustBePi | Agda.TypeChecking.Telescope
MutId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
mutualBlockOf | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mutualChecks | Agda.TypeChecking.Rules.Decl
MutualId | 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.Monad
mutualNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
mutualPositivityCheck | Agda.Syntax.Info
mutualRange | Agda.Syntax.Info
mutualTermCheck | 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
MyMB | Agda.Auto.Syntax
MyPB | Agda.Auto.Syntax
mzero | Agda.Utils.Monad