Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.TopLevelModuleName.Boot

# Documentation

newtype ModuleNameHash Source #

Constructors

ModuleNameHash |

Fields

- moduleNameHash :: Word64

#### Instances

Instances details

EmbPrj ModuleNameHash Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ModuleNameHash -> S Word32 Source # icod_ :: ModuleNameHash -> S Word32 Source # value :: Word32 -> 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 #

ToJSON ModuleNameHash Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: ModuleNameHash -> Value Source # toEncoding :: ModuleNameHash -> Encoding Source # toJSONList :: [ModuleNameHash] -> Value Source # toEncodingList :: [ModuleNameHash] -> Encoding Source # omitField :: ModuleNameHash -> Bool Source #
NFData ModuleNameHash Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName.Boot Methods rnf :: ModuleNameHash -> () Source #
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 Source # show :: ModuleNameHash -> String Source # showList :: [ModuleNameHash] -> ShowS Source #
Eq ModuleNameHash Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName.Boot Methods (==) :: ModuleNameHash -> ModuleNameHash -> Bool Source # (/=) :: ModuleNameHash -> ModuleNameHash -> Bool Source #
Ord ModuleNameHash Source # |

Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

compare :: ModuleNameHash -> ModuleNameHash -> Ordering Source #

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

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

(>) :: ModuleNameHash -> ModuleNameHash -> Bool Source #

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

max :: ModuleNameHash -> ModuleNameHash -> ModuleNameHash Source #

min :: ModuleNameHash -> ModuleNameHash -> ModuleNameHash Source #

Hashable ModuleNameHash Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName.Boot Methods hashWithSalt :: Int -> ModuleNameHash -> Int Source # hash :: ModuleNameHash -> Int Source #
NFData (BiMap RawTopLevelModuleName ModuleNameHash) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: BiMap RawTopLevelModuleName ModuleNameHash -> () Source #
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

- moduleNameRange :: range
- moduleNameId :: !ModuleNameHash
- moduleNameParts :: TopLevelModuleNameParts
- moduleNameInferred :: !Bool

  Was this module name constructed from a file name rather than declared in the file?

#### 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 Word32 Source # icod_ :: TopLevelModuleName -> S Word32 Source # value :: Word32 -> 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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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) :*: S1 ('MetaSel ('Just "moduleNameInferred") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool))))

Methods

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

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

Show range => Show (TopLevelModuleName' range) Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName.Boot Methods showsPrec :: Int -> TopLevelModuleName' range -> ShowS Source # show :: TopLevelModuleName' range -> String Source # showList :: [TopLevelModuleName' range] -> ShowS Source #
Eq (TopLevelModuleName' range) Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName.Boot Methods (==) :: TopLevelModuleName' range -> TopLevelModuleName' range -> Bool Source # (/=) :: TopLevelModuleName' range -> TopLevelModuleName' range -> Bool Source #
Ord (TopLevelModuleName' range) Source # |

Instance details

Defined in Agda.Syntax.TopLevelModuleName.Boot

Methods

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

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

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

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

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

max :: TopLevelModuleName' range -> TopLevelModuleName' range -> TopLevelModuleName' range Source #

min :: TopLevelModuleName' range -> TopLevelModuleName' range -> TopLevelModuleName' range Source #

Hashable (TopLevelModuleName' range) Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName.Boot Methods hashWithSalt :: Int -> TopLevelModuleName' range -> Int Source # hash :: TopLevelModuleName' range -> Int Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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) :*: S1 ('MetaSel ('Just "moduleNameInferred") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool))))