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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Serialise

Description

Structure-sharing serialisation of Agda interface files.

Synopsis

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

# Documentation

encode :: EmbPrj a => a -> TCM 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.

encodeInterface :: Interface -> TCM ByteString Source #

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 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 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 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 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 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 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 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 Methods icode :: TopLevelModuleName -> S Int32 Source # icod_ :: TopLevelModuleName -> S Int32 Source # value :: Int32 -> R TopLevelModuleName 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 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 Methods icode :: ParenPreference -> S Int32 Source # icod_ :: ParenPreference -> S Int32 Source # value :: Int32 -> R ParenPreference 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 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 Methods icode :: PrecedenceLevel -> S Int32 Source # icod_ :: PrecedenceLevel -> S Int32 Source # value :: Int32 -> R PrecedenceLevel Source #
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 Methods icode :: CompiledClauses -> S Int32 Source # icod_ :: CompiledClauses -> S Int32 Source # value :: Int32 -> R CompiledClauses 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 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 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 Methods icode :: LibPositionInfo -> S Int32 Source # icod_ :: LibPositionInfo -> S Int32 Source # value :: Int32 -> R LibPositionInfo 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 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 Methods icode :: NumGeneralizableArgs -> S Int32 Source # icod_ :: NumGeneralizableArgs -> S Int32 Source # value :: Int32 -> R NumGeneralizableArgs 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 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 Methods icode :: SerialisedRange -> S Int32 Source # icod_ :: SerialisedRange -> S Int32 Source # value :: Int32 -> R SerialisedRange 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 (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 (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 (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 (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 #
(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 (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 #
(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 #