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

type Tag ModuleNameHash = ModuleNameHash

Methods

tag :: ModuleNameHash -> Maybe (Tag ModuleNameHash) Source #

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

Methods

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

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

Ord ModuleNameHash Source # 
Instance details

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 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

Methods

toJSON :: ModuleNameHash -> Value #

toEncoding :: ModuleNameHash -> Encoding #

toJSONList :: [ModuleNameHash] -> Value #

toEncodingList :: [ModuleNameHash] -> Encoding #

omitField :: ModuleNameHash -> Bool #

NFData (BiMap RawTopLevelModuleName ModuleNameHash) 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

rnf :: BiMap RawTopLevelModuleName ModuleNameHash -> ()

type Tag ModuleNameHash Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

type Tag ModuleNameHash = ModuleNameHash

noModuleNameHash :: ModuleNameHash Source #

type TopLevelModuleNameParts = List1 Text Source #

data TopLevelModuleName' range Source #

Constructors

TopLevelModuleName 

Fields

Instances

Instances details
Pretty TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

pretty :: TopLevelModuleName -> Doc Source #

prettyPrec :: Int -> TopLevelModuleName -> Doc Source #

prettyList :: [TopLevelModuleName] -> Doc Source #

PrettyTCM TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

EmbPrj TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: TopLevelModuleName -> S Int32 Source #

icod_ :: TopLevelModuleName -> S Int32 Source #

value :: Int32 -> R TopLevelModuleName Source #

Sized TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

size :: TopLevelModuleName -> Int Source #

natSize :: TopLevelModuleName -> Peano Source #

HasRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: TopLevelModuleName' Range -> Range Source #

KillRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (TopLevelModuleName' Range) Source #

SetRange (TopLevelModuleName' Range) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> TopLevelModuleName' Range -> TopLevelModuleName' Range Source #

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

type Tag (TopLevelModuleName' range) = ModuleNameHash

Methods

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

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

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) 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 Tag (TopLevelModuleName' range) = ModuleNameHash
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))))