Agda.Syntax.TopLevelModuleName.Boot · Agda-2.7.0.1

newtypenewtype ModuleNameHash

Constructors

ModuleNameHash
- moduleNameHash :: Word64

Instances10Eq, Ord, Show, Hashable, ToJSON, HasTag, …

Eq ModuleNameHashDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot
Ord ModuleNameHashDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot
Show ModuleNameHashDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot
The record selector is not included in the resulting strings.
NFData ModuleNameHashDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot
Hashable ModuleNameHashDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot
ToJSON ModuleNameHashDefined in Agda-2.7.0.1 · Agda.Interaction.JSONTop · orphan
HasTag ModuleNameHashDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot
EmbPrj ModuleNameHashDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan
NFData (BiMap RawTopLevelModuleName ModuleNameHash)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base · orphan
type Tag ModuleNameHash = ModuleNameHashDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot

valuenoModuleNameHash :: ModuleNameHash

typetype TopLevelModuleNameParts = List1 Text

datadata TopLevelModuleName' range

Constructors

TopLevelModuleName
- moduleNameRange :: range
- moduleNameId :: !ModuleNameHash
- moduleNameParts :: TopLevelModuleNameParts

Instances16Pretty, PrettyTCM, Sized, EmbPrj, Eq, Ord, …

Pretty TopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName · orphan
PrettyTCM TopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Pretty
Sized TopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName · orphan
EmbPrj TopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Eq (TopLevelModuleName' range)Defined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot
Ord (TopLevelModuleName' range)Defined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot
Show range => Show (TopLevelModuleName' range)Defined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot
Generic (TopLevelModuleName' range)Defined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot
NFData (TopLevelModuleName' range)Defined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot
The range is not forced.
Hashable (TopLevelModuleName' range)Defined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot
HasRange (TopLevelModuleName' Range)Defined in Agda-2.7.0.1 · Agda.Syntax.Position
KillRange (TopLevelModuleName' Range)Defined in Agda-2.7.0.1 · Agda.Syntax.Position
SetRange (TopLevelModuleName' Range)Defined in Agda-2.7.0.1 · Agda.Syntax.Position
HasTag (TopLevelModuleName' range)Defined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot
type Rep (TopLevelModuleName' range) = D1 ('MetaData "TopLevelModuleName'" "Agda.Syntax.TopLevelModuleName.Boot" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "TopLevelModuleName" 'PrefixI 'True) (S1 ('MetaSel ('Just "moduleNameRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 range) :*: (S1 ('MetaSel ('Just "moduleNameId") 'SourceUnpack 'SourceStrict 'DecidedUnpack) (Rec0 ModuleNameHash) :*: S1 ('MetaSel ('Just "moduleNameParts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleNameParts))))Defined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot
type Tag (TopLevelModuleName' range) = ModuleNameHashDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName.Boot