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

Index - F

FaceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FaceConstraintCannotBeHiddenAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FaceConstraintCannotBeHidden_Agda.Interaction.Options.Warnings
FaceConstraintCannotBeNamedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FaceConstraintCannotBeNamed_Agda.Interaction.Options.Warnings
faceEqnsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
faceRHSAgda.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
FailedAgda.Auto.NarrowingSearch
failOnRecordFieldWarningsAgda.TypeChecking.Records
fakeDAgda.Compiler.MAlonzo.Misc
FakeDeclAgda.Utils.Haskell.Syntax
fakeDeclAgda.Compiler.MAlonzo.Misc
fakeDQAgda.Compiler.MAlonzo.Misc
fakeDSAgda.Compiler.MAlonzo.Misc
FakeExpAgda.Utils.Haskell.Syntax
fakeExpAgda.Compiler.MAlonzo.Misc
FakeTypeAgda.Utils.Haskell.Syntax
fakeTypeAgda.Compiler.MAlonzo.Misc
fallThroughAgda.TypeChecking.CompiledClause
falseAgda.Utils.Boolean
FamilyOrNotAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
familyOrNotAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
famThingAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
farEmptyAgda.TypeChecking.Serialise.Base
farFreshAgda.TypeChecking.Serialise.Base
fastDistinctAgda.Utils.List
fastNormaliseAgda.TypeChecking.Reduce.Fast
fastReduceAgda.TypeChecking.Reduce.Fast
Favorites 
1 (Type/Class)Agda.Utils.Favorites
2 (Data Constructor)Agda.Utils.Favorites
fcatAgda.Syntax.Common.Pretty
feExtraAgda.TypeChecking.Free.Lazy
feFlexRigAgda.TypeChecking.Free.Lazy
feIgnoreSortsAgda.TypeChecking.Free.Lazy
feModalityAgda.TypeChecking.Free.Lazy
feSingletonAgda.TypeChecking.Free.Lazy
fiberAgda.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
field1Agda.Utils.Lens.Examples
field2Agda.Utils.Lens.Examples
FieldAssignment 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
FieldAssignment'Agda.Syntax.Concrete
FieldBlockAgda.Syntax.Concrete.Definitions.Types
fieldLabelModifierAgda.Interaction.JSON
FieldNameAgda.Syntax.Scope.Base
FieldOutsideRecordAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FieldSAgda.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
FieldSigAgda.Syntax.Concrete
FileNotFoundAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
filePathAgda.Utils.FileName
filePosAgda.Interaction.Library.Base, Agda.Interaction.Library
FileTypeAgda.Syntax.Common
filter 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.Trie
filterAndRestAgda.Utils.List
filterCallStackAgda.Utils.CallStack
filterEdgesAgda.Utils.Graph.AdjacencyMap.Unidirectional
filterKeysAgda.Utils.Map
filterMaybe 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
filterNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
filterNodesKeepingEdgesAgda.Utils.Graph.AdjacencyMap.Unidirectional
filterScopeAgda.Syntax.Scope.Base
filterTCWarningsAgda.TypeChecking.Pretty.Warning
filterUsedAgda.Syntax.Treeless, Agda.Compiler.Backend
filterVarMapAgda.TypeChecking.Free
filterVarMapToListAgda.TypeChecking.Free
FinalChecksAgda.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
FinalTwoArgumentsNotVisibleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
findAgda.Utils.List1
findClauseDeepAgda.Auto.Convert
FindErrorAgda.Interaction.FindFile
findErrorToTypeErrorAgda.Interaction.FindFile
findFileAgda.Interaction.FindFile
findFile'Agda.Interaction.FindFile
findFile''Agda.Interaction.FindFile
findIdxAgda.TypeChecking.MetaVars
FindInstanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
findInstanceAgda.TypeChecking.InstanceArguments
FindInstanceOFAgda.Interaction.Base
findInteractionPoint_Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
findInterfaceFileAgda.Interaction.FindFile
findInterfaceFile'Agda.Interaction.FindFile
findLib'Agda.Interaction.Library
findMentionsAgda.Interaction.SearchAbout
findNameInScopeAgda.Syntax.Scope.Base
findOverlapAgda.Utils.List
findpermAgda.Auto.CaseSplit
findPossibleRecordsAgda.TypeChecking.Records
findProjectRootAgda.Interaction.Library
findRigidBelowAgda.TypeChecking.SizedTypes.WarshallSolver
findWithIndexAgda.Utils.List
fingerprintNoinlineAgda.TypeChecking.Serialise.Base
FiniteAgda.Utils.Warshall
firstHoleAgda.Utils.Zipper
firstMetaAgda.Syntax.Internal.MetaVars
firstNonTakenNameAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
firstPartAgda.TypeChecking.Telescope
fitsInAgda.TypeChecking.Rules.Data
fittingNamedArgAgda.Syntax.Common
fixAgda.Compiler.JS.Substitution
FixitiesAgda.Syntax.Concrete.Fixity
fixitiesAndPolaritiesAgda.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
fixityAssocAgda.Syntax.Common
FixityInRenamingModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FixityInRenamingModule_Agda.Interaction.Options.Warnings
FixityLevelAgda.Syntax.Common
fixityLevelAgda.Syntax.Common
fixityRangeAgda.Syntax.Common
FlagAgda.Interaction.Options, Agda.Compiler.Backend
FlatAgda.Syntax.Common
flatNameAgda.Compiler.JS.Compiler
FlatScopeAgda.Syntax.Scope.Flat
flattenAgda.TypeChecking.Positivity
flattenScopeAgda.Syntax.Scope.Flat
flattenTelAgda.TypeChecking.Telescope
FldNameAgda.Syntax.Scope.Base
Flex 
1 (Data Constructor)Agda.Utils.Warshall
2 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
3 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
flexAgda.TypeChecking.SizedTypes.Syntax
flexArgInfoAgda.TypeChecking.Rules.LHS.Problem
FlexChoiceAgda.TypeChecking.Rules.LHS.Problem
flexForcedAgda.TypeChecking.Rules.LHS.Problem
FlexibleAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
FlexibleVar 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
flexibleVariablesAgda.TypeChecking.SizedTypes
FlexibleVarKindAgda.TypeChecking.Rules.LHS.Problem
FlexibleVarsAgda.TypeChecking.Rules.LHS.Problem
flexibleVarsAgda.TypeChecking.Free
flexiblyAgda.TypeChecking.MetaVars.Occurs
FlexId 
1 (Type/Class)Agda.Utils.Warshall
2 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
flexIdAgda.TypeChecking.SizedTypes.Syntax
flexKindAgda.TypeChecking.Rules.LHS.Problem
FlexOfAgda.TypeChecking.SizedTypes.Syntax
flexPosAgda.TypeChecking.Rules.LHS.Problem
FlexRigAgda.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
flexRigOccurrenceInAgda.TypeChecking.Free
FlexsAgda.TypeChecking.SizedTypes.Syntax
flexsAgda.TypeChecking.SizedTypes.Syntax
flexScopeAgda.Utils.Warshall
flexVarAgda.TypeChecking.Rules.LHS.Problem
flexVarsAgda.TypeChecking.Rules.LHS.Unify.Types
flipCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
flipPAgda.Utils.Permutation
floatAgda.Syntax.Common.Pretty
fmapReduceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fmapTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fmExpAgda.Auto.Convert
fmExpsAgda.Auto.Convert
fmLevelAgda.Auto.Convert
fmTypeAgda.Auto.Convert
focusAgda.Utils.Lens
foldAAgda.Utils.Applicative
foldableAgda.Interaction.JSON
foldAPatternAgda.Syntax.Abstract.Pattern
foldArgsAgda.Auto.SearchControl
foldCPatternAgda.Syntax.Concrete.Pattern
FoldDeclAgda.Syntax.Concrete.Generic
foldDeclAgda.Syntax.Concrete.Generic
foldExpr 
1 (Function)Agda.Syntax.Concrete.Generic
2 (Function)Agda.Syntax.Abstract.Views
FoldExprFnAgda.Syntax.Abstract.Views
FoldExprRecFnAgda.Syntax.Abstract.Views
foldListTAgda.Utils.ListT
foldMapAAgda.Utils.Applicative
foldMatchAgda.TypeChecking.Patterns.Match
foldPatternAgda.Syntax.Internal.Pattern
FoldrAgda.Utils.TypeLevel
foldrAgda.Utils.List1
Foldr'Agda.Utils.TypeLevel
foldrAPatternAgda.Syntax.Abstract.Pattern
foldrCPatternAgda.Syntax.Concrete.Pattern
foldrMetaSetAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
foldrPatternAgda.Syntax.Internal.Pattern
foldTermAgda.Syntax.Internal.Generic
followedByAgda.Syntax.Parser.LexActions
forAgda.Utils.Functor
forAAgda.Utils.Applicative
forallFaceMapsAgda.TypeChecking.Conversion
forallQAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
ForcedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ForcedConstructorNotInstantiatedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
forceEtaExpandRecordAgda.TypeChecking.Records
ForceNotFreeAgda.TypeChecking.Free.Reduce
forceNotFreeAgda.TypeChecking.Free.Reduce
forcePiUsingInjectivityAgda.TypeChecking.Injectivity
forceSortAgda.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
ForeignFileHeaderPragmaAgda.Compiler.MAlonzo.Pragmas
foreignHaskellAgda.Compiler.MAlonzo.Pragmas
ForeignImportAgda.Compiler.MAlonzo.Pragmas
ForeignOtherAgda.Compiler.MAlonzo.Pragmas
ForeignPragmaAgda.Syntax.Concrete
forEither3MAgda.Utils.Three
forgetAllAgda.Utils.IndexedList
forgetIndexAgda.Utils.IndexedList
forgetLoneSigsAgda.Syntax.Concrete.Definitions.Monad
forkTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
forM'Agda.Utils.Monad
formatDebugMessageAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
formatLibErrorAgda.Interaction.Library.Base
formatLibPositionInfoAgda.Interaction.Library.Base
forMaybe 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
forMaybeMAgda.Utils.Monad
forMaybeMMAgda.Utils.Monad
forMMAgda.Utils.Monad
forMM_Agda.Utils.Monad
FracAgda.Utils.Haskell.Syntax
FrameAgda.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
3 (Function)Agda.Auto.Convert
freeInIgnoringSortsAgda.TypeChecking.Free
FreeMAgda.TypeChecking.Free.Lazy
FreeTAgda.TypeChecking.Free.Lazy
FreeVariablesAgda.Syntax.Common
freeVariablesFromListAgda.Syntax.Common
FreeVarsAgda.Auto.Syntax
freeVars 
1 (Function)Agda.Auto.Syntax
2 (Function)Agda.TypeChecking.Free
3 (Function)Agda.Compiler.Treeless.Subst
freevarsAgda.Auto.CaseSplit
freeVars'Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
freeVarsIgnoreAgda.TypeChecking.Free
freeVarsOffsetAgda.Auto.Syntax
freeVarsToApplyAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freezeMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshAbstractNameAgda.Syntax.Scope.Monad
freshAbstractName_Agda.Syntax.Scope.Monad
freshAbstractQNameAgda.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
freshConcreteNameAgda.Syntax.Scope.Monad
freshIntAgda.TypeChecking.Conversion.Pure
freshInteractionIdAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshLensAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FreshNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshNameIdAgda.TypeChecking.Conversion.Pure
FreshNameModeAgda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
freshName_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshNoNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshNoName_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshProblemIdAgda.TypeChecking.Conversion.Pure
freshRecordNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshTCMAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FreshThings 
1 (Type/Class)Agda.TypeChecking.Conversion.Pure
2 (Data Constructor)Agda.TypeChecking.Conversion.Pure
fromAgda.Interaction.Highlighting.Range
fromAbsNameAgda.TypeChecking.Serialise.Instances.Abstract
FromArgsAgda.Interaction.JSON
fromAscList 
1 (Function)Agda.Utils.BoolSet
2 (Function)Agda.Utils.SmallSet
fromBlockedAgda.TypeChecking.Reduce
fromBoolAgda.Utils.Boolean
fromBool1Agda.Utils.Boolean
fromBool2Agda.Utils.Boolean
fromCallSiteListAgda.Utils.CallStack
fromCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fromConPatternInfoAgda.Syntax.Internal
fromCTypeAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
fromDistinctAscendingListsAgda.Utils.BiMap
fromDistinctAscendingListsPreconditionAgda.Utils.BiMap
fromDistinctAscList 
1 (Function)Agda.Utils.BoolSet
2 (Function)Agda.Utils.SmallSet
fromDotNetTimeAgda.Interaction.JSON
fromEdgesAgda.Utils.Graph.AdjacencyMap.Unidirectional
fromEdgesWithAgda.Utils.Graph.AdjacencyMap.Unidirectional
fromEncodingAgda.Interaction.JSON
fromImportedNameAgda.Syntax.Common
fromIndexListAgda.Termination.SparseMatrix
FromJSONAgda.Interaction.JSON
fromJSONAgda.Interaction.JSON
FromJSON1Agda.Interaction.JSON
FromJSON2Agda.Interaction.JSON
FromJSONKeyAgda.Interaction.JSON
fromJSONKeyAgda.Interaction.JSON
FromJSONKeyCoerceAgda.Interaction.JSON
FromJSONKeyFunctionAgda.Interaction.JSON
fromJSONKeyListAgda.Interaction.JSON
FromJSONKeyTextAgda.Interaction.JSON
FromJSONKeyTextParserAgda.Interaction.JSON
FromJSONKeyValueAgda.Interaction.JSON
fromJust 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
fromLeftAgda.Utils.Either
fromLeftMAgda.Utils.Either
fromList 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.VarSet
3 (Function)Agda.Utils.BoolSet
4 (Function)Agda.Utils.Bag
5 (Function)Agda.Utils.SmallSet
6 (Function)Agda.Utils.Singleton, Agda.Termination.CallGraph
7 (Function)Agda.Utils.BiMap
8 (Function)Agda.Utils.Favorites
fromList1Agda.Utils.List2
fromList1EitherAgda.Utils.List2
fromList1MaybeAgda.Utils.List2
fromListMaybeAgda.Utils.List2
fromListNAgda.Utils.List1
fromListPreconditionAgda.Utils.BiMap
fromListsAgda.Termination.SparseMatrix
fromListSafeAgda.Utils.List1
fromLiteralAgda.TypeChecking.Primitive
fromLTypeAgda.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
fromMaybeMPAgda.Utils.Monad
fromMillisecondsAgda.Utils.Time
frommyClauseAgda.Auto.Convert
frommyExpsAgda.Auto.Convert
fromNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
fromNodeSetAgda.Utils.Graph.AdjacencyMap.Unidirectional
fromNonOverlappingNonEmptyAscendingListAgda.Utils.RangeMap
fromOrderingAgda.Utils.PartialOrd
fromOrderingsAgda.Utils.PartialOrd
fromOrdinaryAgda.Syntax.Concrete
fromPatternSubstitutionAgda.TypeChecking.Substitute
fromReduceDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fromReducedTermAgda.TypeChecking.Primitive
fromRightAgda.Utils.Either
fromRightMAgda.Utils.Either
fromSplitPatternAgda.TypeChecking.Coverage.Match
fromSplitPatternsAgda.TypeChecking.Coverage.Match
fromSubscriptDigitAgda.Utils.Suffix
FromTermAgda.TypeChecking.Primitive
fromTermAgda.TypeChecking.Primitive
FromTermFunctionAgda.TypeChecking.Primitive
FrontEndEmacsAgda.Main
FrontEndJsonAgda.Main
FrontEndReplAgda.Main
FrontendTypeAgda.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
fst3Agda.Utils.Tuple
FullAgda.Interaction.Highlighting.Generate
fullAgda.Utils.IntSet.Infinite
fullBoundaryAgda.TypeChecking.Telescope
fullRenderAgda.Syntax.Common.Pretty
fullRenderAnnAgda.Syntax.Common.Pretty
fullyApplyConAgda.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
funAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunArityAgda.Syntax.Internal.Pattern
funArityAgda.Syntax.Internal.Pattern
FunBindAgda.Utils.Haskell.Syntax
FunClauseAgda.Syntax.Concrete
FunClausesAgda.Auto.Auto
funClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funCompiledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funCoveringAgda.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.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
4 (Data Constructor)Agda.Interaction.Response
FunctionCtxAgda.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
FunctionDefnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunctionFlagAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunctionInverseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
functionInverseAgda.TypeChecking.Injectivity
FunctionInverse'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunctionKindAgda.Compiler.MAlonzo.Misc
FunctionReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunctionSpaceDomainCtxAgda.Syntax.Fixity
FunctionTypeInSizeUnivAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
FunDefSAgda.Syntax.Abstract
funErasureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funExtLamAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funFlagAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funFlagsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunInlineAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funInlineAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funInvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funIsKanOpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunKAgda.Compiler.MAlonzo.Misc
FunMacroAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funMacroAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funMutualAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunName 
1 (Data Constructor)Agda.Syntax.Concrete.Definitions.Types
2 (Data Constructor)Agda.Syntax.Scope.Base
funOpaqueAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funProjectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunSigAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
FunSortAgda.Syntax.Internal
funSortAgda.TypeChecking.Substitute
funSort'Agda.TypeChecking.Substitute
funSplitTreeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunStaticAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funStaticAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funTerminatesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funTreelessAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funUnivAgda.Syntax.Internal.Univ, Agda.Syntax.Internal
funWithAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fuseIntervalsAgda.Syntax.Position
fuseRangeAgda.Syntax.Position
fuseRangesAgda.Syntax.Position
FVsAgda.TypeChecking.MetaVars
fwords 
1 (Function)Agda.Syntax.Common.Pretty
2 (Function)Agda.TypeChecking.Pretty