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 #

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

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

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

encodeInterface :: Interface -> TCM ByteString #

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

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

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

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

class Typeable a => EmbPrj a #

Minimal complete definition

icod_, value

Instances

EmbPrj Bool #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Bool -> S Int32 # icod_ :: Bool -> S Int32 # value :: Int32 -> R Bool #
EmbPrj Char #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Char -> S Int32 # icod_ :: Char -> S Int32 # value :: Int32 -> R Char #
EmbPrj Double #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Double -> S Int32 # icod_ :: Double -> S Int32 # value :: Int32 -> R Double #
EmbPrj Int #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Int -> S Int32 # icod_ :: Int -> S Int32 # value :: Int32 -> R Int #
EmbPrj Int32 #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Int32 -> S Int32 # icod_ :: Int32 -> S Int32 # value :: Int32 -> R Int32 #
EmbPrj Integer #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Integer -> S Int32 # icod_ :: Integer -> S Int32 # value :: Int32 -> R Integer #
EmbPrj Word64 #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Word64 -> S Int32 # icod_ :: Word64 -> S Int32 # value :: Int32 -> R Word64 #
EmbPrj () #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: () -> S Int32 # icod_ :: () -> S Int32 # value :: Int32 -> R () #
EmbPrj Void #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Void -> S Int32 # icod_ :: Void -> S Int32 # value :: Int32 -> R Void #
EmbPrj String #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: String -> S Int32 # icod_ :: String -> S Int32 # value :: Int32 -> R String #
EmbPrj ByteString #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ByteString -> S Int32 # icod_ :: ByteString -> S Int32 # value :: Int32 -> R ByteString #
EmbPrj IntSet #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IntSet -> S Int32 # icod_ :: IntSet -> S Int32 # value :: Int32 -> R IntSet #
EmbPrj Doc #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: Doc -> S Int32 # icod_ :: Doc -> S Int32 # value :: Int32 -> R Doc #
EmbPrj Impossible #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Impossible -> S Int32 # icod_ :: Impossible -> S Int32 # value :: Int32 -> R Impossible #
EmbPrj Empty #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Empty -> S Int32 # icod_ :: Empty -> S Int32 # value :: Int32 -> R Empty #
EmbPrj AbsolutePath #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: AbsolutePath -> S Int32 # icod_ :: AbsolutePath -> S Int32 # value :: Int32 -> R AbsolutePath #
EmbPrj Range #	Ranges are always deserialised as `noRange`.
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Range -> S Int32 # icod_ :: Range -> S Int32 # value :: Int32 -> R Range #
EmbPrj Permutation #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Permutation -> S Int32 # icod_ :: Permutation -> S Int32 # value :: Int32 -> R Permutation #
EmbPrj Fixity' #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Fixity' -> S Int32 # icod_ :: Fixity' -> S Int32 # value :: Int32 -> R Fixity' #
EmbPrj MetaId #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: MetaId -> S Int32 # icod_ :: MetaId -> S Int32 # value :: Int32 -> R MetaId #
EmbPrj NameId #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NameId -> S Int32 # icod_ :: NameId -> S Int32 # value :: Int32 -> R NameId #
EmbPrj IsAbstract #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IsAbstract -> S Int32 # icod_ :: IsAbstract -> S Int32 # value :: Int32 -> R IsAbstract #
EmbPrj Access #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Access -> S Int32 # icod_ :: Access -> S Int32 # value :: Int32 -> R Access #
EmbPrj DataOrRecord #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: DataOrRecord -> S Int32 # icod_ :: DataOrRecord -> S Int32 # value :: Int32 -> R DataOrRecord #
EmbPrj ProjOrigin #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ProjOrigin -> S Int32 # icod_ :: ProjOrigin -> S Int32 # value :: Int32 -> R ProjOrigin #
EmbPrj ConOrigin #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ConOrigin -> S Int32 # icod_ :: ConOrigin -> S Int32 # value :: Int32 -> R ConOrigin #
EmbPrj ArgInfo #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ArgInfo -> S Int32 # icod_ :: ArgInfo -> S Int32 # value :: Int32 -> R ArgInfo #
EmbPrj FreeVariables #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FreeVariables -> S Int32 # icod_ :: FreeVariables -> S Int32 # value :: Int32 -> R FreeVariables #
EmbPrj Origin #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Origin -> S Int32 # icod_ :: Origin -> S Int32 # value :: Int32 -> R Origin #
EmbPrj Relevance #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Relevance -> S Int32 # icod_ :: Relevance -> S Int32 # value :: Int32 -> R Relevance #
EmbPrj Quantity #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Quantity -> S Int32 # icod_ :: Quantity -> S Int32 # value :: Int32 -> R Quantity #
EmbPrj Modality #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Modality -> S Int32 # icod_ :: Modality -> S Int32 # value :: Int32 -> R Modality #
EmbPrj Hiding #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Hiding -> S Int32 # icod_ :: Hiding -> S Int32 # value :: Int32 -> R Hiding #
EmbPrj Induction #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Induction -> S Int32 # icod_ :: Induction -> S Int32 # value :: Int32 -> R Induction #
EmbPrj HasEta #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: HasEta -> S Int32 # icod_ :: HasEta -> S Int32 # value :: Int32 -> R HasEta #
EmbPrj Delayed #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Delayed -> S Int32 # icod_ :: Delayed -> S Int32 # value :: Int32 -> R Delayed #
EmbPrj TopLevelModuleName #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: TopLevelModuleName -> S Int32 # icod_ :: TopLevelModuleName -> S Int32 # value :: Int32 -> R TopLevelModuleName #
EmbPrj QName #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QName -> S Int32 # icod_ :: QName -> S Int32 # value :: Int32 -> R QName #
EmbPrj NamePart #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NamePart -> S Int32 # icod_ :: NamePart -> S Int32 # value :: Int32 -> R NamePart #
EmbPrj Name #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Name -> S Int32 # icod_ :: Name -> S Int32 # value :: Int32 -> R Name #
EmbPrj GenPart #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: GenPart -> S Int32 # icod_ :: GenPart -> S Int32 # value :: Int32 -> R GenPart #
EmbPrj AmbiguousQName #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: AmbiguousQName -> S Int32 # icod_ :: AmbiguousQName -> S Int32 # value :: Int32 -> R AmbiguousQName #
EmbPrj ModuleName #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ModuleName -> S Int32 # icod_ :: ModuleName -> S Int32 # value :: Int32 -> R ModuleName #
EmbPrj QName #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QName -> S Int32 # icod_ :: QName -> S Int32 # value :: Int32 -> R QName #
EmbPrj Name #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Name -> S Int32 # icod_ :: Name -> S Int32 # value :: Int32 -> R Name #
EmbPrj Literal #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Literal -> S Int32 # icod_ :: Literal -> S Int32 # value :: Int32 -> R Literal #
EmbPrj Precedence #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Precedence -> S Int32 # icod_ :: Precedence -> S Int32 # value :: Int32 -> R Precedence #
EmbPrj ParenPreference #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ParenPreference -> S Int32 # icod_ :: ParenPreference -> S Int32 # value :: Int32 -> R ParenPreference #
EmbPrj Fixity #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Fixity -> S Int32 # icod_ :: Fixity -> S Int32 # value :: Int32 -> R Fixity #
EmbPrj Associativity #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Associativity -> S Int32 # icod_ :: Associativity -> S Int32 # value :: Int32 -> R Associativity #
EmbPrj PrecedenceLevel #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: PrecedenceLevel -> S Int32 # icod_ :: PrecedenceLevel -> S Int32 # value :: Int32 -> R PrecedenceLevel #
EmbPrj Range #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Range -> S Int32 # icod_ :: Range -> S Int32 # value :: Int32 -> R Range #
EmbPrj Occurrence #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Occurrence -> S Int32 # icod_ :: Occurrence -> S Int32 # value :: Int32 -> R Occurrence #
EmbPrj CompressedFile #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: CompressedFile -> S Int32 # icod_ :: CompressedFile -> S Int32 # value :: Int32 -> R CompressedFile #
EmbPrj TokenBased #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: TokenBased -> S Int32 # icod_ :: TokenBased -> S Int32 # value :: Int32 -> R TokenBased #
EmbPrj DefinitionSite #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: DefinitionSite -> S Int32 # icod_ :: DefinitionSite -> S Int32 # value :: Int32 -> R DefinitionSite #
EmbPrj Aspects #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Aspects -> S Int32 # icod_ :: Aspects -> S Int32 # value :: Int32 -> R Aspects #
EmbPrj OtherAspect #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: OtherAspect -> S Int32 # icod_ :: OtherAspect -> S Int32 # value :: Int32 -> R OtherAspect #
EmbPrj NameKind #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: NameKind -> S Int32 # icod_ :: NameKind -> S Int32 # value :: Int32 -> R NameKind #
EmbPrj Aspect #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Aspect -> S Int32 # icod_ :: Aspect -> S Int32 # value :: Int32 -> R Aspect #
EmbPrj AbstractModule #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbstractModule -> S Int32 # icod_ :: AbstractModule -> S Int32 # value :: Int32 -> R AbstractModule #
EmbPrj AbstractName #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbstractName -> S Int32 # icod_ :: AbstractName -> S Int32 # value :: Int32 -> R AbstractName #
EmbPrj WhyInScope #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: WhyInScope -> S Int32 # icod_ :: WhyInScope -> S Int32 # value :: Int32 -> R WhyInScope #
EmbPrj KindOfName #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: KindOfName -> S Int32 # icod_ :: KindOfName -> S Int32 # value :: Int32 -> R KindOfName #
EmbPrj NameSpace #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameSpace -> S Int32 # icod_ :: NameSpace -> S Int32 # value :: Int32 -> R NameSpace #
EmbPrj LocalVar #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: LocalVar -> S Int32 # icod_ :: LocalVar -> S Int32 # value :: Int32 -> R LocalVar #
EmbPrj Binder #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Binder -> S Int32 # icod_ :: Binder -> S Int32 # value :: Int32 -> R Binder #
EmbPrj ScopeInfo #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ScopeInfo -> S Int32 # icod_ :: ScopeInfo -> S Int32 # value :: Int32 -> R ScopeInfo #
EmbPrj NameSpaceId #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameSpaceId -> S Int32 # icod_ :: NameSpaceId -> S Int32 # value :: Int32 -> R NameSpaceId #
EmbPrj Scope #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Scope -> S Int32 # icod_ :: Scope -> S Int32 # value :: Int32 -> R Scope #
EmbPrj ConPatInfo #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ConPatInfo -> S Int32 # icod_ :: ConPatInfo -> S Int32 # value :: Int32 -> R ConPatInfo #
EmbPrj ConPatternInfo #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConPatternInfo -> S Int32 # icod_ :: ConPatternInfo -> S Int32 # value :: Int32 -> R ConPatternInfo #
EmbPrj DBPatVar #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DBPatVar -> S Int32 # icod_ :: DBPatVar -> S Int32 # value :: Int32 -> R DBPatVar #
EmbPrj PatOrigin #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PatOrigin -> S Int32 # icod_ :: PatOrigin -> S Int32 # value :: Int32 -> R PatOrigin #
EmbPrj Clause #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Clause -> S Int32 # icod_ :: Clause -> S Int32 # value :: Int32 -> R Clause #
EmbPrj LevelAtom #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: LevelAtom -> S Int32 # icod_ :: LevelAtom -> S Int32 # value :: Int32 -> R LevelAtom #
EmbPrj PlusLevel #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PlusLevel -> S Int32 # icod_ :: PlusLevel -> S Int32 # value :: Int32 -> R PlusLevel #
EmbPrj Level #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Level -> S Int32 # icod_ :: Level -> S Int32 # value :: Int32 -> R Level #
EmbPrj Sort #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Sort -> S Int32 # icod_ :: Sort -> S Int32 # value :: Int32 -> R Sort #
EmbPrj Term #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Term -> S Int32 # icod_ :: Term -> S Int32 # value :: Int32 -> R Term #
EmbPrj ConHead #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConHead -> S Int32 # icod_ :: ConHead -> S Int32 # value :: Int32 -> R ConHead #
EmbPrj CompiledClauses #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CompiledClauses -> S Int32 # icod_ :: CompiledClauses -> S Int32 # value :: Int32 -> R CompiledClauses #
EmbPrj BindName #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: BindName -> S Int32 # icod_ :: BindName -> S Int32 # value :: Int32 -> R BindName #
EmbPrj DeclarationWarning #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: DeclarationWarning -> S Int32 # icod_ :: DeclarationWarning -> S Int32 # value :: Int32 -> R DeclarationWarning #
EmbPrj TCWarning #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: TCWarning -> S Int32 # icod_ :: TCWarning -> S Int32 # value :: Int32 -> R TCWarning #
EmbPrj Warning #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: Warning -> S Int32 # icod_ :: Warning -> S Int32 # value :: Int32 -> R Warning #
EmbPrj MutualId #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: MutualId -> S Int32 # icod_ :: MutualId -> S Int32 # value :: Int32 -> R MutualId #
EmbPrj TermHead #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: TermHead -> S Int32 # icod_ :: TermHead -> S Int32 # value :: Int32 -> R TermHead #
EmbPrj Defn #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Defn -> S Int32 # icod_ :: Defn -> S Int32 # value :: Int32 -> R Defn #
EmbPrj FunctionFlag #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: FunctionFlag -> S Int32 # icod_ :: FunctionFlag -> S Int32 # value :: Int32 -> R FunctionFlag #
EmbPrj EtaEquality #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: EtaEquality -> S Int32 # icod_ :: EtaEquality -> S Int32 # value :: Int32 -> R EtaEquality #
EmbPrj ProjLams #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ProjLams -> S Int32 # icod_ :: ProjLams -> S Int32 # value :: Int32 -> R ProjLams #
EmbPrj Projection #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Projection -> S Int32 # icod_ :: Projection -> S Int32 # value :: Int32 -> R Projection #
EmbPrj ExtLamInfo #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ExtLamInfo -> S Int32 # icod_ :: ExtLamInfo -> S Int32 # value :: Int32 -> R ExtLamInfo #
EmbPrj CompilerPragma #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: CompilerPragma -> S Int32 # icod_ :: CompilerPragma -> S Int32 # value :: Int32 -> R CompilerPragma #
EmbPrj IsForced #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: IsForced -> S Int32 # icod_ :: IsForced -> S Int32 # value :: Int32 -> R IsForced #
EmbPrj Polarity #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Polarity -> S Int32 # icod_ :: Polarity -> S Int32 # value :: Int32 -> R Polarity #
EmbPrj Definition #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Definition -> S Int32 # icod_ :: Definition -> S Int32 # value :: Int32 -> R Definition #
EmbPrj RewriteRule #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: RewriteRule -> S Int32 # icod_ :: RewriteRule -> S Int32 # value :: Int32 -> R RewriteRule #
EmbPrj NLPType #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NLPType -> S Int32 # icod_ :: NLPType -> S Int32 # value :: Int32 -> R NLPType #
EmbPrj NLPat #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NLPat -> S Int32 # icod_ :: NLPat -> S Int32 # value :: Int32 -> R NLPat #
EmbPrj DisplayTerm #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DisplayTerm -> S Int32 # icod_ :: DisplayTerm -> S Int32 # value :: Int32 -> R DisplayTerm #
EmbPrj DisplayForm #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DisplayForm -> S Int32 # icod_ :: DisplayForm -> S Int32 # value :: Int32 -> R DisplayForm #
EmbPrj Section #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Section -> S Int32 # icod_ :: Section -> S Int32 # value :: Int32 -> R Section #
EmbPrj Signature #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Signature -> S Int32 # icod_ :: Signature -> S Int32 # value :: Int32 -> R Signature #
EmbPrj Interface #
Instance details Defined in Agda.TypeChecking.Serialise.Instances Methods icode :: Interface -> S Int32 # icod_ :: Interface -> S Int32 # value :: Int32 -> R Interface #
EmbPrj ForeignCode #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: ForeignCode -> S Int32 # icod_ :: ForeignCode -> S Int32 # value :: Int32 -> R ForeignCode #
EmbPrj CheckpointId #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CheckpointId -> S Int32 # icod_ :: CheckpointId -> S Int32 # value :: Int32 -> R CheckpointId #
EmbPrj SerialisedRange #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: SerialisedRange -> S Int32 # icod_ :: SerialisedRange -> S Int32 # value :: Int32 -> R SerialisedRange #
EmbPrj a => EmbPrj [a] #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: [a] -> S Int32 # icod_ :: [a] -> S Int32 # value :: Int32 -> R [a] #
EmbPrj a => EmbPrj (Maybe a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Maybe a -> S Int32 # icod_ :: Maybe a -> S Int32 # value :: Int32 -> R (Maybe a) #
EmbPrj a => EmbPrj (Seq a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Seq a -> S Int32 # icod_ :: Seq a -> S Int32 # value :: Int32 -> R (Seq a) #
(Ord a, EmbPrj a) => EmbPrj (Set a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Set a -> S Int32 # icod_ :: Set a -> S Int32 # value :: Int32 -> R (Set a) #
EmbPrj a => EmbPrj (Maybe a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Maybe a -> S Int32 # icod_ :: Maybe a -> S Int32 # value :: Int32 -> R (Maybe a) #
EmbPrj a => EmbPrj (NonemptyList a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NonemptyList a -> S Int32 # icod_ :: NonemptyList a -> S Int32 # value :: Int32 -> R (NonemptyList a) #
EmbPrj a => EmbPrj (Interval' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Interval' a -> S Int32 # icod_ :: Interval' a -> S Int32 # value :: Int32 -> R (Interval' a) #
EmbPrj a => EmbPrj (Position' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Position' a -> S Int32 # icod_ :: Position' a -> S Int32 # value :: Int32 -> R (Position' a) #
EmbPrj a => EmbPrj (Drop a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Drop a -> S Int32 # icod_ :: Drop a -> S Int32 # value :: Int32 -> R (Drop a) #
EmbPrj a => EmbPrj (Ranged a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Ranged a -> S Int32 # icod_ :: Ranged a -> S Int32 # value :: Int32 -> R (Ranged a) #
EmbPrj a => EmbPrj (Dom a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Dom a -> S Int32 # icod_ :: Dom a -> S Int32 # value :: Int32 -> R (Dom a) #
EmbPrj a => EmbPrj (Arg a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Arg a -> S Int32 # icod_ :: Arg a -> S Int32 # value :: Int32 -> R (Arg a) #
EmbPrj a => EmbPrj (WithHiding a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: WithHiding a -> S Int32 # icod_ :: WithHiding a -> S Int32 # value :: Int32 -> R (WithHiding a) #
EmbPrj a => EmbPrj (FieldAssignment' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FieldAssignment' a -> S Int32 # icod_ :: FieldAssignment' a -> S Int32 # value :: Int32 -> R (FieldAssignment' a) #
EmbPrj a => EmbPrj (Substitution' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Substitution' a -> S Int32 # icod_ :: Substitution' a -> S Int32 # value :: Int32 -> R (Substitution' a) #
EmbPrj a => EmbPrj (Pattern' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Pattern' a -> S Int32 # icod_ :: Pattern' a -> S Int32 # value :: Int32 -> R (Pattern' a) #
EmbPrj a => EmbPrj (Tele a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Tele a -> S Int32 # icod_ :: Tele a -> S Int32 # value :: Int32 -> R (Tele a) #
EmbPrj a => EmbPrj (Type' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Type' a -> S Int32 # icod_ :: Type' a -> S Int32 # value :: Int32 -> R (Type' a) #
EmbPrj a => EmbPrj (Abs a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Abs a -> S Int32 # icod_ :: Abs a -> S Int32 # value :: Int32 -> R (Abs a) #
EmbPrj a => EmbPrj (Elim' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Elim' a -> S Int32 # icod_ :: Elim' a -> S Int32 # value :: Int32 -> R (Elim' a) #
EmbPrj a => EmbPrj (Case a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Case a -> S Int32 # icod_ :: Case a -> S Int32 # value :: Int32 -> R (Case a) #
EmbPrj a => EmbPrj (WithArity a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: WithArity a -> S Int32 # icod_ :: WithArity a -> S Int32 # value :: Int32 -> R (WithArity a) #
EmbPrj a => EmbPrj (Pattern' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Pattern' a -> S Int32 # icod_ :: Pattern' a -> S Int32 # value :: Int32 -> R (Pattern' a) #
EmbPrj a => EmbPrj (Builtin a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Builtin a -> S Int32 # icod_ :: Builtin a -> S Int32 # value :: Int32 -> R (Builtin a) #
EmbPrj a => EmbPrj (FunctionInverse' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: FunctionInverse' a -> S Int32 # icod_ :: FunctionInverse' a -> S Int32 # value :: Int32 -> R (FunctionInverse' a) #
EmbPrj a => EmbPrj (Open a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Open a -> S Int32 # icod_ :: Open a -> S Int32 # value :: Int32 -> R (Open a) #
(EmbPrj a, EmbPrj b) => EmbPrj (Either a b) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Either a b -> S Int32 # icod_ :: Either a b -> S Int32 # value :: Int32 -> R (Either a b) #
(EmbPrj a, EmbPrj b) => EmbPrj (a, b) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: (a, b) -> S Int32 # icod_ :: (a, b) -> S Int32 # value :: Int32 -> R (a, b) #
(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Map a b -> S Int32 # icod_ :: Map a b -> S Int32 # value :: Int32 -> R (Map a b) #
(Eq k, Hashable k, EmbPrj k, EmbPrj v) => EmbPrj (HashMap k v) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: HashMap k v -> S Int32 # icod_ :: HashMap k v -> S Int32 # value :: Int32 -> R (HashMap k v) #
(Ord a, Ord b, EmbPrj a, EmbPrj b) => EmbPrj (BiMap a b) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: BiMap a b -> S Int32 # icod_ :: BiMap a b -> S Int32 # value :: Int32 -> R (BiMap a b) #
(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Trie a b) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Trie a b -> S Int32 # icod_ :: Trie a b -> S Int32 # value :: Int32 -> R (Trie a b) #
(EmbPrj s, EmbPrj t) => EmbPrj (Named s t) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Named s t -> S Int32 # icod_ :: Named s t -> S Int32 # value :: Int32 -> R (Named s t) #
(EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj (a, b, c) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: (a, b, c) -> S Int32 # icod_ :: (a, b, c) -> S Int32 # value :: Int32 -> R (a, b, c) #