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

Fail	Agda.TypeChecking.CompiledClause
Failed	Agda.Auto.NarrowingSearch
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
farEmpty	Agda.TypeChecking.Serialise.Base
farFresh	Agda.TypeChecking.Serialise.Base
farReuse	Agda.TypeChecking.Serialise.Base
fastDistinct	Agda.Utils.List
fastReduce	Agda.TypeChecking.Reduce.Fast
Favorites
1 (Type/Class)	Agda.Utils.Favorites
2 (Data Constructor)	Agda.Utils.Favorites
fcat	Agda.Utils.Pretty
feFlexRig	Agda.TypeChecking.Free.Lazy
feIgnoreSorts	Agda.TypeChecking.Free.Lazy
feRelevance	Agda.TypeChecking.Free.Lazy
feSingleton	Agda.TypeChecking.Free.Lazy
Field
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Interaction.Highlighting.Precise
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
FieldName	Agda.Syntax.Scope.Monad
FieldOutsideRecord	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
File
1 (Type/Class)	Agda.Interaction.Highlighting.Precise
2 (Data Constructor)	Agda.Interaction.Highlighting.Precise
FileNotFound	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
filePath	Agda.Utils.FileName
filter
1 (Function)	Agda.Utils.HashMap
2 (Function)	Agda.Utils.Trie
filterAndRest	Agda.Utils.List
filterEdges	Agda.Utils.Graph.AdjacencyMap.Unidirectional
filterKeys	Agda.Utils.Map
filterMaybe
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
filterResetingState	Agda.TypeChecking.InstanceArguments
filterScope	Agda.Syntax.Scope.Base
filterWithKey	Agda.Utils.HashMap
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
findClauseDeep	Agda.Auto.Convert
FindError	Agda.Interaction.FindFile
findErrorToTypeError	Agda.Interaction.FindFile
findFile	Agda.Interaction.FindFile
findFile'	Agda.Interaction.FindFile
findFile''	Agda.Interaction.FindFile
findIdx	Agda.TypeChecking.MetaVars
FindInScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
findInScope	Agda.TypeChecking.InstanceArguments
findInScope'	Agda.TypeChecking.InstanceArguments
FindInScopeOF	Agda.Interaction.BasicOps
findInteractionPoint_	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
findInterfaceFile	Agda.Interaction.FindFile
findLib'	Agda.Interaction.Library
findMentions	Agda.Interaction.SearchAbout
findperm	Agda.Auto.CaseSplit
findPossibleRecords	Agda.TypeChecking.Records
findRigidBelow	Agda.TypeChecking.SizedTypes.WarshallSolver
Finite	Agda.Utils.Warshall
firstPart	Agda.TypeChecking.Telescope
fitsIn	Agda.TypeChecking.Rules.Data
fix	Agda.Compiler.JS.Substitution
Fixity
1 (Type/Class)	Agda.Syntax.Fixity
2 (Data Constructor)	Agda.Syntax.Fixity
Fixity'
1 (Type/Class)	Agda.Syntax.Fixity
2 (Data Constructor)	Agda.Syntax.Fixity
fixityAssoc	Agda.Syntax.Fixity
fixityLevel	Agda.Syntax.Fixity
fixityRange	Agda.Syntax.Fixity
fixTarget	Agda.TypeChecking.Coverage
Flag	Agda.Interaction.Options, Agda.Compiler.Backend
flatName	Agda.Compiler.JS.Compiler
flatten	Agda.TypeChecking.Positivity
flattenScope	Agda.Syntax.Scope.Base
flattenTel	Agda.TypeChecking.Telescope
FldName	Agda.Syntax.Scope.Base
Flex
1 (Data Constructor)	Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)	Agda.TypeChecking.SizedTypes.Syntax
3 (Data Constructor)	Agda.Utils.Warshall
4 (Data Constructor)	Agda.TypeChecking.MetaVars.Occurs
flex	Agda.TypeChecking.SizedTypes.Syntax
FlexChoice	Agda.TypeChecking.Rules.LHS.Problem
flexHiding	Agda.TypeChecking.Rules.LHS.Problem
Flexible
1 (Data Constructor)	Agda.TypeChecking.Free.Lazy
2 (Data Constructor)	Agda.TypeChecking.Free
3 (Data Constructor)	Agda.TypeChecking.Free.Old
flexiblePatterns	Agda.TypeChecking.Rules.LHS
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
1 (Function)	Agda.TypeChecking.Free
2 (Function)	Agda.TypeChecking.Free.Old
FlexId
1 (Data Constructor)	Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)	Agda.Utils.Warshall
flexId	Agda.TypeChecking.SizedTypes.Syntax
flexKind	Agda.TypeChecking.Rules.LHS.Problem
flexOrigin	Agda.TypeChecking.Rules.LHS.Problem
flexPos	Agda.TypeChecking.Rules.LHS.Problem
FlexRig	Agda.TypeChecking.Free.Lazy
Flexs	Agda.TypeChecking.SizedTypes.Syntax
flexs	Agda.TypeChecking.SizedTypes.Syntax
flexScope	Agda.Utils.Warshall
flexVar	Agda.TypeChecking.Rules.LHS.Problem
flipCmp	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
flipP	Agda.Utils.Permutation
float	Agda.Utils.Pretty
floatEq	Agda.TypeChecking.Primitive
floatLt	Agda.TypeChecking.Primitive
fmapReduce	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fmapTCMT	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fmExp	Agda.Auto.Convert
fmExps	Agda.Auto.Convert
fmLevel	Agda.Auto.Convert
fmType	Agda.Auto.Convert
Focus
1 (Type/Class)	Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)	Agda.TypeChecking.Rules.LHS.Problem
focusCon	Agda.TypeChecking.Rules.LHS.Problem
focusConArgs	Agda.TypeChecking.Rules.LHS.Problem
focusDatatype	Agda.TypeChecking.Rules.LHS.Problem
focusIndices	Agda.TypeChecking.Rules.LHS.Problem
focusOutPat	Agda.TypeChecking.Rules.LHS.Problem
focusParams	Agda.TypeChecking.Rules.LHS.Problem
focusPatOrigin	Agda.TypeChecking.Rules.LHS.Problem
focusRange	Agda.TypeChecking.Rules.LHS.Problem
focusType	Agda.TypeChecking.Rules.LHS.Problem
foldAPattern	Agda.Syntax.Abstract.Pattern
foldArgs	Agda.Auto.SearchControl
foldExpr
1 (Function)	Agda.Syntax.Concrete.Generic
2 (Function)	Agda.Syntax.Abstract.Views
foldl'	Agda.Utils.HashMap
foldListT	Agda.Utils.ListT
foldlWithKey'	Agda.Utils.HashMap
foldMatch	Agda.TypeChecking.Patterns.Match
foldPattern	Agda.Syntax.Internal.Pattern
Foldr	Agda.Utils.TypeLevel
foldr	Agda.Utils.HashMap
Foldr'	Agda.Utils.TypeLevel
foldrAPattern	Agda.Syntax.Abstract.Pattern
FoldRigid	Agda.TypeChecking.MetaVars.Occurs
foldRigid	Agda.TypeChecking.MetaVars.Occurs
foldrPattern	Agda.Syntax.Internal.Pattern
foldrWithKey	Agda.Utils.HashMap
foldTerm	Agda.Syntax.Internal.Generic
followedBy	Agda.Syntax.Parser.LexActions
for	Agda.Utils.Functor
force	Agda.TypeChecking.Forcing
Forced	Agda.Syntax.Common
ForcedVariables	Agda.TypeChecking.Forcing
forcedVariables	Agda.TypeChecking.Forcing
forceEqualTerms	Agda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad, Agda.Compiler.Backend
forceEtaExpandRecord	Agda.TypeChecking.Records
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
ForeignFileHeaderPragma	Agda.Compiler.MAlonzo.Pragmas
foreignHaskell	Agda.Compiler.MAlonzo.Pragmas
ForeignImport	Agda.Compiler.MAlonzo.Pragmas
ForeignOther	Agda.Compiler.MAlonzo.Pragmas
ForeignPragma	Agda.Syntax.Concrete
forgetAll	Agda.Utils.IndexedList
forgetIndex	Agda.Utils.IndexedList
forkTCM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
forM'	Agda.Utils.Monad
formatDebugMessage	Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
forMaybe
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
forMaybeM	Agda.Utils.Monad
Frac	Agda.Utils.Haskell.Syntax
Frame	Agda.TypeChecking.CompiledClause.Match
Free
1 (Data Constructor)	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
2 (Type/Class)	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
3 (Type/Class)	Agda.TypeChecking.Free.Old
FreeEnv
1 (Type/Class)	Agda.TypeChecking.Free.Lazy
2 (Data Constructor)	Agda.TypeChecking.Free.Lazy
freeIn
1 (Function)	Agda.TypeChecking.Free
2 (Function)	Agda.TypeChecking.Free.Old
3 (Function)	Agda.Compiler.Treeless.Subst
4 (Function)	Agda.Auto.Convert
freeInIgnoringSortAnn	Agda.TypeChecking.Free.Old
freeInIgnoringSorts
1 (Function)	Agda.TypeChecking.Free
2 (Function)	Agda.TypeChecking.Free.Old
FreeM	Agda.TypeChecking.Free.Lazy
FreeVars
1 (Type/Class)	Agda.Auto.Syntax
2 (Type/Class)	Agda.TypeChecking.Free
3 (Type/Class)	Agda.TypeChecking.Free.Old
freeVars
1 (Function)	Agda.Auto.Syntax
2 (Function)	Agda.TypeChecking.Free
3 (Function)	Agda.TypeChecking.Free.Old
4 (Function)	Agda.Compiler.Treeless.Subst
freevars	Agda.Auto.CaseSplit
freeVars'	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
freeVarsIgnore	Agda.TypeChecking.Free.Old
freeVarsOffset	Agda.Auto.Syntax
freeVarsToApply	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freezeMetas	Agda.TypeChecking.Monad.MetaVars, 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
FreshAndReuse
1 (Type/Class)	Agda.TypeChecking.Serialise.Base
2 (Data Constructor)	Agda.TypeChecking.Serialise.Base
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
freshNames	Agda.Compiler.MAlonzo.Compiler
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
freshTCM	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
from	Agda.Interaction.Highlighting.Range
fromCmp	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fromConPatternInfo	Agda.Syntax.Internal
fromIndexList	Agda.Termination.SparseMatrix
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.VarSet
2 (Function)	Agda.Utils.BiMap
3 (Function)	Agda.Utils.HashMap
4 (Function)	Agda.Utils.Bag
5 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
6 (Function)	Agda.Utils.Favorites
7 (Function)	Agda.Termination.CallGraph
fromLists	Agda.Termination.SparseMatrix
fromListWith
1 (Function)	Agda.Utils.HashMap
2 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
fromLiteral	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
fromMilliseconds	Agda.Utils.Time
frommyClause	Agda.Auto.Convert
frommyExps	Agda.Auto.Convert
fromNodes	Agda.Utils.Graph.AdjacencyMap.Unidirectional
fromOrdering	Agda.Utils.PartialOrd
fromOrderings	Agda.Utils.PartialOrd
fromOrdinary	Agda.Syntax.Concrete
fromPatternSubstitution	Agda.TypeChecking.Substitute
fromReducedTerm	Agda.TypeChecking.Primitive
fromRight	Agda.Utils.Either
fromRightM	Agda.Utils.Either
fromSubscriptDigit	Agda.Utils.Suffix
FromTerm	Agda.TypeChecking.Primitive
fromTerm	Agda.TypeChecking.Primitive
FromTermFunction	Agda.TypeChecking.Primitive
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.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
fst3	Agda.Utils.Tuple
Full	Agda.Interaction.Highlighting.Generate
fullRender	Agda.Utils.Pretty
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
FunArity	Agda.Syntax.Internal.Pattern
funArity	Agda.Syntax.Internal.Pattern
FunBind	Agda.Utils.Haskell.Syntax
FunClause	Agda.Syntax.Concrete
FunClauses	Agda.Auto.Auto
funClauses	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funCompiled	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funCopatternLHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Function
1 (Data Constructor)	Agda.Interaction.Highlighting.Precise
2 (Data Constructor)	Agda.Interaction.Response
3 (Type/Class)	Agda.Utils.TypeLevel
4 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunctionCtx	Agda.Syntax.Fixity
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
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
FunDef
1 (Data Constructor)	Agda.Syntax.Reflected
2 (Data Constructor)	Agda.Syntax.Abstract
3 (Data Constructor)	Agda.Syntax.Concrete.Definitions
funDelayed	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funExtLam	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
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
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
funProjection	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunSig
1 (Data Constructor)	Agda.Syntax.Abstract
2 (Data Constructor)	Agda.Syntax.Concrete.Definitions
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
funWith	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fuseIntervals	Agda.Syntax.Position
fuseRange	Agda.Syntax.Position
fuseRanges	Agda.Syntax.Position
FV
1 (Data Constructor)	Agda.TypeChecking.Free
2 (Data Constructor)	Agda.TypeChecking.Free.Old
FVs	Agda.TypeChecking.MetaVars
fwords
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty