Agda-2.6.2.2.20221106: A dependently typed functional programming language and proof assistant

Index - F

FaceAgda.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
FailedAgda.Auto.NarrowingSearch
failOnRecordFieldWarningsAgda.TypeChecking.Records
fakeDAgda.Compiler.MAlonzo.Misc
FakeDeclAgda.Utils.Haskell.Syntax
fakeDeclAgda.Compiler.MAlonzo.Misc
fakeDQAgda.Compiler.MAlonzo.Misc
fakeDSAgda.Compiler.MAlonzo.Misc
FakeExpAgda.Utils.Haskell.Syntax
fakeExpAgda.Compiler.MAlonzo.Misc
FakeTypeAgda.Utils.Haskell.Syntax
fakeTypeAgda.Compiler.MAlonzo.Misc
fallThroughAgda.TypeChecking.CompiledClause
FamilyOrNotAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical
familyOrNotAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical
famThingAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical
farEmptyAgda.TypeChecking.Serialise.Base
farFreshAgda.TypeChecking.Serialise.Base
fastDistinctAgda.Utils.List
fastNormaliseAgda.TypeChecking.Reduce.Fast
fastReduceAgda.TypeChecking.Reduce.Fast
Favorites 
1 (Type/Class)Agda.Utils.Favorites
2 (Data Constructor)Agda.Utils.Favorites
fcatAgda.Utils.Pretty
feExtraAgda.TypeChecking.Free.Lazy
feFlexRigAgda.TypeChecking.Free.Lazy
feIgnoreSortsAgda.TypeChecking.Free.Lazy
feModalityAgda.TypeChecking.Free.Lazy
feSingletonAgda.TypeChecking.Free.Lazy
fiberAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical
fibrantLubAgda.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
field1Agda.Utils.Lens.Examples
field2Agda.Utils.Lens.Examples
FieldAssignment 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
FieldAssignment'Agda.Syntax.Concrete
FieldBlockAgda.Syntax.Concrete.Definitions.Types
fieldLabelModifierAgda.Interaction.JSON
FieldNameAgda.Syntax.Scope.Base
FieldOutsideRecordAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FieldSAgda.Syntax.Abstract
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
FieldSigAgda.Syntax.Concrete
FileNotFoundAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
filePathAgda.Utils.FileName
filePosAgda.Interaction.Library.Base, Agda.Interaction.Library
FileTypeAgda.Syntax.Common
filter 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.Trie
filterAndRestAgda.Utils.List
filterCallStackAgda.Utils.CallStack
filterEdgesAgda.Utils.Graph.AdjacencyMap.Unidirectional
filterKeysAgda.Utils.Map
filterMaybe 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
filterNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
filterNodesKeepingEdgesAgda.Utils.Graph.AdjacencyMap.Unidirectional
filterScopeAgda.Syntax.Scope.Base
filterTCWarningsAgda.TypeChecking.Pretty.Warning
filterUsedAgda.Syntax.Treeless, Agda.Compiler.Backend
filterVarMapAgda.TypeChecking.Free
filterVarMapToListAgda.TypeChecking.Free
FinalChecksAgda.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
findClauseDeepAgda.Auto.Convert
FindErrorAgda.Interaction.FindFile
findErrorToTypeErrorAgda.Interaction.FindFile
findFileAgda.Interaction.FindFile
findFile'Agda.Interaction.FindFile
findFile''Agda.Interaction.FindFile
findIdxAgda.TypeChecking.MetaVars
FindInstanceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
findInstanceAgda.TypeChecking.InstanceArguments
FindInstanceOFAgda.Interaction.Base
findInteractionPoint_Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
findInterfaceFileAgda.Interaction.FindFile
findInterfaceFile'Agda.Interaction.FindFile
findLib'Agda.Interaction.Library
findMentionsAgda.Interaction.SearchAbout
findNameInScopeAgda.Syntax.Scope.Base
findOverlapAgda.Utils.List
findpermAgda.Auto.CaseSplit
findPossibleRecordsAgda.TypeChecking.Records
findProjectRootAgda.Interaction.Library
findRigidBelowAgda.TypeChecking.SizedTypes.WarshallSolver
findWithIndexAgda.Utils.List
FiniteAgda.Utils.Warshall
firstHoleAgda.Utils.Zipper
firstMetaAgda.Syntax.Internal.MetaVars
firstNonTakenNameAgda.Syntax.Concrete, Agda.Syntax.Concrete.Name
firstPartAgda.TypeChecking.Telescope
fitsInAgda.TypeChecking.Rules.Data
fittingNamedArgAgda.Syntax.Common
fixAgda.Compiler.JS.Substitution
FixitiesAgda.Syntax.Concrete.Fixity
fixitiesAndPolaritiesAgda.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
fixityAssocAgda.Syntax.Common
FixityInRenamingModuleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FixityInRenamingModule_Agda.Interaction.Options.Warnings
FixityLevelAgda.Syntax.Common
fixityLevelAgda.Syntax.Common
fixityRangeAgda.Syntax.Common
FlagAgda.Interaction.Options, Agda.Compiler.Backend
flagGhcBinAgda.Compiler.MAlonzo.Compiler
flagGhcCallGhcAgda.Compiler.MAlonzo.Compiler
flagGhcCompileAgda.Compiler.MAlonzo.Compiler
flagGhcFlagsAgda.Compiler.MAlonzo.Compiler
flagGhcStrictAgda.Compiler.MAlonzo.Compiler
flagGhcStrictDataAgda.Compiler.MAlonzo.Compiler
FlatAgda.Syntax.Common
flatNameAgda.Compiler.JS.Compiler
FlatScopeAgda.Syntax.Scope.Flat
flattenAgda.TypeChecking.Positivity
flattenScopeAgda.Syntax.Scope.Flat
flattenTelAgda.TypeChecking.Telescope
FldNameAgda.Syntax.Scope.Base
Flex 
1 (Data Constructor)Agda.Utils.Warshall
2 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
3 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
flexAgda.TypeChecking.SizedTypes.Syntax
flexArgInfoAgda.TypeChecking.Rules.LHS.Problem
FlexChoiceAgda.TypeChecking.Rules.LHS.Problem
flexForcedAgda.TypeChecking.Rules.LHS.Problem
FlexibleAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
FlexibleVar 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
flexibleVariablesAgda.TypeChecking.SizedTypes
FlexibleVarKindAgda.TypeChecking.Rules.LHS.Problem
FlexibleVarsAgda.TypeChecking.Rules.LHS.Problem
flexibleVarsAgda.TypeChecking.Free
flexiblyAgda.TypeChecking.MetaVars.Occurs
FlexId 
1 (Type/Class)Agda.Utils.Warshall
2 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
flexIdAgda.TypeChecking.SizedTypes.Syntax
flexKindAgda.TypeChecking.Rules.LHS.Problem
FlexOfAgda.TypeChecking.SizedTypes.Syntax
flexPosAgda.TypeChecking.Rules.LHS.Problem
FlexRigAgda.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
flexRigOccurrenceInAgda.TypeChecking.Free
FlexsAgda.TypeChecking.SizedTypes.Syntax
flexsAgda.TypeChecking.SizedTypes.Syntax
flexScopeAgda.Utils.Warshall
flexVarAgda.TypeChecking.Rules.LHS.Problem
flexVarsAgda.TypeChecking.Rules.LHS.Unify.Types
flipCmpAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
flipPAgda.Utils.Permutation
floatAgda.Utils.Pretty
fmapReduceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
fmapTCMTAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
fmExpAgda.Auto.Convert
fmExpsAgda.Auto.Convert
fmLevelAgda.Auto.Convert
fmTypeAgda.Auto.Convert
focusAgda.Utils.Lens
foldAAgda.Utils.Applicative
foldableAgda.Interaction.JSON
foldAPatternAgda.Syntax.Abstract.Pattern
foldArgsAgda.Auto.SearchControl
foldCPatternAgda.Syntax.Concrete.Pattern
foldExpr 
1 (Function)Agda.Syntax.Concrete.Generic
2 (Function)Agda.Syntax.Abstract.Views
FoldExprFnAgda.Syntax.Abstract.Views
FoldExprRecFnAgda.Syntax.Abstract.Views
foldListTAgda.Utils.ListT
foldMapAAgda.Utils.Applicative
foldMatchAgda.TypeChecking.Patterns.Match
foldPatternAgda.Syntax.Internal.Pattern
FoldrAgda.Utils.TypeLevel
foldrAgda.Utils.List1
Foldr'Agda.Utils.TypeLevel
foldrAPatternAgda.Syntax.Abstract.Pattern
foldrCPatternAgda.Syntax.Concrete.Pattern
foldrMetaSetAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
foldrPatternAgda.Syntax.Internal.Pattern
foldTermAgda.Syntax.Internal.Generic
followedByAgda.Syntax.Parser.LexActions
forAgda.Utils.Functor
forAAgda.Utils.Applicative
forallFaceMapsAgda.TypeChecking.Conversion
forallQAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
ForcedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ForcedConstructorNotInstantiatedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
forceEtaExpandRecordAgda.TypeChecking.Records
ForceNotFreeAgda.TypeChecking.Free.Reduce
forceNotFreeAgda.TypeChecking.Free.Reduce
forcePiUsingInjectivityAgda.TypeChecking.Injectivity
forceSortAgda.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
ForeignFileHeaderPragmaAgda.Compiler.MAlonzo.Pragmas
foreignHaskellAgda.Compiler.MAlonzo.Pragmas
ForeignImportAgda.Compiler.MAlonzo.Pragmas
ForeignOtherAgda.Compiler.MAlonzo.Pragmas
ForeignPragmaAgda.Syntax.Concrete
forEither3MAgda.Utils.Three
forgetAllAgda.Utils.IndexedList
forgetIndexAgda.Utils.IndexedList
forgetLoneSigsAgda.Syntax.Concrete.Definitions.Monad
forkTCMAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
forM'Agda.Utils.Monad
formatDebugMessageAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
formatLibErrorAgda.Interaction.Library.Base
formatLibPositionInfoAgda.Interaction.Library.Base
forMaybe 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
forMaybeMAgda.Utils.Monad
forMaybeMMAgda.Utils.Monad
forMMAgda.Utils.Monad
forMM_Agda.Utils.Monad
FracAgda.Utils.Haskell.Syntax
FrameAgda.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
freeInIgnoringSortsAgda.TypeChecking.Free
FreeMAgda.TypeChecking.Free.Lazy
FreeTAgda.TypeChecking.Free.Lazy
FreeVariablesAgda.Syntax.Common
freeVariablesFromListAgda.Syntax.Common
FreeVarsAgda.Auto.Syntax
freeVars 
1 (Function)Agda.Auto.Syntax
2 (Function)Agda.TypeChecking.Free
3 (Function)Agda.Compiler.Treeless.Subst
freevarsAgda.Auto.CaseSplit
freeVars'Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
freeVarsIgnoreAgda.TypeChecking.Free
freeVarsOffsetAgda.Auto.Syntax
freeVarsToApplyAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
freezeMetasAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
freshAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
freshAbstractNameAgda.Syntax.Scope.Monad
freshAbstractName_Agda.Syntax.Scope.Monad
freshAbstractQNameAgda.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
freshConcreteNameAgda.Syntax.Scope.Monad
freshIntAgda.TypeChecking.Conversion.Pure
freshInteractionIdAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
freshLensAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FreshNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
freshNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
freshNameIdAgda.TypeChecking.Conversion.Pure
FreshNameModeAgda.Syntax.Concrete, Agda.Syntax.Abstract.Name, Agda.Syntax.Concrete.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
freshNamesAgda.Compiler.MAlonzo.Compiler
freshName_Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
freshNoNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
freshNoName_Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
freshProblemIdAgda.TypeChecking.Conversion.Pure
freshRecordNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
freshTCMAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FreshThings 
1 (Type/Class)Agda.TypeChecking.Conversion.Pure
2 (Data Constructor)Agda.TypeChecking.Conversion.Pure
fromAgda.Interaction.Highlighting.Range
fromAbsNameAgda.TypeChecking.Serialise.Instances.Abstract
FromArgsAgda.Interaction.JSON
fromAscList 
1 (Function)Agda.Utils.BoolSet
2 (Function)Agda.Utils.SmallSet
fromCallSiteListAgda.Utils.CallStack
fromCmpAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
fromConPatternInfoAgda.Syntax.Internal
fromCTypeAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
fromDistinctAscendingListsAgda.Utils.BiMap
fromDistinctAscendingListsPreconditionAgda.Utils.BiMap
fromDistinctAscList 
1 (Function)Agda.Utils.BoolSet
2 (Function)Agda.Utils.SmallSet
fromDotNetTimeAgda.Interaction.JSON
fromEdgesAgda.Utils.Graph.AdjacencyMap.Unidirectional
fromEdgesWithAgda.Utils.Graph.AdjacencyMap.Unidirectional
fromEncodingAgda.Interaction.JSON
fromImportedNameAgda.Syntax.Common
fromIndexListAgda.Termination.SparseMatrix
FromJSONAgda.Interaction.JSON
fromJSONAgda.Interaction.JSON
FromJSON1Agda.Interaction.JSON
FromJSON2Agda.Interaction.JSON
FromJSONKeyAgda.Interaction.JSON
fromJSONKeyAgda.Interaction.JSON
FromJSONKeyCoerceAgda.Interaction.JSON
FromJSONKeyFunctionAgda.Interaction.JSON
fromJSONKeyListAgda.Interaction.JSON
FromJSONKeyTextAgda.Interaction.JSON
FromJSONKeyTextParserAgda.Interaction.JSON
FromJSONKeyValueAgda.Interaction.JSON
fromJust 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
fromLeftAgda.Utils.Either
fromLeftMAgda.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.Singleton, Agda.Termination.CallGraph
6 (Function)Agda.Utils.SmallSet
7 (Function)Agda.Utils.BiMap
8 (Function)Agda.Utils.Favorites
fromList1Agda.Utils.List2
fromList1EitherAgda.Utils.List2
fromList1MaybeAgda.Utils.List2
fromListMaybeAgda.Utils.List2
fromListNAgda.Utils.List1
fromListPreconditionAgda.Utils.BiMap
fromListsAgda.Termination.SparseMatrix
fromListSafeAgda.Utils.List1
fromLiteralAgda.TypeChecking.Primitive
fromLTypeAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
fromMaybe 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
fromMaybeM 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
fromMaybeMPAgda.Utils.Monad
fromMillisecondsAgda.Utils.Time
frommyClauseAgda.Auto.Convert
frommyExpsAgda.Auto.Convert
fromNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
fromNodeSetAgda.Utils.Graph.AdjacencyMap.Unidirectional
fromNonOverlappingNonEmptyAscendingListAgda.Utils.RangeMap
fromOrderingAgda.Utils.PartialOrd
fromOrderingsAgda.Utils.PartialOrd
fromOrdinaryAgda.Syntax.Concrete
fromPatternSubstitutionAgda.TypeChecking.Substitute
fromReducedTermAgda.TypeChecking.Primitive
fromRightAgda.Utils.Either
fromRightMAgda.Utils.Either
fromSplitPatternAgda.TypeChecking.Coverage.Match
fromSplitPatternsAgda.TypeChecking.Coverage.Match
fromSubscriptDigitAgda.Utils.Suffix
FromTermAgda.TypeChecking.Primitive
fromTermAgda.TypeChecking.Primitive
FromTermFunctionAgda.TypeChecking.Primitive
FrontEndEmacsAgda.Main
FrontEndJsonAgda.Main
FrontEndReplAgda.Main
FrontendTypeAgda.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
fst3Agda.Utils.Tuple
FullAgda.Interaction.Highlighting.Generate
fullAgda.Utils.IntSet.Infinite
fullBoundaryAgda.TypeChecking.Telescope
fullRenderAgda.Utils.Pretty
Fun 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
3 (Type/Class)Agda.TypeChecking.Primitive
funAbstrAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunArityAgda.Syntax.Internal.Pattern
funArityAgda.Syntax.Internal.Pattern
FunBindAgda.Utils.Haskell.Syntax
FunClauseAgda.Syntax.Concrete
FunClausesAgda.Auto.Auto
funClausesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funCompiledAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funCoveringAgda.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
FunctionCtxAgda.Syntax.Fixity
FunctionData 
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
FunctionDefnAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunctionFlagAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunctionInverseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
functionInverseAgda.TypeChecking.Injectivity
FunctionInverse'Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunctionKindAgda.Compiler.MAlonzo.Misc
FunctionReductionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunctionSpaceDomainCtxAgda.Syntax.Fixity
FunctionTypeInSizeUnivAgda.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
FunDefSAgda.Syntax.Abstract
funDelayedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funExtLamAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funFlagAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funFlagsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunInlineAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funInlineAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funInvAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funIsKanOpAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunKAgda.Compiler.MAlonzo.Misc
FunMacroAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funMacroAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funMutualAgda.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
funProjectionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunSigAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
FunSortAgda.Syntax.Internal
funSortAgda.TypeChecking.Substitute
funSort'Agda.TypeChecking.Substitute
funSplitTreeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunStaticAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funStaticAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funTerminatesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funTreelessAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funWithAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
fuseIntervalsAgda.Syntax.Position
fuseRangeAgda.Syntax.Position
fuseRangesAgda.Syntax.Position
FVsAgda.TypeChecking.MetaVars
fwords 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty