| Face | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Fail | |
| 1 (Data Constructor) | Agda.TypeChecking.CompiledClause |
| 2 (Data Constructor) | Agda.TypeChecking.Empty |
| FailBecause | Agda.TypeChecking.Empty |
| Failed | Agda.Auto.NarrowingSearch |
| 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 |
| famThing | Agda.TypeChecking.Primitive |
| farEmpty | Agda.TypeChecking.Serialise.Base |
| farFresh | Agda.TypeChecking.Serialise.Base |
| farReuse | 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 |
| feFlexRig | Agda.TypeChecking.Free.Lazy |
| feIgnoreSorts | Agda.TypeChecking.Free.Lazy |
| feRelevance | Agda.TypeChecking.Free.Lazy |
| feSingleton | Agda.TypeChecking.Free.Lazy |
| 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 |
| FieldName | Agda.Syntax.Scope.Base |
| FieldOutsideRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| File | |
| 1 (Type/Class) | Agda.Interaction.Highlighting.Precise |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| FileNotFound | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| filePath | Agda.Utils.FileName |
| filePos | Agda.Interaction.Library |
| FileType | Agda.Syntax.Common |
| filter | |
| 1 (Function) | Agda.Utils.HashMap |
| 2 (Function) | Agda.Utils.Trie |
| filterAndRest | Agda.Utils.List |
| filterEdges | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| filterKeys | Agda.Utils.Map |
| filterMaybe | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| filterScope | Agda.Syntax.Scope.Base |
| filterWithKey | Agda.Utils.HashMap |
| 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 |
| 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.BasicOps |
| findInteractionPoint_ | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| findInterfaceFile | Agda.Interaction.FindFile |
| findLib' | Agda.Interaction.Library |
| findMentions | Agda.Interaction.SearchAbout |
| findperm | Agda.Auto.CaseSplit |
| findPossibleRecords | Agda.TypeChecking.Records |
| findRigidBelow | Agda.TypeChecking.SizedTypes.WarshallSolver |
| findWithIndex | Agda.Utils.List |
| Finite | Agda.Utils.Warshall |
| firstHole | Agda.Utils.Zipper |
| firstMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| firstNonTakenName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| firstPart | Agda.TypeChecking.Telescope |
| fitsIn | Agda.TypeChecking.Rules.Data |
| fix | Agda.Compiler.JS.Substitution |
| Fixities | Agda.Syntax.Concrete.Fixity |
| fixitiesAndPolarities | Agda.Syntax.Concrete.Fixity |
| Fixity | |
| 1 (Type/Class) | Agda.Syntax.Fixity |
| 2 (Data Constructor) | Agda.Syntax.Fixity |
| Fixity' | |
| 1 (Type/Class) | Agda.Syntax.Fixity |
| 2 (Data Constructor) | Agda.Syntax.Fixity |
| fixityAssoc | Agda.Syntax.Fixity |
| fixityLevel | Agda.Syntax.Fixity |
| fixityRange | Agda.Syntax.Fixity |
| fixTarget | Agda.TypeChecking.Coverage |
| Flag | Agda.Interaction.Options, Agda.Compiler.Backend |
| 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 |
| 4 (Data Constructor) | Agda.TypeChecking.MetaVars.Occurs |
| flex | Agda.TypeChecking.SizedTypes.Syntax |
| FlexChoice | Agda.TypeChecking.Rules.LHS.Problem |
| flexHiding | Agda.TypeChecking.Rules.LHS.Problem |
| Flexible | |
| 1 (Data Constructor) | Agda.TypeChecking.Free.Lazy |
| 2 (Data Constructor) | Agda.TypeChecking.Free |
| 3 (Data Constructor) | Agda.TypeChecking.Free.Old |
| 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 | |
| 1 (Function) | Agda.TypeChecking.Free |
| 2 (Function) | Agda.TypeChecking.Free.Old |
| 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 |
| flexOrigin | Agda.TypeChecking.Rules.LHS.Problem |
| flexPos | Agda.TypeChecking.Rules.LHS.Problem |
| FlexRig | Agda.TypeChecking.Free.Lazy |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| flipP | Agda.Utils.Permutation |
| float | Agda.Utils.Pretty |
| floatEq | Agda.Utils.Float |
| floatLt | Agda.Utils.Float |
| 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 |
| 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 |
| foldl' | Agda.Utils.HashMap |
| foldListT | Agda.Utils.ListT |
| foldlWithKey' | Agda.Utils.HashMap |
| foldMatch | Agda.TypeChecking.Patterns.Match |
| foldPattern | Agda.Syntax.Internal.Pattern |
| Foldr | Agda.Utils.TypeLevel |
| foldr | Agda.Utils.HashMap |
| Foldr' | Agda.Utils.TypeLevel |
| foldrAPattern | Agda.Syntax.Abstract.Pattern |
| foldrCPattern | Agda.Syntax.Concrete.Pattern |
| FoldRigid | Agda.TypeChecking.MetaVars.Occurs |
| foldRigid | Agda.TypeChecking.MetaVars.Occurs |
| foldrPattern | Agda.Syntax.Internal.Pattern |
| foldrWithKey | Agda.Utils.HashMap |
| foldTerm | Agda.Syntax.Internal.Generic |
| followedBy | Agda.Syntax.Parser.LexActions |
| for | Agda.Utils.Functor |
| forallFaceMaps | Agda.TypeChecking.Conversion |
| forallQ | 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 |
| ForcedVariables | Agda.TypeChecking.Forcing |
| forcedVariables | Agda.TypeChecking.Forcing |
| forceEtaExpandRecord | Agda.TypeChecking.Records |
| ForceNotFree | Agda.TypeChecking.Free.Reduce |
| forceNotFree | Agda.TypeChecking.Free.Reduce |
| forcePiUsingInjectivity | Agda.TypeChecking.Injectivity |
| forceSort | Agda.TypeChecking.Rules.Data |
| forceTranslateTelescope | Agda.TypeChecking.Forcing |
| forcingTranslation | Agda.TypeChecking.Forcing |
| 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 |
| 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 |
| 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 |
| forMaybe | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| forMaybeM | 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 |
| 3 (Type/Class) | Agda.TypeChecking.Free.Old |
| FreeEnv | |
| 1 (Type/Class) | Agda.TypeChecking.Free.Lazy |
| 2 (Data Constructor) | Agda.TypeChecking.Free.Lazy |
| freeIn | |
| 1 (Function) | Agda.TypeChecking.Free |
| 2 (Function) | Agda.TypeChecking.Free.Old |
| 3 (Function) | Agda.Compiler.Treeless.Subst |
| 4 (Function) | Agda.Auto.Convert |
| freeInIgnoringSortAnn | Agda.TypeChecking.Free.Old |
| freeInIgnoringSorts | |
| 1 (Function) | Agda.TypeChecking.Free |
| 2 (Function) | Agda.TypeChecking.Free.Old |
| FreeM | Agda.TypeChecking.Free.Lazy |
| FreeVariables | Agda.Syntax.Common |
| freeVariablesFromList | Agda.Syntax.Common |
| FreeVars | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Type/Class) | Agda.TypeChecking.Free |
| 3 (Type/Class) | Agda.TypeChecking.Free.Old |
| freeVars | |
| 1 (Function) | Agda.Auto.Syntax |
| 2 (Function) | Agda.TypeChecking.Free |
| 3 (Function) | Agda.TypeChecking.Free.Old |
| 4 (Function) | Agda.Compiler.Treeless.Subst |
| freevars | Agda.Auto.CaseSplit |
| freeVars' | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| freeVarsIgnore | Agda.TypeChecking.Free.Old |
| 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 |
| 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 |
| 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 |
| freshNames | Agda.Compiler.MAlonzo.Compiler |
| 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 |
| freshRecordName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| freshTCM | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| from | Agda.Interaction.Highlighting.Range |
| fromCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| fromConPatternInfo | Agda.Syntax.Internal |
| fromCType | Agda.TypeChecking.Rules.Data |
| fromEdges | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| fromEdgesWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| fromIndexList | Agda.Termination.SparseMatrix |
| 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.VarSet |
| 2 (Function) | Agda.Utils.BiMap |
| 3 (Function) | Agda.Utils.HashMap |
| 4 (Function) | Agda.Utils.Bag |
| 5 (Function) | Agda.Utils.NonemptyList |
| 6 (Function) | Agda.Utils.Favorites |
| 7 (Function) | Agda.Termination.CallGraph |
| fromLists | Agda.Termination.SparseMatrix |
| fromListWith | Agda.Utils.HashMap |
| 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 |
| 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 |
| 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.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.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 |
| funCopatternLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| funCovering | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Function | |
| 1 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 2 (Data Constructor) | Agda.Interaction.Response |
| 3 (Type/Class) | Agda.Utils.TypeLevel |
| 4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| FunctionCtx | Agda.Syntax.Fixity |
| 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 |
| 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.Abstract |
| 3 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
| funDelayed | 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 |
| 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 |
| funProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| FunSig | |
| 1 (Data Constructor) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
| 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 |
| funWith | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| fuseIntervals | Agda.Syntax.Position |
| fuseRange | Agda.Syntax.Position |
| fuseRanges | Agda.Syntax.Position |
| FV | |
| 1 (Data Constructor) | Agda.TypeChecking.Free |
| 2 (Data Constructor) | Agda.TypeChecking.Free.Old |
| FVs | Agda.TypeChecking.MetaVars |
| fwords | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |