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

Index - F

FaceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Fail 
1 (Type/Class)Agda.Utils.Fail
2 (Data Constructor)Agda.Utils.Fail
3 (Data Constructor)Agda.TypeChecking.CompiledClause
FailedAgda.Auto.NarrowingSearch
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.Cubical, Agda.TypeChecking.Primitive
famThingAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
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
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
FieldNameAgda.Syntax.Scope.Base
FieldOutsideRecordAgda.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
FieldSigAgda.Syntax.Concrete
File 
1 (Type/Class)Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
FileNotFoundAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
filePathAgda.Utils.FileName
filePosAgda.Interaction.Library
FileTypeAgda.Syntax.Common
filterAgda.Utils.Trie
filterAndRestAgda.Utils.List
filterEdgesAgda.Utils.Graph.AdjacencyMap.Unidirectional
filterKeysAgda.Utils.Map
filterMaybe 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
filterScopeAgda.Syntax.Scope.Base
filterTCWarningsAgda.TypeChecking.Pretty.Warning
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
findInstanceAgda.TypeChecking.InstanceArguments
FindInstanceOFAgda.Interaction.Base
findInteractionPoint_Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
findInterfaceFileAgda.Interaction.FindFile
findInterfaceFile'Agda.Interaction.FindFile
findLib'Agda.Interaction.Library
findMentionsAgda.Interaction.SearchAbout
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.Name, Agda.Syntax.Concrete
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.TypeChecking.Monad, Agda.Compiler.Backend
FixityInRenamingModule_Agda.Interaction.Options.Warnings
FixityLevelAgda.Syntax.Common
fixityLevelAgda.Syntax.Common
fixityRangeAgda.Syntax.Common
FlagAgda.Interaction.Options, Agda.Compiler.Backend
FlatAgda.Syntax.Common
flatNameAgda.Compiler.JS.Compiler
flattenAgda.TypeChecking.Positivity
flattenScopeAgda.Syntax.Scope.Base
flattenTelAgda.TypeChecking.Telescope
FldNameAgda.Syntax.Scope.Base
Flex 
1 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
3 (Data Constructor)Agda.Utils.Warshall
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
flexiblyAgda.TypeChecking.MetaVars.Occurs
FlexId 
1 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)Agda.Utils.Warshall
flexIdAgda.TypeChecking.SizedTypes.Syntax
flexKindAgda.TypeChecking.Rules.LHS.Problem
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
flipCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
flipPAgda.Utils.Permutation
floatAgda.Utils.Pretty
floatEqAgda.Utils.Float
floatLtAgda.Utils.Float
fmapReduceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fmapTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fmExpAgda.Auto.Convert
fmExpsAgda.Auto.Convert
fmLevelAgda.Auto.Convert
fmTypeAgda.Auto.Convert
focusAgda.Utils.Lens
foldAPatternAgda.Syntax.Abstract.Pattern
foldArgsAgda.Auto.SearchControl
foldCPatternAgda.Syntax.Concrete.Pattern
foldExpr 
1 (Function)Agda.Syntax.Concrete.Generic
2 (Function)Agda.Syntax.Abstract.Views
foldListTAgda.Utils.ListT
foldMatchAgda.TypeChecking.Patterns.Match
foldPatternAgda.Syntax.Internal.Pattern
FoldrAgda.Utils.TypeLevel
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
forallFaceMapsAgda.TypeChecking.Conversion
forallQAgda.Syntax.Concrete.Pretty
ForcedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ForcedConstructorNotInstantiatedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
forkTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
forM'Agda.Utils.Monad
formatDebugMessageAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
freeVarsOffsetAgda.Auto.Syntax
freeVarsToApplyAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freezeMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freezeMetas'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshLensAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FreshNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshNameIdAgda.TypeChecking.Conversion.Pure
freshNamesAgda.Compiler.MAlonzo.Compiler
freshName_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshNoNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshNoName_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshProblemIdAgda.TypeChecking.Conversion.Pure
freshRecordNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
freshTCMAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FreshThings 
1 (Type/Class)Agda.TypeChecking.Conversion.Pure
2 (Data Constructor)Agda.TypeChecking.Conversion.Pure
fromAgda.Interaction.Highlighting.Range
fromAbsNameAgda.TypeChecking.Serialise.Instances.Abstract
fromAscListAgda.Utils.SmallSet
fromCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fromConPatternInfoAgda.Syntax.Internal
fromCTypeAgda.TypeChecking.Rules.Data
fromDistinctAscListAgda.Utils.SmallSet
fromEdgesAgda.Utils.Graph.AdjacencyMap.Unidirectional
fromEdgesWithAgda.Utils.Graph.AdjacencyMap.Unidirectional
fromIndexListAgda.Termination.SparseMatrix
fromJust 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
fromLeftAgda.Utils.Either
fromLeftMAgda.Utils.Either
fromList 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.BiMap
3 (Function)Agda.Utils.Bag
4 (Function)Agda.Utils.SmallSet
5 (Function)Agda.Utils.Favorites
6 (Function)Agda.Termination.CallGraph
fromListsAgda.Termination.SparseMatrix
fromLiteralAgda.TypeChecking.Primitive
fromLTypeAgda.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
fromMaybeMPAgda.Utils.Monad
fromMillisecondsAgda.Utils.Time
frommyClauseAgda.Auto.Convert
frommyExpsAgda.Auto.Convert
fromNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
fromNodeSetAgda.Utils.Graph.AdjacencyMap.Unidirectional
fromOrderingAgda.Utils.PartialOrd
fromOrderingsAgda.Utils.PartialOrd
fromOrdinaryAgda.Syntax.Concrete
fromPatternSubstitutionAgda.TypeChecking.Substitute
fromReducedTermAgda.TypeChecking.Primitive
fromRightAgda.Utils.Either
fromRightMAgda.Utils.Either
fromSplitPatternsAgda.TypeChecking.Coverage.Match
fromSubscriptDigitAgda.Utils.Suffix
FromTermAgda.TypeChecking.Primitive
fromTermAgda.TypeChecking.Primitive
FromTermFunctionAgda.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
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.TypeChecking.Monad, Agda.Compiler.Backend
FunArityAgda.Syntax.Internal.Pattern
funArityAgda.Syntax.Internal.Pattern
FunBindAgda.Utils.Haskell.Syntax
FunClauseAgda.Syntax.Concrete
FunClausesAgda.Auto.Auto
funClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funCompiledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funCoveringAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Function 
1 (Data Constructor)Agda.Interaction.Highlighting.Precise
2 (Type/Class)Agda.Utils.TypeLevel
3 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
4 (Data Constructor)Agda.Interaction.Response
FunctionCtxAgda.Syntax.Fixity
FunctionFlagAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunctionInverseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
functionInverseAgda.TypeChecking.Injectivity
FunctionInverse'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunctionReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunctionSpaceDomainCtxAgda.Syntax.Fixity
FunctionTypeInSizeUnivAgda.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
funDelayedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funExtLamAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funFlagAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funFlagsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunInlineAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funInlineAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funInvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunMacroAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funMacroAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funMutualAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunNameAgda.Syntax.Scope.Base
funProjectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunSig 
1 (Data Constructor)Agda.Syntax.Abstract
2 (Data Constructor)Agda.Syntax.Concrete.Definitions
FunSortAgda.Syntax.Internal
funSortAgda.TypeChecking.Substitute
funSort'Agda.TypeChecking.Substitute
funSplitTreeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
FunStaticAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funStaticAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funTerminatesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funTreelessAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
funWithAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
fuseIntervalsAgda.Syntax.Position
fuseRangeAgda.Syntax.Position
fuseRangesAgda.Syntax.Position
FVsAgda.TypeChecking.MetaVars
fwords 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty