Agda-2.2.4: A dependently typed functional programming language and proof assistant Source code Contents Index

Agda.TypeChecking.Serialise

Description

Structure-sharing serialisation of Agda interface files.

Documentation

encode :: EmbPrj a => a -> IO ByteString Source

encodeFile :: EmbPrj a => FilePath -> a -> IO () Source

decode :: EmbPrj a => ByteString -> IO a Source

decodeFile :: EmbPrj a => FilePath -> IO a Source

class Data a => EmbPrj a Source

Instances EmbPrj Bool EmbPrj Char EmbPrj Double EmbPrj Int EmbPrj Integer EmbPrj String EmbPrj Permutation EmbPrj Range EmbPrj Interval EmbPrj Position EmbPrj Literal EmbPrj NameId EmbPrj IsAbstract EmbPrj Access EmbPrj Hiding EmbPrj Induction EmbPrj QName EmbPrj NamePart EmbPrj Name EmbPrj Fixity EmbPrj ModuleName EmbPrj QName EmbPrj Name EmbPrj MetaId EmbPrj Pattern EmbPrj ClauseBody EmbPrj Clause EmbPrj Telescope EmbPrj Sort EmbPrj Type EmbPrj Term EmbPrj AbstractModule EmbPrj AbstractName EmbPrj KindOfName EmbPrj NameSpace EmbPrj Scope EmbPrj Range EmbPrj HighlightingInfo EmbPrj MetaInfo EmbPrj OtherAspect EmbPrj NameKind EmbPrj Aspect EmbPrj CtxId EmbPrj MutualId EmbPrj TermHead EmbPrj FunctionInverse EmbPrj Delayed EmbPrj Defn EmbPrj Occurrence EmbPrj Polarity EmbPrj HaskellRepresentation EmbPrj Definition EmbPrj DisplayTerm EmbPrj DisplayForm EmbPrj Section EmbPrj Signature EmbPrj Interface EmbPrj a => EmbPrj ([] a) EmbPrj a => EmbPrj (Maybe a) EmbPrj a => EmbPrj (Arg a) EmbPrj a => EmbPrj (Abs a) EmbPrj a => EmbPrj (Builtin a) EmbPrj a => EmbPrj (Open a) (EmbPrj a, EmbPrj b) => EmbPrj ((,) a b) (Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b) (EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj ((,,) a b c)

Produced by Haddock version 2.4.2