Fail | Agda.TypeChecking.CompiledClause |
fail | Agda.Utils.Monad |
Failed | Agda.Auto.NarrowingSearch |
failOnException | Agda.Interaction.Exceptions |
Failure | Agda.Utils.QuickCheck |
fakeD | Agda.Compiler.MAlonzo.Misc |
fakeDQ | Agda.Compiler.MAlonzo.Misc |
fakeDS | Agda.Compiler.MAlonzo.Misc |
fakeExp | Agda.Compiler.MAlonzo.Misc |
fakeType | Agda.Compiler.MAlonzo.Misc |
fastDistinct | Agda.Utils.List |
Favorites | |
1 (Type/Class) | Agda.Utils.Favorites |
2 (Data Constructor) | Agda.Utils.Favorites |
fcat | Agda.Utils.Pretty |
fcIgnoreSorts | Agda.TypeChecking.Free |
fCtx | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Field | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Type/Class) | Agda.Syntax.Abstract |
3 (Data Constructor) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
field | Agda.Compiler.JS.Parser |
FieldName | Agda.Syntax.Scope.Monad |
FieldOutsideRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Fields | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
File | Agda.Interaction.Highlighting.Precise |
FileNotFound | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
filePath | Agda.Utils.FileName |
filter | Agda.Utils.HashMap |
filterEdges | |
1 (Function) | Agda.Utils.Graph.AdjacencyMap |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
filterKeys | Agda.Utils.Map |
filterM | Agda.Utils.Monad |
filterMaybe | |
1 (Function) | Agda.Utils.Maybe.Strict |
2 (Function) | Agda.Utils.Maybe |
filterScope | Agda.Syntax.Scope.Base |
filterWithKey | Agda.Utils.HashMap |
finally | Agda.Utils.Monad |
findClause | Agda.Interaction.MakeCase |
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 |
findInjection | Agda.Compiler.Epic.Injection |
FindInScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
findInScope | Agda.TypeChecking.InstanceArguments |
findInScope' | Agda.TypeChecking.InstanceArguments |
FindInScopeOF | Agda.Interaction.BasicOps |
findInterfaceFile | Agda.Interaction.FindFile |
findMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
findPath | |
1 (Function) | Agda.Utils.Graph.AdjacencyMap |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
findperm | Agda.Auto.CaseSplit |
findPosition | Agda.Compiler.Epic.Forcing |
findPossibleRecords | Agda.TypeChecking.Records |
findRigidBelow | Agda.TypeChecking.SizedTypes.WarshallSolver |
Finite | Agda.Utils.Warshall |
fInt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
fInteraction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
firstPart | Agda.TypeChecking.Telescope |
fitsIn | Agda.TypeChecking.Rules.Data |
fix | Agda.Compiler.JS.Substitution |
Fixed | |
1 (Data Constructor) | Agda.Utils.QuickCheck |
2 (Type/Class) | Agda.Utils.QuickCheck |
Fixity | Agda.Syntax.Fixity |
Fixity' | |
1 (Type/Class) | Agda.Syntax.Fixity |
2 (Data Constructor) | Agda.Syntax.Fixity |
fixityLevel | Agda.Syntax.Fixity |
fixSize | Agda.TypeChecking.Test.Generators |
fixSizeConf | Agda.TypeChecking.Test.Generators |
fixTarget | Agda.TypeChecking.Coverage |
Flag | Agda.Interaction.Options |
flattenScope | Agda.Syntax.Scope.Base |
flattenSubstitution | Agda.TypeChecking.Rules.LHS.Unify |
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 |
flexHiding | Agda.TypeChecking.Rules.LHS.Problem |
Flexible | Agda.TypeChecking.Free |
flexiblePatterns | Agda.TypeChecking.Rules.LHS |
FlexibleVar | |
1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem |
flexibleVarFromHiding | 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 |
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 |
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 |
float | Agda.Utils.Pretty |
fmap | Agda.Utils.Monad |
fmapTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
fMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
fmExp | Agda.Auto.Convert |
fmExps | Agda.Auto.Convert |
fmLevel | Agda.Auto.Convert |
FMode | Agda.Auto.Syntax |
fmType | Agda.Auto.Convert |
fMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
fName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Focus | |
1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem |
focusCon | Agda.TypeChecking.Rules.LHS.Problem |
focusConArgs | Agda.TypeChecking.Rules.LHS.Problem |
focusDatatype | Agda.TypeChecking.Rules.LHS.Problem |
focusHoleIx | Agda.TypeChecking.Rules.LHS.Problem |
focusImplicit | Agda.TypeChecking.Rules.LHS.Problem |
focusIndices | Agda.TypeChecking.Rules.LHS.Problem |
focusOutPat | Agda.TypeChecking.Rules.LHS.Problem |
focusParams | Agda.TypeChecking.Rules.LHS.Problem |
focusRange | Agda.TypeChecking.Rules.LHS.Problem |
focusType | Agda.TypeChecking.Rules.LHS.Problem |
foldExpr | Agda.Syntax.Concrete.Generic |
foldl' | Agda.Utils.HashMap |
foldlWithKey' | Agda.Utils.HashMap |
foldM | Agda.Utils.Monad |
foldMatch | Agda.TypeChecking.Patterns.Match |
foldM_ | Agda.Utils.Monad |
foldr | Agda.Utils.HashMap |
foldrWithKey | Agda.Utils.HashMap |
foldTerm | Agda.Syntax.Internal.Generic |
followedBy | Agda.Syntax.Parser.LexActions |
for | Agda.Utils.Functor |
forAll | Agda.Utils.QuickCheck |
forAllProperties | Agda.Utils.QuickCheck |
forAllShrink | Agda.Utils.QuickCheck |
force | Agda.TypeChecking.Forcing |
forceConstrs | Agda.Compiler.Epic.ForceConstrs |
Forced | |
1 (Data Constructor) | Agda.Syntax.Common |
2 (Type/Class) | Agda.Compiler.Epic.Interface |
3 (Data Constructor) | Agda.Compiler.Epic.Interface |
forced | Agda.Compiler.Epic.Interface |
ForcedArgs | Agda.Compiler.Epic.Interface |
forcedArgs | Agda.Compiler.Epic.Interface |
forcedExpr | Agda.Compiler.Epic.Forcing |
forcedVariables | Agda.TypeChecking.Forcing |
forceEqualTerms | Agda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad |
forceFun | Agda.Compiler.Epic.ForceConstrs |
forceHom | Agda.TypeChecking.Rules.LHS.Unify |
forever | Agda.Utils.Monad |
forkTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
forM' | Agda.Utils.Monad |
forMaybe | |
1 (Function) | Agda.Utils.Maybe.Strict |
2 (Function) | Agda.Utils.Maybe |
forM_ | Agda.Utils.Monad |
fProblem | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Frame | Agda.TypeChecking.CompiledClause.Match |
Free | Agda.TypeChecking.Free |
FreeConf | |
1 (Type/Class) | Agda.TypeChecking.Free |
2 (Data Constructor) | Agda.TypeChecking.Free |
freeIn | |
1 (Function) | Agda.TypeChecking.Free |
2 (Function) | Agda.Auto.Convert |
freeInIgnoringSortAnn | Agda.TypeChecking.Free |
freeInIgnoringSorts | Agda.TypeChecking.Free |
FreeVars | Agda.TypeChecking.Free |
freeVars | Agda.TypeChecking.Free |
freevars | Agda.Auto.CaseSplit |
freeVars' | Agda.TypeChecking.Free |
freeVarsToApply | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
freezeMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
Freqs | Agda.TypeChecking.Test.Generators |
Frequencies | Agda.TypeChecking.Test.Generators |
frequency | Agda.Utils.QuickCheck |
Fresh | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
fresh | Agda.Utils.Fresh |
freshAbstractName | Agda.Syntax.Scope.Monad |
freshAbstractName_ | Agda.Syntax.Scope.Monad |
freshAbstractQName | Agda.Syntax.Scope.Monad |
freshName | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
freshName_ | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
freshNoName | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
freshNoName_ | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
freshTCM | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
FreshThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
from | Agda.Interaction.Highlighting.Range |
fromAgda | Agda.Compiler.Epic.FromAgda |
fromCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
fromHom | Agda.TypeChecking.Rules.LHS.Unify |
fromIndexList | Agda.Termination.SparseMatrix |
fromJust | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
fromList | |
1 (Function) | Agda.Utils.VarSet |
2 (Function) | Agda.Utils.HashMap |
3 (Function) | Agda.Utils.BiMap |
4 (Function) | Agda.Utils.Graph.AdjacencyMap |
5 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
6 (Function) | Agda.Utils.Favorites |
7 (Function) | Agda.Termination.CallGraph |
fromLists | Agda.Termination.SparseMatrix |
fromListWith | |
1 (Function) | Agda.Utils.HashMap |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
fromLiteral | Agda.TypeChecking.Primitive |
fromMaybe | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
fromMaybeM | |
1 (Function) | Agda.Utils.Maybe.Strict |
2 (Function) | Agda.Utils.Maybe |
frommy | Agda.Auto.Convert |
frommyClause | Agda.Auto.Convert |
frommyExp | Agda.Auto.Convert |
frommyExps | Agda.Auto.Convert |
frommyType | Agda.Auto.Convert |
fromNodes | |
1 (Function) | Agda.Utils.Graph.AdjacencyMap |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
fromOrdering | Agda.Utils.PartialOrd |
fromOrderings | Agda.Utils.PartialOrd |
fromOrdinary | Agda.Syntax.Concrete |
fromReducedTerm | Agda.TypeChecking.Primitive |
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 |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
fsep | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
fst3 | Agda.Utils.Tuple |
Full | Agda.Interaction.Highlighting.Generate |
fullParen | Agda.Syntax.Concrete.Operators |
fullRender | Agda.Utils.Pretty |
Fun | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
3 (Type/Class) | Agda.Compiler.Epic.AuxAST |
4 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
5 (Type/Class) | Agda.TypeChecking.Primitive |
funAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
funArgs | Agda.Compiler.Epic.AuxAST |
FunArity | Agda.Syntax.Internal.Pattern |
funArity | Agda.Syntax.Internal.Pattern |
FunClause | Agda.Syntax.Concrete |
funClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
funComment | Agda.Compiler.Epic.AuxAST |
funCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
funCopy | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Function | |
1 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
3 (Data Constructor) | Agda.Interaction.Response |
function | Agda.Compiler.JS.Parser |
FunctionCtx | Agda.Syntax.Fixity |
FunctionDef | Agda.Interaction.MakeCase |
FunctionInverse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
functionInverse | Agda.TypeChecking.Injectivity |
FunctionInverse' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
FunctionReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
FunctionSpaceDomainCtx | Agda.Syntax.Fixity |
Functor | Agda.Utils.Monad |
FunDef | |
1 (Data Constructor) | Agda.Syntax.Abstract |
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
funDelayed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
funEpicCode | Agda.Compiler.Epic.AuxAST |
funExpr | Agda.Compiler.Epic.AuxAST |
funExtLam | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
funFreq | Agda.TypeChecking.Test.Generators |
funInline | Agda.Compiler.Epic.AuxAST |
funInv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
funMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
funName | Agda.Compiler.Epic.AuxAST |
funProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
funQName | Agda.Compiler.Epic.AuxAST |
funs | Agda.Compiler.Epic.Erasure |
FunSh | Agda.TypeChecking.Rules.LHS.Unify |
FunSig | |
1 (Data Constructor) | Agda.Syntax.Abstract |
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
funStatic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
funTerminates | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
funWith | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
fuseRange | Agda.Syntax.Position |
fuseRanges | Agda.Syntax.Position |
FV | Agda.TypeChecking.Free |
fv | Agda.Compiler.Epic.AuxAST |
FVs | Agda.TypeChecking.MetaVars |
fwords | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |