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

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- $
- %
- +
- .
- /
- <
- =
- >
- ^
- -
- _
- All

Index - F

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.HashMap
3 (Function) | Agda.Utils.BiMap
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