| 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 |
| 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 |
| 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 |
| 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 |
| findInterfaceFile | Agda.Interaction.FindFile |
| findMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| findPath | Agda.Utils.Graph |
| 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 |
| Fixed | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| Fixity | Agda.Syntax.Fixity |
| fixityLevel | Agda.Syntax.Fixity |
| fixSize | Agda.TypeChecking.Test.Generators |
| fixSizeConf | Agda.TypeChecking.Test.Generators |
| Flag | Agda.Interaction.Options |
| flattenSubmodules | Agda.Compiler.Alonzo.Main |
| flattenSubstitution | Agda.TypeChecking.Rules.LHS.Unify |
| flattenTel | Agda.TypeChecking.Telescope |
| Flex | Agda.Utils.Warshall |
| 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 |
| fMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| fmExp | Agda.Auto.Convert |
| fmExps | 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 |
| foldClauses | Agda.Compiler.Alonzo.Main |
| foldTerm | Agda.Syntax.Internal.Generic |
| followedBy | Agda.Syntax.Parser.LexActions |
| forAll | Agda.Utils.QuickCheck |
| forAllShrink | Agda.Utils.QuickCheck |
| force | Agda.Syntax.Strict |
| forceData | Agda.TypeChecking.Rules.Data |
| forceM | Agda.Utils.Monad |
| forcePi | Agda.TypeChecking.Rules.Term |
| forEachArgM | Agda.Compiler.Agate.Common |
| forgetM | Agda.Utils.Monad |
| Free | Agda.TypeChecking.Free |
| freeIn | Agda.TypeChecking.Free |
| freeInIgnoringSorts | Agda.TypeChecking.Free |
| FreeVars | Agda.TypeChecking.Free |
| freeVars | Agda.TypeChecking.Free |
| freeVarsToApply | Agda.TypeChecking.Monad.Signature, 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 |
| fromCurrentModule | Agda.Compiler.Alonzo.Main |
| fromDiagonals | Agda.Termination.Lexicographic |
| fromIndexList | Agda.Termination.Matrix |
| fromJust | Agda.Utils.Maybe |
| fromList | |
| 1 (Function) | Agda.Utils.Graph |
| 2 (Function) | Agda.Termination.CallGraph |
| fromLists | Agda.Termination.Matrix |
| fromLiteral | Agda.TypeChecking.Primitive |
| fromMaybe | Agda.Utils.Maybe |
| fromMaybeM | Agda.Utils.Maybe |
| frommy | Agda.Auto.Convert |
| frommyExp | Agda.Auto.Convert |
| frommyExps | Agda.Auto.Convert |
| frommyType | Agda.Auto.Convert |
| fromReducedTerm | Agda.TypeChecking.Primitive |
| FromTerm | Agda.TypeChecking.Primitive |
| fromTerm | Agda.TypeChecking.Primitive |
| FromTermFunction | Agda.TypeChecking.Primitive |
| fsep | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| fullRender | Agda.Utils.Pretty |
| Fun | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Syntax.Internal |
| 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 |
| FunClause | Agda.Syntax.Concrete |
| funClauses | 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 |
| FunctionCtx | Agda.Syntax.Fixity |
| 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 |
| funFreq | Agda.TypeChecking.Test.Generators |
| funInv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| funPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| FunV | Agda.Syntax.Internal |
| FunView | Agda.Syntax.Internal |
| funView | Agda.Syntax.Internal |
| fuseRange | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| fuseRanges | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| FV | Agda.TypeChecking.Free |
| fwords | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |