| Face | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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 |
| FamilyOrNot | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| famThing | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| 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.Utils.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 |
| fibrantLub | Agda.TypeChecking.Substitute |
| 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 |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| Fields | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| FieldSig | Agda.Syntax.Concrete |
| FileNotFound | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| findInstance | Agda.TypeChecking.InstanceArguments |
| FindInstanceOF | Agda.Interaction.Base |
| findInteractionPoint_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| findInterfaceFile | Agda.Interaction.FindFile |
| findInterfaceFile' | Agda.Interaction.FindFile |
| findLib' | Agda.Interaction.Library |
| findMentions | Agda.Interaction.SearchAbout |
| 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 |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| FixityInRenamingModule_ | Agda.Interaction.Options.Warnings |
| FixityLevel | Agda.Syntax.Common |
| fixityLevel | Agda.Syntax.Common |
| fixityRange | Agda.Syntax.Common |
| Flag | Agda.Interaction.Options, Agda.Compiler.Backend |
| flagGhcBin | Agda.Compiler.MAlonzo.Compiler |
| flagGhcCallGhc | Agda.Compiler.MAlonzo.Compiler |
| flagGhcCompile | Agda.Compiler.MAlonzo.Compiler |
| flagGhcFlags | Agda.Compiler.MAlonzo.Compiler |
| flagGhcStrict | Agda.Compiler.MAlonzo.Compiler |
| flagGhcStrictData | Agda.Compiler.MAlonzo.Compiler |
| Flat | Agda.Syntax.Common |
| flatName | Agda.Compiler.JS.Compiler |
| flatten | Agda.TypeChecking.Positivity |
| flattenScope | Agda.Syntax.Scope.Base |
| flattenTel | Agda.TypeChecking.Telescope |
| FldName | Agda.Syntax.Scope.Base |
| Flex | |
| 1 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
| 3 (Data Constructor) | Agda.Utils.Warshall |
| 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 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Type/Class) | Agda.Utils.Warshall |
| 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 |
| flipCmp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| flipP | Agda.Utils.Permutation |
| float | Agda.Utils.Pretty |
| fmapReduce | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| fmapTCMT | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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 |
| 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.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.Compiler.Backend, Agda.TypeChecking.Monad |
| ForcedConstructorNotInstantiated | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| forM' | Agda.Utils.Monad |
| formatDebugMessage | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| 2 (Type/Class) | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| 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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| freezeMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| freezeMetas' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| fresh | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| freshLens | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| FreshName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| freshName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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 |
| freshNames | Agda.Compiler.MAlonzo.Compiler |
| freshName_ | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| freshNoName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| freshNoName_ | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| freshProblemId | Agda.TypeChecking.Conversion.Pure |
| freshRecordName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| freshTCM | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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 | Agda.Utils.SmallSet |
| fromCallSiteList | Agda.Utils.CallStack |
| fromCmp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| fromConPatternInfo | Agda.Syntax.Internal |
| fromCType | Agda.TypeChecking.Rules.Data |
| fromDistinctAscendingLists | Agda.Utils.BiMap |
| fromDistinctAscendingListsPrecondition | Agda.Utils.BiMap |
| fromDistinctAscList | 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.Bag |
| 4 (Function) | Agda.Utils.Singleton, Agda.Termination.CallGraph |
| 5 (Function) | Agda.Utils.SmallSet |
| 6 (Function) | Agda.Utils.BiMap |
| 7 (Function) | Agda.Utils.Favorites |
| fromList1 | Agda.Utils.List2 |
| fromList1Maybe | Agda.Utils.List2 |
| fromListMaybe | Agda.Utils.List2 |
| fromListPrecondition | Agda.Utils.BiMap |
| fromLists | Agda.Termination.SparseMatrix |
| fromLiteral | Agda.TypeChecking.Primitive |
| fromLType | Agda.TypeChecking.Rules.Data |
| 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 |
| fromReducedTerm | Agda.TypeChecking.Primitive |
| fromRight | Agda.Utils.Either |
| fromRightM | Agda.Utils.Either |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| fsep | |
| 1 (Function) | Agda.Utils.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.Utils.Pretty |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| funCompiled | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| funCovering | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Function | |
| 1 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 2 (Type/Class) | Agda.Utils.TypeLevel |
| 3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 4 (Data Constructor) | Agda.Interaction.Response |
| FunctionCtx | Agda.Syntax.Fixity |
| FunctionFlag | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| FunctionInverse | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| functionInverse | Agda.TypeChecking.Injectivity |
| FunctionInverse' | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| FunctionKind | Agda.Compiler.MAlonzo.Misc |
| FunctionReductions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| FunctionSpaceDomainCtx | Agda.Syntax.Fixity |
| FunctionTypeInSizeUniv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| FunDef | |
| 1 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions |
| 2 (Data Constructor) | Agda.Syntax.Reflected |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| funDelayed | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| funExtLam | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| funFlag | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| funFlags | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| FunInline | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| funInline | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| funInv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| FunK | Agda.Compiler.MAlonzo.Misc |
| FunMacro | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| funMacro | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| funMutual | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| FunName | |
| 1 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types |
| 2 (Data Constructor) | Agda.Syntax.Scope.Base |
| funProjection | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| FunStatic | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| funStatic | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| funTerminates | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| funTreeless | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| funWith | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| fuseIntervals | Agda.Syntax.Position |
| fuseRange | Agda.Syntax.Position |
| fuseRanges | Agda.Syntax.Position |
| FVs | Agda.TypeChecking.MetaVars |
| fwords | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |