Agda.TypeChecking.Serialise

Structure-sharing serialisation of Agda interface files.

Documentation

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

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

encodeFile :: FilePath -> Interface -> TCM ByteString

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

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

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)

decodeInterface :: ByteString -> TCM (Maybe Interface)

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)

class Typeable a => EmbPrj a

Instances

EmbPrj Bool

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Bool -> S Int32

icod_ :: Bool -> S Int32

value :: Int32 -> R Bool

EmbPrj Char

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Char -> S Int32

icod_ :: Char -> S Int32

value :: Int32 -> R Char

EmbPrj Double

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Double -> S Int32

icod_ :: Double -> S Int32

value :: Int32 -> R Double

EmbPrj Int

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Int -> S Int32

icod_ :: Int -> S Int32

value :: Int32 -> R Int

EmbPrj Int32

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Int32 -> S Int32

icod_ :: Int32 -> S Int32

value :: Int32 -> R Int32

EmbPrj Integer

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Integer -> S Int32

icod_ :: Integer -> S Int32

value :: Int32 -> R Integer

EmbPrj Word64

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Word64 -> S Int32

icod_ :: Word64 -> S Int32

value :: Int32 -> R Word64

EmbPrj ()

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: () -> S Int32

icod_ :: () -> S Int32

value :: Int32 -> R ()

EmbPrj Void

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Void -> S Int32

icod_ :: Void -> S Int32

value :: Int32 -> R Void

EmbPrj String

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: String -> S Int32

icod_ :: String -> S Int32

value :: Int32 -> R String

EmbPrj IntSet

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: IntSet -> S Int32

icod_ :: IntSet -> S Int32

value :: Int32 -> R IntSet

EmbPrj Doc

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Doc -> S Int32

icod_ :: Doc -> S Int32

value :: Int32 -> R Doc

EmbPrj Text

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Text -> S Int32

icod_ :: Text -> S Int32

value :: Int32 -> R Text

EmbPrj CutOff

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: CutOff -> S Int32

icod_ :: CutOff -> S Int32

value :: Int32 -> R CutOff

EmbPrj Impossible

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Impossible -> S Int32

icod_ :: Impossible -> S Int32

value :: Int32 -> R Impossible

EmbPrj Empty

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Empty -> S Int32

icod_ :: Empty -> S Int32

value :: Int32 -> R Empty

EmbPrj WarningName

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningName -> S Int32

icod_ :: WarningName -> S Int32

value :: Int32 -> R WarningName

EmbPrj WarningMode

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningMode -> S Int32

icod_ :: WarningMode -> S Int32

value :: Int32 -> R WarningMode

EmbPrj AbsolutePath

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: AbsolutePath -> S Int32

icod_ :: AbsolutePath -> S Int32

value :: Int32 -> R AbsolutePath

EmbPrj Range

Ranges are always deserialised as noRange.

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Range -> S Int32

icod_ :: Range -> S Int32

value :: Int32 -> R Range

EmbPrj Permutation

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Permutation -> S Int32

icod_ :: Permutation -> S Int32

value :: Int32 -> R Permutation

EmbPrj GenPart

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: GenPart -> S Int32

icod_ :: GenPart -> S Int32

value :: Int32 -> R GenPart

EmbPrj ExpandedEllipsis

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ExpandedEllipsis -> S Int32

icod_ :: ExpandedEllipsis -> S Int32

value :: Int32 -> R ExpandedEllipsis

EmbPrj Fixity'

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Fixity' -> S Int32

icod_ :: Fixity' -> S Int32

value :: Int32 -> R Fixity'

EmbPrj Fixity

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Fixity -> S Int32

icod_ :: Fixity -> S Int32

value :: Int32 -> R Fixity

EmbPrj Associativity

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Associativity -> S Int32

icod_ :: Associativity -> S Int32

value :: Int32 -> R Associativity

EmbPrj FixityLevel

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FixityLevel -> S Int32

icod_ :: FixityLevel -> S Int32

value :: Int32 -> R FixityLevel

EmbPrj MetaId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: MetaId -> S Int32

icod_ :: MetaId -> S Int32

value :: Int32 -> R MetaId

EmbPrj NameId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NameId -> S Int32

icod_ :: NameId -> S Int32

value :: Int32 -> R NameId

EmbPrj IsAbstract

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: IsAbstract -> S Int32

icod_ :: IsAbstract -> S Int32

value :: Int32 -> R IsAbstract

EmbPrj Access

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Access -> S Int32

icod_ :: Access -> S Int32

value :: Int32 -> R Access

EmbPrj DataOrRecord

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: DataOrRecord -> S Int32

icod_ :: DataOrRecord -> S Int32

value :: Int32 -> R DataOrRecord

EmbPrj ProjOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ProjOrigin -> S Int32

icod_ :: ProjOrigin -> S Int32

value :: Int32 -> R ProjOrigin

EmbPrj ConOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ConOrigin -> S Int32

icod_ :: ConOrigin -> S Int32

value :: Int32 -> R ConOrigin

EmbPrj ArgInfo

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ArgInfo -> S Int32

icod_ :: ArgInfo -> S Int32

value :: Int32 -> R ArgInfo

EmbPrj FreeVariables

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FreeVariables -> S Int32

icod_ :: FreeVariables -> S Int32

value :: Int32 -> R FreeVariables

EmbPrj Origin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Origin -> S Int32

icod_ :: Origin -> S Int32

value :: Int32 -> R Origin

EmbPrj Cohesion

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Cohesion -> S Int32

icod_ :: Cohesion -> S Int32

value :: Int32 -> R Cohesion

EmbPrj Relevance

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Relevance -> S Int32

icod_ :: Relevance -> S Int32

value :: Int32 -> R Relevance

EmbPrj Quantity

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Quantity -> S Int32

icod_ :: Quantity -> S Int32

value :: Int32 -> R Quantity

EmbPrj QωOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QωOrigin -> S Int32

icod_ :: QωOrigin -> S Int32

value :: Int32 -> R QωOrigin

EmbPrj Q1Origin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Q1Origin -> S Int32

icod_ :: Q1Origin -> S Int32

value :: Int32 -> R Q1Origin

EmbPrj Q0Origin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Q0Origin -> S Int32

icod_ :: Q0Origin -> S Int32

value :: Int32 -> R Q0Origin

EmbPrj Modality

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Modality -> S Int32

icod_ :: Modality -> S Int32

value :: Int32 -> R Modality

EmbPrj Hiding

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Hiding -> S Int32

icod_ :: Hiding -> S Int32

value :: Int32 -> R Hiding

EmbPrj Induction

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Induction -> S Int32

icod_ :: Induction -> S Int32

value :: Int32 -> R Induction

EmbPrj HasEta

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: HasEta -> S Int32

icod_ :: HasEta -> S Int32

value :: Int32 -> R HasEta

EmbPrj FileType

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FileType -> S Int32

icod_ :: FileType -> S Int32

value :: Int32 -> R FileType

EmbPrj Delayed

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Delayed -> S Int32

icod_ :: Delayed -> S Int32

value :: Int32 -> R Delayed

EmbPrj NameInScope

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NameInScope -> S Int32

icod_ :: NameInScope -> S Int32

value :: Int32 -> R NameInScope

EmbPrj TopLevelModuleName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: TopLevelModuleName -> S Int32

icod_ :: TopLevelModuleName -> S Int32

value :: Int32 -> R TopLevelModuleName

EmbPrj QName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QName -> S Int32

icod_ :: QName -> S Int32

value :: Int32 -> R QName

EmbPrj NamePart

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NamePart -> S Int32

icod_ :: NamePart -> S Int32

value :: Int32 -> R NamePart

EmbPrj Name

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32

icod_ :: Name -> S Int32

value :: Int32 -> R Name

EmbPrj Polarity

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Polarity -> S Int32

icod_ :: Polarity -> S Int32

value :: Int32 -> R Polarity

EmbPrj TCWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: TCWarning -> S Int32

icod_ :: TCWarning -> S Int32

value :: Int32 -> R TCWarning

EmbPrj Warning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Warning -> S Int32

icod_ :: Warning -> S Int32

value :: Int32 -> R Warning

EmbPrj Range

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Range -> S Int32

icod_ :: Range -> S Int32

value :: Int32 -> R Range

EmbPrj AmbiguousQName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: AmbiguousQName -> S Int32

icod_ :: AmbiguousQName -> S Int32

value :: Int32 -> R AmbiguousQName

EmbPrj ModuleName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ModuleName -> S Int32

icod_ :: ModuleName -> S Int32

value :: Int32 -> R ModuleName

EmbPrj QName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QName -> S Int32

icod_ :: QName -> S Int32

value :: Int32 -> R QName

EmbPrj Name

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32

icod_ :: Name -> S Int32

value :: Int32 -> R Name

EmbPrj Precedence

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Precedence -> S Int32

icod_ :: Precedence -> S Int32

value :: Int32 -> R Precedence

EmbPrj ParenPreference

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ParenPreference -> S Int32

icod_ :: ParenPreference -> S Int32

value :: Int32 -> R ParenPreference

EmbPrj Literal

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Literal -> S Int32

icod_ :: Literal -> S Int32

value :: Int32 -> R Literal

EmbPrj LibWarning'

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning' -> S Int32

icod_ :: LibWarning' -> S Int32

value :: Int32 -> R LibWarning'

EmbPrj Occurrence

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Occurrence -> S Int32

icod_ :: Occurrence -> S Int32

value :: Int32 -> R Occurrence

EmbPrj SplitTag

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: SplitTag -> S Int32

icod_ :: SplitTag -> S Int32

value :: Int32 -> R SplitTag

EmbPrj LazySplit

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: LazySplit -> S Int32

icod_ :: LazySplit -> S Int32

value :: Int32 -> R LazySplit

EmbPrj CompressedFile

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: CompressedFile -> S Int32

icod_ :: CompressedFile -> S Int32

value :: Int32 -> R CompressedFile

EmbPrj TokenBased

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: TokenBased -> S Int32

icod_ :: TokenBased -> S Int32

value :: Int32 -> R TokenBased

EmbPrj DefinitionSite

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: DefinitionSite -> S Int32

icod_ :: DefinitionSite -> S Int32

value :: Int32 -> R DefinitionSite

EmbPrj Aspects

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspects -> S Int32

icod_ :: Aspects -> S Int32

value :: Int32 -> R Aspects

EmbPrj OtherAspect

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: OtherAspect -> S Int32

icod_ :: OtherAspect -> S Int32

value :: Int32 -> R OtherAspect

EmbPrj NameKind

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: NameKind -> S Int32

icod_ :: NameKind -> S Int32

value :: Int32 -> R NameKind

EmbPrj Aspect

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspect -> S Int32

icod_ :: Aspect -> S Int32

value :: Int32 -> R Aspect

EmbPrj AbstractModule

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractModule -> S Int32

icod_ :: AbstractModule -> S Int32

value :: Int32 -> R AbstractModule

EmbPrj NameMetadata

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameMetadata -> S Int32

icod_ :: NameMetadata -> S Int32

value :: Int32 -> R NameMetadata

EmbPrj AbstractName

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractName -> S Int32

icod_ :: AbstractName -> S Int32

value :: Int32 -> R AbstractName

EmbPrj WhyInScope

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: WhyInScope -> S Int32

icod_ :: WhyInScope -> S Int32

value :: Int32 -> R WhyInScope

EmbPrj KindOfName

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: KindOfName -> S Int32

icod_ :: KindOfName -> S Int32

value :: Int32 -> R KindOfName

EmbPrj NameOrModule

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameOrModule -> S Int32

icod_ :: NameOrModule -> S Int32

value :: Int32 -> R NameOrModule

EmbPrj NameSpace

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameSpace -> S Int32

icod_ :: NameSpace -> S Int32

value :: Int32 -> R NameSpace

EmbPrj LocalVar

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: LocalVar -> S Int32

icod_ :: LocalVar -> S Int32

value :: Int32 -> R LocalVar

EmbPrj BindingSource

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindingSource -> S Int32

icod_ :: BindingSource -> S Int32

value :: Int32 -> R BindingSource

EmbPrj ScopeInfo

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ScopeInfo -> S Int32

icod_ :: ScopeInfo -> S Int32

value :: Int32 -> R ScopeInfo

EmbPrj NameSpaceId

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameSpaceId -> S Int32

icod_ :: NameSpaceId -> S Int32

value :: Int32 -> R NameSpaceId

EmbPrj Scope

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Scope -> S Int32

icod_ :: Scope -> S Int32

value :: Int32 -> R Scope

EmbPrj ConPatLazy

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ConPatLazy -> S Int32

icod_ :: ConPatLazy -> S Int32

value :: Int32 -> R ConPatLazy

EmbPrj ConPatInfo

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ConPatInfo -> S Int32

icod_ :: ConPatInfo -> S Int32

value :: Int32 -> R ConPatInfo

EmbPrj ConPatternInfo

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ConPatternInfo -> S Int32

icod_ :: ConPatternInfo -> S Int32

value :: Int32 -> R ConPatternInfo

EmbPrj DBPatVar

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DBPatVar -> S Int32

icod_ :: DBPatVar -> S Int32

value :: Int32 -> R DBPatVar

EmbPrj PatOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PatOrigin -> S Int32

icod_ :: PatOrigin -> S Int32

value :: Int32 -> R PatOrigin

EmbPrj PatternInfo

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PatternInfo -> S Int32

icod_ :: PatternInfo -> S Int32

value :: Int32 -> R PatternInfo

EmbPrj Clause

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Clause -> S Int32

icod_ :: Clause -> S Int32

value :: Int32 -> R Clause

EmbPrj Blocked_

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Blocked_ -> S Int32

icod_ :: Blocked_ -> S Int32

value :: Int32 -> R Blocked_

EmbPrj NotBlocked

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NotBlocked -> S Int32

icod_ :: NotBlocked -> S Int32

value :: Int32 -> R NotBlocked

EmbPrj LevelAtom

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: LevelAtom -> S Int32

icod_ :: LevelAtom -> S Int32

value :: Int32 -> R LevelAtom

EmbPrj PlusLevel

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PlusLevel -> S Int32

icod_ :: PlusLevel -> S Int32

value :: Int32 -> R PlusLevel

EmbPrj Level

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Level -> S Int32

icod_ :: Level -> S Int32

value :: Int32 -> R Level

EmbPrj Sort

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Sort -> S Int32

icod_ :: Sort -> S Int32

value :: Int32 -> R Sort

EmbPrj Term

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Term -> S Int32

icod_ :: Term -> S Int32

value :: Int32 -> R Term

EmbPrj ConHead

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ConHead -> S Int32

icod_ :: ConHead -> S Int32

value :: Int32 -> R ConHead

EmbPrj CompiledClauses

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompiledClauses -> S Int32

icod_ :: CompiledClauses -> S Int32

value :: Int32 -> R CompiledClauses

EmbPrj BindName

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindName -> S Int32

icod_ :: BindName -> S Int32

value :: Int32 -> R BindName

EmbPrj DeclarationWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: DeclarationWarning -> S Int32

icod_ :: DeclarationWarning -> S Int32

value :: Int32 -> R DeclarationWarning

EmbPrj LibWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning -> S Int32

icod_ :: LibWarning -> S Int32

value :: Int32 -> R LibWarning

EmbPrj LibPositionInfo

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibPositionInfo -> S Int32

icod_ :: LibPositionInfo -> S Int32

value :: Int32 -> R LibPositionInfo

EmbPrj PragmaOptions

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: PragmaOptions -> S Int32

icod_ :: PragmaOptions -> S Int32

value :: Int32 -> R PragmaOptions

EmbPrj MutualId

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: MutualId -> S Int32

icod_ :: MutualId -> S Int32

value :: Int32 -> R MutualId

EmbPrj TermHead

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: TermHead -> S Int32

icod_ :: TermHead -> S Int32

value :: Int32 -> R TermHead

EmbPrj Defn

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Defn -> S Int32

icod_ :: Defn -> S Int32

value :: Int32 -> R Defn

EmbPrj CompKit

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompKit -> S Int32

icod_ :: CompKit -> S Int32

value :: Int32 -> R CompKit

EmbPrj FunctionFlag

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: FunctionFlag -> S Int32

icod_ :: FunctionFlag -> S Int32

value :: Int32 -> R FunctionFlag

EmbPrj EtaEquality

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: EtaEquality -> S Int32

icod_ :: EtaEquality -> S Int32

value :: Int32 -> R EtaEquality

EmbPrj ProjLams

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ProjLams -> S Int32

icod_ :: ProjLams -> S Int32

value :: Int32 -> R ProjLams

EmbPrj Projection

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Projection -> S Int32

icod_ :: Projection -> S Int32

value :: Int32 -> R Projection

EmbPrj ExtLamInfo

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ExtLamInfo -> S Int32

icod_ :: ExtLamInfo -> S Int32

value :: Int32 -> R ExtLamInfo

EmbPrj System

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: System -> S Int32

icod_ :: System -> S Int32

value :: Int32 -> R System

EmbPrj CompilerPragma

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

Methods

icode :: CompilerPragma -> S Int32

icod_ :: CompilerPragma -> S Int32

value :: Int32 -> R CompilerPragma

EmbPrj IsForced

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: IsForced -> S Int32

icod_ :: IsForced -> S Int32

value :: Int32 -> R IsForced

EmbPrj NumGeneralizableArgs

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NumGeneralizableArgs -> S Int32

icod_ :: NumGeneralizableArgs -> S Int32

value :: Int32 -> R NumGeneralizableArgs

EmbPrj Definition

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Definition -> S Int32

icod_ :: Definition -> S Int32

value :: Int32 -> R Definition

EmbPrj RewriteRule

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: RewriteRule -> S Int32

icod_ :: RewriteRule -> S Int32

value :: Int32 -> R RewriteRule

EmbPrj NLPSort

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NLPSort -> S Int32

icod_ :: NLPSort -> S Int32

value :: Int32 -> R NLPSort

EmbPrj NLPType

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NLPType -> S Int32

icod_ :: NLPType -> S Int32

value :: Int32 -> R NLPType

EmbPrj NLPat

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NLPat -> S Int32

icod_ :: NLPat -> S Int32

value :: Int32 -> R NLPat

EmbPrj DisplayTerm

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DisplayTerm -> S Int32

icod_ :: DisplayTerm -> S Int32

value :: Int32 -> R DisplayTerm

EmbPrj DisplayForm

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DisplayForm -> S Int32

icod_ :: DisplayForm -> S Int32

value :: Int32 -> R DisplayForm

EmbPrj Section

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Section -> S Int32

icod_ :: Section -> S Int32

value :: Int32 -> R Section

EmbPrj Signature

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Signature -> S Int32

icod_ :: Signature -> S Int32

value :: Int32 -> R Signature

EmbPrj DoGeneralize

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DoGeneralize -> S Int32

icod_ :: DoGeneralize -> S Int32

value :: Int32 -> R DoGeneralize

EmbPrj Interface

Defined in Agda.TypeChecking.Serialise.Instances

Methods

icode :: Interface -> S Int32

icod_ :: Interface -> S Int32

value :: Int32 -> R Interface

EmbPrj ForeignCode

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

Methods

icode :: ForeignCode -> S Int32

icod_ :: ForeignCode -> S Int32

value :: Int32 -> R ForeignCode

EmbPrj CheckpointId

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CheckpointId -> S Int32

icod_ :: CheckpointId -> S Int32

value :: Int32 -> R CheckpointId

EmbPrj SerialisedRange

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: SerialisedRange -> S Int32

icod_ :: SerialisedRange -> S Int32

value :: Int32 -> R SerialisedRange

EmbPrj AbsNameWithFixity

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbsNameWithFixity -> S Int32

icod_ :: AbsNameWithFixity -> S Int32

value :: Int32 -> R AbsNameWithFixity

EmbPrj a => EmbPrj [a]

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: [a] -> S Int32

icod_ :: [a] -> S Int32

value :: Int32 -> R [a]

EmbPrj a => EmbPrj (Maybe a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Maybe a -> S Int32

icod_ :: Maybe a -> S Int32

value :: Int32 -> R (Maybe a)

EmbPrj a => EmbPrj (NonEmpty a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NonEmpty a -> S Int32

icod_ :: NonEmpty a -> S Int32

value :: Int32 -> R (NonEmpty a)

EmbPrj a => EmbPrj (Seq a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Seq a -> S Int32

icod_ :: Seq a -> S Int32

value :: Int32 -> R (Seq a)

(Ord a, EmbPrj a) => EmbPrj (Set a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Set a -> S Int32

icod_ :: Set a -> S Int32

value :: Int32 -> R (Set a)

EmbPrj a => EmbPrj (Maybe a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Maybe a -> S Int32

icod_ :: Maybe a -> S Int32

value :: Int32 -> R (Maybe a)

EmbPrj a => EmbPrj (Interval' a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Interval' a -> S Int32

icod_ :: Interval' a -> S Int32

value :: Int32 -> R (Interval' a)

EmbPrj a => EmbPrj (Position' a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Position' a -> S Int32

icod_ :: Position' a -> S Int32

value :: Int32 -> R (Position' a)

EmbPrj a => EmbPrj (Drop a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Drop a -> S Int32

icod_ :: Drop a -> S Int32

value :: Int32 -> R (Drop a)

EmbPrj a => EmbPrj (Ranged a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Ranged a -> S Int32

icod_ :: Ranged a -> S Int32

value :: Int32 -> R (Ranged a)

EmbPrj a => EmbPrj (Arg a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Arg a -> S Int32

icod_ :: Arg a -> S Int32

value :: Int32 -> R (Arg a)

EmbPrj a => EmbPrj (WithOrigin a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: WithOrigin a -> S Int32

icod_ :: WithOrigin a -> S Int32

value :: Int32 -> R (WithOrigin a)

EmbPrj a => EmbPrj (WithHiding a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: WithHiding a -> S Int32

icod_ :: WithHiding a -> S Int32

value :: Int32 -> R (WithHiding a)

EmbPrj a => EmbPrj (FieldAssignment' a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FieldAssignment' a -> S Int32

icod_ :: FieldAssignment' a -> S Int32

value :: Int32 -> R (FieldAssignment' a)

EmbPrj a => EmbPrj (SplitTree' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: SplitTree' a -> S Int32

icod_ :: SplitTree' a -> S Int32

value :: Int32 -> R (SplitTree' a)

EmbPrj a => EmbPrj (Substitution' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Substitution' a -> S Int32

icod_ :: Substitution' a -> S Int32

value :: Int32 -> R (Substitution' a)

EmbPrj a => EmbPrj (Pattern' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Pattern' a -> S Int32

icod_ :: Pattern' a -> S Int32

value :: Int32 -> R (Pattern' a)

EmbPrj a => EmbPrj (Tele a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Tele a -> S Int32

icod_ :: Tele a -> S Int32

value :: Int32 -> R (Tele a)

EmbPrj a => EmbPrj (Type' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Type' a -> S Int32

icod_ :: Type' a -> S Int32

value :: Int32 -> R (Type' a)

EmbPrj a => EmbPrj (Abs a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Abs a -> S Int32

icod_ :: Abs a -> S Int32

value :: Int32 -> R (Abs a)

EmbPrj a => EmbPrj (Elim' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Elim' a -> S Int32

icod_ :: Elim' a -> S Int32

value :: Int32 -> R (Elim' a)

EmbPrj a => EmbPrj (Dom a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Int32

icod_ :: Dom a -> S Int32

value :: Int32 -> R (Dom a)

EmbPrj a => EmbPrj (Case a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Case a -> S Int32

icod_ :: Case a -> S Int32

value :: Int32 -> R (Case a)

EmbPrj a => EmbPrj (WithArity a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: WithArity a -> S Int32

icod_ :: WithArity a -> S Int32

value :: Int32 -> R (WithArity a)

EmbPrj a => EmbPrj (Pattern' a)

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Pattern' a -> S Int32

icod_ :: Pattern' a -> S Int32

value :: Int32 -> R (Pattern' a)

Typeable b => EmbPrj (WithDefault b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: WithDefault b -> S Int32

icod_ :: WithDefault b -> S Int32

value :: Int32 -> R (WithDefault b)

EmbPrj a => EmbPrj (Builtin a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Builtin a -> S Int32

icod_ :: Builtin a -> S Int32

value :: Int32 -> R (Builtin a)

EmbPrj a => EmbPrj (FunctionInverse' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: FunctionInverse' a -> S Int32

icod_ :: FunctionInverse' a -> S Int32

value :: Int32 -> R (FunctionInverse' a)

EmbPrj a => EmbPrj (Open a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Open a -> S Int32

icod_ :: Open a -> S Int32

value :: Int32 -> R (Open a)

(EmbPrj a, EmbPrj b) => EmbPrj (Either a b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Either a b -> S Int32

icod_ :: Either a b -> S Int32

value :: Int32 -> R (Either a b)

(EmbPrj a, EmbPrj b) => EmbPrj (a, b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: (a, b) -> S Int32

icod_ :: (a, b) -> S Int32

value :: Int32 -> R (a, b)

(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Map a b -> S Int32

icod_ :: Map a b -> S Int32

value :: Int32 -> R (Map a b)

(Ord a, Ord b, EmbPrj a, EmbPrj b) => EmbPrj (BiMap a b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: BiMap a b -> S Int32

icod_ :: BiMap a b -> S Int32

value :: Int32 -> R (BiMap a b)

(Eq k, Hashable k, EmbPrj k, EmbPrj v) => EmbPrj (HashMap k v)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: HashMap k v -> S Int32

icod_ :: HashMap k v -> S Int32

value :: Int32 -> R (HashMap k v)

(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Trie a b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Trie a b -> S Int32

icod_ :: Trie a b -> S Int32

value :: Int32 -> R (Trie a b)

(EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ImportedName' a b -> S Int32

icod_ :: ImportedName' a b -> S Int32

value :: Int32 -> R (ImportedName' a b)

(EmbPrj s, EmbPrj t) => EmbPrj (Named s t)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Named s t -> S Int32

icod_ :: Named s t -> S Int32

value :: Int32 -> R (Named s t)

(EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj (a, b, c)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: (a, b, c) -> S Int32

icod_ :: (a, b, c) -> S Int32

value :: Int32 -> R (a, b, c)