Agda-2.7.0.1: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Serialise.Instances.Common

Synopsis

Documentation

newtype SerialisedRange Source #

Ranges that should be serialised properly.

Constructors

SerialisedRange 

Orphan instances

EmbPrj OptionsPragma Source # 
Instance details

EmbPrj AmbiguousQName Source # 
Instance details

EmbPrj ModuleName Source # 
Instance details

EmbPrj Name Source # 
Instance details

EmbPrj QName Source # 
Instance details

EmbPrj BuiltinId Source # 
Instance details

EmbPrj PrimitiveId Source # 
Instance details

EmbPrj SomeBuiltin Source # 
Instance details

EmbPrj Annotation Source # 
Instance details

EmbPrj ArgInfo Source # 
Instance details

EmbPrj Associativity Source # 
Instance details

EmbPrj BoundVariablePosition Source # 
Instance details

EmbPrj Cohesion Source # 
Instance details

EmbPrj ConOrigin Source # 
Instance details

EmbPrj Cubical Source # 
Instance details

EmbPrj ExpandedEllipsis Source # 
Instance details

EmbPrj FileType Source # 
Instance details

EmbPrj Fixity Source # 
Instance details

EmbPrj Fixity' Source # 
Instance details

EmbPrj FixityLevel Source # 
Instance details

EmbPrj FreeVariables Source # 
Instance details

EmbPrj Hiding Source # 
Instance details

EmbPrj IsAbstract Source # 
Instance details

EmbPrj IsInstance Source # 
Instance details

EmbPrj IsOpaque Source # 
Instance details

EmbPrj Language Source # 
Instance details

EmbPrj Lock Source # 
Instance details

EmbPrj MetaId Source # 
Instance details

EmbPrj Modality Source # 
Instance details

EmbPrj NameId Source # 
Instance details

EmbPrj NotationPart Source # 
Instance details

EmbPrj OpaqueId Source # 
Instance details

EmbPrj Origin Source # 
Instance details

EmbPrj OverlapMode Source # 
Instance details

EmbPrj PatternOrCopattern Source # 
Instance details

EmbPrj ProblemId Source # 
Instance details

EmbPrj ProjOrigin Source # 
Instance details

EmbPrj Q0Origin Source # 
Instance details

EmbPrj Q1Origin Source # 
Instance details

EmbPrj Quantity Source # 
Instance details

EmbPrj QωOrigin Source # 
Instance details

EmbPrj Relevance Source # 
Instance details

EmbPrj Induction Source # 
Instance details

EmbPrj KwRange Source # 
Instance details

EmbPrj RecordDirective Source # 
Instance details

EmbPrj Name Source # 
Instance details

EmbPrj NameInScope Source # 
Instance details

EmbPrj NamePart Source # 
Instance details

EmbPrj QName Source # 
Instance details

EmbPrj Literal Source # 
Instance details

EmbPrj Range Source #

Ranges are always deserialised as noRange.

Instance details

EmbPrj RangeFile Source # 
Instance details

EmbPrj TopLevelModuleName Source # 
Instance details

EmbPrj ModuleNameHash Source # 
Instance details

EmbPrj Impossible Source # 
Instance details

EmbPrj Void Source # 
Instance details

EmbPrj Int32 Source # 
Instance details

EmbPrj CallStack Source # 
Instance details

EmbPrj SrcLoc Source # 
Instance details

EmbPrj Word64 Source # 
Instance details

EmbPrj IntSet Source # 
Instance details

EmbPrj Text Source # 
Instance details

EmbPrj Text Source # 
Instance details

EmbPrj String Source # 
Instance details

EmbPrj Integer Source # 
Instance details

EmbPrj () Source # 
Instance details

Methods

icode :: () -> S Int32 Source #

icod_ :: () -> S Int32 Source #

value :: Int32 -> R () Source #

EmbPrj Bool Source # 
Instance details

EmbPrj Char Source # 
Instance details

EmbPrj Double Source # 
Instance details

EmbPrj Int Source # 
Instance details

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

Methods

icode :: Arg a -> S Int32 Source #

icod_ :: Arg a -> S Int32 Source #

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

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

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

Methods

icode :: Ranged a -> S Int32 Source #

icod_ :: Ranged a -> S Int32 Source #

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

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

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

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

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

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

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

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

Methods

icode :: List1 a -> S Int32 Source #

icod_ :: List1 a -> S Int32 Source #

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

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

Methods

icode :: List2 a -> S Int32 Source #

icod_ :: List2 a -> S Int32 Source #

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

Typeable a => EmbPrj (SmallSet a) Source # 
Instance details

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

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

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

Methods

icode :: Maybe a -> S Int32 Source #

icod_ :: Maybe a -> S Int32 Source #

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

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

Methods

icode :: Maybe a -> S Int32 Source #

icod_ :: Maybe a -> S Int32 Source #

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

EmbPrj a => EmbPrj [a] Source # 
Instance details

Methods

icode :: [a] -> S Int32 Source #

icod_ :: [a] -> S Int32 Source #

value :: Int32 -> R [a] Source #

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

(EmbPrj s, EmbPrj t) => EmbPrj (Named s t) Source # 
Instance details

Methods

icode :: Named s t -> S Int32 Source #

icod_ :: Named s t -> S Int32 Source #

value :: Int32 -> R (Named s t) Source #

(EmbPrj k, EmbPrj v, EmbPrj (Tag v)) => EmbPrj (BiMap k v) Source # 
Instance details

Methods

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

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

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

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

Methods

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

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

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

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

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

Methods

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

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

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

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

Methods

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

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

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

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

Methods

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

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

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

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

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

Methods

icode :: (a, b) -> S Int32 Source #

icod_ :: (a, b) -> S Int32 Source #

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

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

Methods

icode :: (a, b, c) -> S Int32 Source #

icod_ :: (a, b, c) -> S Int32 Source #

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