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 Aspect

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspect -> S Int32

icod_ :: Aspect -> S Int32

value :: Int32 -> R Aspect

EmbPrj Aspects

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspects -> S Int32

icod_ :: Aspects -> S Int32

value :: Int32 -> R Aspects

EmbPrj DefinitionSite

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: DefinitionSite -> S Int32

icod_ :: DefinitionSite -> S Int32

value :: Int32 -> R DefinitionSite

EmbPrj NameKind

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: NameKind -> S Int32

icod_ :: NameKind -> S Int32

value :: Int32 -> R NameKind

EmbPrj OtherAspect

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: OtherAspect -> S Int32

icod_ :: OtherAspect -> S Int32

value :: Int32 -> R OtherAspect

EmbPrj TokenBased

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: TokenBased -> S Int32

icod_ :: TokenBased -> S Int32

value :: Int32 -> R TokenBased

EmbPrj Range

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Range -> S Int32

icod_ :: Range -> S Int32

value :: Int32 -> R Range

EmbPrj ExecutablesFile

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ExecutablesFile -> S Int32

icod_ :: ExecutablesFile -> S Int32

value :: Int32 -> R ExecutablesFile

EmbPrj LibPositionInfo

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibPositionInfo -> S Int32

icod_ :: LibPositionInfo -> S Int32

value :: Int32 -> R LibPositionInfo

EmbPrj LibWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning -> S Int32

icod_ :: LibWarning -> S Int32

value :: Int32 -> R LibWarning

EmbPrj LibWarning'

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning' -> S Int32

icod_ :: LibWarning' -> S Int32

value :: Int32 -> R LibWarning'

EmbPrj ConfluenceCheck

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ConfluenceCheck -> S Int32

icod_ :: ConfluenceCheck -> S Int32

value :: Int32 -> R ConfluenceCheck

EmbPrj InfectiveCoinfective

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: InfectiveCoinfective -> S Int32

icod_ :: InfectiveCoinfective -> S Int32

value :: Int32 -> R InfectiveCoinfective

EmbPrj PragmaOptions

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: PragmaOptions -> S Int32

icod_ :: PragmaOptions -> S Int32

value :: Int32 -> R PragmaOptions

EmbPrj WarningMode

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningMode -> S Int32

icod_ :: WarningMode -> S Int32

value :: Int32 -> R WarningMode

EmbPrj WarningName

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningName -> S Int32

icod_ :: WarningName -> S Int32

value :: Int32 -> R WarningName

EmbPrj BindName

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindName -> S Int32

icod_ :: BindName -> S Int32

value :: Int32 -> R BindName

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 Name

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32

icod_ :: Name -> S Int32

value :: Int32 -> R Name

EmbPrj QName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QName -> S Int32

icod_ :: QName -> S Int32

value :: Int32 -> R QName

EmbPrj Suffix

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Suffix -> S Int32

icod_ :: Suffix -> S Int32

value :: Int32 -> R Suffix

EmbPrj Access

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Access -> S Int32

icod_ :: Access -> S Int32

value :: Int32 -> R Access

EmbPrj Annotation

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Annotation -> S Int32

icod_ :: Annotation -> S Int32

value :: Int32 -> R Annotation

EmbPrj ArgInfo

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ArgInfo -> S Int32

icod_ :: ArgInfo -> S Int32

value :: Int32 -> R ArgInfo

EmbPrj Associativity

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Associativity -> S Int32

icod_ :: Associativity -> S Int32

value :: Int32 -> R Associativity

EmbPrj BoundVariablePosition

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: BoundVariablePosition -> S Int32

icod_ :: BoundVariablePosition -> S Int32

value :: Int32 -> R BoundVariablePosition

EmbPrj Cohesion

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Cohesion -> S Int32

icod_ :: Cohesion -> S Int32

value :: Int32 -> R Cohesion

EmbPrj ConOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ConOrigin -> S Int32

icod_ :: ConOrigin -> S Int32

value :: Int32 -> R ConOrigin

EmbPrj Cubical

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Cubical -> S Int32

icod_ :: Cubical -> S Int32

value :: Int32 -> R Cubical

EmbPrj Delayed

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Delayed -> S Int32

icod_ :: Delayed -> S Int32

value :: Int32 -> R Delayed

EmbPrj ExpandedEllipsis

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ExpandedEllipsis -> S Int32

icod_ :: ExpandedEllipsis -> S Int32

value :: Int32 -> R ExpandedEllipsis

EmbPrj FileType

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FileType -> S Int32

icod_ :: FileType -> S Int32

value :: Int32 -> R FileType

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 FixityLevel

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FixityLevel -> S Int32

icod_ :: FixityLevel -> S Int32

value :: Int32 -> R FixityLevel

EmbPrj FreeVariables

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FreeVariables -> S Int32

icod_ :: FreeVariables -> S Int32

value :: Int32 -> R FreeVariables

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 IsAbstract

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: IsAbstract -> S Int32

icod_ :: IsAbstract -> S Int32

value :: Int32 -> R IsAbstract

EmbPrj Language

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Language -> S Int32

icod_ :: Language -> S Int32

value :: Int32 -> R Language

EmbPrj Lock

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Lock -> S Int32

icod_ :: Lock -> S Int32

value :: Int32 -> R Lock

EmbPrj MetaId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: MetaId -> S Int32

icod_ :: MetaId -> S Int32

value :: Int32 -> R MetaId

EmbPrj Modality

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Modality -> S Int32

icod_ :: Modality -> S Int32

value :: Int32 -> R Modality

EmbPrj ModuleNameHash

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ModuleNameHash -> S Int32

icod_ :: ModuleNameHash -> S Int32

value :: Int32 -> R ModuleNameHash

EmbPrj NameId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NameId -> S Int32

icod_ :: NameId -> S Int32

value :: Int32 -> R NameId

EmbPrj NotationPart

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NotationPart -> S Int32

icod_ :: NotationPart -> S Int32

value :: Int32 -> R NotationPart

EmbPrj Origin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Origin -> S Int32

icod_ :: Origin -> S Int32

value :: Int32 -> R Origin

EmbPrj PatternOrCopattern

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: PatternOrCopattern -> S Int32

icod_ :: PatternOrCopattern -> S Int32

value :: Int32 -> R PatternOrCopattern

EmbPrj ProjOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ProjOrigin -> S Int32

icod_ :: ProjOrigin -> S Int32

value :: Int32 -> R ProjOrigin

EmbPrj Q0Origin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Q0Origin -> S Int32

icod_ :: Q0Origin -> S Int32

value :: Int32 -> R Q0Origin

EmbPrj Q1Origin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Q1Origin -> S Int32

icod_ :: Q1Origin -> S Int32

value :: Int32 -> R Q1Origin

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 Relevance

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Relevance -> S Int32

icod_ :: Relevance -> S Int32

value :: Int32 -> R Relevance

EmbPrj DeclarationWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: DeclarationWarning -> S Int32

icod_ :: DeclarationWarning -> S Int32

value :: Int32 -> R DeclarationWarning

EmbPrj DeclarationWarning'

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: DeclarationWarning' -> S Int32

icod_ :: DeclarationWarning' -> S Int32

value :: Int32 -> R DeclarationWarning'

EmbPrj UnicodeOrAscii

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: UnicodeOrAscii -> S Int32

icod_ :: UnicodeOrAscii -> S Int32

value :: Int32 -> R UnicodeOrAscii

EmbPrj Name

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32

icod_ :: Name -> S Int32

value :: Int32 -> R Name

EmbPrj NameInScope

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NameInScope -> S Int32

icod_ :: NameInScope -> S Int32

value :: Int32 -> R NameInScope

EmbPrj NamePart

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NamePart -> S Int32

icod_ :: NamePart -> S Int32

value :: Int32 -> R NamePart

EmbPrj QName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QName -> S Int32

icod_ :: QName -> S Int32

value :: Int32 -> R QName

EmbPrj ParenPreference

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ParenPreference -> S Int32

icod_ :: ParenPreference -> S Int32

value :: Int32 -> R ParenPreference

EmbPrj Precedence

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Precedence -> S Int32

icod_ :: Precedence -> S Int32

value :: Int32 -> R Precedence

EmbPrj ConPatInfo

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ConPatInfo -> S Int32

icod_ :: ConPatInfo -> S Int32

value :: Int32 -> R ConPatInfo

EmbPrj ConPatLazy

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ConPatLazy -> S Int32

icod_ :: ConPatLazy -> S Int32

value :: Int32 -> R ConPatLazy

EmbPrj Blocked_

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Blocked_ -> S Int32

icod_ :: Blocked_ -> S Int32

value :: Int32 -> R Blocked_

EmbPrj Clause

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Clause -> S Int32

icod_ :: Clause -> S Int32

value :: Int32 -> R Clause

EmbPrj ConHead

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ConHead -> S Int32

icod_ :: ConHead -> S Int32

value :: Int32 -> R ConHead

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 DataOrRecord

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DataOrRecord -> S Int32

icod_ :: DataOrRecord -> S Int32

value :: Int32 -> R DataOrRecord

EmbPrj IsFibrant

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: IsFibrant -> S Int32

icod_ :: IsFibrant -> S Int32

value :: Int32 -> R IsFibrant

EmbPrj Level

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Level -> S Int32

icod_ :: Level -> S Int32

value :: Int32 -> R Level

EmbPrj NotBlocked

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NotBlocked -> S Int32

icod_ :: NotBlocked -> S Int32

value :: Int32 -> R NotBlocked

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 PlusLevel

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PlusLevel -> S Int32

icod_ :: PlusLevel -> S Int32

value :: Int32 -> R PlusLevel

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 Literal

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Literal -> S Int32

icod_ :: Literal -> S Int32

value :: Int32 -> R Literal

EmbPrj ParseWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ParseWarning -> S Int32

icod_ :: ParseWarning -> S Int32

value :: Int32 -> R ParseWarning

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 RangeFile

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: RangeFile -> S Int32

icod_ :: RangeFile -> S Int32

value :: Int32 -> R RangeFile

EmbPrj AbstractModule

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractModule -> S Int32

icod_ :: AbstractModule -> S Int32

value :: Int32 -> R AbstractModule

EmbPrj AbstractName

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractName -> S Int32

icod_ :: AbstractName -> S Int32

value :: Int32 -> R AbstractName

EmbPrj BindingSource

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindingSource -> S Int32

icod_ :: BindingSource -> S Int32

value :: Int32 -> R BindingSource

EmbPrj DataOrRecordModule

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: DataOrRecordModule -> S Int32

icod_ :: DataOrRecordModule -> S Int32

value :: Int32 -> R DataOrRecordModule

EmbPrj KindOfName

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: KindOfName -> S Int32

icod_ :: KindOfName -> S Int32

value :: Int32 -> R KindOfName

EmbPrj LocalVar

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: LocalVar -> S Int32

icod_ :: LocalVar -> S Int32

value :: Int32 -> R LocalVar

EmbPrj NameMetadata

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameMetadata -> S Int32

icod_ :: NameMetadata -> S Int32

value :: Int32 -> R NameMetadata

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

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ScopeInfo -> S Int32

icod_ :: ScopeInfo -> S Int32

value :: Int32 -> R ScopeInfo

EmbPrj WhyInScope

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: WhyInScope -> S Int32

icod_ :: WhyInScope -> S Int32

value :: Int32 -> R WhyInScope

EmbPrj TopLevelModuleName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: TopLevelModuleName -> S Int32

icod_ :: TopLevelModuleName -> S Int32

value :: Int32 -> R TopLevelModuleName

EmbPrj CutOff

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: CutOff -> S Int32

icod_ :: CutOff -> S Int32

value :: Int32 -> R CutOff

EmbPrj CompiledClauses

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompiledClauses -> S Int32

icod_ :: CompiledClauses -> S Int32

value :: Int32 -> R CompiledClauses

EmbPrj LazySplit

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: LazySplit -> S Int32

icod_ :: LazySplit -> S Int32

value :: Int32 -> R LazySplit

EmbPrj SplitTag

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: SplitTag -> S Int32

icod_ :: SplitTag -> S Int32

value :: Int32 -> R SplitTag

EmbPrj CheckpointId

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CheckpointId -> S Int32

icod_ :: CheckpointId -> S Int32

value :: Int32 -> R CheckpointId

EmbPrj CompKit

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompKit -> S Int32

icod_ :: CompKit -> S Int32

value :: Int32 -> R CompKit

EmbPrj Comparison

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Comparison -> S Int32

icod_ :: Comparison -> S Int32

value :: Int32 -> R Comparison

EmbPrj CompilerPragma

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

Methods

icode :: CompilerPragma -> S Int32

icod_ :: CompilerPragma -> S Int32

value :: Int32 -> R CompilerPragma

EmbPrj Definition

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Definition -> S Int32

icod_ :: Definition -> S Int32

value :: Int32 -> R Definition

EmbPrj Defn

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Defn -> S Int32

icod_ :: Defn -> S Int32

value :: Int32 -> R Defn

EmbPrj DisplayForm

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DisplayForm -> S Int32

icod_ :: DisplayForm -> S Int32

value :: Int32 -> R DisplayForm

EmbPrj DisplayTerm

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DisplayTerm -> S Int32

icod_ :: DisplayTerm -> S Int32

value :: Int32 -> R DisplayTerm

EmbPrj DoGeneralize

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DoGeneralize -> S Int32

icod_ :: DoGeneralize -> S Int32

value :: Int32 -> R DoGeneralize

EmbPrj EtaEquality

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: EtaEquality -> S Int32

icod_ :: EtaEquality -> S Int32

value :: Int32 -> R EtaEquality

EmbPrj ExtLamInfo

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ExtLamInfo -> S Int32

icod_ :: ExtLamInfo -> S Int32

value :: Int32 -> R ExtLamInfo

EmbPrj ForeignCode

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

Methods

icode :: ForeignCode -> S Int32

icod_ :: ForeignCode -> S Int32

value :: Int32 -> R ForeignCode

EmbPrj FunctionFlag

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: FunctionFlag -> S Int32

icod_ :: FunctionFlag -> S Int32

value :: Int32 -> R FunctionFlag

EmbPrj Instantiation

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Instantiation -> S Int32

icod_ :: Instantiation -> S Int32

value :: Int32 -> R Instantiation

EmbPrj Interface

Defined in Agda.TypeChecking.Serialise.Instances

Methods

icode :: Interface -> S Int32

icod_ :: Interface -> S Int32

value :: Int32 -> R Interface

EmbPrj IsForced

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: IsForced -> S Int32

icod_ :: IsForced -> S Int32

value :: Int32 -> R IsForced

EmbPrj MutualId

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: MutualId -> S Int32

icod_ :: MutualId -> S Int32

value :: Int32 -> R MutualId

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 NumGeneralizableArgs

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NumGeneralizableArgs -> S Int32

icod_ :: NumGeneralizableArgs -> S Int32

value :: Int32 -> R NumGeneralizableArgs

EmbPrj Polarity

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Polarity -> S Int32

icod_ :: Polarity -> S Int32

value :: Int32 -> R Polarity

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 ProjectionLikenessMissing

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ProjectionLikenessMissing -> S Int32

icod_ :: ProjectionLikenessMissing -> S Int32

value :: Int32 -> R ProjectionLikenessMissing

EmbPrj RecordFieldWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: RecordFieldWarning -> S Int32

icod_ :: RecordFieldWarning -> S Int32

value :: Int32 -> R RecordFieldWarning

EmbPrj RemoteMetaVariable

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: RemoteMetaVariable -> S Int32

icod_ :: RemoteMetaVariable -> S Int32

value :: Int32 -> R RemoteMetaVariable

EmbPrj RewriteRule

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: RewriteRule -> S Int32

icod_ :: RewriteRule -> S Int32

value :: Int32 -> R RewriteRule

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 System

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: System -> S Int32

icod_ :: System -> S Int32

value :: Int32 -> R System

EmbPrj TCWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: TCWarning -> S Int32

icod_ :: TCWarning -> S Int32

value :: Int32 -> R TCWarning

EmbPrj TermHead

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: TermHead -> S Int32

icod_ :: TermHead -> S Int32

value :: Int32 -> R TermHead

EmbPrj Warning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Warning -> S Int32

icod_ :: Warning -> S Int32

value :: Int32 -> R Warning

EmbPrj Occurrence

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Occurrence -> S Int32

icod_ :: Occurrence -> S Int32

value :: Int32 -> R Occurrence

EmbPrj AbsNameWithFixity

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbsNameWithFixity -> S Int32

icod_ :: AbsNameWithFixity -> S Int32

value :: Int32 -> R AbsNameWithFixity

EmbPrj SerialisedRange

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: SerialisedRange -> S Int32

icod_ :: SerialisedRange -> S Int32

value :: Int32 -> R SerialisedRange

EmbPrj Impossible

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Impossible -> S Int32

icod_ :: Impossible -> S Int32

value :: Int32 -> R Impossible

EmbPrj Permutation

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Permutation -> S Int32

icod_ :: Permutation -> S Int32

value :: Int32 -> R Permutation

EmbPrj ProfileOption

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ProfileOption -> S Int32

icod_ :: ProfileOption -> S Int32

value :: Int32 -> R ProfileOption

EmbPrj ProfileOptions

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ProfileOptions -> S Int32

icod_ :: ProfileOptions -> S Int32

value :: Int32 -> R ProfileOptions

EmbPrj Void

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Void -> S Int32

icod_ :: Void -> S Int32

value :: Int32 -> R Void

EmbPrj Int32

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Int32 -> S Int32

icod_ :: Int32 -> S Int32

value :: Int32 -> R Int32

EmbPrj CallStack

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: CallStack -> S Int32

icod_ :: CallStack -> S Int32

value :: Int32 -> R CallStack

EmbPrj SrcLoc

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: SrcLoc -> S Int32

icod_ :: SrcLoc -> S Int32

value :: Int32 -> R SrcLoc

EmbPrj Word64

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Word64 -> S Int32

icod_ :: Word64 -> S Int32

value :: Int32 -> R Word64

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 Text

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Text -> S Int32

icod_ :: Text -> S Int32

value :: Int32 -> R Text

EmbPrj String

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: String -> S Int32

icod_ :: String -> S Int32

value :: Int32 -> R String

EmbPrj Integer

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Integer -> S Int32

icod_ :: Integer -> S Int32

value :: Int32 -> R Integer

EmbPrj ()

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: () -> S Int32

icod_ :: () -> S Int32

value :: Int32 -> R ()

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

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 (HasEta' a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: HasEta' a -> S Int32

icod_ :: HasEta' a -> S Int32

value :: Int32 -> R (HasEta' 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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (Judgement a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Judgement a -> S Int32

icod_ :: Judgement a -> S Int32

value :: Int32 -> R (Judgement 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 (List1 a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: List1 a -> S Int32

icod_ :: List1 a -> S Int32

value :: Int32 -> R (List1 a)

EmbPrj a => EmbPrj (List2 a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: List2 a -> S Int32

icod_ :: List2 a -> S Int32

value :: Int32 -> R (List2 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 (RangeMap a)

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: RangeMap a -> S Int32

icod_ :: RangeMap a -> S Int32

value :: Int32 -> R (RangeMap 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 (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 (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 [a]

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: [a] -> S Int32

icod_ :: [a] -> S Int32

value :: Int32 -> R [a]

(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 k, EmbPrj v, EmbPrj (Tag v)) => EmbPrj (BiMap k v)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: BiMap k v -> S Int32

icod_ :: BiMap k v -> S Int32

value :: Int32 -> R (BiMap 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 (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)

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Pair a b -> S Int32

icod_ :: Pair a b -> S Int32

value :: Int32 -> R (Pair 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)

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

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