Agda-2.3.2.1: A dependently typed functional programming language and proof assistant

Index - F

FailAgda.TypeChecking.CompiledClause
FailedAgda.Auto.NarrowingSearch
failOnExceptionAgda.Interaction.Exceptions
FailureAgda.Utils.QuickCheck
fakeDAgda.Compiler.MAlonzo.Misc
fakeDQAgda.Compiler.MAlonzo.Misc
fakeDSAgda.Compiler.MAlonzo.Misc
fakeExpAgda.Compiler.MAlonzo.Misc
fakeTypeAgda.Compiler.MAlonzo.Misc
fastDistinctAgda.Utils.List
fcatAgda.Utils.Pretty
fCtxAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
fieldAgda.Compiler.JS.Parser
FieldNameAgda.Syntax.Scope.Monad
FieldOutsideRecordAgda.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
FileAgda.Interaction.Highlighting.Precise
FileNotFoundAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
filePathAgda.Utils.FileName
filterAgda.Utils.HashMap
filterEdgesAgda.Utils.Graph
filterKeysAgda.Utils.Map
filterScopeAgda.Syntax.Scope.Base
filterWithKeyAgda.Utils.HashMap
finallyAgda.Utils.Monad
findClauseAgda.Interaction.MakeCase
findClauseDeepAgda.Auto.Convert
FindErrorAgda.Interaction.FindFile
findErrorToTypeErrorAgda.Interaction.FindFile
findFileAgda.Interaction.FindFile
findFile'Agda.Interaction.FindFile
findFile''Agda.Interaction.FindFile
findIdxAgda.TypeChecking.MetaVars
findInjectionAgda.Compiler.Epic.Injection
FindInScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
findInScopeAgda.TypeChecking.InstanceArguments
findInScope'Agda.TypeChecking.InstanceArguments
FindInScopeOFAgda.Interaction.BasicOps
findInterfaceFileAgda.Interaction.FindFile
findMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
findPathAgda.Utils.Graph
findpermAgda.Auto.CaseSplit
findPositionAgda.Compiler.Epic.Forcing
findPossibleRecordsAgda.TypeChecking.Records
FiniteAgda.Utils.Warshall
fIntAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fInteractionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
firstPartAgda.TypeChecking.Telescope
fitsInAgda.TypeChecking.Rules.Data
fixAgda.Compiler.JS.Substitution
Fixed 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
FixityAgda.Syntax.Fixity
Fixity' 
1 (Type/Class)Agda.Syntax.Fixity
2 (Data Constructor)Agda.Syntax.Fixity
fixityLevelAgda.Syntax.Fixity
fixSizeAgda.TypeChecking.Test.Generators
fixSizeConfAgda.TypeChecking.Test.Generators
FlagAgda.Interaction.Options
flattenScopeAgda.Syntax.Scope.Base
flattenSubstitutionAgda.TypeChecking.Rules.LHS.Unify
flattenTelAgda.TypeChecking.Telescope
FldNameAgda.Syntax.Scope.Base
Flex 
1 (Data Constructor)Agda.Utils.Warshall
2 (Data Constructor)Agda.TypeChecking.MetaVars.Occurs
FlexibleAgda.TypeChecking.Free
flexiblePatternsAgda.TypeChecking.Rules.LHS
flexibleVariablesAgda.TypeChecking.SizedTypes
FlexibleVarsAgda.TypeChecking.Rules.LHS.Problem
flexibleVarsAgda.TypeChecking.Free
FlexIdAgda.Utils.Warshall
flexScopeAgda.Utils.Warshall
floatAgda.Utils.Pretty
fmapTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fMetaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fmExpAgda.Auto.Convert
fmExpsAgda.Auto.Convert
fmLevelAgda.Auto.Convert
FModeAgda.Auto.Syntax
fmTypeAgda.Auto.Convert
fMutualAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Focus 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
focusConAgda.TypeChecking.Rules.LHS.Problem
focusConArgsAgda.TypeChecking.Rules.LHS.Problem
focusDatatypeAgda.TypeChecking.Rules.LHS.Problem
focusHoleIxAgda.TypeChecking.Rules.LHS.Problem
focusIndicesAgda.TypeChecking.Rules.LHS.Problem
focusOutPatAgda.TypeChecking.Rules.LHS.Problem
focusParamsAgda.TypeChecking.Rules.LHS.Problem
focusRangeAgda.TypeChecking.Rules.LHS.Problem
focusTypeAgda.TypeChecking.Rules.LHS.Problem
foldl'Agda.Utils.HashMap
foldlWithKey'Agda.Utils.HashMap
foldrAgda.Utils.HashMap
foldrWithKeyAgda.Utils.HashMap
foldTermAgda.Syntax.Internal.Generic
followedByAgda.Syntax.Parser.LexActions
forAllAgda.Utils.QuickCheck
forAllShrinkAgda.Utils.QuickCheck
forceAgda.TypeChecking.Forcing
forceConstrsAgda.Compiler.Epic.ForceConstrs
Forced 
1 (Data Constructor)Agda.Syntax.Common
2 (Type/Class)Agda.Compiler.Epic.Interface
3 (Data Constructor)Agda.Compiler.Epic.Interface
forcedAgda.Compiler.Epic.Interface
ForcedArgsAgda.Compiler.Epic.Interface
forcedArgsAgda.Compiler.Epic.Interface
forcedExprAgda.Compiler.Epic.Forcing
forcedVariablesAgda.TypeChecking.Forcing
forceEqualTermsAgda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
forceFunAgda.Compiler.Epic.ForceConstrs
forceHomAgda.TypeChecking.Rules.LHS.Unify
forkTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
forM'Agda.Utils.Monad
fProblemAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FreeAgda.TypeChecking.Free
freeIn 
1 (Function)Agda.TypeChecking.Free
2 (Function)Agda.Auto.Convert
freeInIgnoringSortAnnAgda.TypeChecking.Free
freeInIgnoringSortsAgda.TypeChecking.Free
FreeVarsAgda.TypeChecking.Free
freeVarsAgda.TypeChecking.Free
freevarsAgda.Auto.CaseSplit
freeVarsToApplyAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
freezeMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
FreqsAgda.TypeChecking.Test.Generators
FrequenciesAgda.TypeChecking.Test.Generators
frequencyAgda.Utils.QuickCheck
FreshAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
freshAgda.Utils.Fresh
freshAbstractNameAgda.Syntax.Scope.Monad
freshAbstractName_Agda.Syntax.Scope.Monad
freshAbstractQNameAgda.Syntax.Scope.Monad
freshNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
freshName_Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
freshNoNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
freshNoName_Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
FreshThingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fromAgda.Interaction.Highlighting.Range
fromAgdaAgda.Compiler.Epic.FromAgda
fromDiagonalsAgda.Termination.Lexicographic
fromHomAgda.TypeChecking.Rules.LHS.Unify
fromIndexList 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Termination.SparseMatrix
fromJustAgda.Utils.Maybe
fromList 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.HashMap
3 (Function)Agda.Termination.CallGraph
4 (Function)Agda.Utils.Graph
fromLists 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Termination.SparseMatrix
fromListWithAgda.Utils.HashMap
fromLiteralAgda.TypeChecking.Primitive
fromMaybeAgda.Utils.Maybe
fromMaybeMAgda.Utils.Maybe
frommyAgda.Auto.Convert
frommyClauseAgda.Auto.Convert
frommyExpAgda.Auto.Convert
frommyExpsAgda.Auto.Convert
frommyTypeAgda.Auto.Convert
fromNodesAgda.Utils.Graph
fromOrdinaryAgda.Syntax.Concrete
fromReducedTermAgda.TypeChecking.Primitive
fromSubscriptDigitAgda.Utils.Suffix
FromTermAgda.TypeChecking.Primitive
fromTermAgda.TypeChecking.Primitive
FromTermFunctionAgda.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
fst3Agda.Utils.Tuple
FullAgda.Interaction.Highlighting.Generate
fullParenAgda.Syntax.Concrete.Operators
fullRenderAgda.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
funAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funArgsAgda.Compiler.Epic.AuxAST
FunClauseAgda.Syntax.Concrete
funClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funCommentAgda.Compiler.Epic.AuxAST
funCompiledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funCopyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Function 
1 (Data Constructor)Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
functionAgda.Compiler.JS.Parser
FunctionCtxAgda.Syntax.Fixity
FunctionDefAgda.Interaction.MakeCase
FunctionInverseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
functionInverseAgda.TypeChecking.Injectivity
FunctionInverse'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FunctionSpaceDomainCtxAgda.Syntax.Fixity
FunDef 
1 (Data Constructor)Agda.Syntax.Abstract
2 (Data Constructor)Agda.Syntax.Concrete.Definitions
funDelayedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funEpicCodeAgda.Compiler.Epic.AuxAST
funExprAgda.Compiler.Epic.AuxAST
funFreqAgda.TypeChecking.Test.Generators
funInlineAgda.Compiler.Epic.AuxAST
funInvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funMutualAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funNameAgda.Compiler.Epic.AuxAST
funProjectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funQNameAgda.Compiler.Epic.AuxAST
funsAgda.Compiler.Epic.Erasure
FunShAgda.TypeChecking.Rules.LHS.Unify
FunSigAgda.Syntax.Concrete.Definitions
funStaticAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funTerminatesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fuseRangeAgda.Syntax.Position
fuseRangesAgda.Syntax.Position
FVAgda.TypeChecking.Free
fvAgda.Compiler.Epic.AuxAST
FVsAgda.TypeChecking.MetaVars
fwords 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty