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
feBinders	Agda.TypeChecking.Free.Lazy
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
Fields
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
File
1 (Type/Class)	Agda.Interaction.Highlighting.Precise
2 (Data Constructor)	Agda.Interaction.Highlighting.Precise
FileNotFound	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
filePath	Agda.Utils.FileName
filter	Agda.Utils.HashMap
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
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
findInjection	Agda.Compiler.Epic.Injection
FindInScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
findInScope	Agda.TypeChecking.InstanceArguments
findInScope'	Agda.TypeChecking.InstanceArguments
FindInScopeOF	Agda.Interaction.BasicOps
findInteractionPoint_	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
findInterfaceFile	Agda.Interaction.FindFile
findMentions	Agda.Interaction.SearchAbout
findperm	Agda.Auto.CaseSplit
findPosition	Agda.Compiler.Epic.Forcing
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
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.Old
3 (Data Constructor)	Agda.TypeChecking.Free
flexiblePatterns	Agda.TypeChecking.Rules.LHS
FlexibleVar
1 (Type/Class)	Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)	Agda.TypeChecking.Rules.LHS.Problem
flexibleVarFromHiding	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.Old
2 (Function)	Agda.TypeChecking.Free
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
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
flipP	Agda.Utils.Permutation
float	Agda.Utils.Pretty
floatEq	Agda.TypeChecking.Primitive
floatLt	Agda.TypeChecking.Primitive
fmapReduce	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fmapTCMT	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fmExp	Agda.Auto.Convert
fmExps	Agda.Auto.Convert
fmLevel	Agda.Auto.Convert
FMode	Agda.Auto.Syntax
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
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
foldr	Agda.Utils.HashMap
FoldRigid	Agda.TypeChecking.MetaVars.Occurs
foldRigid	Agda.TypeChecking.MetaVars.Occurs
foldrWithKey	Agda.Utils.HashMap
foldTerm	Agda.Syntax.Internal.Generic
followedBy	Agda.Syntax.Parser.LexActions
for	Agda.Utils.Functor
force	Agda.TypeChecking.Forcing
forceConstrs	Agda.Compiler.Epic.ForceConstrs
Forced
1 (Data Constructor)	Agda.Syntax.Common
2 (Type/Class)	Agda.Compiler.Epic.Interface
3 (Data Constructor)	Agda.Compiler.Epic.Interface
forced	Agda.Compiler.Epic.Interface
ForcedArgs	Agda.Compiler.Epic.Interface
forcedArgs	Agda.Compiler.Epic.Interface
forcedExpr	Agda.Compiler.Epic.Forcing
ForcedVariables	Agda.TypeChecking.Forcing
forcedVariables	Agda.TypeChecking.Forcing
forceEqualTerms	Agda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
forceEtaExpandRecord	Agda.TypeChecking.Records
forceFun	Agda.Compiler.Epic.ForceConstrs
forceSort	Agda.TypeChecking.Rules.Data
forkTCM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
forM'	Agda.Utils.Monad
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.Old
3 (Type/Class)	Agda.TypeChecking.Free
Free'	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
FreeEnv
1 (Type/Class)	Agda.TypeChecking.Free.Lazy
2 (Data Constructor)	Agda.TypeChecking.Free.Lazy
freeIn
1 (Function)	Agda.TypeChecking.Free.Old
2 (Function)	Agda.TypeChecking.Free
3 (Function)	Agda.Compiler.Treeless.Subst
4 (Function)	Agda.Auto.Convert
freeInIgnoringSortAnn	Agda.TypeChecking.Free.Old
freeInIgnoringSorts
1 (Function)	Agda.TypeChecking.Free.Old
2 (Function)	Agda.TypeChecking.Free
FreeM	Agda.TypeChecking.Free.Lazy
FreeV	Agda.TypeChecking.Free
FreeVars
1 (Type/Class)	Agda.TypeChecking.Free.Old
2 (Type/Class)	Agda.TypeChecking.Free
freeVars
1 (Function)	Agda.TypeChecking.Free.Old
2 (Function)	Agda.TypeChecking.Free
3 (Function)	Agda.Compiler.Treeless.Subst
freevars	Agda.Auto.CaseSplit
freeVars'	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
freeVarsIgnore	Agda.TypeChecking.Free.Old
freeVarsToApply	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
FreeVS	Agda.TypeChecking.Free
freezeMetas	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
freezeMetas'	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
fresh	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
freshLocalName	Agda.Compiler.UHC.CompileState
FreshName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
freshName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
freshNames	Agda.Compiler.MAlonzo.Compiler
freshName_	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
freshNoName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
freshNoName_	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
freshTCM	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
from	Agda.Interaction.Highlighting.Range
fromAgda	Agda.Compiler.Epic.FromAgda
fromAgdaModule	Agda.Compiler.UHC.FromAgda
fromCmp	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fromConPatternInfo	Agda.Syntax.Internal
fromIndexList	Agda.Termination.SparseMatrix
fromJust
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
fromLeft	Agda.Utils.Either
fromList
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.HashMap
3 (Function)	Agda.Utils.BiMap
4 (Function)	Agda.Utils.Bag
5 (Function)	Agda.Utils.Favorites
6 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
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
frommy	Agda.Auto.Convert
frommyClause	Agda.Auto.Convert
frommyExp	Agda.Auto.Convert
frommyExps	Agda.Auto.Convert
frommyType	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
fromSubscriptDigit	Agda.Utils.Suffix
FromTerm	Agda.TypeChecking.Primitive
fromTerm	Agda.TypeChecking.Primitive
FromTermFunction	Agda.TypeChecking.Primitive
fromTopLevelModuleName	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
Frozen
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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 (Type/Class)	Agda.Compiler.Epic.AuxAST
3 (Data Constructor)	Agda.Compiler.Epic.AuxAST
4 (Data Constructor)	Agda.Syntax.Abstract
5 (Type/Class)	Agda.TypeChecking.Primitive
funAbstr	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funArgs	Agda.Compiler.Epic.AuxAST
FunArity	Agda.Syntax.Internal.Pattern
funArity	Agda.Syntax.Internal.Pattern
FunBind	Agda.Utils.Haskell.Syntax
FunClause	Agda.Syntax.Concrete
funClauses	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funComment	Agda.Compiler.Epic.AuxAST
funCompiled	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funCopatternLHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Function
1 (Data Constructor)	Agda.Interaction.Highlighting.Precise
2 (Data Constructor)	Agda.Interaction.Response
3 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FunctionCtx	Agda.Syntax.Fixity
FunctionFlag	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FunctionInverse	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
functionInverse	Agda.TypeChecking.Injectivity
FunctionInverse'	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FunctionReductions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FunctionSpaceDomainCtx	Agda.Syntax.Fixity
FunctionTypeInSizeUniv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FunDef
1 (Data Constructor)	Agda.Syntax.Reflected
2 (Data Constructor)	Agda.Syntax.Concrete.Definitions
3 (Data Constructor)	Agda.Syntax.Abstract
funDelayed	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funEpicCode	Agda.Compiler.Epic.AuxAST
funExpr	Agda.Compiler.Epic.AuxAST
funExtLam	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funFlag	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funFlags	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FunInline	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funInline
1 (Function)	Agda.Compiler.Epic.AuxAST
2 (Function)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funInv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FunMacro	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funMacro	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funMutual	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funName	Agda.Compiler.Epic.AuxAST
funProjection	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funQName	Agda.Compiler.Epic.AuxAST
funs	Agda.Compiler.Epic.Erasure
FunSig
1 (Data Constructor)	Agda.Syntax.Concrete.Definitions
2 (Data Constructor)	Agda.Syntax.Abstract
FunStatic	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funStatic	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funTerminates	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funTreeless	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funWith	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fuseIntervals	Agda.Syntax.Position
fuseRange	Agda.Syntax.Position
fuseRanges	Agda.Syntax.Position
FV
1 (Data Constructor)	Agda.TypeChecking.Free.Old
2 (Data Constructor)	Agda.TypeChecking.Free
fv	Agda.Compiler.Epic.AuxAST
FVs	Agda.TypeChecking.MetaVars
fwords
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty