Agda-2.6.2.2: 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 Encoded Source #

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

encodeFile :: FilePath -> Interface -> TCM ByteString Source #

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

An uncompressed bytestring corresponding to the encoded interface is returned.

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

Decodes an uncompressed bytestring (without extra hashes or magic numbers). The result depends on the include path.

Returns Nothing if a decoding error is encountered.

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

Decodes an interface. The result depends on the include path.

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

class Typeable a => EmbPrj a Source #

Instances

Instances details
EmbPrj Bool Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Char Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Double Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Int Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Int32 Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Integer Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Word64 Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj CallStack Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

EmbPrj Text Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Text Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Void Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj SrcLoc Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj IntSet Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Doc Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj CutOff Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj Impossible Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Permutation Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj AbsolutePath Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Range Source #

Ranges are always deserialised as noRange.

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj GenPart Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ExpandedEllipsis Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Fixity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Associativity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj FixityLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj NameId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ModuleNameHash Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj IsAbstract Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Access Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj ProjOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ConOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj FreeVariables Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Cohesion Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Lock Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Annotation Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj QωOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Q1Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Q0Origin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Modality Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Induction Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj PatternOrCopattern Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Language Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Cubical Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj FileType Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Delayed Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Precedence Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj ParenPreference Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj UnicodeOrAscii Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj NameInScope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj TopLevelModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj QName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj NamePart Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Name Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj Warning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj Suffix Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj AmbiguousQName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj QName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Name Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj Literal Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj WarningName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj WarningMode Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj ParseWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj LibWarning' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj LibWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj LibPositionInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj ExecutablesFile Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj Range Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj LazySplit Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj DeclarationWarning' Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj DeclarationWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj AbstractModule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj NameMetadata Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj AbstractName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj WhyInScope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj KindOfName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj NameOrModule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj NameSpace Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj LocalVar Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj BindingSource Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj ScopeInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj NameSpaceId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj DataOrRecordModule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj Scope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj ConPatLazy Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj ConPatInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj TokenBased Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj DefinitionSite Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj Aspects Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj OtherAspect Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj NameKind Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj Aspect Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

EmbPrj ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj PatOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj PatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Clause Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Blocked_ Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj NotBlocked Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Level Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Sort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj IsFibrant Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Term Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj ConHead Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj DataOrRecord Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj BindName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

EmbPrj ConfluenceCheck Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj PragmaOptions Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj RecordFieldWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

EmbPrj MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Defn Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Projection Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj System Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

EmbPrj IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Definition Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Section Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Signature Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Interface Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances

EmbPrj ForeignCode Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

EmbPrj CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj SerialisedRange Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

EmbPrj AbsNameWithFixity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: List2 a -> S Int32 Source #

icod_ :: List2 a -> S Int32 Source #

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

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

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Int32 Source #

icod_ :: Dom a -> S Int32 Source #

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

EmbPrj a => EmbPrj (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

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

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

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 #

(Eq k, Hashable k, EmbPrj k, EmbPrj v) => EmbPrj (HashMap k v) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

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

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

value :: Int32 -> R (HashMap k v) Source #

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

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

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

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

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

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

value :: Int32 -> R (BiMap k v) Source #

(EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

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