Face | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
faceEqns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
faceRHS | Agda.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 |
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 |
false | Agda.Utils.Boolean |
FamilyOrNot | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
familyOrNot | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
famThing | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
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.Syntax.Common.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 |
fiber | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
Field | |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
2 (Data Constructor) | Agda.Syntax.Concrete |
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.TypeChecking.Monad, Agda.Compiler.Backend |
FieldS | Agda.Syntax.Abstract |
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 |
FieldSig | Agda.Syntax.Concrete |
FileNotFound | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.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.Base |
findInteractionPoint_ | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
findInterfaceFile | Agda.Interaction.FindFile |
findInterfaceFile' | Agda.Interaction.FindFile |
findLib' | Agda.Interaction.Library |
findMentions | Agda.Interaction.SearchAbout |
findNameInScope | Agda.Syntax.Scope.Base |
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.TypeChecking.Monad, Agda.Compiler.Backend |
FixityInRenamingModule_ | Agda.Interaction.Options.Warnings |
FixityLevel | Agda.Syntax.Common |
fixityLevel | Agda.Syntax.Common |
fixityRange | Agda.Syntax.Common |
Flag | Agda.Interaction.Options, Agda.Compiler.Backend |
Flat | Agda.Syntax.Common |
flatName | Agda.Compiler.JS.Compiler |
FlatScope | Agda.Syntax.Scope.Flat |
flatten | Agda.TypeChecking.Positivity |
flattenScope | Agda.Syntax.Scope.Flat |
flattenTel | Agda.TypeChecking.Telescope |
FldName | Agda.Syntax.Scope.Base |
Flex | |
1 (Data Constructor) | Agda.Utils.Warshall |
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
3 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
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 (Type/Class) | Agda.Utils.Warshall |
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
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 |
flexVars | Agda.TypeChecking.Rules.LHS.Unify.Types |
flipCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
flipP | Agda.Utils.Permutation |
float | Agda.Syntax.Common.Pretty |
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 |
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.List1 |
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.TypeChecking.Monad, Agda.Compiler.Backend |
ForcedConstructorNotInstantiated | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ForeignCodeStack | |
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 |
forgetLoneSigs | Agda.Syntax.Concrete.Definitions.Monad |
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 |
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 (Type/Class) | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
2 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
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.TypeChecking.Monad.Signature, 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 |
freshConcreteName | Agda.Syntax.Scope.Monad |
freshInt | Agda.TypeChecking.Conversion.Pure |
freshInteractionId | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
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 |
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 |
freshProblemId | Agda.TypeChecking.Conversion.Pure |
freshRecordName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
freshTCM | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 | |
1 (Function) | Agda.Utils.BoolSet |
2 (Function) | Agda.Utils.SmallSet |
fromBlocked | Agda.TypeChecking.Reduce |
fromBool | Agda.Utils.Boolean |
fromBool1 | Agda.Utils.Boolean |
fromBool2 | Agda.Utils.Boolean |
fromCallSiteList | Agda.Utils.CallStack |
fromCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
fromConPatternInfo | Agda.Syntax.Internal |
fromCType | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
fromDistinctAscendingLists | Agda.Utils.BiMap |
fromDistinctAscendingListsPrecondition | Agda.Utils.BiMap |
fromDistinctAscList | |
1 (Function) | Agda.Utils.BoolSet |
2 (Function) | 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.BoolSet |
4 (Function) | Agda.Utils.Bag |
5 (Function) | Agda.Utils.SmallSet |
6 (Function) | Agda.Utils.Singleton, Agda.Termination.CallGraph |
7 (Function) | Agda.Utils.BiMap |
8 (Function) | Agda.Utils.Favorites |
fromList1 | Agda.Utils.List2 |
fromList1Either | Agda.Utils.List2 |
fromList1Maybe | Agda.Utils.List2 |
fromListMaybe | Agda.Utils.List2 |
fromListN | Agda.Utils.List1 |
fromListPrecondition | Agda.Utils.BiMap |
fromLists | Agda.Termination.SparseMatrix |
fromListSafe | Agda.Utils.List1 |
fromLiteral | Agda.TypeChecking.Primitive |
fromLType | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
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 |
fromReduceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
fromReducedTerm | Agda.TypeChecking.Primitive |
fromRight | Agda.Utils.Either |
fromRightM | Agda.Utils.Either |
fromSplitPattern | Agda.TypeChecking.Coverage.Match |
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.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
fsep | |
1 (Function) | Agda.Syntax.Common.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.Syntax.Common.Pretty |
fullRenderAnn | Agda.Syntax.Common.Pretty |
fullyApplyCon | Agda.TypeChecking.Datatypes |
fullyApplyCon' | Agda.TypeChecking.Datatypes |
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 |
funCovering | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Function | |
1 (Type/Class) | Agda.Utils.TypeLevel |
2 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
4 (Data Constructor) | Agda.Interaction.Response |
FunctionCtx | Agda.Syntax.Fixity |
FunctionData | |
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 |
FunctionDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
FunctionKind | Agda.Compiler.MAlonzo.Misc |
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.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions |
3 (Data Constructor) | Agda.Syntax.Abstract |
FunDefS | Agda.Syntax.Abstract |
funErasure | 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 |
funIsKanOp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
FunK | Agda.Compiler.MAlonzo.Misc |
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 |
FunName | |
1 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types |
2 (Data Constructor) | Agda.Syntax.Scope.Base |
funOpaque | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
funProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.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 |
funUniv | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
funWith | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
fuseIntervals | Agda.Syntax.Position |
fuseRange | Agda.Syntax.Position |
fuseRanges | Agda.Syntax.Position |
FVs | Agda.TypeChecking.MetaVars |
fwords | |
1 (Function) | Agda.Syntax.Common.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |