| Fail | Agda.TypeChecking.CompiledClause |
| 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 |
| fastDistinct | Agda.Utils.List |
| 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 |
| 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, Agda.Interaction.GhciTop |
| findInterfaceFile | Agda.Interaction.FindFile |
| findMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| findPath | Agda.Utils.Graph |
| findperm | Agda.Auto.CaseSplit |
| findPosition | Agda.Compiler.Epic.Forcing |
| 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 |
| Fixity' | |
| 1 (Type/Class) | Agda.Syntax.Fixity |
| 2 (Data Constructor) | Agda.Syntax.Fixity |
| fixityLevel | Agda.Syntax.Fixity |
| fixSize | Agda.TypeChecking.Test.Generators |
| fixSizeConf | Agda.TypeChecking.Test.Generators |
| Flag | Agda.Interaction.Options |
| flattenSubstitution | Agda.TypeChecking.Rules.LHS.Unify |
| flattenTel | Agda.TypeChecking.Telescope |
| Flex | |
| 1 (Data Constructor) | Agda.Utils.Warshall |
| 2 (Data Constructor) | Agda.TypeChecking.MetaVars.Occurs |
| 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 |
| fmapM | Agda.Utils.Monad |
| 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 |
| focusType | Agda.TypeChecking.Rules.LHS.Problem |
| foldM' | Agda.Compiler.Epic.Forcing |
| FoldState | |
| 1 (Type/Class) | Agda.Compiler.Epic.Forcing |
| 2 (Data Constructor) | Agda.Compiler.Epic.Forcing |
| foldTerm | Agda.Syntax.Internal.Generic |
| followedBy | Agda.Syntax.Parser.LexActions |
| forAll | Agda.Utils.QuickCheck |
| forAllShrink | Agda.Utils.QuickCheck |
| force | |
| 1 (Function) | Agda.Syntax.Strict |
| 2 (Function) | Agda.TypeChecking.Forcing |
| Forced | Agda.Syntax.Common |
| forceData | Agda.TypeChecking.Rules.Data |
| forcedVariables | Agda.TypeChecking.Forcing |
| forceM | Agda.Utils.Monad |
| forcePi | Agda.TypeChecking.Rules.Term |
| forgetM | Agda.Utils.Monad |
| Free | Agda.TypeChecking.Free |
| freeIn | |
| 1 (Function) | Agda.TypeChecking.Free |
| 2 (Function) | Agda.Auto.Convert |
| freeInIgnoringSorts | Agda.TypeChecking.Free |
| FreeVars | Agda.TypeChecking.Free |
| freeVars | Agda.TypeChecking.Free |
| freevars | Agda.Auto.CaseSplit |
| 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 |
| fromAgda | Agda.Compiler.Epic.FromAgda |
| fromDiagonals | Agda.Termination.Lexicographic |
| fromIndexList | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| fromJust | Agda.Utils.Maybe |
| fromList | |
| 1 (Function) | Agda.Utils.Graph |
| 2 (Function) | Agda.Termination.CallGraph |
| fromLists | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| fromLiteral | Agda.TypeChecking.Primitive |
| fromMaybe | Agda.Utils.Maybe |
| fromMaybeM | Agda.Utils.Maybe |
| frommy | Agda.Auto.Convert |
| frommyClause | 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 (Type/Class) | Agda.Compiler.Epic.AuxAST |
| 2 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| 3 (Data Constructor) | Agda.Syntax.Concrete |
| 4 (Data Constructor) | Agda.Syntax.Internal |
| 5 (Data Constructor) | Agda.Syntax.Abstract |
| 6 (Type/Class) | Agda.TypeChecking.Primitive |
| funAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| funArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| funArgs | Agda.Compiler.Epic.AuxAST |
| FunClause | Agda.Syntax.Concrete |
| funClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| funComment | Agda.Compiler.Epic.AuxAST |
| funCompiled | 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 |
| funEpicCode | Agda.Compiler.Epic.AuxAST |
| funExpr | Agda.Compiler.Epic.AuxAST |
| funFreq | Agda.TypeChecking.Test.Generators |
| funInline | Agda.Compiler.Epic.AuxAST |
| funInv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| funName | Agda.Compiler.Epic.AuxAST |
| funPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| funProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| funs | Agda.Compiler.Epic.Erasure |
| 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 |
| fv | Agda.Compiler.Epic.AuxAST |
| FVs | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| fwords | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |