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 - F

Face | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FaceConstraintCannotBeHidden | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FaceConstraintCannotBeHidden_ | Agda.Interaction.Options.Warnings
FaceConstraintCannotBeNamed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FaceConstraintCannotBeNamed_ | Agda.Interaction.Options.Warnings
FaceConstraintDisjunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FaceConstraintDisjunction_ | Agda.Interaction.Options.Errors
FaceConstraintUnsatisfiable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FaceConstraintUnsatisfiable_ | Agda.Interaction.Options.Errors
faceEqns | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
faceRHS | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Fail |
1 (Type/Class) | Agda.Utils.Fail
2 (Data Constructor) | Agda.Utils.Fail
3 (Data Constructor) | Agda.TypeChecking.CompiledClause
failOnRecordFieldWarnings | Agda.TypeChecking.Records
fakeD | Agda.Compiler.MAlonzo.Misc
FakeDecl | Agda.Utils.Haskell.Syntax
fakeDecl | Agda.Compiler.MAlonzo.Misc
fakeDQ | Agda.Compiler.MAlonzo.Misc
fakeDS | Agda.Compiler.MAlonzo.Misc
FakeExp | Agda.Utils.Haskell.Syntax
fakeExp | Agda.Compiler.MAlonzo.Misc
FakeType | Agda.Utils.Haskell.Syntax
fakeType | Agda.Compiler.MAlonzo.Misc
fallThrough | Agda.TypeChecking.CompiledClause
false | Agda.Utils.Boolean
FamilyOrNot | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
familyOrNot | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
famThing | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
farEmpty | Agda.TypeChecking.Serialise.Base
farFresh | Agda.TypeChecking.Serialise.Base
fastDistinct | Agda.Utils.List
fastNormalise | Agda.TypeChecking.Reduce.Fast
fastReduce | Agda.TypeChecking.Reduce.Fast
Favorites |
1 (Type/Class) | Agda.Utils.Favorites
2 (Data Constructor) | Agda.Utils.Favorites
fcat | Agda.Syntax.Common.Pretty
feExtra | Agda.TypeChecking.Free.Lazy
feFlexRig | Agda.TypeChecking.Free.Lazy
feIgnoreSorts | Agda.TypeChecking.Free.Lazy
feModality | Agda.TypeChecking.Free.Lazy
feSingleton | Agda.TypeChecking.Free.Lazy
fiber | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
Field |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Type/Class) | Agda.Syntax.Abstract
4 (Data Constructor) | Agda.Syntax.Abstract
field1 | Agda.Utils.Lens.Examples
field2 | Agda.Utils.Lens.Examples
FieldAssignment |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
FieldAssignment' | Agda.Syntax.Concrete
FieldBlock | Agda.Syntax.Concrete.Definitions.Types
fieldLabelModifier | Agda.Interaction.JSON
FieldName | Agda.Syntax.Scope.Base
FieldOutsideRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FieldOutsideRecord_ | Agda.Interaction.Options.Errors
FieldOverlap | Agda.Syntax.Common
FieldS | Agda.Syntax.Abstract
Fields |
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
FieldSig | Agda.Syntax.Concrete
figureOutTopLevelModule | Agda.Syntax.Parser.Helpers
File | Agda.Utils.FileId
FileDict |
1 (Type/Class) | Agda.Utils.FileId
2 (Data Constructor) | Agda.Utils.FileId
fileDict |
1 (Function) | Agda.Utils.FileId
2 (Function) | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FileDictBuilder |
1 (Type/Class) | Agda.Utils.FileId, Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Utils.FileId
fileDictBuilder | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FileDictWithBuiltins |
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
fileFromId | Agda.Utils.FileId, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FileId |
1 (Type/Class) | Agda.Utils.FileId, Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Utils.FileId
FileNotFound | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FileNotFound_ | Agda.Interaction.Options.Errors
filePath | Agda.Utils.FileName
filePos | Agda.Interaction.Library.Base, Agda.Interaction.Library
FileToId | Agda.Utils.FileId
fileToId | Agda.Utils.FileId
FileType | Agda.Syntax.Common
filter |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.Utils.VarSet
3 (Function) | Agda.Utils.Set1
4 (Function) | Agda.Utils.Map1
5 (Function) | Agda.Utils.Trie
filterAndRest | Agda.Utils.List
filterCallStack | Agda.Utils.CallStack
FilterCandidates | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
filterEdges | Agda.Utils.Graph.AdjacencyMap.Unidirectional
filterGE | Agda.Utils.VarSet
filterKeys | Agda.Utils.Map
filterM | Agda.Utils.Monad
filterMaybe |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
filterNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
filterNodesKeepingEdges | Agda.Utils.Graph.AdjacencyMap.Unidirectional
filterScope | Agda.Syntax.Scope.Base
filterTCWarnings | Agda.TypeChecking.Pretty.Warning
filterUsed | Agda.Syntax.Treeless, Agda.Compiler.Backend
filterVarMap | Agda.TypeChecking.Free
filterVarMapToList | Agda.TypeChecking.Free
filterWithKey | Agda.Utils.Map1
FinalChecks | Agda.TypeChecking.Rules.Decl
finally |
1 (Function) | Agda.Utils.Monad
2 (Function) | Agda.Utils.Benchmark
finally_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FinalTwoArgumentsNotVisible | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
find | Agda.Utils.List1
FindError | Agda.Interaction.FindFile
findErrorToTypeError | Agda.Interaction.FindFile
findFile | Agda.Interaction.FindFile
findFile' | Agda.Interaction.FindFile
findFile'' | Agda.Interaction.FindFile
findFile'_ | Agda.Interaction.FindFile
findIdx | Agda.TypeChecking.MetaVars
findIndex |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
FindInstance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
findInstance | Agda.TypeChecking.InstanceArguments
FindInstanceOF | Agda.Interaction.Base
findInteractionPoint_ | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
findInterfaceFile | Agda.Interaction.FindFile
findInterfaceFile' | Agda.Interaction.FindFile
findLib' | Agda.Interaction.Library
findMax |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
findMentions | Agda.Interaction.SearchAbout
findMin |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
findNameInScope | Agda.Syntax.Scope.Base
findOverlap | Agda.Utils.List
findPossibleRecords | Agda.TypeChecking.Records
findProjectRoot | Agda.Interaction.Library
findRigidBelow | Agda.TypeChecking.SizedTypes.WarshallSolver
findWithDefault | Agda.Utils.Map1
findWithIndex | Agda.Utils.List
findWithInfo | Agda.Utils.IO.Directory
fingerprintNoinline | Agda.TypeChecking.Serialise.Base
firstHole | Agda.Utils.Zipper
firstMeta | Agda.Syntax.Internal.MetaVars
firstNonTakenName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
firstOr | Agda.Mimer.Options
firstPart | Agda.TypeChecking.Telescope
fitsIn | Agda.TypeChecking.Rules.Data
fittingNamedArg | Agda.Syntax.Common
fix | Agda.Compiler.JS.Substitution
FixedPoint | Agda.Compiler.ToTreeless
FixingCohesion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FixingCohesion_ | Agda.Interaction.Options.Warnings
FixingPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FixingPolarity_ | Agda.Interaction.Options.Warnings
FixingRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FixingRelevance_ | Agda.Interaction.Options.Warnings
Fixities | Agda.Syntax.Concrete.Fixity
fixitiesAndPolarities | Agda.Syntax.Concrete.Fixity
Fixity |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
Fixity' |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
fixityAssoc | Agda.Syntax.Common
FixityInRenamingModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FixityInRenamingModule_ | Agda.Interaction.Options.Warnings
FixityLevel | Agda.Syntax.Common
fixityLevel | Agda.Syntax.Common
fixityRange | Agda.Syntax.Common
Flag | Agda.Interaction.Options, Agda.Compiler.Backend
Flat | Agda.Syntax.Common
flatName | Agda.Compiler.JS.Compiler
FlatScope | Agda.Syntax.Scope.Flat
flatten | Agda.TypeChecking.Positivity
flattenContext | Agda.TypeChecking.Telescope
flattenScope | Agda.Syntax.Scope.Flat
flattenTel | Agda.TypeChecking.Telescope
FldName | Agda.Syntax.Scope.Base
Flex |
1 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax
flex | Agda.TypeChecking.SizedTypes.Syntax
flexArgInfo | Agda.TypeChecking.Rules.LHS.Problem
FlexChoice | Agda.TypeChecking.Rules.LHS.Problem
flexForced | Agda.TypeChecking.Rules.LHS.Problem
Flexible | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
FlexibleVar |
1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem
flexibleVariables | Agda.TypeChecking.SizedTypes
FlexibleVarKind | Agda.TypeChecking.Rules.LHS.Problem
FlexibleVars | Agda.TypeChecking.Rules.LHS.Problem
flexibleVars | Agda.TypeChecking.Free
flexibly | Agda.TypeChecking.MetaVars.Occurs
FlexId | Agda.TypeChecking.SizedTypes.Syntax
flexId | Agda.TypeChecking.SizedTypes.Syntax
FlexK | Agda.TypeChecking.DiscrimTree.Types
flexKind | Agda.TypeChecking.Rules.LHS.Problem
FlexOf | Agda.TypeChecking.SizedTypes.Syntax
flexPos | Agda.TypeChecking.Rules.LHS.Problem
FlexRig | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
FlexRig' | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
FlexRigMap |
1 (Type/Class) | Agda.TypeChecking.Free.Lazy
2 (Data Constructor) | Agda.TypeChecking.Free.Lazy
flexRigOccurrenceIn | Agda.TypeChecking.Free
Flexs | Agda.TypeChecking.SizedTypes.Syntax
flexs | Agda.TypeChecking.SizedTypes.Syntax
flexVar | Agda.TypeChecking.Rules.LHS.Problem
flexVars | Agda.TypeChecking.Rules.LHS.Unify.Types
flipCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
flipP | Agda.Utils.Permutation
float | Agda.Syntax.Common.Pretty
flushInstanceConstraints | Agda.TypeChecking.InstanceArguments
fmapReduce | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fmapTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
focus | Agda.Utils.Lens
foldA | Agda.Utils.Applicative
foldable | Agda.Interaction.JSON
foldAPattern | Agda.Syntax.Abstract.Pattern
foldCPattern | Agda.Syntax.Concrete.Pattern
FoldDecl | Agda.Syntax.Concrete.Generic
foldDecl | Agda.Syntax.Concrete.Generic
foldExpr |
1 (Function) | Agda.Syntax.Concrete.Generic
2 (Function) | Agda.Syntax.Abstract.Views
FoldExprFn | Agda.Syntax.Abstract.Views
FoldExprRecFn | Agda.Syntax.Abstract.Views
foldl |
1 (Function) | Agda.Utils.Map1
2 (Function) | Agda.Utils.Set1
foldl' |
1 (Function) | Agda.Utils.Map1
2 (Function) | Agda.Utils.Set1
foldl1 |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
foldl1' |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
foldlArray | Agda.Utils.IArray
foldlArray' | Agda.Utils.IArray
foldlArrayM' | Agda.Utils.IArray
foldListT | Agda.Utils.ListT
foldlWithKey | Agda.Utils.Map1
foldlWithKey' | Agda.Utils.Map1
foldM | Agda.Utils.Monad
foldMapA | Agda.Utils.Applicative
foldMapWithKey | Agda.Utils.Map1
foldMatch | Agda.TypeChecking.Patterns.Match
foldPattern | Agda.Syntax.Internal.Pattern
Foldr | Agda.Utils.TypeLevel
foldr |
1 (Function) | Agda.Utils.Map1
2 (Function) | Agda.Utils.Set1
3 (Function) | Agda.Utils.List1
Foldr' | Agda.Utils.TypeLevel
foldr' |
1 (Function) | Agda.Utils.Map1
2 (Function) | Agda.Utils.Set1
foldr1 |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
foldr1' |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
foldrAPattern | Agda.Syntax.Abstract.Pattern
foldrArray | Agda.Utils.IArray
foldrArray' | Agda.Utils.IArray
foldrArrayM' | Agda.Utils.IArray
foldrCPattern | Agda.Syntax.Concrete.Pattern
foldrMetaSet | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
foldrPattern | Agda.Syntax.Internal.Pattern
foldrTelescopeM | Agda.TypeChecking.Telescope
foldrWithKey | Agda.Utils.Map1
foldrWithKey' | Agda.Utils.Map1
foldTerm | Agda.Syntax.Internal.Generic
followedBy | Agda.Syntax.Parser.LexActions
for | Agda.Utils.Functor
forA | Agda.Utils.Applicative
forallFaceMaps | Agda.TypeChecking.Conversion
forallM | Agda.Utils.Monad
forallPi | Agda.Syntax.Parser.Helpers
forallQ | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
forArray_ | Agda.Utils.IArray
Forced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ForcedConstructorNotInstantiated | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ForcedConstructorNotInstantiated_ | Agda.Interaction.Options.Errors
forceEtaExpandRecord | Agda.TypeChecking.Records
ForceNotFree | Agda.TypeChecking.Free.Reduce
forceNotFree | Agda.TypeChecking.Free.Reduce
forcePiUsingInjectivity | Agda.TypeChecking.Injectivity
forceSort | Agda.TypeChecking.Rules.Data
ForeignCode |
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
ForeignCodeStack |
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
ForeignFileHeaderPragma | Agda.Compiler.MAlonzo.Pragmas
foreignHaskell | Agda.Compiler.MAlonzo.Pragmas
ForeignImport | Agda.Compiler.MAlonzo.Pragmas
ForeignOther | Agda.Compiler.MAlonzo.Pragmas
ForeignPragma | Agda.Syntax.Concrete
forEither3M | Agda.Utils.Three
forgetAll | Agda.Utils.IndexedList
forgetIndex | Agda.Utils.IndexedList
forgetLoneSigs | Agda.Syntax.Concrete.Definitions.Monad
forkTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
forM | Agda.Utils.Monad
forM' | Agda.Utils.Monad
formatDebugMessage | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
formatLibError | Agda.Interaction.Library.Base
formatLibErrors | Agda.Interaction.Library.Base
formatLibPositionInfo | Agda.Interaction.Library.Base
forMaybe |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
forMaybeM | Agda.Utils.Monad
forMaybeMM | Agda.Utils.Monad
forMM | Agda.Utils.Monad
forMM_ | Agda.Utils.Monad
forM_ | Agda.Utils.Monad
Frac | Agda.Utils.Haskell.Syntax
Frame | Agda.TypeChecking.CompiledClause.Match
Free |
1 (Type/Class) | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
2 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
FreeEnv |
1 (Type/Class) | Agda.TypeChecking.Free.Lazy
2 (Data Constructor) | Agda.TypeChecking.Free.Lazy
FreeEnv' | Agda.TypeChecking.Free.Lazy
freeIn |
1 (Function) | Agda.TypeChecking.Free
2 (Function) | Agda.Compiler.Treeless.Subst
freeInIgnoringSorts | Agda.TypeChecking.Free
FreeM | Agda.TypeChecking.Free.Lazy
FreeT | Agda.TypeChecking.Free.Lazy
FreeVariables | Agda.Syntax.Common
freeVariablesFromList | Agda.Syntax.Common
freeVars |
1 (Function) | Agda.TypeChecking.Free
2 (Function) | Agda.Compiler.Treeless.Subst
freeVars' | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
freeVarsIgnore | Agda.TypeChecking.Free
freeVarsToApply | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freezeMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fresh | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshAbstractName | Agda.Syntax.Scope.Monad
freshAbstractName_ | Agda.Syntax.Scope.Monad
freshAbstractQName | Agda.Syntax.Scope.Monad
freshAbstractQName' | Agda.Syntax.Scope.Monad
freshAbstractQName'_ | Agda.TypeChecking.Rules.Data
FreshAndReuse |
1 (Type/Class) | Agda.TypeChecking.Serialise.Base
2 (Data Constructor) | Agda.TypeChecking.Serialise.Base
freshConcreteName | Agda.Syntax.Scope.Monad
freshInt | Agda.TypeChecking.Conversion.Pure
freshInteractionId | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshLens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FreshName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshNameId | Agda.TypeChecking.Conversion.Pure
FreshNameMode | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Concrete, Agda.Syntax.Abstract, Agda.Compiler.Backend
freshName_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshNoName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshNoName_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshProblemId | Agda.TypeChecking.Conversion.Pure
FreshRecCon | Agda.Syntax.Abstract
freshRecordName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshTCM | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FreshThings |
1 (Type/Class) | Agda.TypeChecking.Conversion.Pure
2 (Data Constructor) | Agda.TypeChecking.Conversion.Pure
from | Agda.Interaction.Highlighting.Range
fromAbsName | Agda.TypeChecking.Serialise.Instances.Abstract
FromArgs | Agda.Interaction.JSON
fromAscList |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
3 (Function) | Agda.Utils.BoolSet
4 (Function) | Agda.Utils.SmallSet
fromAscListWith | Agda.Utils.Map1
fromAscListWithKey | Agda.Utils.Map1
fromBlocked | Agda.TypeChecking.Reduce
fromBool | Agda.Utils.Boolean
fromBool1 | Agda.Utils.Boolean
fromBool2 | Agda.Utils.Boolean
fromCallSiteList | Agda.Utils.CallStack
fromCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fromConPatternInfo | Agda.Syntax.Internal
fromCType | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
fromDescList |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
fromDescListWith | Agda.Utils.Map1
fromDescListWithKey | Agda.Utils.Map1
fromDistinctAscendingLists | Agda.Utils.BiMap
fromDistinctAscendingListsPrecondition | Agda.Utils.BiMap
fromDistinctAscList |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
3 (Function) | Agda.Utils.BoolSet
4 (Function) | Agda.Utils.SmallSet
fromDistinctDescList |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
fromDotNetTime | Agda.Interaction.JSON
fromEdges | Agda.Utils.Graph.AdjacencyMap.Unidirectional
fromEdgesWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional
fromEncoding | Agda.Interaction.JSON
fromImportedName | Agda.Syntax.Common
fromIndexList | Agda.Termination.SparseMatrix
FromJSON | Agda.Interaction.JSON
fromJSON | Agda.Interaction.JSON
FromJSON1 | Agda.Interaction.JSON
FromJSON2 | Agda.Interaction.JSON
FromJSONKey | Agda.Interaction.JSON
fromJSONKey | Agda.Interaction.JSON
FromJSONKeyCoerce | Agda.Interaction.JSON
FromJSONKeyFunction | Agda.Interaction.JSON
fromJSONKeyList | Agda.Interaction.JSON
FromJSONKeyText | Agda.Interaction.JSON
FromJSONKeyTextParser | Agda.Interaction.JSON
FromJSONKeyValue | Agda.Interaction.JSON
fromJust |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
fromLeft | Agda.Utils.Either
fromLeftM | Agda.Utils.Either
fromList |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.Utils.VarSet
3 (Function) | Agda.Utils.Map1
4 (Function) | Agda.Utils.Set1
5 (Function) | Agda.Utils.Bag
6 (Function) | Agda.Utils.BoolSet
7 (Function) | Agda.Utils.SmallSet
8 (Function) | Agda.Utils.Singleton, Agda.Termination.CallGraph
9 (Function) | Agda.Utils.Favorites
10 (Function) | Agda.Utils.BiMap
fromList1 | Agda.Utils.List2
fromList1Either | Agda.Utils.List2
fromList1Maybe | Agda.Utils.List2
fromListMaybe | Agda.Utils.List2
fromListN | Agda.Utils.List1
fromListPrecondition | Agda.Utils.BiMap
fromLists | Agda.Termination.SparseMatrix
fromListSafe | Agda.Utils.List1
fromListWith | Agda.Utils.Map1
fromListWithKey | Agda.Utils.Map1
fromLiteral | Agda.TypeChecking.Primitive
fromLType | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
fromMaybe |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
fromMaybeM |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
fromMaybeMP | Agda.Utils.Monad
fromMilliseconds | Agda.Utils.Time
fromNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
fromNodeSet | Agda.Utils.Graph.AdjacencyMap.Unidirectional
fromNonOverlappingNonEmptyAscendingList | Agda.Utils.RangeMap
fromOrdering | Agda.Utils.PartialOrd
fromOrderings | Agda.Utils.PartialOrd
fromOrdinary | Agda.Syntax.Concrete
fromPatternSubstitution | Agda.TypeChecking.Substitute
fromReduceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fromReducedTerm | Agda.TypeChecking.Primitive
fromRight | Agda.Utils.Either
fromRightM | Agda.Utils.Either
fromSet | Agda.Utils.Map1
fromSplitPattern | Agda.TypeChecking.Coverage.Match
fromSplitPatterns | Agda.TypeChecking.Coverage.Match
fromSubscriptDigit | Agda.Utils.Suffix
FromTerm | Agda.TypeChecking.Primitive
fromTerm | Agda.TypeChecking.Primitive
FromTermFunction | Agda.TypeChecking.Primitive
FrontEndBuildLibrary | Agda.Main
FrontEndEmacs | Agda.Main
FrontEndInteraction | Agda.Main
FrontEndJson | Agda.Main
FrontEndRepl | Agda.Main
FrontendType | Agda.Main
Frozen |
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
fsep |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.TypeChecking.Pretty
fst3 | Agda.Utils.Tuple
Full | Agda.Interaction.Highlighting.Generate
full | Agda.Utils.IntSet.Infinite
fullBoundary | Agda.TypeChecking.Telescope
fullRender | Agda.Syntax.Common.Pretty
fullRenderAnn | Agda.Syntax.Common.Pretty
fullyApplyCon | Agda.TypeChecking.Datatypes
fullyApplyCon' | Agda.TypeChecking.Datatypes
Fun |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
3 (Type/Class) | Agda.TypeChecking.Primitive
funAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunAbstract | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funAbstract | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funAbstract_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funAbstr_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunArity | Agda.Syntax.Internal.Pattern
funArity | Agda.Syntax.Internal.Pattern
FunBind | Agda.Utils.Haskell.Syntax
FunClause | Agda.Syntax.Concrete
funClauseOrTypeSigs | Agda.Syntax.Parser.Helpers
funClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funCovering | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Function |
1 (Type/Class) | Agda.Utils.TypeLevel
2 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
3 (Data Constructor) | Agda.Interaction.Response.Base, Agda.Interaction.Response
4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunctionCtx | Agda.Syntax.Fixity
FunctionData |
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
FunctionDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunctionFlag | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunctionInverse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
functionInverse | Agda.TypeChecking.Injectivity
FunctionInverse' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunctionKind | Agda.Compiler.MAlonzo.Misc
FunctionReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunctionSpaceDomainCtx | Agda.Syntax.Fixity
FunctionTypeInSizeUniv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunctionTypeInSizeUniv_ | Agda.Interaction.Options.Errors
FunDef |
1 (Data Constructor) | Agda.Syntax.Reflected
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
3 (Data Constructor) | Agda.Syntax.Abstract
FunDefS | Agda.Syntax.Abstract
FunErasure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funErasure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funExtLam | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunFirstOrder | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funFirstOrder | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funFlag | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funFlags | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funFlag_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunInline | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funInline | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funInv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funIsKanOp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunK | Agda.Compiler.MAlonzo.Misc
FunMacro | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funMacro | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funMacro_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunName |
1 (Data Constructor) | Agda.Syntax.Scope.Base
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types
FunName_ | Agda.Interaction.Options.Errors
funOpaque | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunProj | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funProj | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funProj_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunSig | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
FunSort | Agda.Syntax.Internal
funSort | Agda.TypeChecking.Substitute
funSort' | Agda.TypeChecking.Substitute
funSplitTree | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunStatic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funStatic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funTerminates | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funTreeless | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funUniv | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
funWith | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fuseIntervals | Agda.Syntax.Position
fuseRange | Agda.Syntax.Position
fuseRanges | Agda.Syntax.Position
FVs | Agda.TypeChecking.MetaVars
fwords |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.TypeChecking.Pretty