S | |
1 (Type/Class) | Agda.TypeChecking.Serialise.Base |
2 (Type/Class) | Agda.Auto.Convert |
3 (Data Constructor) | Agda.Auto.Convert |
SafeFlagNonTerminating | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
SafeFlagNoPositivityCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
SafeFlagPostulate | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
SafeFlagPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
SafeFlagPrimTrustMe | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
SafeFlagTerminating | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
SafeMode | Agda.Interaction.Options.Lenses |
safePermute | Agda.Utils.Permutation |
Same | Agda.Compiler.Epic.Injection |
sameDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
sameVars | Agda.TypeChecking.Conversion |
sample | Agda.Utils.QuickCheck |
sample' | Agda.Utils.QuickCheck |
sat | Agda.Utils.Parser.MemoisedCPS |
sat' | Agda.Syntax.Concrete.Operators.Parser |
satisfy | Agda.Utils.Parser.ReadP |
scale | Agda.Utils.QuickCheck |
sccDAG | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
sccDAG' | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
sccomcount | Agda.Auto.NarrowingSearch |
sccs | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
sccs' | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
scflip | Agda.Auto.NarrowingSearch |
sChecked | Agda.Interaction.Response |
SClause | Agda.TypeChecking.Coverage |
sConsts | Agda.Auto.Convert |
Scope | |
1 (Type/Class) | Agda.Utils.Warshall |
2 (Type/Class) | Agda.Syntax.Scope.Base |
3 (Data Constructor) | Agda.Syntax.Scope.Base |
ScopeCheckDeclaration | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ScopeCheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
scopeCheckImport | Agda.Interaction.Imports |
ScopeCheckLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
scopeCurrent | Agda.Syntax.Scope.Base |
scopeDatatypeModule | Agda.Syntax.Scope.Base |
ScopedDecl | Agda.Syntax.Abstract |
ScopedExpr | Agda.Syntax.Abstract |
scopeImports | Agda.Syntax.Scope.Base |
ScopeInfo | |
1 (Type/Class) | Agda.Syntax.Scope.Base |
2 (Data Constructor) | Agda.Syntax.Scope.Base |
scopeInScope | Agda.Syntax.Scope.Base |
scopeInverseModule | Agda.Syntax.Scope.Base |
scopeInverseName | Agda.Syntax.Scope.Base |
scopeLocals | Agda.Syntax.Scope.Base |
scopeLookup | Agda.Syntax.Scope.Base |
scopeLookup' | Agda.Syntax.Scope.Base |
ScopeM | Agda.Syntax.Scope.Monad |
scopeModules | Agda.Syntax.Scope.Base |
scopeName | Agda.Syntax.Scope.Base |
scopeNameSpace | Agda.Syntax.Scope.Base |
ScopeNameSpaces | Agda.Syntax.Scope.Base |
scopeNameSpaces | Agda.Syntax.Scope.Base |
scopeParents | Agda.Syntax.Scope.Base |
scopePrecedence | Agda.Syntax.Scope.Base |
Scoping | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
scPats | Agda.TypeChecking.Coverage |
scsub1 | Agda.Auto.NarrowingSearch |
scsub2 | Agda.Auto.NarrowingSearch |
scSubst | Agda.TypeChecking.Coverage |
scTarget | Agda.TypeChecking.Coverage |
scTel | Agda.TypeChecking.Coverage |
sCurMeta | Agda.Auto.Convert |
searchAbout | Agda.Interaction.InteractionTop |
secondPart | Agda.TypeChecking.Telescope |
secTelescope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Section | |
1 (Data Constructor) | Agda.Syntax.Abstract |
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
SectionApp | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
Sections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
sectIsSection | Agda.Syntax.Fixity |
sectKind | Agda.Syntax.Fixity |
sectLevel | Agda.Syntax.Fixity |
sectNotation | Agda.Syntax.Fixity |
selectC | Agda.Interaction.Highlighting.Precise |
Self | Agda.Compiler.JS.Syntax |
self | Agda.Compiler.JS.Substitution |
semi | Agda.Utils.Pretty |
SemiRing | |
1 (Type/Class) | Agda.Utils.SemiRing |
2 (Type/Class) | Agda.Termination.Semiring |
Semiring | |
1 (Type/Class) | Agda.Termination.Semiring |
2 (Data Constructor) | Agda.Termination.Semiring |
semiringInvariant | Agda.Termination.Semiring |
sep | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
sepBy | Agda.Utils.Parser.ReadP |
sepBy1 | Agda.Utils.Parser.ReadP |
SeqArg | |
1 (Type/Class) | Agda.Compiler.Treeless.Subst |
2 (Data Constructor) | Agda.Compiler.Treeless.Subst |
seqc | Agda.Auto.NarrowingSearch |
seqctx | Agda.Auto.CaseSplit |
seqPO | Agda.Utils.PartialOrd |
sEqs | Agda.Auto.Convert |
Serialization | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
Serialize | Agda.Compiler.UHC.Bridge |
serialize | Agda.Compiler.UHC.Bridge |
Set | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
3 (Data Constructor) | Agda.Auto.Syntax |
set | Agda.Utils.Lens |
setAbsoluteIncludePaths | Agda.Interaction.Options.Lenses |
setArgInfo | Agda.Syntax.Common |
setArgOccurrences | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
setBenchmarking | Agda.Utils.Benchmark |
setBuiltinThings | Agda.TypeChecking.Monad.Builtin |
setCommandLineOptions | |
1 (Function) | Agda.Interaction.Options.Lenses |
2 (Function) | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
setCommandLineOptions' | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
setCommandLineOpts | Agda.Interaction.InteractionTop |
setCompiledArgUse | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
setConName | Agda.Syntax.Internal |
setContextPrecedence | Agda.Syntax.Scope.Monad |
setCurrentModule | Agda.Syntax.Scope.Monad |
setCurrentRange | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad |
setDecodedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
setEtaEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
setFoldl | Agda.TypeChecking.SizedTypes.WarshallSolver |
setFreqs | Agda.TypeChecking.Test.Generators |
setHiding | Agda.Syntax.Common |
setImportedName | Agda.Syntax.Common |
setImportedSignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
setIncludeDirs | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
setIncludePaths | Agda.Interaction.Options.Lenses |
setInput | Agda.Syntax.Parser.LookAhead |
setInputFile | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
setInteractionOutputCallback | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
setInterface | Agda.Compiler.Common |
setLastPos | Agda.Syntax.Parser.Monad |
setLexInput | Agda.Syntax.Parser.Alex |
setLibraryIncludes | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
setLibraryPaths | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
setLocalVars | Agda.Syntax.Scope.Monad |
setMetaNameSuggestion | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
setMutual | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
setMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
SetN | Agda.Syntax.Concrete |
setNamedScope | Agda.Syntax.Scope.Monad |
setNameSpace | Agda.Syntax.Scope.Base |
SetOmegaNotValidType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
setOptionsFromPragma | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
setParsePos | Agda.Syntax.Parser.Monad |
setPatternSyns | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
setPersistentVerbosity | Agda.Interaction.Options.Lenses |
setPolarity | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
setPragmaOptions | |
1 (Function) | Agda.Interaction.Options.Lenses |
2 (Function) | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
setPrevToken | Agda.Syntax.Parser.Monad |
setPtr | Agda.Utils.Pointer, Agda.Syntax.Internal |
SetRange | |
1 (Type/Class) | Agda.Syntax.Position |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
setRange | Agda.Syntax.Position |
setRelevance | Agda.Syntax.Common |
SetS | Agda.Syntax.Reflected |
setSafeMode | Agda.Interaction.Options.Lenses |
setScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
setScopeAccess | Agda.Syntax.Scope.Base |
setScopeLocals | Agda.Syntax.Scope.Base |
setSignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
setTag | |
1 (Function) | Agda.Compiler.UHC.Pragmas.Base, Agda.Compiler.UHC.Pragmas.Parse |
2 (Function) | Agda.Compiler.Epic.Injection |
setTerminates | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
SetToInfty | Agda.TypeChecking.SizedTypes.WarshallSolver |
setToInfty | Agda.TypeChecking.SizedTypes.WarshallSolver |
setTopLevelModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
setTreeless | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
setValueMetaName | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
setVerbosity | Agda.Interaction.Options.Lenses |
setVisitedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
several | Agda.Interaction.Highlighting.Precise |
severalC | Agda.Interaction.Highlighting.Precise |
sgListT | Agda.Utils.ListT |
sgMListT | Agda.Utils.ListT |
SgTel | Agda.Syntax.Internal |
sgTel | Agda.Syntax.Internal |
ShadowedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ShadowedVar | Agda.Syntax.Scope.Base |
shadowLocal | Agda.Syntax.Scope.Base |
Shared | Agda.Syntax.Internal |
shared | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
sharedFun | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
sharedType | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
shared_ | Agda.Syntax.Internal |
sharing | Agda.Utils.Update |
shift | Agda.Compiler.JS.Substitution |
shifter | Agda.Compiler.JS.Substitution |
shiftFrom | Agda.Compiler.JS.Substitution |
ShouldBeApplicationOf | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ShouldBeAppliedToTheDatatypeParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ShouldBeASort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ShouldBeEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ShouldBePi | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ShouldBeRecordPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ShouldBeRecordType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ShouldEndInApplicationOfTheDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
shouldEtaContractImplicit | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
shouldReifyInteractionPoints | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
showA | Agda.Syntax.Abstract.Pretty |
showATop | Agda.Syntax.Abstract.Pretty |
showChar' | Agda.Syntax.Literal |
showComparison | Agda.Interaction.BasicOps |
showConstraints | Agda.Interaction.CommandLine |
showContext | Agda.Interaction.CommandLine |
ShowHead | Agda.TypeChecking.Rules.Decl |
showHead | Agda.TypeChecking.Rules.Decl |
ShowImplicitArgs | Agda.Interaction.InteractionTop |
showImplicitArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
showIndex | Agda.Utils.String |
showIrrelevantArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
showMetas | Agda.Interaction.CommandLine |
showModuleContents | Agda.Interaction.InteractionTop |
showOpenMetas | Agda.Interaction.InteractionTop |
showPat' | Agda.TypeChecking.Pretty |
showQNameId | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
showScope | Agda.Interaction.CommandLine |
showString' | Agda.Syntax.Literal |
showThousandSep | Agda.Utils.String |
shrink | Agda.Utils.QuickCheck |
Shrink2 | |
1 (Data Constructor) | Agda.Utils.QuickCheck |
2 (Type/Class) | Agda.Utils.QuickCheck |
ShrinkC | Agda.TypeChecking.Test.Generators |
shrinkC | Agda.TypeChecking.Test.Generators |
Shrinking | |
1 (Data Constructor) | Agda.Utils.QuickCheck |
2 (Type/Class) | Agda.Utils.QuickCheck |
shrinking | Agda.Utils.QuickCheck |
shrinkInit | Agda.Utils.QuickCheck |
shrinkIntegral | Agda.Utils.QuickCheck |
shrinkList | Agda.Utils.QuickCheck |
shrinkNothing | Agda.Utils.QuickCheck |
shrinkRealFrac | Agda.Utils.QuickCheck |
shrinkRealFracToInteger | Agda.Utils.QuickCheck |
ShrinkState | Agda.Utils.QuickCheck |
shrinkState | Agda.Utils.QuickCheck |
shuffle | Agda.Utils.QuickCheck |
Sidecondition | Agda.Auto.NarrowingSearch |
Sig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
sigDefinitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
sigMName | Agda.Compiler.Common |
Signature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
sigRewriteRules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
sigSections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Simplification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Simplified | Agda.Interaction.BasicOps |
Simplify | Agda.TypeChecking.Reduce |
simplify | Agda.TypeChecking.Reduce |
simplify' | Agda.TypeChecking.Reduce |
simplify1 | Agda.TypeChecking.SizedTypes.Syntax |
simplifyBlocked' | Agda.TypeChecking.Reduce |
simplifyLevelConstraint | Agda.TypeChecking.LevelConstraints |
simplifyTTerm | Agda.Compiler.Treeless.Simplify |
simplifyWithHypotheses | Agda.TypeChecking.SizedTypes.WarshallSolver |
singleConstructorType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
Singleton | Agda.Utils.Singleton |
singleton | |
1 (Function) | Agda.Utils.VarSet |
2 (Function) | Agda.Utils.HashMap |
3 (Function) | Agda.Utils.Singleton |
4 (Function) | Agda.Utils.BiMap |
5 (Function) | Agda.Utils.Bag |
6 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
7 (Function) | Agda.Utils.Trie |
8 (Function) | Agda.Interaction.Highlighting.Precise |
singletonC | Agda.Interaction.Highlighting.Precise |
SingletonRecords | Agda.TypeChecking.MetaVars |
singletonS | Agda.TypeChecking.Substitute |
SingleVar | Agda.TypeChecking.Free.Lazy |
Size | |
1 (Type/Class) | Agda.Termination.SparseMatrix |
2 (Data Constructor) | Agda.Termination.SparseMatrix |
size | |
1 (Function) | Agda.Utils.HashMap |
2 (Function) | Agda.Utils.Bag |
3 (Function) | Agda.Utils.Size |
4 (Function) | Agda.Termination.SparseMatrix |
SizeConst | Agda.Utils.Warshall |
SizeConstraint | Agda.TypeChecking.SizedTypes.Solve |
sizeConstraint | Agda.TypeChecking.SizedTypes.Solve |
sizeContext | Agda.TypeChecking.SizedTypes.Solve |
Sized | Agda.Utils.Size |
sized | Agda.Utils.QuickCheck |
SizedList | |
1 (Type/Class) | Agda.TypeChecking.Test.Generators |
2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
sizedText | Agda.Utils.Pretty |
SizedThing | |
1 (Type/Class) | Agda.Utils.Size |
2 (Data Constructor) | Agda.Utils.Size |
sizedThing | Agda.Utils.Size |
SizeExpr | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Type/Class) | Agda.Utils.Warshall |
sizeExpr | Agda.TypeChecking.SizedTypes.Solve |
SizeExpr' | Agda.TypeChecking.SizedTypes.Syntax |
sizeHypIds | Agda.TypeChecking.SizedTypes.Solve |
sizeHypotheses | Agda.TypeChecking.SizedTypes.Solve |
SizeInf | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
sizeInvariant | Agda.Termination.SparseMatrix |
SizeLtSat | Agda.Interaction.BasicOps |
sizeMax | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
SizeMaxView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
sizeMaxView | Agda.TypeChecking.SizedTypes |
SizeMeta | |
1 (Data Constructor) | Agda.TypeChecking.SizedTypes |
2 (Type/Class) | Agda.TypeChecking.SizedTypes.Solve |
3 (Data Constructor) | Agda.TypeChecking.SizedTypes.Solve |
sizeMetaArgs | Agda.TypeChecking.SizedTypes.Solve |
sizeMetaId | Agda.TypeChecking.SizedTypes.Solve |
sizePolarity | Agda.TypeChecking.Polarity |
sizeRigid | Agda.Utils.Warshall |
sizeSort | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
SizeSuc | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
sizeSuc | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
sizeSucName | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
sizeSuc_ | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
sizeThing | Agda.Utils.Size |
sizeType | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
sizeType_ | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
SizeUniv | Agda.Syntax.Internal |
sizeUniv | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
SizeVar | Agda.Utils.Warshall |
SizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
sizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
SizeViewComparable | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
sizeViewComparable | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
sizeViewComparableWithMax | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
sizeViewOffset | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
sizeViewPred | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
sizeViewSuc_ | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
Skip | Agda.Auto.Syntax |
skipBlock | Agda.Syntax.Parser.Comments |
skipMany | Agda.Utils.Parser.ReadP |
skipMany1 | Agda.Utils.Parser.ReadP |
skipSpaces | Agda.Utils.Parser.ReadP |
SleepingConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
sLub | Agda.TypeChecking.Substitute |
sMainMeta | Agda.Auto.Convert |
Small | |
1 (Data Constructor) | Agda.Utils.QuickCheck |
2 (Type/Class) | Agda.Utils.QuickCheck |
3 (Data Constructor) | Agda.Syntax.Common |
smallest | Agda.TypeChecking.SizedTypes.WarshallSolver |
smallestPos | Agda.Interaction.Highlighting.Precise |
smallestPosC | Agda.Interaction.Highlighting.Precise |
smallParams | Agda.TypeChecking.Rules.Data |
Smart | |
1 (Data Constructor) | Agda.Utils.QuickCheck |
2 (Type/Class) | Agda.Utils.QuickCheck |
smash'em | Agda.Compiler.Epic.Smashing |
smashable | Agda.Compiler.Epic.Smashing |
smashTel | Agda.Syntax.Concrete.Pretty |
sMetas | Agda.Auto.Convert |
snd3 | Agda.Utils.Tuple |
Sol | Agda.Auto.CaseSplit |
Solution | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Type/Class) | Agda.Utils.Warshall |
solve | |
1 (Function) | Agda.Utils.Warshall |
2 (Function) | Agda.Compiler.Epic.Injection |
solveAwakeConstraints | Agda.TypeChecking.Constraints |
solveAwakeConstraints' | Agda.TypeChecking.Constraints |
solveCluster | Agda.TypeChecking.SizedTypes.Solve |
solveConstraint | Agda.TypeChecking.Constraints |
solveConstraint_ | Agda.TypeChecking.Constraints |
SolvedButOpenHoles | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
solveGraph | Agda.TypeChecking.SizedTypes.WarshallSolver |
solveGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver |
solveSizeConstraints | Agda.TypeChecking.SizedTypes.Solve |
solveSizeConstraints_ | Agda.TypeChecking.SizedTypes.Solve |
solvingProblem | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
solvingProblems | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
SomeWarnings | Agda.Interaction.Imports |
SomeWhere | Agda.Syntax.Concrete |
Sort | |
1 (Type/Class) | Agda.Syntax.Reflected |
2 (Data Constructor) | Agda.Syntax.Reflected |
3 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
4 (Type/Class) | Agda.Syntax.Internal |
5 (Data Constructor) | Agda.Syntax.Internal |
6 (Data Constructor) | Agda.Auto.Syntax |
7 (Type/Class) | Agda.Auto.Syntax |
sort | Agda.Syntax.Internal |
SortCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
sortDefs | Agda.Compiler.Common |
sorted | Agda.Utils.List |
sortFreq | Agda.TypeChecking.Test.Generators |
SortFreqs | |
1 (Type/Class) | Agda.TypeChecking.Test.Generators |
2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
sortFreqs | Agda.TypeChecking.Test.Generators |
SortHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
sortInteractionPoints | Agda.Interaction.InteractionTop |
sortOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
sortTm | Agda.TypeChecking.Substitute |
sortUniq | Agda.Utils.PartialOrd |
source | Agda.Utils.Graph.AdjacencyMap.Unidirectional, Agda.Termination.CallGraph |
sourceNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
SourceToModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
sourceToModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
space | Agda.Utils.Pretty |
spanAllowedBeforeModule | Agda.Syntax.Concrete |
spanJust | Agda.Utils.List |
Specified | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
spec_updateAt | Agda.Utils.List |
spec_updateHead | Agda.Utils.List |
spec_updateLast | Agda.Utils.List |
SpineClause | Agda.Syntax.Abstract |
SpineLHS | |
1 (Type/Class) | Agda.Syntax.Abstract |
2 (Data Constructor) | Agda.Syntax.Abstract |
spineToLhs | Agda.Syntax.Abstract |
spineToLhsCore | Agda.Syntax.Abstract |
splashScreen | Agda.Interaction.CommandLine |
spLhsDefName | Agda.Syntax.Abstract |
spLhsInfo | Agda.Syntax.Abstract |
spLhsPats | Agda.Syntax.Abstract |
spLhsWithPats | Agda.Syntax.Abstract |
Split | Agda.TypeChecking.Rules.LHS.Problem |
splitApplyElims | Agda.Syntax.Internal |
splitArg | Agda.TypeChecking.Coverage.SplitTree |
splitAsNames | Agda.TypeChecking.Rules.LHS.Problem |
SplitAt | Agda.TypeChecking.Coverage.SplitTree |
splitAtC | Agda.Interaction.Highlighting.Precise |
splitBindings | Agda.TypeChecking.Coverage.SplitTree |
splitC | Agda.TypeChecking.CompiledClause.Compile |
SplitClause | Agda.TypeChecking.Coverage |
splitClauses | Agda.TypeChecking.Coverage |
splitClauseWithAbsurd | Agda.TypeChecking.Coverage |
splitCommas | Agda.Interaction.Library.Parse |
SplitError | |
1 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
splitExactlyAt | Agda.Utils.List |
splitFocus | Agda.TypeChecking.Rules.LHS.Problem |
splitLast | Agda.TypeChecking.Coverage |
splitLPats | Agda.TypeChecking.Rules.LHS.Problem |
splitOn | Agda.TypeChecking.CompiledClause.Compile |
SplitOnIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
splitPerm | Agda.TypeChecking.Telescope |
SplitProblem | Agda.TypeChecking.Rules.LHS.Problem |
splitProblem | Agda.TypeChecking.Rules.LHS.Split |
splitProjection | Agda.TypeChecking.Rules.LHS.Problem |
SplitRest | Agda.TypeChecking.Rules.LHS.Problem |
splitRestType | Agda.TypeChecking.Rules.LHS.Problem |
splitResult | Agda.TypeChecking.Coverage |
splitRPats | Agda.TypeChecking.Rules.LHS.Problem |
splitS | Agda.TypeChecking.Substitute |
SplitTel | |
1 (Type/Class) | Agda.TypeChecking.Telescope |
2 (Data Constructor) | Agda.TypeChecking.Telescope |
splitTelescope | Agda.TypeChecking.Telescope |
splitTelescopeExact | Agda.TypeChecking.Telescope |
splitTelForWith | Agda.TypeChecking.With |
SplittingDone | Agda.TypeChecking.Coverage.SplitTree |
SplitTree | Agda.TypeChecking.Coverage.SplitTree |
SplitTree' | Agda.TypeChecking.Coverage.SplitTree |
SplitTreeLabel | |
1 (Type/Class) | Agda.TypeChecking.Coverage.SplitTree |
2 (Data Constructor) | Agda.TypeChecking.Coverage.SplitTree |
SplitTrees | Agda.TypeChecking.Coverage.SplitTree |
splitTrees | Agda.TypeChecking.Coverage.SplitTree |
SplitTrees' | Agda.TypeChecking.Coverage.SplitTree |
square | Agda.Termination.SparseMatrix |
src | Agda.TypeChecking.SizedTypes.WarshallSolver |
SrcFile | Agda.Syntax.Position |
srcFile | Agda.Syntax.Position |
srcNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
SRes | Agda.Auto.NarrowingSearch |
sShowImplicitArguments | Agda.Interaction.Response |
sSizeUniv | Agda.TypeChecking.Primitive |
sSuc | Agda.Syntax.Internal |
St | |
1 (Type/Class) | Agda.TypeChecking.Serialise.Base |
2 (Data Constructor) | Agda.TypeChecking.Serialise.Base |
stAccumStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Stack | Agda.TypeChecking.CompiledClause.Match |
standardOptions | Agda.Interaction.Options |
standardOptions_ | Agda.Interaction.Options |
StarSemiRing | Agda.Utils.SemiRing |
startPos | Agda.Syntax.Position |
StaticPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
Statistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stats | Agda.TypeChecking.Serialise.Base |
Status | |
1 (Type/Class) | Agda.Interaction.Response |
2 (Data Constructor) | Agda.Interaction.Response |
status | Agda.Interaction.InteractionTop |
stAwakeConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stBenchmark | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stBuiltinThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stdArgs | Agda.Utils.QuickCheck |
stDecodedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stDirty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stDisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stealConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
step | Agda.Compiler.Epic.Erasure |
stFreshCtxId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stFreshInt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stFreshInteractionId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stFreshMetaId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stFreshMutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stFreshNameId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stFreshProblemId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stHaskellCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stHaskellImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stHaskellImportsUHC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stImportedDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stImportsDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stInstanceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stInteractionOutputCallback | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stLoadedFileCache | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stLocalBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
storeDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
storeDisambiguatedName | Agda.Interaction.Highlighting.Generate |
stPatternSynImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPersistentOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPersistentState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostAwakeConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostDirty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostDisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostFreshCtxId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostFreshInt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostFreshMetaId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostFreshMutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostFreshNameId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostFreshProblemId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostImportedDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostImportsDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostInstanceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostLocalBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostScopeState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostSleepingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPostSyntaxInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPreFreshInteractionId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPreHaskellCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPreHaskellImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPreHaskellImportsUHC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPreImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPreImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPreImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPreModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPrePatternSynImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPrePatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPrePragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPreScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPreScopeState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPreTokens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stPreVisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Str | |
1 (Type/Class) | Agda.Utils.String |
2 (Data Constructor) | Agda.Utils.String |
Strengthen | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
strengthen | Agda.TypeChecking.Substitute |
strengthenS | Agda.TypeChecking.Substitute |
StrictPos | Agda.TypeChecking.Positivity.Occurrence |
String | |
1 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
2 (Data Constructor) | Agda.Compiler.JS.Syntax |
string | Agda.Utils.Parser.ReadP |
stringC | Agda.TypeChecking.Serialise.Base |
stringChr | Agda.Compiler.JS.Parser |
stringD | Agda.TypeChecking.Serialise.Base |
stringE | Agda.TypeChecking.Serialise.Base |
stringLit | Agda.Compiler.JS.Parser |
stringNameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
stringParts | Agda.Syntax.Notation |
stringStr | Agda.Compiler.JS.Parser |
stringToArgName | Agda.Syntax.Internal |
stringToMyId | Agda.Auto.Syntax |
stringToRawName | Agda.Syntax.Common |
stripComments | Agda.Interaction.Library.Parse |
stripDontCare | Agda.Syntax.Internal |
stripNoNames | Agda.Syntax.Scope.Monad |
stripUnusedArguments | Agda.Compiler.Treeless.Unused |
stripWithClausePatterns | Agda.TypeChecking.With |
strMsg | Agda.Utils.Except |
strongly | Agda.TypeChecking.MetaVars.Occurs |
StronglyRigid | |
1 (Data Constructor) | Agda.TypeChecking.Free.Lazy |
2 (Data Constructor) | Agda.TypeChecking.Free.Old |
3 (Data Constructor) | Agda.TypeChecking.Free |
4 (Data Constructor) | Agda.TypeChecking.MetaVars.Occurs |
stronglyRigidVars | |
1 (Function) | Agda.TypeChecking.Free.Old |
2 (Function) | Agda.TypeChecking.Free |
StrPart | Agda.TypeChecking.Unquote |
stScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stSleepingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stSyntaxInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
stTokens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
StuckOn | Agda.Syntax.Internal |
stuckOn | Agda.Syntax.Internal |
stVisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Style | |
1 (Type/Class) | Agda.Utils.Pretty |
2 (Data Constructor) | Agda.Utils.Pretty |
style | Agda.Utils.Pretty |
Sub | |
1 (Type/Class) | Agda.TypeChecking.Rewriting.NonLinMatch |
2 (Data Constructor) | Agda.Auto.Syntax |
sub | Agda.Auto.Syntax |
SubConstraints | |
1 (Type/Class) | Agda.Auto.NarrowingSearch |
2 (Data Constructor) | Agda.Auto.NarrowingSearch |
subi | Agda.Auto.Syntax |
sublistOf | Agda.Utils.QuickCheck |
Subscript | Agda.Utils.Suffix |
Subst | Agda.TypeChecking.Substitute |
subst | |
1 (Function) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Function) | Agda.Compiler.JS.Substitution |
3 (Function) | Agda.Compiler.Epic.AuxAST |
4 (Function) | Agda.TypeChecking.Substitute |
subst' | Agda.Compiler.JS.Substitution |
substBody | Agda.TypeChecking.CompiledClause.Compile |
substBranch | Agda.Compiler.Epic.AuxAST |
SubstCand | Agda.TypeChecking.MetaVars |
SubstExpr | Agda.Syntax.Abstract |
substExpr | Agda.Syntax.Abstract |
substForDot | Agda.Compiler.Epic.Injection |
Substitute | Agda.TypeChecking.SizedTypes.Syntax |
substituter | Agda.Compiler.JS.Substitution |
Substitution | |
1 (Type/Class) | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
2 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
Substitution' | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
substLit | Agda.Compiler.Epic.FromAgda |
substPattern | Agda.Syntax.Abstract |
substs | Agda.Compiler.Epic.AuxAST |
substTerm | Agda.Compiler.Epic.FromAgda |
substUnder | Agda.TypeChecking.Substitute |
subsvars | Agda.Auto.SearchControl |
subterms | Agda.Utils.QuickCheck |
subtract | Agda.Utils.VarSet |
subtypingForSizeLt | Agda.TypeChecking.MetaVars |
Success | Agda.Utils.QuickCheck |
suchThat | Agda.Utils.QuickCheck |
suchThatMaybe | Agda.Utils.QuickCheck |
sucName | Agda.TypeChecking.Level |
Suffix | |
1 (Type/Class) | Agda.Utils.Suffix |
2 (Type/Class) | Agda.Utils.List |
suffixView | Agda.Utils.Suffix |
Suggest | Agda.Syntax.Internal |
suggest | Agda.Syntax.Internal |
supremum | Agda.Termination.Order |
swap | Agda.Utils.Tuple |
swap01 | Agda.TypeChecking.Abstract |
switchBenchmarking | Agda.Utils.Benchmark |
SymArrow | Agda.Syntax.Parser.Tokens |
SymAs | Agda.Syntax.Parser.Tokens |
SymBar | Agda.Syntax.Parser.Tokens |
Symbol | |
1 (Type/Class) | Agda.Syntax.Parser.Tokens |
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
symbol | Agda.Syntax.Parser.LexActions |
SymCloseBrace | Agda.Syntax.Parser.Tokens |
SymCloseParen | Agda.Syntax.Parser.Tokens |
SymClosePragma | Agda.Syntax.Parser.Tokens |
SymCloseVirtualBrace | Agda.Syntax.Parser.Tokens |
SymColon | Agda.Syntax.Parser.Tokens |
SymDot | Agda.Syntax.Parser.Tokens |
SymDotDot | Agda.Syntax.Parser.Tokens |
SymDoubleCloseBrace | Agda.Syntax.Parser.Tokens |
SymDoubleOpenBrace | Agda.Syntax.Parser.Tokens |
SymEllipsis | Agda.Syntax.Parser.Tokens |
SymEndComment | Agda.Syntax.Parser.Tokens |
SymEqual | Agda.Syntax.Parser.Tokens |
SymLambda | Agda.Syntax.Parser.Tokens |
SymOpenBrace | Agda.Syntax.Parser.Tokens |
SymOpenParen | Agda.Syntax.Parser.Tokens |
SymOpenPragma | Agda.Syntax.Parser.Tokens |
SymOpenVirtualBrace | Agda.Syntax.Parser.Tokens |
SymQuestionMark | Agda.Syntax.Parser.Tokens |
SymSemi | Agda.Syntax.Parser.Tokens |
SymUnderscore | Agda.Syntax.Parser.Tokens |
SymVirtualSemi | Agda.Syntax.Parser.Tokens |
sync | Agda.Syntax.Parser.LookAhead |
SynEq | Agda.TypeChecking.SyntacticEquality |
Syntax | Agda.Syntax.Concrete |
SyntaxBindingLambda | Agda.Syntax.Concrete |
syntaxOf | Agda.Syntax.Fixity |