Agda.Syntax.TopLevelModuleName.Boot

Documentation

newtype ModuleNameHash

Constructors

ModuleNameHash

Fields

• moduleNameHash :: Word64

Instances

EmbPrj ModuleNameHash

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ModuleNameHash -> S Int32

icod_ :: ModuleNameHash -> S Int32

value :: Int32 -> R ModuleNameHash

HasTag ModuleNameHash

Defined in Agda.Syntax.TopLevelModuleName.Boot

Associated Types

type Tag ModuleNameHash

Methods

tag :: ModuleNameHash -> Maybe (Tag ModuleNameHash)

Show ModuleNameHash

The record selector is not included in the resulting strings.

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

showsPrec :: Int -> ModuleNameHash -> ShowS

show :: ModuleNameHash -> String

showList :: [ModuleNameHash] -> ShowS

NFData ModuleNameHash

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

rnf :: ModuleNameHash -> ()

Eq ModuleNameHash

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

(==) :: ModuleNameHash -> ModuleNameHash -> Bool

(/=) :: ModuleNameHash -> ModuleNameHash -> Bool

Ord ModuleNameHash

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

compare :: ModuleNameHash -> ModuleNameHash -> Ordering

(<) :: ModuleNameHash -> ModuleNameHash -> Bool

(<=) :: ModuleNameHash -> ModuleNameHash -> Bool

(>) :: ModuleNameHash -> ModuleNameHash -> Bool

(>=) :: ModuleNameHash -> ModuleNameHash -> Bool

max :: ModuleNameHash -> ModuleNameHash -> ModuleNameHash

min :: ModuleNameHash -> ModuleNameHash -> ModuleNameHash

Hashable ModuleNameHash

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

hashWithSalt :: Int -> ModuleNameHash -> Int

hash :: ModuleNameHash -> Int

ToJSON ModuleNameHash

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: ModuleNameHash -> Value

toEncoding :: ModuleNameHash -> Encoding

toJSONList :: [ModuleNameHash] -> Value

toEncodingList :: [ModuleNameHash] -> Encoding

omitField :: ModuleNameHash -> Bool

NFData (BiMap RawTopLevelModuleName ModuleNameHash)

Defined in Agda.TypeChecking.Monad.Base

Methods

rnf :: BiMap RawTopLevelModuleName ModuleNameHash -> ()

type Tag ModuleNameHash

Defined in Agda.Syntax.TopLevelModuleName.Boot

type Tag ModuleNameHash = ModuleNameHash

noModuleNameHash :: ModuleNameHash

type TopLevelModuleNameParts = List1 Text

data TopLevelModuleName' range

Constructors

TopLevelModuleName

Fields

• moduleNameRange :: range
• moduleNameId :: !ModuleNameHash
• moduleNameParts :: TopLevelModuleNameParts

Instances

Pretty TopLevelModuleName

Defined in Agda.Syntax.TopLevelModuleName

Methods

pretty :: TopLevelModuleName -> Doc

prettyPrec :: Int -> TopLevelModuleName -> Doc

prettyList :: [TopLevelModuleName] -> Doc

PrettyTCM TopLevelModuleName

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => TopLevelModuleName -> m Doc

EmbPrj TopLevelModuleName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: TopLevelModuleName -> S Int32

icod_ :: TopLevelModuleName -> S Int32

value :: Int32 -> R TopLevelModuleName

Sized TopLevelModuleName

Defined in Agda.Syntax.TopLevelModuleName

Methods

size :: TopLevelModuleName -> Int

natSize :: TopLevelModuleName -> Peano

HasRange (TopLevelModuleName' Range)

Defined in Agda.Syntax.Position

Methods

getRange :: TopLevelModuleName' Range -> Range

KillRange (TopLevelModuleName' Range)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (TopLevelModuleName' Range)

SetRange (TopLevelModuleName' Range)

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> TopLevelModuleName' Range -> TopLevelModuleName' Range

HasTag (TopLevelModuleName' range)

Defined in Agda.Syntax.TopLevelModuleName.Boot

Associated Types

type Tag (TopLevelModuleName' range)

Methods

tag :: TopLevelModuleName' range -> Maybe (Tag (TopLevelModuleName' range))

Generic (TopLevelModuleName' range)

Defined in Agda.Syntax.TopLevelModuleName.Boot

Associated Types

type Rep (TopLevelModuleName' range) :: Type -> Type

Methods

from :: TopLevelModuleName' range -> Rep (TopLevelModuleName' range) x

to :: Rep (TopLevelModuleName' range) x -> TopLevelModuleName' range

Show range => Show (TopLevelModuleName' range)

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

showsPrec :: Int -> TopLevelModuleName' range -> ShowS

show :: TopLevelModuleName' range -> String

showList :: [TopLevelModuleName' range] -> ShowS

NFData (TopLevelModuleName' range)

The range is not forced.

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

rnf :: TopLevelModuleName' range -> ()

Eq (TopLevelModuleName' range)

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

(==) :: TopLevelModuleName' range -> TopLevelModuleName' range -> Bool

(/=) :: TopLevelModuleName' range -> TopLevelModuleName' range -> Bool

Ord (TopLevelModuleName' range)

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

compare :: TopLevelModuleName' range -> TopLevelModuleName' range -> Ordering

(<) :: TopLevelModuleName' range -> TopLevelModuleName' range -> Bool

(<=) :: TopLevelModuleName' range -> TopLevelModuleName' range -> Bool

(>) :: TopLevelModuleName' range -> TopLevelModuleName' range -> Bool

(>=) :: TopLevelModuleName' range -> TopLevelModuleName' range -> Bool

max :: TopLevelModuleName' range -> TopLevelModuleName' range -> TopLevelModuleName' range

min :: TopLevelModuleName' range -> TopLevelModuleName' range -> TopLevelModuleName' range

Hashable (TopLevelModuleName' range)

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

hashWithSalt :: Int -> TopLevelModuleName' range -> Int

hash :: TopLevelModuleName' range -> Int

type Tag (TopLevelModuleName' range)

Defined in Agda.Syntax.TopLevelModuleName.Boot

type Tag (TopLevelModuleName' range) = ModuleNameHash

type Rep (TopLevelModuleName' range)

Defined in Agda.Syntax.TopLevelModuleName.Boot

type Rep (TopLevelModuleName' range) = D1 ('MetaData "TopLevelModuleName'" "Agda.Syntax.TopLevelModuleName.Boot" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "TopLevelModuleName" 'PrefixI 'True) (S1 ('MetaSel ('Just "moduleNameRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 range) :*: (S1 ('MetaSel ('Just "moduleNameId") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash) :*: S1 ('MetaSel ('Just "moduleNameParts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleNameParts))))