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
failOnException	Agda.Interaction.Exceptions, Agda.Interaction.GhciTop
Failure	Agda.Utils.QuickCheck
fakeD	Agda.Compiler.MAlonzo.Misc
fakeDQ	Agda.Compiler.MAlonzo.Misc
fakeDS	Agda.Compiler.MAlonzo.Misc
fakeExp	Agda.Compiler.MAlonzo.Misc
fakeType	Agda.Compiler.MAlonzo.Misc
fastDistinct	Agda.Utils.List
fcat	Agda.Utils.Pretty
fCtx	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Field
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.Syntax.Concrete
3 (Data Constructor)	Agda.Syntax.Abstract
4 (Data Constructor)	Agda.Interaction.Highlighting.Precise
field	Agda.Compiler.JS.Parser
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	Agda.Interaction.Highlighting.Precise
FileNotFound	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
filePath	Agda.Utils.FileName
filterKeys	Agda.Utils.Map
filterScope	Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
finally	Agda.Utils.Monad
findClause	Agda.Interaction.MakeCase
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, Agda.Interaction.GhciTop
findInjection	Agda.Compiler.Epic.Injection
FindInScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FindInScopeOF	Agda.Interaction.BasicOps
findInterfaceFile	Agda.Interaction.FindFile
findMutualBlock	Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
findPath	Agda.Utils.Graph
findperm	Agda.Auto.CaseSplit
findPosition	Agda.Compiler.Epic.Forcing
findPossibleRecords	Agda.TypeChecking.Records
Finite	Agda.Utils.Warshall
fInteger	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fInteraction	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
firstPart	Agda.TypeChecking.Telescope
fitsIn	Agda.TypeChecking.Rules.Data
fix	Agda.Compiler.JS.Substitution
Fixed
1 (Data Constructor)	Agda.Utils.QuickCheck
2 (Type/Class)	Agda.Utils.QuickCheck
Fixity	Agda.Syntax.Fixity
Fixity'
1 (Type/Class)	Agda.Syntax.Fixity
2 (Data Constructor)	Agda.Syntax.Fixity
fixityLevel	Agda.Syntax.Fixity
fixSize	Agda.TypeChecking.Test.Generators
fixSizeConf	Agda.TypeChecking.Test.Generators
Flag	Agda.Interaction.Options
flattenSubstitution	Agda.TypeChecking.Rules.LHS.Unify
flattenTel	Agda.TypeChecking.Telescope
Flex
1 (Data Constructor)	Agda.Utils.Warshall
2 (Data Constructor)	Agda.TypeChecking.MetaVars.Occurs
Flexible	Agda.TypeChecking.Free
flexiblePatterns	Agda.TypeChecking.Rules.LHS
flexibleVariables	Agda.TypeChecking.SizedTypes
FlexibleVars	Agda.TypeChecking.Rules.LHS.Problem
flexibleVars	Agda.TypeChecking.Free
FlexId	Agda.Utils.Warshall
flexScope	Agda.Utils.Warshall
float	Agda.Utils.Pretty
fmapM	Agda.Utils.Monad
fMeta	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
fMutual	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
focusHoleIx	Agda.TypeChecking.Rules.LHS.Problem
focusIndices	Agda.TypeChecking.Rules.LHS.Problem
focusOutPat	Agda.TypeChecking.Rules.LHS.Problem
focusParams	Agda.TypeChecking.Rules.LHS.Problem
focusRange	Agda.TypeChecking.Rules.LHS.Problem
focusType	Agda.TypeChecking.Rules.LHS.Problem
foldTerm	Agda.Syntax.Internal.Generic
followedBy	Agda.Syntax.Parser.LexActions
forAll	Agda.Utils.QuickCheck
forAllShrink	Agda.Utils.QuickCheck
force
1 (Function)	Agda.Syntax.Strict
2 (Function)	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
forceData	Agda.TypeChecking.Rules.Data
forcedExpr	Agda.Compiler.Epic.Forcing
forcedVariables	Agda.TypeChecking.Forcing
forceFun	Agda.Compiler.Epic.ForceConstrs
forceHom	Agda.TypeChecking.Rules.LHS.Unify
forceM	Agda.Utils.Monad
forgetM	Agda.Utils.Monad
fProblem	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Free	Agda.TypeChecking.Free
freeIn
1 (Function)	Agda.TypeChecking.Free
2 (Function)	Agda.Auto.Convert
freeInIgnoringSorts	Agda.TypeChecking.Free
FreeVars	Agda.TypeChecking.Free
freeVars	Agda.TypeChecking.Free
freevars	Agda.Auto.CaseSplit
freeVarsToApply	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
freezeMetas	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
Freqs	Agda.TypeChecking.Test.Generators
Frequencies	Agda.TypeChecking.Test.Generators
frequency	Agda.Utils.QuickCheck
Fresh	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fresh	Agda.Utils.Fresh
freshAbstractName	Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
freshAbstractName_	Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
freshAbstractQName	Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
freshName	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
freshName_	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
freshNoName	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
freshNoName_	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
FreshThings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
from	Agda.Interaction.Highlighting.Range
fromAgda	Agda.Compiler.Epic.FromAgda
fromDiagonals	Agda.Termination.Lexicographic
fromHom	Agda.TypeChecking.Rules.LHS.Unify
fromIndexList
1 (Function)	Agda.Termination.SparseMatrix
2 (Function)	Agda.Termination.Matrix
fromJust	Agda.Utils.Maybe
fromList
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.Graph
3 (Function)	Agda.Termination.CallGraph
fromLists
1 (Function)	Agda.Termination.SparseMatrix
2 (Function)	Agda.Termination.Matrix
fromLiteral	Agda.TypeChecking.Primitive
fromMaybe	Agda.Utils.Maybe
fromMaybeM	Agda.Utils.Maybe
frommy	Agda.Auto.Convert
frommyClause	Agda.Auto.Convert
frommyExp	Agda.Auto.Convert
frommyExps	Agda.Auto.Convert
frommyType	Agda.Auto.Convert
fromOrdinary	Agda.Syntax.Concrete
fromReducedTerm	Agda.TypeChecking.Primitive
FromTerm	Agda.TypeChecking.Primitive
fromTerm	Agda.TypeChecking.Primitive
FromTermFunction	Agda.TypeChecking.Primitive
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
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
funArgOccurrences	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funArgs	Agda.Compiler.Epic.AuxAST
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
Function
1 (Data Constructor)	Agda.Interaction.Highlighting.Precise
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
function	Agda.Compiler.JS.Parser
FunctionCtx	Agda.Syntax.Fixity
FunctionDef	Agda.Interaction.MakeCase
FunctionInverse	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
functionInverse	Agda.TypeChecking.Injectivity
FunctionSpaceDomainCtx	Agda.Syntax.Fixity
FunDef
1 (Data Constructor)	Agda.Syntax.Abstract
2 (Data Constructor)	Agda.Syntax.Concrete.Definitions
funDelayed	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funEpicCode	Agda.Compiler.Epic.AuxAST
funExpr	Agda.Compiler.Epic.AuxAST
funFreq	Agda.TypeChecking.Test.Generators
funInline	Agda.Compiler.Epic.AuxAST
funInv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funName	Agda.Compiler.Epic.AuxAST
funPolarity	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funProjection	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funQName	Agda.Compiler.Epic.AuxAST
funs	Agda.Compiler.Epic.Erasure
FunSh	Agda.TypeChecking.Rules.LHS.Unify
FunSig	Agda.Syntax.Concrete.Definitions
funStatic	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fuseRange	Agda.Syntax.Position, Agda.Interaction.GhciTop
fuseRanges	Agda.Syntax.Position, Agda.Interaction.GhciTop
FV	Agda.TypeChecking.Free
fv	Agda.Compiler.Epic.AuxAST
FVs	Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
fwords
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty