Agda-2.6.2.2: 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.Compiler.Backend, Agda.TypeChecking.Monad
Fail |
1 (Type/Class) | Agda.Utils.Fail
2 (Data Constructor) | Agda.Utils.Fail
3 (Data Constructor) | Agda.TypeChecking.CompiledClause
Failed | Agda.Auto.NarrowingSearch
failOnRecordFieldWarnings | Agda.TypeChecking.Records
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, Agda.TypeChecking.Primitive.Cubical
famThing | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
farEmpty | Agda.TypeChecking.Serialise.Base
farFresh | 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
feExtra | Agda.TypeChecking.Free.Lazy
feFlexRig | Agda.TypeChecking.Free.Lazy
feIgnoreSorts | Agda.TypeChecking.Free.Lazy
feModality | Agda.TypeChecking.Free.Lazy
feSingleton | Agda.TypeChecking.Free.Lazy
fibrantLub | Agda.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
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
FieldBlock | Agda.Syntax.Concrete.Definitions.Types
fieldLabelModifier | Agda.Interaction.JSON
FieldName | Agda.Syntax.Scope.Base
FieldOutsideRecord | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
FieldSig | Agda.Syntax.Concrete
FileNotFound | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
filePath | Agda.Utils.FileName
filePos | Agda.Interaction.Library.Base, Agda.Interaction.Library
FileType | Agda.Syntax.Common
filter |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.Utils.Trie
filterAndRest | Agda.Utils.List
filterCallStack | Agda.Utils.CallStack
filterEdges | Agda.Utils.Graph.AdjacencyMap.Unidirectional
filterKeys | Agda.Utils.Map
filterMaybe |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
filterNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
filterNodesKeepingEdges | Agda.Utils.Graph.AdjacencyMap.Unidirectional
filterScope | Agda.Syntax.Scope.Base
filterTCWarnings | Agda.TypeChecking.Pretty.Warning
filterUsed | Agda.Syntax.Treeless, Agda.Compiler.Backend
filterVarMap | Agda.TypeChecking.Free
filterVarMapToList | Agda.TypeChecking.Free
FinalChecks | Agda.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
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.Compiler.Backend, Agda.TypeChecking.Monad
findInstance | Agda.TypeChecking.InstanceArguments
FindInstanceOF | Agda.Interaction.Base
findInteractionPoint_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
findInterfaceFile | Agda.Interaction.FindFile
findInterfaceFile' | Agda.Interaction.FindFile
findLib' | Agda.Interaction.Library
findMentions | Agda.Interaction.SearchAbout
findOverlap | Agda.Utils.List
findperm | Agda.Auto.CaseSplit
findPossibleRecords | Agda.TypeChecking.Records
findProjectRoot | Agda.Interaction.Library
findRigidBelow | Agda.TypeChecking.SizedTypes.WarshallSolver
findWithIndex | Agda.Utils.List
Finite | Agda.Utils.Warshall
firstHole | Agda.Utils.Zipper
firstMeta | Agda.Syntax.Internal.MetaVars
firstNonTakenName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
firstPart | Agda.TypeChecking.Telescope
fitsIn | Agda.TypeChecking.Rules.Data
fittingNamedArg | Agda.Syntax.Common
fix | Agda.Compiler.JS.Substitution
Fixities | Agda.Syntax.Concrete.Fixity
fixitiesAndPolarities | Agda.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
fixityAssoc | Agda.Syntax.Common
FixityInRenamingModule | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FixityInRenamingModule_ | Agda.Interaction.Options.Warnings
FixityLevel | Agda.Syntax.Common
fixityLevel | Agda.Syntax.Common
fixityRange | Agda.Syntax.Common
Flag | Agda.Interaction.Options, Agda.Compiler.Backend
flagGhcBin | Agda.Compiler.MAlonzo.Compiler
flagGhcCallGhc | Agda.Compiler.MAlonzo.Compiler
flagGhcCompile | Agda.Compiler.MAlonzo.Compiler
flagGhcFlags | Agda.Compiler.MAlonzo.Compiler
flagGhcStrict | Agda.Compiler.MAlonzo.Compiler
flagGhcStrictData | Agda.Compiler.MAlonzo.Compiler
Flat | Agda.Syntax.Common
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
flex | Agda.TypeChecking.SizedTypes.Syntax
flexArgInfo | Agda.TypeChecking.Rules.LHS.Problem
FlexChoice | Agda.TypeChecking.Rules.LHS.Problem
flexForced | Agda.TypeChecking.Rules.LHS.Problem
Flexible | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
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 | Agda.TypeChecking.Free
flexibly | Agda.TypeChecking.MetaVars.Occurs
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
FlexOf | Agda.TypeChecking.SizedTypes.Syntax
flexPos | Agda.TypeChecking.Rules.LHS.Problem
FlexRig | Agda.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
flexRigOccurrenceIn | Agda.TypeChecking.Free
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.Compiler.Backend, Agda.TypeChecking.Monad
flipP | Agda.Utils.Permutation
float | Agda.Utils.Pretty
fmapReduce | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
fmapTCMT | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
fmExp | Agda.Auto.Convert
fmExps | Agda.Auto.Convert
fmLevel | Agda.Auto.Convert
fmType | Agda.Auto.Convert
focus | Agda.Utils.Lens
foldA | Agda.Utils.Applicative
foldable | Agda.Interaction.JSON
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
FoldExprFn | Agda.Syntax.Abstract.Views
FoldExprRecFn | Agda.Syntax.Abstract.Views
foldListT | Agda.Utils.ListT
foldMapA | Agda.Utils.Applicative
foldMatch | Agda.TypeChecking.Patterns.Match
foldPattern | Agda.Syntax.Internal.Pattern
Foldr | Agda.Utils.TypeLevel
Foldr' | Agda.Utils.TypeLevel
foldrAPattern | Agda.Syntax.Abstract.Pattern
foldrCPattern | Agda.Syntax.Concrete.Pattern
foldrMetaSet | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
foldrPattern | Agda.Syntax.Internal.Pattern
foldTerm | Agda.Syntax.Internal.Generic
followedBy | Agda.Syntax.Parser.LexActions
for | Agda.Utils.Functor
forA | Agda.Utils.Applicative
forallFaceMaps | Agda.TypeChecking.Conversion
forallQ | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
Forced | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ForcedConstructorNotInstantiated | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
forceEtaExpandRecord | Agda.TypeChecking.Records
ForceNotFree | Agda.TypeChecking.Free.Reduce
forceNotFree | Agda.TypeChecking.Free.Reduce
forcePiUsingInjectivity | Agda.TypeChecking.Injectivity
forceSort | Agda.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
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
forgetLoneSigs | Agda.Syntax.Concrete.Definitions.Monad
forkTCM | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
forM' | Agda.Utils.Monad
formatDebugMessage | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
formatLibError | Agda.Interaction.Library.Base
formatLibPositionInfo | Agda.Interaction.Library.Base
forMaybe |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
forMaybeM | Agda.Utils.Monad
forMaybeMM | Agda.Utils.Monad
forMM | 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
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
freeInIgnoringSorts | Agda.TypeChecking.Free
FreeM | Agda.TypeChecking.Free.Lazy
FreeT | Agda.TypeChecking.Free.Lazy
FreeVariables | Agda.Syntax.Common
freeVariablesFromList | Agda.Syntax.Common
FreeVars | Agda.Auto.Syntax
freeVars |
1 (Function) | Agda.Auto.Syntax
2 (Function) | Agda.TypeChecking.Free
3 (Function) | Agda.Compiler.Treeless.Subst
freevars | Agda.Auto.CaseSplit
freeVars' | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
freeVarsIgnore | Agda.TypeChecking.Free
freeVarsOffset | Agda.Auto.Syntax
freeVarsToApply | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
freezeMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
fresh | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
freshConcreteName | Agda.Syntax.Scope.Monad
freshInt | Agda.TypeChecking.Conversion.Pure
freshInteractionId | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
freshLens | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FreshName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
freshName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
freshNameId | Agda.TypeChecking.Conversion.Pure
FreshNameMode | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
freshNames | Agda.Compiler.MAlonzo.Compiler
freshName_ | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
freshNoName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
freshNoName_ | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
freshProblemId | Agda.TypeChecking.Conversion.Pure
freshRecordName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
freshTCM | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FreshThings |
1 (Type/Class) | Agda.TypeChecking.Conversion.Pure
2 (Data Constructor) | Agda.TypeChecking.Conversion.Pure
from | Agda.Interaction.Highlighting.Range
fromAbsName | Agda.TypeChecking.Serialise.Instances.Abstract
FromArgs | Agda.Interaction.JSON
fromAscList | Agda.Utils.SmallSet
fromCallSiteList | Agda.Utils.CallStack
fromCmp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
fromConPatternInfo | Agda.Syntax.Internal
fromCType | Agda.TypeChecking.Rules.Data
fromDistinctAscendingLists | Agda.Utils.BiMap
fromDistinctAscendingListsPrecondition | Agda.Utils.BiMap
fromDistinctAscList | Agda.Utils.SmallSet
fromDotNetTime | Agda.Interaction.JSON
fromEdges | Agda.Utils.Graph.AdjacencyMap.Unidirectional
fromEdgesWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional
fromEncoding | Agda.Interaction.JSON
fromImportedName | Agda.Syntax.Common
fromIndexList | Agda.Termination.SparseMatrix
FromJSON | Agda.Interaction.JSON
fromJSON | Agda.Interaction.JSON
FromJSON1 | Agda.Interaction.JSON
FromJSON2 | Agda.Interaction.JSON
FromJSONKey | Agda.Interaction.JSON
fromJSONKey | Agda.Interaction.JSON
FromJSONKeyCoerce | Agda.Interaction.JSON
FromJSONKeyFunction | Agda.Interaction.JSON
fromJSONKeyList | Agda.Interaction.JSON
FromJSONKeyText | Agda.Interaction.JSON
FromJSONKeyTextParser | Agda.Interaction.JSON
FromJSONKeyValue | Agda.Interaction.JSON
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.List1
2 (Function) | Agda.Utils.VarSet
3 (Function) | Agda.Utils.Bag
4 (Function) | Agda.Utils.Singleton, Agda.Termination.CallGraph
5 (Function) | Agda.Utils.SmallSet
6 (Function) | Agda.Utils.BiMap
7 (Function) | Agda.Utils.Favorites
fromList1 | Agda.Utils.List2
fromList1Maybe | Agda.Utils.List2
fromListMaybe | Agda.Utils.List2
fromListPrecondition | Agda.Utils.BiMap
fromLists | Agda.Termination.SparseMatrix
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
fromNonOverlappingNonEmptyAscendingList | Agda.Utils.RangeMap
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
FrontEndEmacs | Agda.Main
FrontEndJson | Agda.Main
FrontEndRepl | Agda.Main
FrontendType | Agda.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
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.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
funCompiled | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funCovering | Agda.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
FunctionCtx | Agda.Syntax.Fixity
FunctionFlag | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunctionInverse | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
functionInverse | Agda.TypeChecking.Injectivity
FunctionInverse' | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunctionKind | Agda.Compiler.MAlonzo.Misc
FunctionReductions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunctionSpaceDomainCtx | Agda.Syntax.Fixity
FunctionTypeInSizeUniv | Agda.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
funDelayed | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funExtLam | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funFlag | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funFlags | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunInline | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funInline | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funInv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunK | Agda.Compiler.MAlonzo.Misc
FunMacro | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funMacro | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funMutual | Agda.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
funProjection | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunSig | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
FunSort | Agda.Syntax.Internal
funSort | Agda.TypeChecking.Substitute
funSort' | Agda.TypeChecking.Substitute
funSplitTree | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
FunStatic | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funStatic | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funTerminates | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funTreeless | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
funWith | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
fuseIntervals | Agda.Syntax.Position
fuseRange | Agda.Syntax.Position
fuseRanges | Agda.Syntax.Position
FVs | Agda.TypeChecking.MetaVars
fwords |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty