| Face | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| FaceConstraintCannotBeHidden | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| FaceConstraintCannotBeHidden_ | Agda.Interaction.Options.Warnings | 
| FaceConstraintCannotBeNamed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| FaceConstraintCannotBeNamed_ | Agda.Interaction.Options.Warnings | 
| faceEqns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| faceRHS | Agda.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 | 
| Failed | Agda.Auto.NarrowingSearch | 
| failOnRecordFieldWarnings | Agda.TypeChecking.Records | 
| 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 | 
| fallThrough | Agda.TypeChecking.CompiledClause | 
| false | Agda.Utils.Boolean | 
| FamilyOrNot | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive | 
| familyOrNot | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive | 
| famThing | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive | 
| farEmpty | Agda.TypeChecking.Serialise.Base | 
| farFresh | Agda.TypeChecking.Serialise.Base | 
| fastDistinct | Agda.Utils.List | 
| fastNormalise | Agda.TypeChecking.Reduce.Fast | 
| fastReduce | Agda.TypeChecking.Reduce.Fast | 
| Favorites |  | 
| 1 (Type/Class) | Agda.Utils.Favorites | 
| 2 (Data Constructor) | Agda.Utils.Favorites | 
| fcat | Agda.Syntax.Common.Pretty | 
| feExtra | Agda.TypeChecking.Free.Lazy | 
| feFlexRig | Agda.TypeChecking.Free.Lazy | 
| feIgnoreSorts | Agda.TypeChecking.Free.Lazy | 
| feModality | Agda.TypeChecking.Free.Lazy | 
| feSingleton | Agda.TypeChecking.Free.Lazy | 
| fiber | Agda.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 | 
| 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 | 
| FieldBlock | Agda.Syntax.Concrete.Definitions.Types | 
| fieldLabelModifier | Agda.Interaction.JSON | 
| FieldName | Agda.Syntax.Scope.Base | 
| FieldOutsideRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| FieldS | Agda.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 | 
| FieldSig | Agda.Syntax.Concrete | 
| FileNotFound | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| filePath | Agda.Utils.FileName | 
| filePos | Agda.Interaction.Library.Base, Agda.Interaction.Library | 
| FileType | Agda.Syntax.Common | 
| filter |  | 
| 1 (Function) | Agda.Utils.List1 | 
| 2 (Function) | Agda.Utils.Trie | 
| filterAndRest | Agda.Utils.List | 
| filterCallStack | Agda.Utils.CallStack | 
| filterEdges | Agda.Utils.Graph.AdjacencyMap.Unidirectional | 
| filterKeys | Agda.Utils.Map | 
| filterMaybe |  | 
| 1 (Function) | Agda.Utils.Maybe | 
| 2 (Function) | Agda.Utils.Maybe.Strict | 
| filterNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional | 
| filterNodesKeepingEdges | Agda.Utils.Graph.AdjacencyMap.Unidirectional | 
| filterScope | Agda.Syntax.Scope.Base | 
| filterTCWarnings | Agda.TypeChecking.Pretty.Warning | 
| filterUsed | Agda.Syntax.Treeless, Agda.Compiler.Backend | 
| filterVarMap | Agda.TypeChecking.Free | 
| filterVarMapToList | Agda.TypeChecking.Free | 
| 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 | 
| FinalTwoArgumentsNotVisible | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| find | Agda.Utils.List1 | 
| 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 | 
| FindInstance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| findInstance | Agda.TypeChecking.InstanceArguments | 
| FindInstanceOF | Agda.Interaction.Base | 
| findInteractionPoint_ | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| findInterfaceFile | Agda.Interaction.FindFile | 
| findInterfaceFile' | Agda.Interaction.FindFile | 
| findLib' | Agda.Interaction.Library | 
| findMentions | Agda.Interaction.SearchAbout | 
| findNameInScope | Agda.Syntax.Scope.Base | 
| findOverlap | Agda.Utils.List | 
| findperm | Agda.Auto.CaseSplit | 
| findPossibleRecords | Agda.TypeChecking.Records | 
| findProjectRoot | Agda.Interaction.Library | 
| findRigidBelow | Agda.TypeChecking.SizedTypes.WarshallSolver | 
| findWithIndex | Agda.Utils.List | 
| fingerprintNoinline | Agda.TypeChecking.Serialise.Base | 
| Finite | Agda.Utils.Warshall | 
| firstHole | Agda.Utils.Zipper | 
| firstMeta | Agda.Syntax.Internal.MetaVars | 
| firstNonTakenName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete | 
| firstPart | Agda.TypeChecking.Telescope | 
| fitsIn | Agda.TypeChecking.Rules.Data | 
| fittingNamedArg | Agda.Syntax.Common | 
| fix | Agda.Compiler.JS.Substitution | 
| Fixities | Agda.Syntax.Concrete.Fixity | 
| fixitiesAndPolarities | Agda.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 | 
| fixityAssoc | Agda.Syntax.Common | 
| FixityInRenamingModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| FixityInRenamingModule_ | Agda.Interaction.Options.Warnings | 
| FixityLevel | Agda.Syntax.Common | 
| fixityLevel | Agda.Syntax.Common | 
| fixityRange | Agda.Syntax.Common | 
| Flag | Agda.Interaction.Options, Agda.Compiler.Backend | 
| Flat | Agda.Syntax.Common | 
| flatName | Agda.Compiler.JS.Compiler | 
| FlatScope | Agda.Syntax.Scope.Flat | 
| flatten | Agda.TypeChecking.Positivity | 
| flattenScope | Agda.Syntax.Scope.Flat | 
| flattenTel | Agda.TypeChecking.Telescope | 
| FldName | Agda.Syntax.Scope.Base | 
| Flex |  | 
| 1 (Data Constructor) | Agda.Utils.Warshall | 
| 2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax | 
| 3 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax | 
| flex | Agda.TypeChecking.SizedTypes.Syntax | 
| flexArgInfo | Agda.TypeChecking.Rules.LHS.Problem | 
| FlexChoice | Agda.TypeChecking.Rules.LHS.Problem | 
| flexForced | Agda.TypeChecking.Rules.LHS.Problem | 
| Flexible | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free | 
| 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 | Agda.TypeChecking.Free | 
| flexibly | Agda.TypeChecking.MetaVars.Occurs | 
| FlexId |  | 
| 1 (Type/Class) | Agda.Utils.Warshall | 
| 2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax | 
| flexId | Agda.TypeChecking.SizedTypes.Syntax | 
| flexKind | Agda.TypeChecking.Rules.LHS.Problem | 
| FlexOf | Agda.TypeChecking.SizedTypes.Syntax | 
| flexPos | Agda.TypeChecking.Rules.LHS.Problem | 
| FlexRig | Agda.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 | 
| flexRigOccurrenceIn | Agda.TypeChecking.Free | 
| Flexs | Agda.TypeChecking.SizedTypes.Syntax | 
| flexs | Agda.TypeChecking.SizedTypes.Syntax | 
| flexScope | Agda.Utils.Warshall | 
| flexVar | Agda.TypeChecking.Rules.LHS.Problem | 
| flexVars | Agda.TypeChecking.Rules.LHS.Unify.Types | 
| flipCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| flipP | Agda.Utils.Permutation | 
| float | Agda.Syntax.Common.Pretty | 
| 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 | Agda.Utils.Lens | 
| foldA | Agda.Utils.Applicative | 
| foldable | Agda.Interaction.JSON | 
| foldAPattern | Agda.Syntax.Abstract.Pattern | 
| foldArgs | Agda.Auto.SearchControl | 
| foldCPattern | Agda.Syntax.Concrete.Pattern | 
| FoldDecl | Agda.Syntax.Concrete.Generic | 
| foldDecl | Agda.Syntax.Concrete.Generic | 
| foldExpr |  | 
| 1 (Function) | Agda.Syntax.Concrete.Generic | 
| 2 (Function) | Agda.Syntax.Abstract.Views | 
| FoldExprFn | Agda.Syntax.Abstract.Views | 
| FoldExprRecFn | Agda.Syntax.Abstract.Views | 
| foldListT | Agda.Utils.ListT | 
| foldMapA | Agda.Utils.Applicative | 
| foldMatch | Agda.TypeChecking.Patterns.Match | 
| foldPattern | Agda.Syntax.Internal.Pattern | 
| Foldr | Agda.Utils.TypeLevel | 
| foldr | Agda.Utils.List1 | 
| Foldr' | Agda.Utils.TypeLevel | 
| foldrAPattern | Agda.Syntax.Abstract.Pattern | 
| foldrCPattern | Agda.Syntax.Concrete.Pattern | 
| foldrMetaSet | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free | 
| foldrPattern | Agda.Syntax.Internal.Pattern | 
| foldTerm | Agda.Syntax.Internal.Generic | 
| followedBy | Agda.Syntax.Parser.LexActions | 
| for | Agda.Utils.Functor | 
| forA | Agda.Utils.Applicative | 
| forallFaceMaps | Agda.TypeChecking.Conversion | 
| forallQ | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty | 
| Forced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| ForcedConstructorNotInstantiated | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| forceEtaExpandRecord | Agda.TypeChecking.Records | 
| ForceNotFree | Agda.TypeChecking.Free.Reduce | 
| forceNotFree | Agda.TypeChecking.Free.Reduce | 
| forcePiUsingInjectivity | Agda.TypeChecking.Injectivity | 
| 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 | 
| 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 | 
| ForeignFileHeaderPragma | Agda.Compiler.MAlonzo.Pragmas | 
| foreignHaskell | Agda.Compiler.MAlonzo.Pragmas | 
| ForeignImport | Agda.Compiler.MAlonzo.Pragmas | 
| ForeignOther | Agda.Compiler.MAlonzo.Pragmas | 
| ForeignPragma | Agda.Syntax.Concrete | 
| forEither3M | Agda.Utils.Three | 
| forgetAll | Agda.Utils.IndexedList | 
| forgetIndex | Agda.Utils.IndexedList | 
| forgetLoneSigs | Agda.Syntax.Concrete.Definitions.Monad | 
| 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 | 
| formatLibError | Agda.Interaction.Library.Base | 
| formatLibPositionInfo | Agda.Interaction.Library.Base | 
| forMaybe |  | 
| 1 (Function) | Agda.Utils.Maybe | 
| 2 (Function) | Agda.Utils.Maybe.Strict | 
| forMaybeM | Agda.Utils.Monad | 
| forMaybeMM | Agda.Utils.Monad | 
| forMM | Agda.Utils.Monad | 
| forMM_ | Agda.Utils.Monad | 
| Frac | Agda.Utils.Haskell.Syntax | 
| Frame | Agda.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 | 
| freeInIgnoringSorts | Agda.TypeChecking.Free | 
| FreeM | Agda.TypeChecking.Free.Lazy | 
| FreeT | Agda.TypeChecking.Free.Lazy | 
| FreeVariables | Agda.Syntax.Common | 
| freeVariablesFromList | Agda.Syntax.Common | 
| FreeVars | Agda.Auto.Syntax | 
| freeVars |  | 
| 1 (Function) | Agda.Auto.Syntax | 
| 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 | 
| 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 | 
| 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 | 
| 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 | 
| freshConcreteName | Agda.Syntax.Scope.Monad | 
| freshInt | Agda.TypeChecking.Conversion.Pure | 
| freshInteractionId | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| 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 | 
| freshNameId | Agda.TypeChecking.Conversion.Pure | 
| FreshNameMode | Agda.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 | 
| freshNoName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| freshNoName_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| freshProblemId | Agda.TypeChecking.Conversion.Pure | 
| freshRecordName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| freshTCM | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| FreshThings |  | 
| 1 (Type/Class) | Agda.TypeChecking.Conversion.Pure | 
| 2 (Data Constructor) | Agda.TypeChecking.Conversion.Pure | 
| from | Agda.Interaction.Highlighting.Range | 
| fromAbsName | Agda.TypeChecking.Serialise.Instances.Abstract | 
| FromArgs | Agda.Interaction.JSON | 
| fromAscList |  | 
| 1 (Function) | Agda.Utils.BoolSet | 
| 2 (Function) | Agda.Utils.SmallSet | 
| fromBlocked | Agda.TypeChecking.Reduce | 
| fromBool | Agda.Utils.Boolean | 
| fromBool1 | Agda.Utils.Boolean | 
| fromBool2 | Agda.Utils.Boolean | 
| fromCallSiteList | Agda.Utils.CallStack | 
| fromCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| fromConPatternInfo | Agda.Syntax.Internal | 
| fromCType | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive | 
| fromDistinctAscendingLists | Agda.Utils.BiMap | 
| fromDistinctAscendingListsPrecondition | Agda.Utils.BiMap | 
| fromDistinctAscList |  | 
| 1 (Function) | Agda.Utils.BoolSet | 
| 2 (Function) | Agda.Utils.SmallSet | 
| fromDotNetTime | Agda.Interaction.JSON | 
| fromEdges | Agda.Utils.Graph.AdjacencyMap.Unidirectional | 
| fromEdgesWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional | 
| fromEncoding | Agda.Interaction.JSON | 
| fromImportedName | Agda.Syntax.Common | 
| fromIndexList | Agda.Termination.SparseMatrix | 
| FromJSON | Agda.Interaction.JSON | 
| fromJSON | Agda.Interaction.JSON | 
| FromJSON1 | Agda.Interaction.JSON | 
| FromJSON2 | Agda.Interaction.JSON | 
| FromJSONKey | Agda.Interaction.JSON | 
| fromJSONKey | Agda.Interaction.JSON | 
| FromJSONKeyCoerce | Agda.Interaction.JSON | 
| FromJSONKeyFunction | Agda.Interaction.JSON | 
| fromJSONKeyList | Agda.Interaction.JSON | 
| FromJSONKeyText | Agda.Interaction.JSON | 
| FromJSONKeyTextParser | Agda.Interaction.JSON | 
| FromJSONKeyValue | Agda.Interaction.JSON | 
| 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.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 | 
| fromList1 | Agda.Utils.List2 | 
| fromList1Either | Agda.Utils.List2 | 
| fromList1Maybe | Agda.Utils.List2 | 
| fromListMaybe | Agda.Utils.List2 | 
| fromListN | Agda.Utils.List1 | 
| fromListPrecondition | Agda.Utils.BiMap | 
| fromLists | Agda.Termination.SparseMatrix | 
| fromListSafe | Agda.Utils.List1 | 
| fromLiteral | Agda.TypeChecking.Primitive | 
| fromLType | Agda.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 | 
| fromMaybeMP | Agda.Utils.Monad | 
| fromMilliseconds | Agda.Utils.Time | 
| frommyClause | Agda.Auto.Convert | 
| frommyExps | Agda.Auto.Convert | 
| fromNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional | 
| fromNodeSet | Agda.Utils.Graph.AdjacencyMap.Unidirectional | 
| fromNonOverlappingNonEmptyAscendingList | Agda.Utils.RangeMap | 
| fromOrdering | Agda.Utils.PartialOrd | 
| fromOrderings | Agda.Utils.PartialOrd | 
| fromOrdinary | Agda.Syntax.Concrete | 
| fromPatternSubstitution | Agda.TypeChecking.Substitute | 
| fromReduceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| fromReducedTerm | Agda.TypeChecking.Primitive | 
| fromRight | Agda.Utils.Either | 
| fromRightM | Agda.Utils.Either | 
| fromSplitPattern | Agda.TypeChecking.Coverage.Match | 
| fromSplitPatterns | Agda.TypeChecking.Coverage.Match | 
| fromSubscriptDigit | Agda.Utils.Suffix | 
| FromTerm | Agda.TypeChecking.Primitive | 
| fromTerm | Agda.TypeChecking.Primitive | 
| FromTermFunction | Agda.TypeChecking.Primitive | 
| FrontEndEmacs | Agda.Main | 
| FrontEndJson | Agda.Main | 
| FrontEndRepl | Agda.Main | 
| FrontendType | Agda.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 | 
| fst3 | Agda.Utils.Tuple | 
| Full | Agda.Interaction.Highlighting.Generate | 
| full | Agda.Utils.IntSet.Infinite | 
| fullBoundary | Agda.TypeChecking.Telescope | 
| fullRender | Agda.Syntax.Common.Pretty | 
| fullRenderAnn | Agda.Syntax.Common.Pretty | 
| fullyApplyCon | Agda.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 | 
| 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 | 
| funCovering | Agda.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 | 
| FunctionCtx | Agda.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 | 
| FunctionDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| 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 | 
| FunctionKind | Agda.Compiler.MAlonzo.Misc | 
| 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.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions | 
| 3 (Data Constructor) | Agda.Syntax.Abstract | 
| FunDefS | Agda.Syntax.Abstract | 
| funErasure | 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 | 
| funIsKanOp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| FunK | Agda.Compiler.MAlonzo.Misc | 
| 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 | 
| FunName |  | 
| 1 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types | 
| 2 (Data Constructor) | Agda.Syntax.Scope.Base | 
| funOpaque | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| funProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| FunSig | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions | 
| FunSort | Agda.Syntax.Internal | 
| funSort | Agda.TypeChecking.Substitute | 
| funSort' | Agda.TypeChecking.Substitute | 
| funSplitTree | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| 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 | 
| funUniv | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal | 
| funWith | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend | 
| fuseIntervals | Agda.Syntax.Position | 
| fuseRange | Agda.Syntax.Position | 
| fuseRanges | Agda.Syntax.Position | 
| FVs | Agda.TypeChecking.MetaVars | 
| fwords |  | 
| 1 (Function) | Agda.Syntax.Common.Pretty | 
| 2 (Function) | Agda.TypeChecking.Pretty |