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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Serialise

Description

Structure-sharing serialisation of Agda interface files.

Synopsis

- encode :: EmbPrj a => a -> TCM Encoded
- encodeFile :: FilePath -> Interface -> TCM ByteString
- encodeInterface :: Interface -> TCM Encoded
- decode :: EmbPrj a => ByteString -> TCM (Maybe a)
- decodeFile :: FilePath -> TCM (Maybe Interface)
- decodeInterface :: ByteString -> TCM (Maybe Interface)
- decodeHashes :: ByteString -> Maybe (Hash, Hash)
- class Typeable a => EmbPrj a

# Documentation

encode :: EmbPrj a => a -> TCM Encoded Source #

Encodes something. To ensure relocatability file paths in positions are replaced with module names.

encodeFile :: FilePath -> Interface -> TCM ByteString Source #

Encodes an interface. To ensure relocatability file paths in positions are replaced with module names.

An uncompressed bytestring corresponding to the encoded interface is returned.

encodeInterface :: Interface -> TCM Encoded Source #

decode :: EmbPrj a => ByteString -> TCM (Maybe a) Source #

Decodes an uncompressed bytestring (without extra hashes or magic numbers). The result depends on the include path.

Returns `Nothing` if a decoding error is encountered.

decodeFile :: FilePath -> TCM (Maybe Interface) Source #

decodeInterface :: ByteString -> TCM (Maybe Interface) Source #

Decodes an interface. The result depends on the include path.

Returns `Nothing` if the file does not start with the right magic number or some other decoding error is encountered.

decodeHashes :: ByteString -> Maybe (Hash, Hash) Source #

class Typeable a => EmbPrj a Source #

#### Instances

Instances details

EmbPrj Range Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Range -> S Word32 Source # icod_ :: Range -> S Word32 Source # value :: Word32 -> R Range Source #
EmbPrj ExecutablesFile Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ExecutablesFile -> S Word32 Source # icod_ :: ExecutablesFile -> S Word32 Source # value :: Word32 -> R ExecutablesFile Source #
EmbPrj LibPositionInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: LibPositionInfo -> S Word32 Source # icod_ :: LibPositionInfo -> S Word32 Source # value :: Word32 -> R LibPositionInfo Source #
EmbPrj LibWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: LibWarning -> S Word32 Source # icod_ :: LibWarning -> S Word32 Source # value :: Word32 -> R LibWarning Source #
EmbPrj LibWarning' Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: LibWarning' -> S Word32 Source # icod_ :: LibWarning' -> S Word32 Source # value :: Word32 -> R LibWarning' Source #
EmbPrj OptionsPragma Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OptionsPragma -> S Word32 Source # icod_ :: OptionsPragma -> S Word32 Source # value :: Word32 -> R OptionsPragma Source #
EmbPrj OptionWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: OptionWarning -> S Word32 Source # icod_ :: OptionWarning -> S Word32 Source # value :: Word32 -> R OptionWarning Source #
EmbPrj ConfluenceCheck Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ConfluenceCheck -> S Word32 Source # icod_ :: ConfluenceCheck -> S Word32 Source # value :: Word32 -> R ConfluenceCheck Source #
EmbPrj InfectiveCoinfective Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: InfectiveCoinfective -> S Word32 Source # icod_ :: InfectiveCoinfective -> S Word32 Source # value :: Word32 -> R InfectiveCoinfective Source #
EmbPrj PragmaOptions Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: PragmaOptions -> S Word32 Source # icod_ :: PragmaOptions -> S Word32 Source # value :: Word32 -> R PragmaOptions Source #
EmbPrj WarningMode Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningMode -> S Word32 Source # icod_ :: WarningMode -> S Word32 Source # value :: Word32 -> R WarningMode Source #
EmbPrj WarningModeError Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningModeError -> S Word32 Source # icod_ :: WarningModeError -> S Word32 Source # value :: Word32 -> R WarningModeError Source #
EmbPrj WarningName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningName -> S Word32 Source # icod_ :: WarningName -> S Word32 Source # value :: Word32 -> R WarningName Source #
EmbPrj BindName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: BindName -> S Word32 Source # icod_ :: BindName -> S Word32 Source # value :: Word32 -> R BindName Source #
EmbPrj Pattern Source # | Hackish serialization for patterns that deletes dot patterns. So that we can serialize the `WithClauseProjectionFixityMismatch` without having to define serialization of expressions.
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Pattern -> S Word32 Source # icod_ :: Pattern -> S Word32 Source # value :: Word32 -> R Pattern Source #
EmbPrj AmbiguousQName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: AmbiguousQName -> S Word32 Source # icod_ :: AmbiguousQName -> S Word32 Source # value :: Word32 -> R AmbiguousQName Source #
EmbPrj ModuleName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ModuleName -> S Word32 Source # icod_ :: ModuleName -> S Word32 Source # value :: Word32 -> R ModuleName Source #
EmbPrj Name Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Name -> S Word32 Source # icod_ :: Name -> S Word32 Source # value :: Word32 -> R Name Source #
EmbPrj QName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QName -> S Word32 Source # icod_ :: QName -> S Word32 Source # value :: Word32 -> R QName Source #
EmbPrj Suffix Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Suffix -> S Word32 Source # icod_ :: Suffix -> S Word32 Source # value :: Word32 -> R Suffix Source #
EmbPrj BuiltinId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: BuiltinId -> S Word32 Source # icod_ :: BuiltinId -> S Word32 Source # value :: Word32 -> R BuiltinId Source #
EmbPrj PrimitiveId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: PrimitiveId -> S Word32 Source # icod_ :: PrimitiveId -> S Word32 Source # value :: Word32 -> R PrimitiveId Source #
EmbPrj SomeBuiltin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: SomeBuiltin -> S Word32 Source # icod_ :: SomeBuiltin -> S Word32 Source # value :: Word32 -> R SomeBuiltin Source #
EmbPrj Access Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Access -> S Word32 Source # icod_ :: Access -> S Word32 Source # value :: Word32 -> R Access Source #
EmbPrj Annotation Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Annotation -> S Word32 Source # icod_ :: Annotation -> S Word32 Source # value :: Word32 -> R Annotation Source #
EmbPrj ArgInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ArgInfo -> S Word32 Source # icod_ :: ArgInfo -> S Word32 Source # value :: Word32 -> R ArgInfo Source #
EmbPrj Associativity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Associativity -> S Word32 Source # icod_ :: Associativity -> S Word32 Source # value :: Word32 -> R Associativity Source #
EmbPrj BoundVariablePosition Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: BoundVariablePosition -> S Word32 Source # icod_ :: BoundVariablePosition -> S Word32 Source # value :: Word32 -> R BoundVariablePosition Source #
EmbPrj Catchall Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Catchall -> S Word32 Source # icod_ :: Catchall -> S Word32 Source # value :: Word32 -> R Catchall Source #
EmbPrj Cohesion Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Cohesion -> S Word32 Source # icod_ :: Cohesion -> S Word32 Source # value :: Word32 -> R Cohesion Source #
EmbPrj ConOrigin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ConOrigin -> S Word32 Source # icod_ :: ConOrigin -> S Word32 Source # value :: Word32 -> R ConOrigin Source #
EmbPrj ConstructorOrPatternSynonym Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ConstructorOrPatternSynonym -> S Word32 Source # icod_ :: ConstructorOrPatternSynonym -> S Word32 Source # value :: Word32 -> R ConstructorOrPatternSynonym Source #
EmbPrj Cubical Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Cubical -> S Word32 Source # icod_ :: Cubical -> S Word32 Source # value :: Word32 -> R Cubical Source #
EmbPrj ExpandedEllipsis Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ExpandedEllipsis -> S Word32 Source # icod_ :: ExpandedEllipsis -> S Word32 Source # value :: Word32 -> R ExpandedEllipsis Source #
EmbPrj FileType Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FileType -> S Word32 Source # icod_ :: FileType -> S Word32 Source # value :: Word32 -> R FileType Source #
EmbPrj Fixity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Fixity -> S Word32 Source # icod_ :: Fixity -> S Word32 Source # value :: Word32 -> R Fixity Source #
EmbPrj Fixity' Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Fixity' -> S Word32 Source # icod_ :: Fixity' -> S Word32 Source # value :: Word32 -> R Fixity' Source #
EmbPrj FixityLevel Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FixityLevel -> S Word32 Source # icod_ :: FixityLevel -> S Word32 Source # value :: Word32 -> R FixityLevel Source #
EmbPrj FreeVariables Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FreeVariables -> S Word32 Source # icod_ :: FreeVariables -> S Word32 Source # value :: Word32 -> R FreeVariables Source #
EmbPrj Hiding Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Hiding -> S Word32 Source # icod_ :: Hiding -> S Word32 Source # value :: Word32 -> R Hiding Source #
EmbPrj IsAbstract Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IsAbstract -> S Word32 Source # icod_ :: IsAbstract -> S Word32 Source # value :: Word32 -> R IsAbstract Source #
EmbPrj IsInstance Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IsInstance -> S Word32 Source # icod_ :: IsInstance -> S Word32 Source # value :: Word32 -> R IsInstance Source #
EmbPrj IsOpaque Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IsOpaque -> S Word32 Source # icod_ :: IsOpaque -> S Word32 Source # value :: Word32 -> R IsOpaque Source #
EmbPrj Language Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Language -> S Word32 Source # icod_ :: Language -> S Word32 Source # value :: Word32 -> R Language Source #
EmbPrj Lock Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Lock -> S Word32 Source # icod_ :: Lock -> S Word32 Source # value :: Word32 -> R Lock Source #
EmbPrj MetaId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: MetaId -> S Word32 Source # icod_ :: MetaId -> S Word32 Source # value :: Word32 -> R MetaId Source #
EmbPrj ModalPolarity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ModalPolarity -> S Word32 Source # icod_ :: ModalPolarity -> S Word32 Source # value :: Word32 -> R ModalPolarity Source #
EmbPrj Modality Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Modality -> S Word32 Source # icod_ :: Modality -> S Word32 Source # value :: Word32 -> R Modality Source #
EmbPrj NameId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NameId -> S Word32 Source # icod_ :: NameId -> S Word32 Source # value :: Word32 -> R NameId Source #
EmbPrj NotationPart Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NotationPart -> S Word32 Source # icod_ :: NotationPart -> S Word32 Source # value :: Word32 -> R NotationPart Source #
EmbPrj OpaqueId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OpaqueId -> S Word32 Source # icod_ :: OpaqueId -> S Word32 Source # value :: Word32 -> R OpaqueId Source #
EmbPrj Origin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Origin -> S Word32 Source # icod_ :: Origin -> S Word32 Source # value :: Word32 -> R Origin Source #
EmbPrj OriginIrrelevant Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OriginIrrelevant -> S Word32 Source # icod_ :: OriginIrrelevant -> S Word32 Source # value :: Word32 -> R OriginIrrelevant Source #
EmbPrj OriginRelevant Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OriginRelevant -> S Word32 Source # icod_ :: OriginRelevant -> S Word32 Source # value :: Word32 -> R OriginRelevant Source #
EmbPrj OriginShapeIrrelevant Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OriginShapeIrrelevant -> S Word32 Source # icod_ :: OriginShapeIrrelevant -> S Word32 Source # value :: Word32 -> R OriginShapeIrrelevant Source #
EmbPrj OverlapMode Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OverlapMode -> S Word32 Source # icod_ :: OverlapMode -> S Word32 Source # value :: Word32 -> R OverlapMode Source #
EmbPrj PatternOrCopattern Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: PatternOrCopattern -> S Word32 Source # icod_ :: PatternOrCopattern -> S Word32 Source # value :: Word32 -> R PatternOrCopattern Source #
EmbPrj PolarityModality Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: PolarityModality -> S Word32 Source # icod_ :: PolarityModality -> S Word32 Source # value :: Word32 -> R PolarityModality Source #
EmbPrj ProblemId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ProblemId -> S Word32 Source # icod_ :: ProblemId -> S Word32 Source # value :: Word32 -> R ProblemId Source #
EmbPrj ProjOrigin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ProjOrigin -> S Word32 Source # icod_ :: ProjOrigin -> S Word32 Source # value :: Word32 -> R ProjOrigin Source #
EmbPrj Q0Origin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Q0Origin -> S Word32 Source # icod_ :: Q0Origin -> S Word32 Source # value :: Word32 -> R Q0Origin Source #
EmbPrj Q1Origin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Q1Origin -> S Word32 Source # icod_ :: Q1Origin -> S Word32 Source # value :: Word32 -> R Q1Origin Source #
EmbPrj Quantity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Quantity -> S Word32 Source # icod_ :: Quantity -> S Word32 Source # value :: Word32 -> R Quantity Source #
EmbPrj QωOrigin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QωOrigin -> S Word32 Source # icod_ :: QωOrigin -> S Word32 Source # value :: Word32 -> R QωOrigin Source #
EmbPrj Relevance Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Relevance -> S Word32 Source # icod_ :: Relevance -> S Word32 Source # value :: Word32 -> R Relevance Source #
EmbPrj Aspect Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Aspect -> S Word32 Source # icod_ :: Aspect -> S Word32 Source # value :: Word32 -> R Aspect Source #
EmbPrj Aspects Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Aspects -> S Word32 Source # icod_ :: Aspects -> S Word32 Source # value :: Word32 -> R Aspects Source #
EmbPrj DefinitionSite Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: DefinitionSite -> S Word32 Source # icod_ :: DefinitionSite -> S Word32 Source # value :: Word32 -> R DefinitionSite Source #
EmbPrj Induction Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Induction -> S Word32 Source # icod_ :: Induction -> S Word32 Source # value :: Word32 -> R Induction Source #
EmbPrj NameKind Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: NameKind -> S Word32 Source # icod_ :: NameKind -> S Word32 Source # value :: Word32 -> R NameKind Source #
EmbPrj OtherAspect Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: OtherAspect -> S Word32 Source # icod_ :: OtherAspect -> S Word32 Source # value :: Word32 -> R OtherAspect Source #
EmbPrj TokenBased Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: TokenBased -> S Word32 Source # icod_ :: TokenBased -> S Word32 Source # value :: Word32 -> R TokenBased Source #
EmbPrj KwRange Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: KwRange -> S Word32 Source # icod_ :: KwRange -> S Word32 Source # value :: Word32 -> R KwRange Source #
EmbPrj Doc Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: Doc -> S Word32 Source # icod_ :: Doc -> S Word32 Source # value :: Word32 -> R Doc Source #
EmbPrj RecordDirective Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: RecordDirective -> S Word32 Source # icod_ :: RecordDirective -> S Word32 Source # value :: Word32 -> R RecordDirective Source #
EmbPrj DeclarationWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: DeclarationWarning -> S Word32 Source # icod_ :: DeclarationWarning -> S Word32 Source # value :: Word32 -> R DeclarationWarning Source #
EmbPrj DeclarationWarning' Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: DeclarationWarning' -> S Word32 Source # icod_ :: DeclarationWarning' -> S Word32 Source # value :: Word32 -> R DeclarationWarning' Source #
EmbPrj OpenOrImport Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: OpenOrImport -> S Word32 Source # icod_ :: OpenOrImport -> S Word32 Source # value :: Word32 -> R OpenOrImport Source #
EmbPrj UnicodeOrAscii Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: UnicodeOrAscii -> S Word32 Source # icod_ :: UnicodeOrAscii -> S Word32 Source # value :: Word32 -> R UnicodeOrAscii Source #
EmbPrj Name Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Name -> S Word32 Source # icod_ :: Name -> S Word32 Source # value :: Word32 -> R Name Source #
EmbPrj NameInScope Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NameInScope -> S Word32 Source # icod_ :: NameInScope -> S Word32 Source # value :: Word32 -> R NameInScope Source #
EmbPrj NamePart Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NamePart -> S Word32 Source # icod_ :: NamePart -> S Word32 Source # value :: Word32 -> R NamePart Source #
EmbPrj QName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QName -> S Word32 Source # icod_ :: QName -> S Word32 Source # value :: Word32 -> R QName Source #
EmbPrj ParenPreference Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ParenPreference -> S Word32 Source # icod_ :: ParenPreference -> S Word32 Source # value :: Word32 -> R ParenPreference Source #
EmbPrj Precedence Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Precedence -> S Word32 Source # icod_ :: Precedence -> S Word32 Source # value :: Word32 -> R Precedence Source #
EmbPrj ConPatInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ConPatInfo -> S Word32 Source # icod_ :: ConPatInfo -> S Word32 Source # value :: Word32 -> R ConPatInfo Source #
EmbPrj ConPatLazy Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ConPatLazy -> S Word32 Source # icod_ :: ConPatLazy -> S Word32 Source # value :: Word32 -> R ConPatLazy Source #
EmbPrj Blocked_ Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Blocked_ -> S Word32 Source # icod_ :: Blocked_ -> S Word32 Source # value :: Word32 -> R Blocked_ Source #
EmbPrj Clause Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Clause -> S Word32 Source # icod_ :: Clause -> S Word32 Source # value :: Word32 -> R Clause Source #
EmbPrj ConHead Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConHead -> S Word32 Source # icod_ :: ConHead -> S Word32 Source # value :: Word32 -> R ConHead Source #
EmbPrj ConPatternInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConPatternInfo -> S Word32 Source # icod_ :: ConPatternInfo -> S Word32 Source # value :: Word32 -> R ConPatternInfo Source #
EmbPrj DBPatVar Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DBPatVar -> S Word32 Source # icod_ :: DBPatVar -> S Word32 Source # value :: Word32 -> R DBPatVar Source #
EmbPrj DataOrRecord Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DataOrRecord -> S Word32 Source # icod_ :: DataOrRecord -> S Word32 Source # value :: Word32 -> R DataOrRecord Source #
EmbPrj Level Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Level -> S Word32 Source # icod_ :: Level -> S Word32 Source # value :: Word32 -> R Level Source #
EmbPrj NotBlocked Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NotBlocked -> S Word32 Source # icod_ :: NotBlocked -> S Word32 Source # value :: Word32 -> R NotBlocked Source #
EmbPrj PatOrigin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PatOrigin -> S Word32 Source # icod_ :: PatOrigin -> S Word32 Source # value :: Word32 -> R PatOrigin Source #
EmbPrj PatternInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PatternInfo -> S Word32 Source # icod_ :: PatternInfo -> S Word32 Source # value :: Word32 -> R PatternInfo Source #
EmbPrj PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PlusLevel -> S Word32 Source # icod_ :: PlusLevel -> S Word32 Source # value :: Word32 -> R PlusLevel Source #
EmbPrj Sort Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Sort -> S Word32 Source # icod_ :: Sort -> S Word32 Source # value :: Word32 -> R Sort Source #
EmbPrj Term Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Term -> S Word32 Source # icod_ :: Term -> S Word32 Source # value :: Word32 -> R Term Source #
EmbPrj IsFibrant Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: IsFibrant -> S Word32 Source # icod_ :: IsFibrant -> S Word32 Source # value :: Word32 -> R IsFibrant Source #
EmbPrj Univ Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Univ -> S Word32 Source # icod_ :: Univ -> S Word32 Source # value :: Word32 -> R Univ Source #
EmbPrj Literal Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Literal -> S Word32 Source # icod_ :: Literal -> S Word32 Source # value :: Word32 -> R Literal Source #
EmbPrj ParseWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ParseWarning -> S Word32 Source # icod_ :: ParseWarning -> S Word32 Source # value :: Word32 -> R ParseWarning Source #
EmbPrj Range Source # | Ranges are always deserialised as `noRange`.
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Range -> S Word32 Source # icod_ :: Range -> S Word32 Source # value :: Word32 -> R Range Source #
EmbPrj RangeFile Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: RangeFile -> S Word32 Source # icod_ :: RangeFile -> S Word32 Source # value :: Word32 -> R RangeFile Source #
EmbPrj AbstractModule Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbstractModule -> S Word32 Source # icod_ :: AbstractModule -> S Word32 Source # value :: Word32 -> R AbstractModule Source #
EmbPrj AbstractName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbstractName -> S Word32 Source # icod_ :: AbstractName -> S Word32 Source # value :: Word32 -> R AbstractName Source #
EmbPrj BindingSource Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: BindingSource -> S Word32 Source # icod_ :: BindingSource -> S Word32 Source # value :: Word32 -> R BindingSource Source #
EmbPrj DataOrRecordModule Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: DataOrRecordModule -> S Word32 Source # icod_ :: DataOrRecordModule -> S Word32 Source # value :: Word32 -> R DataOrRecordModule Source #
EmbPrj KindOfName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: KindOfName -> S Word32 Source # icod_ :: KindOfName -> S Word32 Source # value :: Word32 -> R KindOfName Source #
EmbPrj LocalVar Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: LocalVar -> S Word32 Source # icod_ :: LocalVar -> S Word32 Source # value :: Word32 -> R LocalVar Source #
EmbPrj NameMetadata Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameMetadata -> S Word32 Source # icod_ :: NameMetadata -> S Word32 Source # value :: Word32 -> R NameMetadata Source #
EmbPrj NameOrModule Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameOrModule -> S Word32 Source # icod_ :: NameOrModule -> S Word32 Source # value :: Word32 -> R NameOrModule Source #
EmbPrj NameSpace Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameSpace -> S Word32 Source # icod_ :: NameSpace -> S Word32 Source # value :: Word32 -> R NameSpace Source #
EmbPrj NameSpaceId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameSpaceId -> S Word32 Source # icod_ :: NameSpaceId -> S Word32 Source # value :: Word32 -> R NameSpaceId Source #
EmbPrj Scope Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Scope -> S Word32 Source # icod_ :: Scope -> S Word32 Source # value :: Word32 -> R Scope Source #
EmbPrj ScopeInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ScopeInfo -> S Word32 Source # icod_ :: ScopeInfo -> S Word32 Source # value :: Word32 -> R ScopeInfo Source #
EmbPrj WhyInScope Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: WhyInScope -> S Word32 Source # icod_ :: WhyInScope -> S Word32 Source # value :: Word32 -> R WhyInScope 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 #
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 #
EmbPrj CutOff Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: CutOff -> S Word32 Source # icod_ :: CutOff -> S Word32 Source # value :: Word32 -> R CutOff Source #
EmbPrj CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CompiledClauses -> S Word32 Source # icod_ :: CompiledClauses -> S Word32 Source # value :: Word32 -> R CompiledClauses Source #
EmbPrj LazySplit Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: LazySplit -> S Word32 Source # icod_ :: LazySplit -> S Word32 Source # value :: Word32 -> R LazySplit Source #
EmbPrj SplitTag Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: SplitTag -> S Word32 Source # icod_ :: SplitTag -> S Word32 Source # value :: Word32 -> R SplitTag Source #
EmbPrj Key Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Key -> S Word32 Source # icod_ :: Key -> S Word32 Source # value :: Word32 -> R Key Source #
EmbPrj BuiltinSort Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: BuiltinSort -> S Word32 Source # icod_ :: BuiltinSort -> S Word32 Source # value :: Word32 -> R BuiltinSort Source #
EmbPrj CheckpointId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CheckpointId -> S Word32 Source # icod_ :: CheckpointId -> S Word32 Source # value :: Word32 -> R CheckpointId Source #
EmbPrj CompKit Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CompKit -> S Word32 Source # icod_ :: CompKit -> S Word32 Source # value :: Word32 -> R CompKit Source #
EmbPrj CompilerPragma Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: CompilerPragma -> S Word32 Source # icod_ :: CompilerPragma -> S Word32 Source # value :: Word32 -> R CompilerPragma Source #
EmbPrj Definition Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Definition -> S Word32 Source # icod_ :: Definition -> S Word32 Source # value :: Word32 -> R Definition Source #
EmbPrj Defn Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Defn -> S Word32 Source # icod_ :: Defn -> S Word32 Source # value :: Word32 -> R Defn Source #
EmbPrj DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DisplayForm -> S Word32 Source # icod_ :: DisplayForm -> S Word32 Source # value :: Word32 -> R DisplayForm Source #
EmbPrj DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DisplayTerm -> S Word32 Source # icod_ :: DisplayTerm -> S Word32 Source # value :: Word32 -> R DisplayTerm Source #
EmbPrj DoGeneralize Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DoGeneralize -> S Word32 Source # icod_ :: DoGeneralize -> S Word32 Source # value :: Word32 -> R DoGeneralize Source #
EmbPrj EtaEquality Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: EtaEquality -> S Word32 Source # icod_ :: EtaEquality -> S Word32 Source # value :: Word32 -> R EtaEquality Source #
EmbPrj ExtLamInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ExtLamInfo -> S Word32 Source # icod_ :: ExtLamInfo -> S Word32 Source # value :: Word32 -> R ExtLamInfo Source #
EmbPrj ForeignCode Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: ForeignCode -> S Word32 Source # icod_ :: ForeignCode -> S Word32 Source # value :: Word32 -> R ForeignCode Source #
EmbPrj ForeignCodeStack Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: ForeignCodeStack -> S Word32 Source # icod_ :: ForeignCodeStack -> S Word32 Source # value :: Word32 -> R ForeignCodeStack Source #
EmbPrj FunctionFlag Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: FunctionFlag -> S Word32 Source # icod_ :: FunctionFlag -> S Word32 Source # value :: Word32 -> R FunctionFlag Source #
EmbPrj IllegalRewriteRuleReason Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: IllegalRewriteRuleReason -> S Word32 Source # icod_ :: IllegalRewriteRuleReason -> S Word32 Source # value :: Word32 -> R IllegalRewriteRuleReason Source #
EmbPrj InstanceInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: InstanceInfo -> S Word32 Source # icod_ :: InstanceInfo -> S Word32 Source # value :: Word32 -> R InstanceInfo Source #
EmbPrj InstanceTable Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: InstanceTable -> S Word32 Source # icod_ :: InstanceTable -> S Word32 Source # value :: Word32 -> R InstanceTable Source #
EmbPrj Instantiation Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Instantiation -> S Word32 Source # icod_ :: Instantiation -> S Word32 Source # value :: Word32 -> R Instantiation Source #
EmbPrj Interface Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances Methods icode :: Interface -> S Word32 Source # icod_ :: Interface -> S Word32 Source # value :: Word32 -> R Interface Source #
EmbPrj IsAmbiguous Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: IsAmbiguous -> S Word32 Source # icod_ :: IsAmbiguous -> S Word32 Source # value :: Word32 -> R IsAmbiguous Source #
EmbPrj IsForced Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: IsForced -> S Word32 Source # icod_ :: IsForced -> S Word32 Source # value :: Word32 -> R IsForced Source #
EmbPrj LHSOrPatSyn Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: LHSOrPatSyn -> S Word32 Source # icod_ :: LHSOrPatSyn -> S Word32 Source # value :: Word32 -> R LHSOrPatSyn Source #
EmbPrj MutualId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: MutualId -> S Word32 Source # icod_ :: MutualId -> S Word32 Source # value :: Word32 -> R MutualId Source #
EmbPrj NLPSort Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NLPSort -> S Word32 Source # icod_ :: NLPSort -> S Word32 Source # value :: Word32 -> R NLPSort Source #
EmbPrj NLPType Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NLPType -> S Word32 Source # icod_ :: NLPType -> S Word32 Source # value :: Word32 -> R NLPType Source #
EmbPrj NLPat Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NLPat -> S Word32 Source # icod_ :: NLPat -> S Word32 Source # value :: Word32 -> R NLPat Source #
EmbPrj NumGeneralizableArgs Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NumGeneralizableArgs -> S Word32 Source # icod_ :: NumGeneralizableArgs -> S Word32 Source # value :: Word32 -> R NumGeneralizableArgs Source #
EmbPrj OpaqueBlock Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: OpaqueBlock -> S Word32 Source # icod_ :: OpaqueBlock -> S Word32 Source # value :: Word32 -> R OpaqueBlock Source #
EmbPrj ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ProjLams -> S Word32 Source # icod_ :: ProjLams -> S Word32 Source # value :: Word32 -> R ProjLams Source #
EmbPrj Projection Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Projection -> S Word32 Source # icod_ :: Projection -> S Word32 Source # value :: Word32 -> R Projection Source #
EmbPrj ProjectionLikenessMissing Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ProjectionLikenessMissing -> S Word32 Source # icod_ :: ProjectionLikenessMissing -> S Word32 Source # value :: Word32 -> R ProjectionLikenessMissing Source #
EmbPrj RemoteMetaVariable Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: RemoteMetaVariable -> S Word32 Source # icod_ :: RemoteMetaVariable -> S Word32 Source # value :: Word32 -> R RemoteMetaVariable Source #
EmbPrj RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: RewriteRule -> S Word32 Source # icod_ :: RewriteRule -> S Word32 Source # value :: Word32 -> R RewriteRule Source #
EmbPrj Section Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Section -> S Word32 Source # icod_ :: Section -> S Word32 Source # value :: Word32 -> R Section Source #
EmbPrj Signature Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Signature -> S Word32 Source # icod_ :: Signature -> S Word32 Source # value :: Word32 -> R Signature Source #
EmbPrj System Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: System -> S Word32 Source # icod_ :: System -> S Word32 Source # value :: Word32 -> R System Source #
EmbPrj TCWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: TCWarning -> S Word32 Source # icod_ :: TCWarning -> S Word32 Source # value :: Word32 -> R TCWarning Source #
EmbPrj TermHead Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: TermHead -> S Word32 Source # icod_ :: TermHead -> S Word32 Source # value :: Word32 -> R TermHead Source #
EmbPrj Warning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: Warning -> S Word32 Source # icod_ :: Warning -> S Word32 Source # value :: Word32 -> R Warning Source #
EmbPrj Comparison Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Comparison -> S Word32 Source # icod_ :: Comparison -> S Word32 Source # value :: Word32 -> R Comparison Source #
EmbPrj Polarity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Polarity -> S Word32 Source # icod_ :: Polarity -> S Word32 Source # value :: Word32 -> R Polarity Source #
EmbPrj RecordFieldWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: RecordFieldWarning -> S Word32 Source # icod_ :: RecordFieldWarning -> S Word32 Source # value :: Word32 -> R RecordFieldWarning Source #
EmbPrj UselessPublicReason Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: UselessPublicReason -> S Word32 Source # icod_ :: UselessPublicReason -> S Word32 Source # value :: Word32 -> R UselessPublicReason Source #
EmbPrj Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Occurrence -> S Word32 Source # icod_ :: Occurrence -> S Word32 Source # value :: Word32 -> R Occurrence Source #
EmbPrj AbsNameWithFixity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbsNameWithFixity -> S Word32 Source # icod_ :: AbsNameWithFixity -> S Word32 Source # value :: Word32 -> R AbsNameWithFixity Source #
EmbPrj SerialisedRange Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: SerialisedRange -> S Word32 Source # icod_ :: SerialisedRange -> S Word32 Source # value :: Word32 -> R SerialisedRange Source #
EmbPrj Impossible Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Impossible -> S Word32 Source # icod_ :: Impossible -> S Word32 Source # value :: Word32 -> R Impossible Source #
EmbPrj Permutation Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Permutation -> S Word32 Source # icod_ :: Permutation -> S Word32 Source # value :: Word32 -> R Permutation Source #
EmbPrj ProfileOption Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ProfileOption -> S Word32 Source # icod_ :: ProfileOption -> S Word32 Source # value :: Word32 -> R ProfileOption Source #
EmbPrj ProfileOptions Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ProfileOptions -> S Word32 Source # icod_ :: ProfileOptions -> S Word32 Source # value :: Word32 -> R ProfileOptions Source #
EmbPrj IntSet Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IntSet -> S Word32 Source # icod_ :: IntSet -> S Word32 Source # value :: Word32 -> R IntSet Source #
EmbPrj Void Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Void -> S Word32 Source # icod_ :: Void -> S Word32 Source # value :: Word32 -> R Void Source #
EmbPrj Int32 Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Int32 -> S Word32 Source # icod_ :: Int32 -> S Word32 Source # value :: Word32 -> R Int32 Source #
EmbPrj CallStack Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: CallStack -> S Word32 Source # icod_ :: CallStack -> S Word32 Source # value :: Word32 -> R CallStack Source #
EmbPrj SrcLoc Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: SrcLoc -> S Word32 Source # icod_ :: SrcLoc -> S Word32 Source # value :: Word32 -> R SrcLoc Source #
EmbPrj Word32 Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Word32 -> S Word32 Source # icod_ :: Word32 -> S Word32 Source # value :: Word32 -> R Word32 Source #
EmbPrj Word64 Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Word64 -> S Word32 Source # icod_ :: Word64 -> S Word32 Source # value :: Word32 -> R Word64 Source #
EmbPrj Text Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Text -> S Word32 Source # icod_ :: Text -> S Word32 Source # value :: Word32 -> R Text Source #
EmbPrj Text Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Text -> S Word32 Source # icod_ :: Text -> S Word32 Source # value :: Word32 -> R Text Source #
EmbPrj Integer Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Integer -> S Word32 Source # icod_ :: Integer -> S Word32 Source # value :: Word32 -> R Integer Source #
EmbPrj String Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: String -> S Word32 Source # icod_ :: String -> S Word32 Source # value :: Word32 -> R String Source #
EmbPrj () Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: () -> S Word32 Source # icod_ :: () -> S Word32 Source # value :: Word32 -> R () Source #
EmbPrj Bool Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Bool -> S Word32 Source # icod_ :: Bool -> S Word32 Source # value :: Word32 -> R Bool Source #
EmbPrj Char Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Char -> S Word32 Source # icod_ :: Char -> S Word32 Source # value :: Word32 -> R Char Source #
EmbPrj Double Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Double -> S Word32 Source # icod_ :: Double -> S Word32 Source # value :: Word32 -> R Double Source #
EmbPrj Int Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Int -> S Word32 Source # icod_ :: Int -> S Word32 Source # value :: Word32 -> R Int Source #
EmbPrj a => EmbPrj (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Pattern' a -> S Word32 Source # icod_ :: Pattern' a -> S Word32 Source # value :: Word32 -> R (Pattern' a) Source #
EmbPrj a => EmbPrj (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Arg a -> S Word32 Source # icod_ :: Arg a -> S Word32 Source # value :: Word32 -> R (Arg a) Source #
EmbPrj a => EmbPrj (HasEta' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: HasEta' a -> S Word32 Source # icod_ :: HasEta' a -> S Word32 Source # value :: Word32 -> R (HasEta' a) Source #
EmbPrj a => EmbPrj (Ranged a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Ranged a -> S Word32 Source # icod_ :: Ranged a -> S Word32 Source # value :: Word32 -> R (Ranged a) Source #
EmbPrj a => EmbPrj (RecordDirectives' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: RecordDirectives' a -> S Word32 Source # icod_ :: RecordDirectives' a -> S Word32 Source # value :: Word32 -> R (RecordDirectives' a) Source #
EmbPrj a => EmbPrj (WithHiding a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: WithHiding a -> S Word32 Source # icod_ :: WithHiding a -> S Word32 Source # value :: Word32 -> R (WithHiding a) Source #
EmbPrj a => EmbPrj (WithOrigin a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: WithOrigin a -> S Word32 Source # icod_ :: WithOrigin a -> S Word32 Source # value :: Word32 -> R (WithOrigin a) Source #
EmbPrj a => EmbPrj (FieldAssignment' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FieldAssignment' a -> S Word32 Source # icod_ :: FieldAssignment' a -> S Word32 Source # value :: Word32 -> R (FieldAssignment' a) Source #
EmbPrj a => EmbPrj (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Abs a -> S Word32 Source # icod_ :: Abs a -> S Word32 Source # value :: Word32 -> R (Abs a) Source #
EmbPrj a => EmbPrj (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Dom a -> S Word32 Source # icod_ :: Dom a -> S Word32 Source # value :: Word32 -> R (Dom a) Source #
EmbPrj a => EmbPrj (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Pattern' a -> S Word32 Source # icod_ :: Pattern' a -> S Word32 Source # value :: Word32 -> R (Pattern' a) Source #
EmbPrj a => EmbPrj (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Substitution' a -> S Word32 Source # icod_ :: Substitution' a -> S Word32 Source # value :: Word32 -> R (Substitution' a) Source #
EmbPrj a => EmbPrj (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Tele a -> S Word32 Source # icod_ :: Tele a -> S Word32 Source # value :: Word32 -> R (Tele a) Source #
EmbPrj a => EmbPrj (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Type' a -> S Word32 Source # icod_ :: Type' a -> S Word32 Source # value :: Word32 -> R (Type' a) Source #
EmbPrj a => EmbPrj (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Elim' a -> S Word32 Source # icod_ :: Elim' a -> S Word32 Source # value :: Word32 -> R (Elim' a) Source #
EmbPrj a => EmbPrj (Interval' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Interval' a -> S Word32 Source # icod_ :: Interval' a -> S Word32 Source # value :: Word32 -> R (Interval' a) Source #
EmbPrj a => EmbPrj (Position' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Position' a -> S Word32 Source # icod_ :: Position' a -> S Word32 Source # value :: Word32 -> R (Position' a) Source #
EmbPrj a => EmbPrj (Case a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Case a -> S Word32 Source # icod_ :: Case a -> S Word32 Source # value :: Word32 -> R (Case a) Source #
EmbPrj a => EmbPrj (WithArity a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: WithArity a -> S Word32 Source # icod_ :: WithArity a -> S Word32 Source # value :: Word32 -> R (WithArity a) Source #
EmbPrj a => EmbPrj (SplitTree' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: SplitTree' a -> S Word32 Source # icod_ :: SplitTree' a -> S Word32 Source # value :: Word32 -> R (SplitTree' a) Source #
(EmbPrj a, Ord a) => EmbPrj (DiscrimTree a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DiscrimTree a -> S Word32 Source # icod_ :: DiscrimTree a -> S Word32 Source # value :: Word32 -> R (DiscrimTree a) Source #
EmbPrj a => EmbPrj (Builtin a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Builtin a -> S Word32 Source # icod_ :: Builtin a -> S Word32 Source # value :: Word32 -> R (Builtin a) Source #
EmbPrj a => EmbPrj (FunctionInverse' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: FunctionInverse' a -> S Word32 Source # icod_ :: FunctionInverse' a -> S Word32 Source # value :: Word32 -> R (FunctionInverse' a) Source #
EmbPrj a => EmbPrj (Judgement a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Judgement a -> S Word32 Source # icod_ :: Judgement a -> S Word32 Source # value :: Word32 -> R (Judgement a) Source #
EmbPrj a => EmbPrj (Open a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Open a -> S Word32 Source # icod_ :: Open a -> S Word32 Source # value :: Word32 -> R (Open a) Source #
EmbPrj a => EmbPrj (List1 a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: List1 a -> S Word32 Source # icod_ :: List1 a -> S Word32 Source # value :: Word32 -> R (List1 a) Source #
EmbPrj a => EmbPrj (List2 a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: List2 a -> S Word32 Source # icod_ :: List2 a -> S Word32 Source # value :: Word32 -> R (List2 a) Source #
EmbPrj a => EmbPrj (Drop a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Drop a -> S Word32 Source # icod_ :: Drop a -> S Word32 Source # value :: Word32 -> R (Drop a) Source #
EmbPrj a => EmbPrj (RangeMap a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: RangeMap a -> S Word32 Source # icod_ :: RangeMap a -> S Word32 Source # value :: Word32 -> R (RangeMap a) Source #
(Ord a, EmbPrj a) => EmbPrj (Set1 a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Set1 a -> S Word32 Source # icod_ :: Set1 a -> S Word32 Source # value :: Word32 -> R (Set1 a) Source #
Typeable a => EmbPrj (SmallSet a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: SmallSet a -> S Word32 Source # icod_ :: SmallSet a -> S Word32 Source # value :: Word32 -> R (SmallSet a) Source #
EmbPrj a => EmbPrj (Seq a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Seq a -> S Word32 Source # icod_ :: Seq a -> S Word32 Source # value :: Word32 -> R (Seq a) Source #
(Ord a, EmbPrj a) => EmbPrj (Set a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Set a -> S Word32 Source # icod_ :: Set a -> S Word32 Source # value :: Word32 -> R (Set a) Source #
EmbPrj a => EmbPrj (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Maybe a -> S Word32 Source # icod_ :: Maybe a -> S Word32 Source # value :: Word32 -> R (Maybe a) Source #
EmbPrj a => EmbPrj (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Maybe a -> S Word32 Source # icod_ :: Maybe a -> S Word32 Source # value :: Word32 -> R (Maybe a) Source #
EmbPrj a => EmbPrj [a] Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: [a] -> S Word32 Source # icod_ :: [a] -> S Word32 Source # value :: Word32 -> R [a] Source #
(EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ImportedName' a b -> S Word32 Source # icod_ :: ImportedName' a b -> S Word32 Source # value :: Word32 -> R (ImportedName' a b) Source #
(EmbPrj s, EmbPrj t) => EmbPrj (Named s t) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Named s t -> S Word32 Source # icod_ :: Named s t -> S Word32 Source # value :: Word32 -> R (Named s t) Source #
(EmbPrj k, EmbPrj v, EmbPrj (Tag v)) => EmbPrj (BiMap k v) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: BiMap k v -> S Word32 Source # icod_ :: BiMap k v -> S Word32 Source # value :: Word32 -> R (BiMap k v) Source #
(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Trie a b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Trie a b -> S Word32 Source # icod_ :: Trie a b -> S Word32 Source # value :: Word32 -> R (Trie a b) Source #
(EmbPrj a, Typeable b) => EmbPrj (WithDefault' a b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: WithDefault' a b -> S Word32 Source # icod_ :: WithDefault' a b -> S Word32 Source # value :: Word32 -> R (WithDefault' a b) Source #
(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Map a b -> S Word32 Source # icod_ :: Map a b -> S Word32 Source # value :: Word32 -> R (Map a b) Source #
(EmbPrj a, EmbPrj b) => EmbPrj (Either a b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Either a b -> S Word32 Source # icod_ :: Either a b -> S Word32 Source # value :: Word32 -> R (Either a b) Source #
(EmbPrj a, EmbPrj b) => EmbPrj (Pair a b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Pair a b -> S Word32 Source # icod_ :: Pair a b -> S Word32 Source # value :: Word32 -> R (Pair a b) Source #
(Eq k, Hashable k, EmbPrj k, EmbPrj v) => EmbPrj (HashMap k v) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: HashMap k v -> S Word32 Source # icod_ :: HashMap k v -> S Word32 Source # value :: Word32 -> R (HashMap k v) Source #
(EmbPrj a, EmbPrj b) => EmbPrj (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: (a, b) -> S Word32 Source # icod_ :: (a, b) -> S Word32 Source # value :: Word32 -> R (a, b) Source #
(EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj (a, b, c) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: (a, b, c) -> S Word32 Source # icod_ :: (a, b, c) -> S Word32 Source # value :: Word32 -> R (a, b, c) Source #