Agda-2.6.2.2: 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
MainFunctionDef |
1 (Type/Class) | Agda.Compiler.MAlonzo.Primitives
2 (Data Constructor) | Agda.Compiler.MAlonzo.Primitives
mainFunctionDefs | Agda.Compiler.MAlonzo.Primitives
MainMode | Agda.Main
MainModePrintAgdaDir | Agda.Main
MainModePrintHelp | Agda.Main
MainModePrintVersion | Agda.Main
MainModeRun | Agda.Main
makeAbstract | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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
makeName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
makeOpen | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Open
makePatternVarsVisible | Agda.Interaction.MakeCase
makePi | Agda.Syntax.Concrete
makeProjection | Agda.TypeChecking.ProjectionLike
makeRHSEmptyRecord | Agda.Interaction.MakeCase
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.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
mapAbstraction | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
mapAnnotation | Agda.Syntax.Common
mapAPattern | Agda.Syntax.Abstract.Pattern
mapArgInfo | Agda.Syntax.Common
mapAwakeConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
mapBenchmarkOn | Agda.Utils.Benchmark
mapChangeT | Agda.Utils.Update
mapClosure | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Closure
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
mapEither3M | Agda.Utils.Three
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
mapKeysMonotonic | Agda.Utils.AssocList
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.Maybe.Strict
3 (Function) | Agda.Utils.List1
mapMaybeAndRest | Agda.Utils.List
mapMaybeM | Agda.Utils.Monad
mapMaybeMM | Agda.Utils.Monad
mapMemberShip | Agda.Utils.SmallSet
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
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
mapPragmaOptions | Agda.Interaction.Options.Lenses
mapQuantity | Agda.Syntax.Common
mapQuantityMod | Agda.Syntax.Common
mapRedEnv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mapRedEnvSt | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mapRedSt | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
mapScopeM | Agda.Syntax.Scope.Base
mapScopeM_ | Agda.Syntax.Scope.Base
mapScopeNS | Agda.Syntax.Scope.Base
mapScope_ | Agda.Syntax.Scope.Base
mapSleepingConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
mapSnd | Agda.Utils.Tuple
mapSndM | Agda.Utils.Tuple
mapSubTries | Agda.Utils.Trie
mapTCMT | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mapTimings | Agda.Utils.Benchmark
mapUsing | Agda.Syntax.Common
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.BiMap
2 (Function) | Agda.Utils.AssocList
mapWithKeyFixedTags | Agda.Utils.BiMap
mapWithKeyFixedTagsPrecondition | Agda.Utils.BiMap
mapWithKeyM | Agda.Utils.AssocList
mapWithKeyPrecondition | Agda.Utils.BiMap
MArgList | Agda.Auto.Syntax
markInjective | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
markInline | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
markStatic | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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.Coverage.Match
5 (Type/Class) | Agda.TypeChecking.Rewriting.NonLinMatch
match |
1 (Function) | Agda.Syntax.Parser.LookAhead
2 (Function) | Agda.TypeChecking.Coverage.Match
3 (Function) | Agda.TypeChecking.Rewriting.NonLinMatch
4 (Function) | Agda.Interaction.Highlighting.Vim
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
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.Compiler.Backend, Agda.TypeChecking.Monad
maxInversionDepth | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
maxName | Agda.TypeChecking.Level
MaxNat |
1 (Type/Class) | Agda.Utils.Monoid
2 (Data Constructor) | Agda.Utils.Monoid
maxViewCons | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
maxViewMax | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
maxViewSuc_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
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
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.Compiler.Backend, Agda.TypeChecking.Monad
MaybeReduced | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MaybeReducedArgs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MaybeReducedElims | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
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
mazRTEFloatImport | Agda.Compiler.MAlonzo.Compiler
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.Types, 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.Bag
3 (Function) | Agda.Utils.IntSet.Infinite
4 (Function) | Agda.Utils.SmallSet
5 (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
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
mergeEdges | Agda.TypeChecking.Positivity
mergeElim | Agda.TypeChecking.Patterns.Match
mergeElims | Agda.TypeChecking.Patterns.Match
mergeHiding | Agda.Syntax.Common
mergeModules | Agda.Compiler.JS.Compiler
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 |
1 (Data Constructor) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Syntax.Reflected
MetaArg | Agda.TypeChecking.Positivity.Occurrence
MetaCannotDependOn | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
metaCheck | Agda.TypeChecking.MetaVars.Occurs
MetaEnv | Agda.Auto.NarrowingSearch
MetaErasedSolution | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
metaFrozen | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MetaInstantiation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MetaIrrelevantSolution | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MetaKind | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
MetaliseOKH | Agda.Auto.Syntax
metaliseOKH | Agda.Auto.Syntax
metaliseokh | Agda.Auto.Syntax
MetaNameSuggestion | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
metaNameSuggestion | Agda.Syntax.Info
metaNumber | Agda.Syntax.Info
metaOccurs | Agda.TypeChecking.MetaVars.Occurs
MetaOccursInItself | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
metaOccursQName | Agda.TypeChecking.MetaVars.Occurs
MetaPriority |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
metaRange | Agda.Syntax.Info
MetaS | Agda.Syntax.Internal
metaScope | Agda.Syntax.Info
metasCreatedBy | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
MetaSet |
1 (Type/Class) | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
2 (Data Constructor) | Agda.TypeChecking.Free.Lazy
MetaStore | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
metaType | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
MetaV | Agda.Syntax.Internal
MetaVar | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Metavar |
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
MetaVariable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
meta_not_constructor | Agda.Auto.Typecheck
MExp | Agda.Auto.Syntax
mextrarefs | Agda.Auto.NarrowingSearch
miClosRange | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MId | Agda.Auto.Syntax
Middle | Agda.Syntax.Common
miGeneralizable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
miInterface | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
miMetaOccursCheck | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mimicGHCi | Agda.Interaction.EmacsTop
miModality | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
miMode | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
miNameSuggestion | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
miPrimitive | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MissingClauses | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
MissingDeclarations | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
MissingDeclarations_ | Agda.Interaction.Options.Warnings
MissingDefinition | Agda.Interaction.Highlighting.Precise
MissingDefinitions | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
MissingDefinitions_ | Agda.Interaction.Options.Warnings
MissingWithClauses | Agda.Syntax.Concrete.Definitions.Errors
miWarnings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
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
mkCon | Agda.TypeChecking.Records
mkDef | Agda.Syntax.Translation.ReflectedToAbstract
mkDefInfo | Agda.Syntax.Info
mkDefInfoInstance | Agda.Syntax.Info
mkDomainFree | Agda.Syntax.Abstract
mkGComp | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
mkIf | Agda.Compiler.MAlonzo.Compiler
mkInterfaceFile | Agda.Interaction.FindFile
mkIsSizeConstraint | Agda.TypeChecking.SizedTypes
mkLam |
1 (Function) | Agda.Syntax.Concrete
2 (Function) | Agda.TypeChecking.Substitute
mkLet |
1 (Function) | Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Function) | Agda.Syntax.Concrete
3 (Function) | Agda.Syntax.Abstract
mkLibM | Agda.Interaction.Library
mkMatrix | Agda.Utils.Warshall
mkMetaInfo | Agda.Syntax.Translation.ReflectedToAbstract
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 |
1 (Function) | Agda.Syntax.Abstract
2 (Function) | Agda.TypeChecking.Substitute
mkPiSort | Agda.TypeChecking.Substitute
mkPragma | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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
mkPrimSetOmega | Agda.TypeChecking.Primitive
mkProp | Agda.Syntax.Internal
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
mkVar | Agda.Syntax.Translation.ReflectedToAbstract
mkVarName | Agda.Syntax.Translation.ReflectedToAbstract
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
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
MNormal | Agda.Auto.Options
mobs | Agda.Auto.NarrowingSearch
Mod | Agda.Syntax.Concrete
Modality |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
modalityAction | Agda.TypeChecking.CheckInternal
modalityOfConst | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
modCohesion | Agda.Syntax.Common
modDecls | Agda.Syntax.Concrete
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
modifyArgOccurrences | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
modifyAwakeConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
modifyBenchmark |
1 (Function) | Agda.Utils.Benchmark
2 (Function) | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyCommandLineOptions | Agda.Interaction.Options.Lenses
modifyConcreteNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyContext | Agda.Syntax.Parser.Monad
modifyContextInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
modifyCounter | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics
modifyCurrentNameSpace | Agda.Syntax.Scope.Monad
modifyCurrentScope | Agda.Syntax.Scope.Monad
modifyCurrentScopeM | Agda.Syntax.Scope.Monad
modifyFunClauses | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
modifyGlobalDefinition | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyImportedSignature | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyIncludePaths | Agda.Interaction.Options.Lenses
modifyInstanceDefs | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyInteractionPoints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
modifyIORef | Agda.Utils.IORef
modifyIORef' | Agda.Utils.IORef
modifyLocalVars | Agda.Syntax.Scope.Monad
modifyMetaStore | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
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.Compiler.Backend, Agda.TypeChecking.Monad
modifyPersistentState | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyPersistentVerbosity | Agda.Interaction.Options.Lenses
modifyPragmaOptions | Agda.Interaction.Options.Lenses
modifySafeMode | Agda.Interaction.Options.Lenses
modifyScope | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyScopes | Agda.Syntax.Scope.Monad
modifyScope_ | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifySignature | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifySleepingConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
modifyStatistics | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics
modifySystem | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyTC | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyTC' | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyTCLens | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyTCLensM | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
modifyTheInteractionPoints | Agda.Interaction.InteractionTop
modifyVerbosity | Agda.Interaction.Options.Lenses
modName | Agda.Compiler.JS.Syntax
modname | Agda.Compiler.JS.Pretty
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 (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.Compiler.Backend, Agda.TypeChecking.Monad
ModuleAssignment |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
ModuleCheckMode | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ModuleContents | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
moduleContents | Agda.Interaction.BasicOps
ModuleDefinedInOtherFile | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ModuleDoesntExport | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
ModuleNameHash |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
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.Compiler.Backend, Agda.TypeChecking.Monad
ModuleNotName | Agda.Syntax.Scope.Base
moduleParamsToApply | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
moduleParser |
1 (Function) | Agda.Syntax.Parser.Parser
2 (Function) | Agda.Syntax.Parser
ModulePragma | Agda.Utils.Haskell.Syntax
ModuleScopeChecked | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ModulesInScope | Agda.Syntax.Scope.Base
ModuleTag | Agda.Syntax.Scope.Base
ModuleToSource | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ModuleTypeChecked | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadAbsToCon | Agda.TypeChecking.Pretty, Agda.Syntax.Translation.AbstractToConcrete
MonadAddContext | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
MonadBench | Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
MonadBlock | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadChange | Agda.Utils.Update
MonadCheckInternal | Agda.TypeChecking.CheckInternal
MonadConstraint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
MonadConversion | Agda.TypeChecking.Conversion
MonadDebug | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadFixityError | Agda.Syntax.Concrete.Fixity
MonadFresh | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadGetDefs | Agda.Syntax.Internal.Defs
MonadGHCIO | Agda.Compiler.MAlonzo.Compiler
MonadInteractionPoints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
MonadMatch | Agda.TypeChecking.Patterns.Match
MonadMetaSolver | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
MonadPlus | Agda.Utils.Monad
MonadPretty | Agda.TypeChecking.Pretty
MonadReduce | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadReflectedToAbstract | Agda.Syntax.Translation.ReflectedToAbstract
MonadReify | Agda.Syntax.Translation.InternalToAbstract
MonadStatistics | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics
MonadStConcreteNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadTCEnv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadTCError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadTCM | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadTCState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MonadTer | Agda.Termination.Monad
MonadTrace | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace
MonadWarning | Agda.TypeChecking.Warnings
moreCohesion | Agda.Syntax.Common
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 |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.Compiler.JS.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
MultipleAttributes | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
MultipleAttributes_ | Agda.Interaction.Options.Warnings
MultipleEllipses | Agda.Syntax.Concrete.Definitions.Errors
MultipleFixityDecls | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MultiplePolarityPragmas | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mustBeFinite | Agda.TypeChecking.SizedTypes.WarshallSolver
mustBePi | Agda.TypeChecking.Telescope
MutId | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Mutual |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
MutualBlock |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mutualBlockOf | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual
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 | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MutualInfo |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
mutualInfo | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mutuallyRecursive | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
MutualNames | Agda.Termination.Monad
mutualNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mutualPositivity | Agda.Syntax.Concrete.Definitions.Types
mutualPositivityCheck | Agda.Syntax.Info
mutualRange | Agda.Syntax.Info
mutualTermination | Agda.Syntax.Concrete.Definitions.Types
mutualTerminationCheck | Agda.Syntax.Info
mvFrozen | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mvInfo | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mvInstantiation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mvJudgement | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mvListeners | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mvPermutation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mvPriority | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
mvTwin | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
MyMB | Agda.Auto.Syntax
MyPB | Agda.Auto.Syntax
mzero | Agda.Utils.Monad