Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.TopLevelModuleName.Boot

Documentation

newtype ModuleNameHash Source #

Constructors

ModuleNameHash 

Fields

Instances

Instances details
EmbPrj ModuleNameHash Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ModuleNameHash -> S Int32 Source #

icod_ :: ModuleNameHash -> S Int32 Source #

value :: Int32 -> R ModuleNameHash Source #

HasTag ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Associated Types

type Tag ModuleNameHash 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

NFData ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

rnf :: ModuleNameHash -> ()

Show ModuleNameHash Source #

The record selector is not included in the resulting strings.

Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

showsPrec :: Int -> ModuleNameHash -> ShowS

show :: ModuleNameHash -> String

showList :: [ModuleNameHash] -> ShowS

Eq ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Ord ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Hashable ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

hashWithSalt :: Int -> ModuleNameHash -> Int

hash :: ModuleNameHash -> Int

ToJSON ModuleNameHash Source # 
Instance details

Defined in Agda.Interaction.JSONTop

NFData (BiMap RawTopLevelModuleName ModuleNameHash) 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type Tag ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

data TopLevelModuleName' range Source #

Instances

Instances details
Pretty TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

PrettyTCM TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

EmbPrj TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Sized TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

HasRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

KillRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

SetRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

HasTag (TopLevelModuleName' range) Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Associated Types

type Tag (TopLevelModuleName' range) 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

NFData (TopLevelModuleName' range) Source #

The range is not forced.

Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

rnf :: TopLevelModuleName' range -> ()

Generic (TopLevelModuleName' range) Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Associated Types

type Rep (TopLevelModuleName' range) 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

type Rep (TopLevelModuleName' range) = D1 ('MetaData "TopLevelModuleName'" "Agda.Syntax.TopLevelModuleName.Boot" "Agda-2.6.20240714-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))))

Methods

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

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

Show range => Show (TopLevelModuleName' range) Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

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

show :: TopLevelModuleName' range -> String

showList :: [TopLevelModuleName' range] -> ShowS

Eq (TopLevelModuleName' range) Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

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

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

Ord (TopLevelModuleName' range) Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Hashable (TopLevelModuleName' range) Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

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

hash :: TopLevelModuleName' range -> Int

type Tag (TopLevelModuleName' range) Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

type Rep (TopLevelModuleName' range) Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

type Rep (TopLevelModuleName' range) = D1 ('MetaData "TopLevelModuleName'" "Agda.Syntax.TopLevelModuleName.Boot" "Agda-2.6.20240714-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))))