Agda-2.7.0: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Serialise

Description

Structure-sharing serialisation of Agda interface files.

Synopsis

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 Int32 Source #

icod_ :: Range -> S Int32 Source #

value :: Int32 -> R Range Source #

EmbPrj ExecutablesFile Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ExecutablesFile -> S Int32 Source #

icod_ :: ExecutablesFile -> S Int32 Source #

value :: Int32 -> R ExecutablesFile Source #

EmbPrj LibPositionInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibPositionInfo -> S Int32 Source #

icod_ :: LibPositionInfo -> S Int32 Source #

value :: Int32 -> R LibPositionInfo Source #

EmbPrj LibWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning -> S Int32 Source #

icod_ :: LibWarning -> S Int32 Source #

value :: Int32 -> R LibWarning Source #

EmbPrj LibWarning' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LibWarning' -> S Int32 Source #

icod_ :: LibWarning' -> S Int32 Source #

value :: Int32 -> R LibWarning' Source #

EmbPrj OptionsPragma Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: OptionsPragma -> S Int32 Source #

icod_ :: OptionsPragma -> S Int32 Source #

value :: Int32 -> R OptionsPragma Source #

EmbPrj ConfluenceCheck Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ConfluenceCheck -> S Int32 Source #

icod_ :: ConfluenceCheck -> S Int32 Source #

value :: Int32 -> R ConfluenceCheck Source #

EmbPrj InfectiveCoinfective Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: InfectiveCoinfective -> S Int32 Source #

icod_ :: InfectiveCoinfective -> S Int32 Source #

value :: Int32 -> R InfectiveCoinfective Source #

EmbPrj OptionWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: OptionWarning -> S Int32 Source #

icod_ :: OptionWarning -> S Int32 Source #

value :: Int32 -> R OptionWarning Source #

EmbPrj PragmaOptions Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: PragmaOptions -> S Int32 Source #

icod_ :: PragmaOptions -> S Int32 Source #

value :: Int32 -> R PragmaOptions Source #

EmbPrj WarningMode Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningMode -> S Int32 Source #

icod_ :: WarningMode -> S Int32 Source #

value :: Int32 -> R WarningMode Source #

EmbPrj WarningModeError Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningModeError -> S Int32 Source #

icod_ :: WarningModeError -> S Int32 Source #

value :: Int32 -> R WarningModeError Source #

EmbPrj WarningName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningName -> S Int32 Source #

icod_ :: WarningName -> S Int32 Source #

value :: Int32 -> R WarningName Source #

EmbPrj BindName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindName -> S Int32 Source #

icod_ :: BindName -> S Int32 Source #

value :: Int32 -> R BindName Source #

EmbPrj AmbiguousQName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: AmbiguousQName -> S Int32 Source #

icod_ :: AmbiguousQName -> S Int32 Source #

value :: Int32 -> R AmbiguousQName Source #

EmbPrj ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ModuleName -> S Int32 Source #

icod_ :: ModuleName -> S Int32 Source #

value :: Int32 -> R ModuleName Source #

EmbPrj Name Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32 Source #

icod_ :: Name -> S Int32 Source #

value :: Int32 -> R Name Source #

EmbPrj QName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QName -> S Int32 Source #

icod_ :: QName -> S Int32 Source #

value :: Int32 -> R QName Source #

EmbPrj Suffix Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Suffix -> S Int32 Source #

icod_ :: Suffix -> S Int32 Source #

value :: Int32 -> R Suffix Source #

EmbPrj BuiltinId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: BuiltinId -> S Int32 Source #

icod_ :: BuiltinId -> S Int32 Source #

value :: Int32 -> R BuiltinId Source #

EmbPrj PrimitiveId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: PrimitiveId -> S Int32 Source #

icod_ :: PrimitiveId -> S Int32 Source #

value :: Int32 -> R PrimitiveId Source #

EmbPrj SomeBuiltin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: SomeBuiltin -> S Int32 Source #

icod_ :: SomeBuiltin -> S Int32 Source #

value :: Int32 -> R SomeBuiltin Source #

EmbPrj Access Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Access -> S Int32 Source #

icod_ :: Access -> S Int32 Source #

value :: Int32 -> R Access Source #

EmbPrj Annotation Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Annotation -> S Int32 Source #

icod_ :: Annotation -> S Int32 Source #

value :: Int32 -> R Annotation Source #

EmbPrj ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ArgInfo -> S Int32 Source #

icod_ :: ArgInfo -> S Int32 Source #

value :: Int32 -> R ArgInfo Source #

EmbPrj Associativity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Associativity -> S Int32 Source #

icod_ :: Associativity -> S Int32 Source #

value :: Int32 -> R Associativity Source #

EmbPrj BoundVariablePosition Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: BoundVariablePosition -> S Int32 Source #

icod_ :: BoundVariablePosition -> S Int32 Source #

value :: Int32 -> R BoundVariablePosition Source #

EmbPrj Cohesion Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Cohesion -> S Int32 Source #

icod_ :: Cohesion -> S Int32 Source #

value :: Int32 -> R Cohesion Source #

EmbPrj ConOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ConOrigin -> S Int32 Source #

icod_ :: ConOrigin -> S Int32 Source #

value :: Int32 -> R ConOrigin Source #

EmbPrj Cubical Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Cubical -> S Int32 Source #

icod_ :: Cubical -> S Int32 Source #

value :: Int32 -> R Cubical Source #

EmbPrj ExpandedEllipsis Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ExpandedEllipsis -> S Int32 Source #

icod_ :: ExpandedEllipsis -> S Int32 Source #

value :: Int32 -> R ExpandedEllipsis Source #

EmbPrj FileType Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FileType -> S Int32 Source #

icod_ :: FileType -> S Int32 Source #

value :: Int32 -> R FileType Source #

EmbPrj Fixity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Fixity -> S Int32 Source #

icod_ :: Fixity -> S Int32 Source #

value :: Int32 -> R Fixity Source #

EmbPrj Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Fixity' -> S Int32 Source #

icod_ :: Fixity' -> S Int32 Source #

value :: Int32 -> R Fixity' Source #

EmbPrj FixityLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FixityLevel -> S Int32 Source #

icod_ :: FixityLevel -> S Int32 Source #

value :: Int32 -> R FixityLevel Source #

EmbPrj FreeVariables Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FreeVariables -> S Int32 Source #

icod_ :: FreeVariables -> S Int32 Source #

value :: Int32 -> R FreeVariables Source #

EmbPrj Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Hiding -> S Int32 Source #

icod_ :: Hiding -> S Int32 Source #

value :: Int32 -> R Hiding Source #

EmbPrj IsAbstract Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: IsAbstract -> S Int32 Source #

icod_ :: IsAbstract -> S Int32 Source #

value :: Int32 -> R IsAbstract Source #

EmbPrj IsInstance Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: IsInstance -> S Int32 Source #

icod_ :: IsInstance -> S Int32 Source #

value :: Int32 -> R IsInstance Source #

EmbPrj IsOpaque Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: IsOpaque -> S Int32 Source #

icod_ :: IsOpaque -> S Int32 Source #

value :: Int32 -> R IsOpaque Source #

EmbPrj Language Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Language -> S Int32 Source #

icod_ :: Language -> S Int32 Source #

value :: Int32 -> R Language Source #

EmbPrj Lock Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Lock -> S Int32 Source #

icod_ :: Lock -> S Int32 Source #

value :: Int32 -> R Lock Source #

EmbPrj MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: MetaId -> S Int32 Source #

icod_ :: MetaId -> S Int32 Source #

value :: Int32 -> R MetaId Source #

EmbPrj Modality Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Modality -> S Int32 Source #

icod_ :: Modality -> S Int32 Source #

value :: Int32 -> R Modality Source #

EmbPrj NameId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NameId -> S Int32 Source #

icod_ :: NameId -> S Int32 Source #

value :: Int32 -> R NameId Source #

EmbPrj NotationPart Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NotationPart -> S Int32 Source #

icod_ :: NotationPart -> S Int32 Source #

value :: Int32 -> R NotationPart Source #

EmbPrj OpaqueId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: OpaqueId -> S Int32 Source #

icod_ :: OpaqueId -> S Int32 Source #

value :: Int32 -> R OpaqueId Source #

EmbPrj Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Origin -> S Int32 Source #

icod_ :: Origin -> S Int32 Source #

value :: Int32 -> R Origin Source #

EmbPrj OverlapMode Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: OverlapMode -> S Int32 Source #

icod_ :: OverlapMode -> S Int32 Source #

value :: Int32 -> R OverlapMode Source #

EmbPrj PatternOrCopattern Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: PatternOrCopattern -> S Int32 Source #

icod_ :: PatternOrCopattern -> S Int32 Source #

value :: Int32 -> R PatternOrCopattern Source #

EmbPrj ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ProblemId -> S Int32 Source #

icod_ :: ProblemId -> S Int32 Source #

value :: Int32 -> R ProblemId Source #

EmbPrj ProjOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ProjOrigin -> S Int32 Source #

icod_ :: ProjOrigin -> S Int32 Source #

value :: Int32 -> R ProjOrigin Source #

EmbPrj Q0Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Q0Origin -> S Int32 Source #

icod_ :: Q0Origin -> S Int32 Source #

value :: Int32 -> R Q0Origin Source #

EmbPrj Q1Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Q1Origin -> S Int32 Source #

icod_ :: Q1Origin -> S Int32 Source #

value :: Int32 -> R Q1Origin Source #

EmbPrj Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Quantity -> S Int32 Source #

icod_ :: Quantity -> S Int32 Source #

value :: Int32 -> R Quantity Source #

EmbPrj QωOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QωOrigin -> S Int32 Source #

icod_ :: QωOrigin -> S Int32 Source #

value :: Int32 -> R QωOrigin Source #

EmbPrj Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Relevance -> S Int32 Source #

icod_ :: Relevance -> S Int32 Source #

value :: Int32 -> R Relevance Source #

EmbPrj Aspect Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspect -> S Int32 Source #

icod_ :: Aspect -> S Int32 Source #

value :: Int32 -> R Aspect Source #

EmbPrj Aspects Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspects -> S Int32 Source #

icod_ :: Aspects -> S Int32 Source #

value :: Int32 -> R Aspects Source #

EmbPrj DefinitionSite Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: DefinitionSite -> S Int32 Source #

icod_ :: DefinitionSite -> S Int32 Source #

value :: Int32 -> R DefinitionSite Source #

EmbPrj Induction Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Induction -> S Int32 Source #

icod_ :: Induction -> S Int32 Source #

value :: Int32 -> R Induction Source #

EmbPrj NameKind Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: NameKind -> S Int32 Source #

icod_ :: NameKind -> S Int32 Source #

value :: Int32 -> R NameKind Source #

EmbPrj OtherAspect Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: OtherAspect -> S Int32 Source #

icod_ :: OtherAspect -> S Int32 Source #

value :: Int32 -> R OtherAspect Source #

EmbPrj TokenBased Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: TokenBased -> S Int32 Source #

icod_ :: TokenBased -> S Int32 Source #

value :: Int32 -> R TokenBased Source #

EmbPrj KwRange Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: KwRange -> S Int32 Source #

icod_ :: KwRange -> S Int32 Source #

value :: Int32 -> R KwRange Source #

EmbPrj Doc Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Doc -> S Int32 Source #

icod_ :: Doc -> S Int32 Source #

value :: Int32 -> R Doc Source #

EmbPrj RecordDirective Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: RecordDirective -> S Int32 Source #

icod_ :: RecordDirective -> S Int32 Source #

value :: Int32 -> R RecordDirective Source #

EmbPrj DeclarationWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: DeclarationWarning -> S Int32 Source #

icod_ :: DeclarationWarning -> S Int32 Source #

value :: Int32 -> R DeclarationWarning Source #

EmbPrj DeclarationWarning' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: DeclarationWarning' -> S Int32 Source #

icod_ :: DeclarationWarning' -> S Int32 Source #

value :: Int32 -> R DeclarationWarning' Source #

EmbPrj UnicodeOrAscii Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: UnicodeOrAscii -> S Int32 Source #

icod_ :: UnicodeOrAscii -> S Int32 Source #

value :: Int32 -> R UnicodeOrAscii Source #

EmbPrj Name Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32 Source #

icod_ :: Name -> S Int32 Source #

value :: Int32 -> R Name Source #

EmbPrj NameInScope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NameInScope -> S Int32 Source #

icod_ :: NameInScope -> S Int32 Source #

value :: Int32 -> R NameInScope Source #

EmbPrj NamePart Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NamePart -> S Int32 Source #

icod_ :: NamePart -> S Int32 Source #

value :: Int32 -> R NamePart Source #

EmbPrj QName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QName -> S Int32 Source #

icod_ :: QName -> S Int32 Source #

value :: Int32 -> R QName Source #

EmbPrj ParenPreference Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ParenPreference -> S Int32 Source #

icod_ :: ParenPreference -> S Int32 Source #

value :: Int32 -> R ParenPreference Source #

EmbPrj Precedence Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Precedence -> S Int32 Source #

icod_ :: Precedence -> S Int32 Source #

value :: Int32 -> R Precedence Source #

EmbPrj ConPatInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ConPatInfo -> S Int32 Source #

icod_ :: ConPatInfo -> S Int32 Source #

value :: Int32 -> R ConPatInfo Source #

EmbPrj ConPatLazy Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ConPatLazy -> S Int32 Source #

icod_ :: ConPatLazy -> S Int32 Source #

value :: Int32 -> R ConPatLazy Source #

EmbPrj Blocked_ Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Blocked_ -> S Int32 Source #

icod_ :: Blocked_ -> S Int32 Source #

value :: Int32 -> R Blocked_ Source #

EmbPrj Clause Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Clause -> S Int32 Source #

icod_ :: Clause -> S Int32 Source #

value :: Int32 -> R Clause Source #

EmbPrj ConHead Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ConHead -> S Int32 Source #

icod_ :: ConHead -> S Int32 Source #

value :: Int32 -> R ConHead Source #

EmbPrj ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ConPatternInfo -> S Int32 Source #

icod_ :: ConPatternInfo -> S Int32 Source #

value :: Int32 -> R ConPatternInfo Source #

EmbPrj DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DBPatVar -> S Int32 Source #

icod_ :: DBPatVar -> S Int32 Source #

value :: Int32 -> R DBPatVar Source #

EmbPrj DataOrRecord Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DataOrRecord -> S Int32 Source #

icod_ :: DataOrRecord -> S Int32 Source #

value :: Int32 -> R DataOrRecord Source #

EmbPrj Level Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Level -> S Int32 Source #

icod_ :: Level -> S Int32 Source #

value :: Int32 -> R Level Source #

EmbPrj NotBlocked Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NotBlocked -> S Int32 Source #

icod_ :: NotBlocked -> S Int32 Source #

value :: Int32 -> R NotBlocked Source #

EmbPrj PatOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PatOrigin -> S Int32 Source #

icod_ :: PatOrigin -> S Int32 Source #

value :: Int32 -> R PatOrigin Source #

EmbPrj PatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PatternInfo -> S Int32 Source #

icod_ :: PatternInfo -> S Int32 Source #

value :: Int32 -> R PatternInfo Source #

EmbPrj PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PlusLevel -> S Int32 Source #

icod_ :: PlusLevel -> S Int32 Source #

value :: Int32 -> R PlusLevel Source #

EmbPrj Sort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Sort -> S Int32 Source #

icod_ :: Sort -> S Int32 Source #

value :: Int32 -> R Sort Source #

EmbPrj Term Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Term -> S Int32 Source #

icod_ :: Term -> S Int32 Source #

value :: Int32 -> R Term Source #

EmbPrj IsFibrant Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: IsFibrant -> S Int32 Source #

icod_ :: IsFibrant -> S Int32 Source #

value :: Int32 -> R IsFibrant Source #

EmbPrj Univ Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Univ -> S Int32 Source #

icod_ :: Univ -> S Int32 Source #

value :: Int32 -> R Univ Source #

EmbPrj Literal Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Literal -> S Int32 Source #

icod_ :: Literal -> S Int32 Source #

value :: Int32 -> R Literal Source #

EmbPrj ParseWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ParseWarning -> S Int32 Source #

icod_ :: ParseWarning -> S Int32 Source #

value :: Int32 -> 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 Int32 Source #

icod_ :: Range -> S Int32 Source #

value :: Int32 -> R Range Source #

EmbPrj RangeFile Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: RangeFile -> S Int32 Source #

icod_ :: RangeFile -> S Int32 Source #

value :: Int32 -> R RangeFile Source #

EmbPrj AbstractModule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractModule -> S Int32 Source #

icod_ :: AbstractModule -> S Int32 Source #

value :: Int32 -> R AbstractModule Source #

EmbPrj AbstractName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractName -> S Int32 Source #

icod_ :: AbstractName -> S Int32 Source #

value :: Int32 -> R AbstractName Source #

EmbPrj BindingSource Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindingSource -> S Int32 Source #

icod_ :: BindingSource -> S Int32 Source #

value :: Int32 -> R BindingSource Source #

EmbPrj DataOrRecordModule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: DataOrRecordModule -> S Int32 Source #

icod_ :: DataOrRecordModule -> S Int32 Source #

value :: Int32 -> R DataOrRecordModule Source #

EmbPrj KindOfName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: KindOfName -> S Int32 Source #

icod_ :: KindOfName -> S Int32 Source #

value :: Int32 -> R KindOfName Source #

EmbPrj LocalVar Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: LocalVar -> S Int32 Source #

icod_ :: LocalVar -> S Int32 Source #

value :: Int32 -> R LocalVar Source #

EmbPrj NameMetadata Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameMetadata -> S Int32 Source #

icod_ :: NameMetadata -> S Int32 Source #

value :: Int32 -> R NameMetadata Source #

EmbPrj NameOrModule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameOrModule -> S Int32 Source #

icod_ :: NameOrModule -> S Int32 Source #

value :: Int32 -> R NameOrModule Source #

EmbPrj NameSpace Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameSpace -> S Int32 Source #

icod_ :: NameSpace -> S Int32 Source #

value :: Int32 -> R NameSpace Source #

EmbPrj NameSpaceId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameSpaceId -> S Int32 Source #

icod_ :: NameSpaceId -> S Int32 Source #

value :: Int32 -> R NameSpaceId Source #

EmbPrj Scope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Scope -> S Int32 Source #

icod_ :: Scope -> S Int32 Source #

value :: Int32 -> R Scope Source #

EmbPrj ScopeInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ScopeInfo -> S Int32 Source #

icod_ :: ScopeInfo -> S Int32 Source #

value :: Int32 -> R ScopeInfo Source #

EmbPrj WhyInScope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: WhyInScope -> S Int32 Source #

icod_ :: WhyInScope -> S Int32 Source #

value :: Int32 -> R WhyInScope Source #

EmbPrj TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: TopLevelModuleName -> S Int32 Source #

icod_ :: TopLevelModuleName -> S Int32 Source #

value :: Int32 -> R TopLevelModuleName Source #

EmbPrj ModuleNameHash Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ModuleNameHash -> S Int32 Source #

icod_ :: ModuleNameHash -> S Int32 Source #

value :: Int32 -> R ModuleNameHash Source #

EmbPrj CutOff Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: CutOff -> S Int32 Source #

icod_ :: CutOff -> S Int32 Source #

value :: Int32 -> R CutOff Source #

EmbPrj CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompiledClauses -> S Int32 Source #

icod_ :: CompiledClauses -> S Int32 Source #

value :: Int32 -> R CompiledClauses Source #

EmbPrj LazySplit Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: LazySplit -> S Int32 Source #

icod_ :: LazySplit -> S Int32 Source #

value :: Int32 -> R LazySplit Source #

EmbPrj SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: SplitTag -> S Int32 Source #

icod_ :: SplitTag -> S Int32 Source #

value :: Int32 -> R SplitTag Source #

EmbPrj Key Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Key -> S Int32 Source #

icod_ :: Key -> S Int32 Source #

value :: Int32 -> R Key Source #

EmbPrj BuiltinSort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: BuiltinSort -> S Int32 Source #

icod_ :: BuiltinSort -> S Int32 Source #

value :: Int32 -> R BuiltinSort Source #

EmbPrj CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CheckpointId -> S Int32 Source #

icod_ :: CheckpointId -> S Int32 Source #

value :: Int32 -> R CheckpointId Source #

EmbPrj CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompKit -> S Int32 Source #

icod_ :: CompKit -> S Int32 Source #

value :: Int32 -> R CompKit Source #

EmbPrj Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Comparison -> S Int32 Source #

icod_ :: Comparison -> S Int32 Source #

value :: Int32 -> R Comparison Source #

EmbPrj CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

Methods

icode :: CompilerPragma -> S Int32 Source #

icod_ :: CompilerPragma -> S Int32 Source #

value :: Int32 -> R CompilerPragma Source #

EmbPrj Definition Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Definition -> S Int32 Source #

icod_ :: Definition -> S Int32 Source #

value :: Int32 -> R Definition Source #

EmbPrj Defn Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Defn -> S Int32 Source #

icod_ :: Defn -> S Int32 Source #

value :: Int32 -> R Defn Source #

EmbPrj DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DisplayForm -> S Int32 Source #

icod_ :: DisplayForm -> S Int32 Source #

value :: Int32 -> R DisplayForm Source #

EmbPrj DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DisplayTerm -> S Int32 Source #

icod_ :: DisplayTerm -> S Int32 Source #

value :: Int32 -> R DisplayTerm Source #

EmbPrj DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DoGeneralize -> S Int32 Source #

icod_ :: DoGeneralize -> S Int32 Source #

value :: Int32 -> R DoGeneralize Source #

EmbPrj EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: EtaEquality -> S Int32 Source #

icod_ :: EtaEquality -> S Int32 Source #

value :: Int32 -> R EtaEquality Source #

EmbPrj ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ExtLamInfo -> S Int32 Source #

icod_ :: ExtLamInfo -> S Int32 Source #

value :: Int32 -> R ExtLamInfo Source #

EmbPrj ForeignCode Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

Methods

icode :: ForeignCode -> S Int32 Source #

icod_ :: ForeignCode -> S Int32 Source #

value :: Int32 -> R ForeignCode Source #

EmbPrj ForeignCodeStack Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

Methods

icode :: ForeignCodeStack -> S Int32 Source #

icod_ :: ForeignCodeStack -> S Int32 Source #

value :: Int32 -> R ForeignCodeStack Source #

EmbPrj FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: FunctionFlag -> S Int32 Source #

icod_ :: FunctionFlag -> S Int32 Source #

value :: Int32 -> R FunctionFlag Source #

EmbPrj IllegalRewriteRuleReason Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: IllegalRewriteRuleReason -> S Int32 Source #

icod_ :: IllegalRewriteRuleReason -> S Int32 Source #

value :: Int32 -> R IllegalRewriteRuleReason Source #

EmbPrj InstanceInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: InstanceInfo -> S Int32 Source #

icod_ :: InstanceInfo -> S Int32 Source #

value :: Int32 -> R InstanceInfo Source #

EmbPrj InstanceTable Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: InstanceTable -> S Int32 Source #

icod_ :: InstanceTable -> S Int32 Source #

value :: Int32 -> R InstanceTable Source #

EmbPrj Instantiation Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Instantiation -> S Int32 Source #

icod_ :: Instantiation -> S Int32 Source #

value :: Int32 -> R Instantiation Source #

EmbPrj Interface Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances

Methods

icode :: Interface -> S Int32 Source #

icod_ :: Interface -> S Int32 Source #

value :: Int32 -> R Interface Source #

EmbPrj IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: IsForced -> S Int32 Source #

icod_ :: IsForced -> S Int32 Source #

value :: Int32 -> R IsForced Source #

EmbPrj LHSOrPatSyn Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: LHSOrPatSyn -> S Int32 Source #

icod_ :: LHSOrPatSyn -> S Int32 Source #

value :: Int32 -> R LHSOrPatSyn Source #

EmbPrj MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: MutualId -> S Int32 Source #

icod_ :: MutualId -> S Int32 Source #

value :: Int32 -> R MutualId Source #

EmbPrj NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NLPSort -> S Int32 Source #

icod_ :: NLPSort -> S Int32 Source #

value :: Int32 -> R NLPSort Source #

EmbPrj NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NLPType -> S Int32 Source #

icod_ :: NLPType -> S Int32 Source #

value :: Int32 -> R NLPType Source #

EmbPrj NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NLPat -> S Int32 Source #

icod_ :: NLPat -> S Int32 Source #

value :: Int32 -> R NLPat Source #

EmbPrj NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NumGeneralizableArgs -> S Int32 Source #

icod_ :: NumGeneralizableArgs -> S Int32 Source #

value :: Int32 -> R NumGeneralizableArgs Source #

EmbPrj OpaqueBlock Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: OpaqueBlock -> S Int32 Source #

icod_ :: OpaqueBlock -> S Int32 Source #

value :: Int32 -> R OpaqueBlock Source #

EmbPrj Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Polarity -> S Int32 Source #

icod_ :: Polarity -> S Int32 Source #

value :: Int32 -> R Polarity Source #

EmbPrj ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ProjLams -> S Int32 Source #

icod_ :: ProjLams -> S Int32 Source #

value :: Int32 -> R ProjLams Source #

EmbPrj Projection Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Projection -> S Int32 Source #

icod_ :: Projection -> S Int32 Source #

value :: Int32 -> R Projection Source #

EmbPrj ProjectionLikenessMissing Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ProjectionLikenessMissing -> S Int32 Source #

icod_ :: ProjectionLikenessMissing -> S Int32 Source #

value :: Int32 -> R ProjectionLikenessMissing Source #

EmbPrj RemoteMetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: RemoteMetaVariable -> S Int32 Source #

icod_ :: RemoteMetaVariable -> S Int32 Source #

value :: Int32 -> R RemoteMetaVariable Source #

EmbPrj RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: RewriteRule -> S Int32 Source #

icod_ :: RewriteRule -> S Int32 Source #

value :: Int32 -> R RewriteRule Source #

EmbPrj Section Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Section -> S Int32 Source #

icod_ :: Section -> S Int32 Source #

value :: Int32 -> R Section Source #

EmbPrj Signature Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Signature -> S Int32 Source #

icod_ :: Signature -> S Int32 Source #

value :: Int32 -> R Signature Source #

EmbPrj System Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: System -> S Int32 Source #

icod_ :: System -> S Int32 Source #

value :: Int32 -> R System Source #

EmbPrj TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: TCWarning -> S Int32 Source #

icod_ :: TCWarning -> S Int32 Source #

value :: Int32 -> R TCWarning Source #

EmbPrj TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: TermHead -> S Int32 Source #

icod_ :: TermHead -> S Int32 Source #

value :: Int32 -> R TermHead Source #

EmbPrj Warning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Warning -> S Int32 Source #

icod_ :: Warning -> S Int32 Source #

value :: Int32 -> R Warning Source #

EmbPrj RecordFieldWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: RecordFieldWarning -> S Int32 Source #

icod_ :: RecordFieldWarning -> S Int32 Source #

value :: Int32 -> R RecordFieldWarning Source #

EmbPrj Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Occurrence -> S Int32 Source #

icod_ :: Occurrence -> S Int32 Source #

value :: Int32 -> R Occurrence Source #

EmbPrj AbsNameWithFixity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbsNameWithFixity -> S Int32 Source #

icod_ :: AbsNameWithFixity -> S Int32 Source #

value :: Int32 -> R AbsNameWithFixity Source #

EmbPrj SerialisedRange Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: SerialisedRange -> S Int32 Source #

icod_ :: SerialisedRange -> S Int32 Source #

value :: Int32 -> R SerialisedRange Source #

EmbPrj Impossible Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Impossible -> S Int32 Source #

icod_ :: Impossible -> S Int32 Source #

value :: Int32 -> R Impossible Source #

EmbPrj Permutation Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Permutation -> S Int32 Source #

icod_ :: Permutation -> S Int32 Source #

value :: Int32 -> R Permutation Source #

EmbPrj ProfileOption Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ProfileOption -> S Int32 Source #

icod_ :: ProfileOption -> S Int32 Source #

value :: Int32 -> R ProfileOption Source #

EmbPrj ProfileOptions Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ProfileOptions -> S Int32 Source #

icod_ :: ProfileOptions -> S Int32 Source #

value :: Int32 -> R ProfileOptions Source #

EmbPrj Void Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Void -> S Int32 Source #

icod_ :: Void -> S Int32 Source #

value :: Int32 -> R Void Source #

EmbPrj Int32 Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Int32 -> S Int32 Source #

icod_ :: Int32 -> S Int32 Source #

value :: Int32 -> R Int32 Source #

EmbPrj CallStack Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: CallStack -> S Int32 Source #

icod_ :: CallStack -> S Int32 Source #

value :: Int32 -> R CallStack Source #

EmbPrj SrcLoc Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: SrcLoc -> S Int32 Source #

icod_ :: SrcLoc -> S Int32 Source #

value :: Int32 -> R SrcLoc Source #

EmbPrj Word64 Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Word64 -> S Int32 Source #

icod_ :: Word64 -> S Int32 Source #

value :: Int32 -> R Word64 Source #

EmbPrj IntSet Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: IntSet -> S Int32 Source #

icod_ :: IntSet -> S Int32 Source #

value :: Int32 -> R IntSet Source #

EmbPrj Text Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Text -> S Int32 Source #

icod_ :: Text -> S Int32 Source #

value :: Int32 -> R Text Source #

EmbPrj Text Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Text -> S Int32 Source #

icod_ :: Text -> S Int32 Source #

value :: Int32 -> R Text Source #

EmbPrj String Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: String -> S Int32 Source #

icod_ :: String -> S Int32 Source #

value :: Int32 -> R String Source #

EmbPrj Integer Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Integer -> S Int32 Source #

icod_ :: Integer -> S Int32 Source #

value :: Int32 -> R Integer Source #

EmbPrj () Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: () -> S Int32 Source #

icod_ :: () -> S Int32 Source #

value :: Int32 -> R () Source #

EmbPrj Bool Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Bool -> S Int32 Source #

icod_ :: Bool -> S Int32 Source #

value :: Int32 -> R Bool Source #

EmbPrj Char Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Char -> S Int32 Source #

icod_ :: Char -> S Int32 Source #

value :: Int32 -> R Char Source #

EmbPrj Double Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Double -> S Int32 Source #

icod_ :: Double -> S Int32 Source #

value :: Int32 -> R Double Source #

EmbPrj Int Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Int -> S Int32 Source #

icod_ :: Int -> S Int32 Source #

value :: Int32 -> R Int Source #

EmbPrj a => EmbPrj (Pattern' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Pattern' a -> S Int32 Source #

icod_ :: Pattern' a -> S Int32 Source #

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

EmbPrj a => EmbPrj (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Arg a -> S Int32 Source #

icod_ :: Arg a -> S Int32 Source #

value :: Int32 -> R (Arg a) Source #

EmbPrj a => EmbPrj (HasEta' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: HasEta' a -> S Int32 Source #

icod_ :: HasEta' a -> S Int32 Source #

value :: Int32 -> R (HasEta' a) Source #

EmbPrj a => EmbPrj (Ranged a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Ranged a -> S Int32 Source #

icod_ :: Ranged a -> S Int32 Source #

value :: Int32 -> R (Ranged a) Source #

EmbPrj a => EmbPrj (RecordDirectives' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: RecordDirectives' a -> S Int32 Source #

icod_ :: RecordDirectives' a -> S Int32 Source #

value :: Int32 -> R (RecordDirectives' a) Source #

EmbPrj a => EmbPrj (WithHiding a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: WithHiding a -> S Int32 Source #

icod_ :: WithHiding a -> S Int32 Source #

value :: Int32 -> R (WithHiding a) Source #

EmbPrj a => EmbPrj (WithOrigin a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: WithOrigin a -> S Int32 Source #

icod_ :: WithOrigin a -> S Int32 Source #

value :: Int32 -> R (WithOrigin a) Source #

EmbPrj a => EmbPrj (FieldAssignment' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FieldAssignment' a -> S Int32 Source #

icod_ :: FieldAssignment' a -> S Int32 Source #

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

EmbPrj a => EmbPrj (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Abs a -> S Int32 Source #

icod_ :: Abs a -> S Int32 Source #

value :: Int32 -> R (Abs a) Source #

EmbPrj a => EmbPrj (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Int32 Source #

icod_ :: Dom a -> S Int32 Source #

value :: Int32 -> R (Dom a) Source #

EmbPrj a => EmbPrj (Pattern' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Pattern' a -> S Int32 Source #

icod_ :: Pattern' a -> S Int32 Source #

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

EmbPrj a => EmbPrj (Substitution' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Substitution' a -> S Int32 Source #

icod_ :: Substitution' a -> S Int32 Source #

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

EmbPrj a => EmbPrj (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Tele a -> S Int32 Source #

icod_ :: Tele a -> S Int32 Source #

value :: Int32 -> R (Tele a) Source #

EmbPrj a => EmbPrj (Type' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Type' a -> S Int32 Source #

icod_ :: Type' a -> S Int32 Source #

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

EmbPrj a => EmbPrj (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Elim' a -> S Int32 Source #

icod_ :: Elim' a -> S Int32 Source #

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

EmbPrj a => EmbPrj (Interval' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Interval' a -> S Int32 Source #

icod_ :: Interval' a -> S Int32 Source #

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

EmbPrj a => EmbPrj (Position' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Position' a -> S Int32 Source #

icod_ :: Position' a -> S Int32 Source #

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

EmbPrj a => EmbPrj (Case a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Case a -> S Int32 Source #

icod_ :: Case a -> S Int32 Source #

value :: Int32 -> R (Case a) Source #

EmbPrj a => EmbPrj (WithArity a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: WithArity a -> S Int32 Source #

icod_ :: WithArity a -> S Int32 Source #

value :: Int32 -> R (WithArity a) Source #

EmbPrj a => EmbPrj (SplitTree' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: SplitTree' a -> S Int32 Source #

icod_ :: SplitTree' a -> S Int32 Source #

value :: Int32 -> 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 Int32 Source #

icod_ :: DiscrimTree a -> S Int32 Source #

value :: Int32 -> R (DiscrimTree a) Source #

EmbPrj a => EmbPrj (Builtin a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Builtin a -> S Int32 Source #

icod_ :: Builtin a -> S Int32 Source #

value :: Int32 -> R (Builtin a) Source #

EmbPrj a => EmbPrj (FunctionInverse' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: FunctionInverse' a -> S Int32 Source #

icod_ :: FunctionInverse' a -> S Int32 Source #

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

EmbPrj a => EmbPrj (Judgement a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Judgement a -> S Int32 Source #

icod_ :: Judgement a -> S Int32 Source #

value :: Int32 -> R (Judgement a) Source #

EmbPrj a => EmbPrj (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Open a -> S Int32 Source #

icod_ :: Open a -> S Int32 Source #

value :: Int32 -> R (Open a) Source #

EmbPrj a => EmbPrj (List1 a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: List1 a -> S Int32 Source #

icod_ :: List1 a -> S Int32 Source #

value :: Int32 -> R (List1 a) Source #

EmbPrj a => EmbPrj (List2 a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: List2 a -> S Int32 Source #

icod_ :: List2 a -> S Int32 Source #

value :: Int32 -> R (List2 a) Source #

EmbPrj a => EmbPrj (Drop a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Drop a -> S Int32 Source #

icod_ :: Drop a -> S Int32 Source #

value :: Int32 -> R (Drop a) Source #

EmbPrj a => EmbPrj (RangeMap a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: RangeMap a -> S Int32 Source #

icod_ :: RangeMap a -> S Int32 Source #

value :: Int32 -> R (RangeMap a) Source #

Typeable a => EmbPrj (SmallSet a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: SmallSet a -> S Int32 Source #

icod_ :: SmallSet a -> S Int32 Source #

value :: Int32 -> R (SmallSet a) Source #

EmbPrj a => EmbPrj (Seq a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Seq a -> S Int32 Source #

icod_ :: Seq a -> S Int32 Source #

value :: Int32 -> 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 Int32 Source #

icod_ :: Set a -> S Int32 Source #

value :: Int32 -> R (Set a) Source #

EmbPrj a => EmbPrj (Maybe a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Maybe a -> S Int32 Source #

icod_ :: Maybe a -> S Int32 Source #

value :: Int32 -> R (Maybe a) Source #

EmbPrj a => EmbPrj (Maybe a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Maybe a -> S Int32 Source #

icod_ :: Maybe a -> S Int32 Source #

value :: Int32 -> R (Maybe a) Source #

EmbPrj a => EmbPrj [a] Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: [a] -> S Int32 Source #

icod_ :: [a] -> S Int32 Source #

value :: Int32 -> 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 Int32 Source #

icod_ :: ImportedName' a b -> S Int32 Source #

value :: Int32 -> 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 Int32 Source #

icod_ :: Named s t -> S Int32 Source #

value :: Int32 -> 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 Int32 Source #

icod_ :: BiMap k v -> S Int32 Source #

value :: Int32 -> 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 Int32 Source #

icod_ :: Trie a b -> S Int32 Source #

value :: Int32 -> 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 Int32 Source #

icod_ :: WithDefault' a b -> S Int32 Source #

value :: Int32 -> R (WithDefault' 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 Int32 Source #

icod_ :: Either a b -> S Int32 Source #

value :: Int32 -> R (Either 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 Int32 Source #

icod_ :: Map a b -> S Int32 Source #

value :: Int32 -> R (Map 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 Int32 Source #

icod_ :: Pair a b -> S Int32 Source #

value :: Int32 -> 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 Int32 Source #

icod_ :: HashMap k v -> S Int32 Source #

value :: Int32 -> 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 Int32 Source #

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

value :: Int32 -> 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 Int32 Source #

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

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