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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Serialise

Description

Structure-sharing serialisation of Agda interface files.

Synopsis

Documentation

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

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

encodeFile :: FilePath -> Interface -> TCM () Source #

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

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

Decodes something. The result depends on the include path.

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

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

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

Decodes something. 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
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 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 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 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 () Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: () -> S Int32 Source #

icod_ :: () -> S Int32 Source #

value :: Int32 -> R () 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 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 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 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 Empty Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Empty -> S Int32 Source #

icod_ :: Empty -> S Int32 Source #

value :: Int32 -> R Empty 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 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 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 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 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 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 AbsolutePath Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: AbsolutePath -> S Int32 Source #

icod_ :: AbsolutePath -> S Int32 Source #

value :: Int32 -> R AbsolutePath 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 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 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 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 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 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 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 DataOrRecord Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: DataOrRecord -> S Int32 Source #

icod_ :: DataOrRecord -> S Int32 Source #

value :: Int32 -> R DataOrRecord 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 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 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 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 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 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 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 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 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 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 HasEta Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: HasEta -> S Int32 Source #

icod_ :: HasEta -> S Int32 Source #

value :: Int32 -> R HasEta 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 Delayed Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Delayed -> S Int32 Source #

icod_ :: Delayed -> S Int32 Source #

value :: Int32 -> R Delayed Source #

EmbPrj GenPart Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: GenPart -> S Int32 Source #

icod_ :: GenPart -> S Int32 Source #

value :: Int32 -> R GenPart 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 TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

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 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 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 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 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 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 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 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 ParenPreference Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

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 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 PrecedenceLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

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 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 CompressedFile Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: CompressedFile -> S Int32 Source #

icod_ :: CompressedFile -> S Int32 Source #

value :: Int32 -> R CompressedFile 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 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 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 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 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 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 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 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 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 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 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 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 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 Binder Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Binder -> S Int32 Source #

icod_ :: Binder -> S Int32 Source #

value :: Int32 -> R Binder 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 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 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 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 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 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 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 LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: LevelAtom -> S Int32 Source #

icod_ :: LevelAtom -> S Int32 Source #

value :: Int32 -> R LevelAtom 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 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 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 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 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 CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

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 DeclarationWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

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 LibPositionInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

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 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 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 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 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 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 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 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 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 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 SerialisedRange Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

(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 (NonemptyList a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NonemptyList a -> S Int32 Source #

icod_ :: NonemptyList a -> S Int32 Source #

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

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 (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 (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 (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 (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Dom a -> S Int32 Source #

icod_ :: Dom a -> S Int32 Source #

value :: Int32 -> R (Dom 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 (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 (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 (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 (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 (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 (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 (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 (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 => 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 (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 #

Typeable b => EmbPrj (WithDefault b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: WithDefault b -> S Int32 Source #

icod_ :: WithDefault b -> S Int32 Source #

value :: Int32 -> R (WithDefault b) 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 (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 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 #

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

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

(Ord a, Ord b, EmbPrj a, EmbPrj b) => EmbPrj (BiMap a b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: BiMap a b -> S Int32 Source #

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

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

(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, 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 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 #