Agda.Syntax.Common
data Delayed
data Induction
data Hiding
data WithHiding a
class LensHiding a
data Big
data Relevance
class LensRelevance a
data ArgInfo
class LensArgInfo a
data Arg e
class Underscore a
data Dom e
data Named name a
type Named_
type NamedArg a
data Ranged a
type RawName
type RString
data ConPOrigin
data IsInfix
data Access
data IsAbstract
data IsInstance
data IsMacro
type Nat
type Arity
data NameId
data MetaId
data Constr a
data Placeholder
data MaybePlaceholder e
data InteractionId
data ImportDirective' a b
data Using' a b
data ImportedName' a b
data Renaming' a b
data TerminationCheck m
type PositivityCheck