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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Serialise.Instances.Common

Contents

Orphan instances

EmbPrj Bool Source # 
EmbPrj Char Source # 
EmbPrj Double Source # 
EmbPrj Int Source # 
EmbPrj Int32 Source # 
EmbPrj Integer Source # 
EmbPrj Word64 Source # 
EmbPrj () Source # 

Methods

icode :: () -> S Int32 Source #

icod_ :: () -> S Int32 Source #

value :: Int32 -> R () Source #

EmbPrj Void Source # 
EmbPrj String Source # 
EmbPrj ByteString Source # 
EmbPrj AbsolutePath Source # 
EmbPrj Range Source #

Ranges are always deserialised as noRange.

EmbPrj MetaId Source # 
EmbPrj NameId Source # 
EmbPrj IsAbstract Source # 
EmbPrj ConPOrigin Source # 
EmbPrj ArgInfo Source # 
EmbPrj Relevance Source # 
EmbPrj Hiding Source # 
EmbPrj Induction Source # 
EmbPrj Delayed Source # 
EmbPrj TopLevelModuleName Source # 
EmbPrj QName Source # 
EmbPrj NamePart Source # 
EmbPrj Name Source # 
EmbPrj Fixity' Source # 
EmbPrj AmbiguousQName Source # 
EmbPrj ModuleName Source # 
EmbPrj QName Source # 
EmbPrj Name Source # 
EmbPrj Literal Source # 
EmbPrj GenPart Source # 
EmbPrj Fixity Source # 
EmbPrj Associativity Source # 
EmbPrj PrecedenceLevel Source # 
EmbPrj a => EmbPrj [a] Source # 

Methods

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

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

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

EmbPrj a => EmbPrj (Maybe a) Source # 

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 # 

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 # 

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 # 

Methods

icode :: Maybe a -> S Int32 Source #

icod_ :: Maybe a -> S Int32 Source #

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

EmbPrj a => EmbPrj (Interval' a) Source # 
EmbPrj a => EmbPrj (Position' a) Source # 
EmbPrj a => EmbPrj (Ranged a) Source # 

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 # 

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 # 

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 # 
EmbPrj a => EmbPrj (FieldAssignment' a) Source # 
(EmbPrj a, EmbPrj b) => EmbPrj (Either a b) Source # 

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 # 

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 # 

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 # 

Methods

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

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

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

(Ord a, Ord b, EmbPrj a, EmbPrj b) => EmbPrj (BiMap a b) Source # 

Methods

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

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

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

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

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 # 

Methods

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

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

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