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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Serialise.Instances.Common

Contents

Orphan instances

EmbPrj Bool # 

Methods

icode :: Bool -> S Int32 #

icod_ :: Bool -> S Int32 #

value :: Int32 -> R Bool #

EmbPrj Char # 

Methods

icode :: Char -> S Int32 #

icod_ :: Char -> S Int32 #

value :: Int32 -> R Char #

EmbPrj Double # 

Methods

icode :: Double -> S Int32 #

icod_ :: Double -> S Int32 #

value :: Int32 -> R Double #

EmbPrj Int # 

Methods

icode :: Int -> S Int32 #

icod_ :: Int -> S Int32 #

value :: Int32 -> R Int #

EmbPrj Int32 # 

Methods

icode :: Int32 -> S Int32 #

icod_ :: Int32 -> S Int32 #

value :: Int32 -> R Int32 #

EmbPrj Integer # 
EmbPrj Word64 # 

Methods

icode :: Word64 -> S Int32 #

icod_ :: Word64 -> S Int32 #

value :: Int32 -> R Word64 #

EmbPrj () # 

Methods

icode :: () -> S Int32 #

icod_ :: () -> S Int32 #

value :: Int32 -> R () #

EmbPrj Void # 

Methods

icode :: Void -> S Int32 #

icod_ :: Void -> S Int32 #

value :: Int32 -> R Void #

EmbPrj String # 

Methods

icode :: String -> S Int32 #

icod_ :: String -> S Int32 #

value :: Int32 -> R String #

EmbPrj ByteString # 
EmbPrj AbsolutePath # 
EmbPrj Range #

Ranges are always deserialised as noRange.

Methods

icode :: Range -> S Int32 #

icod_ :: Range -> S Int32 #

value :: Int32 -> R Range #

EmbPrj Fixity' # 
EmbPrj MetaId # 

Methods

icode :: MetaId -> S Int32 #

icod_ :: MetaId -> S Int32 #

value :: Int32 -> R MetaId #

EmbPrj NameId # 

Methods

icode :: NameId -> S Int32 #

icod_ :: NameId -> S Int32 #

value :: Int32 -> R NameId #

EmbPrj IsAbstract # 
EmbPrj ProjOrigin # 
EmbPrj ConOrigin # 
EmbPrj ArgInfo # 
EmbPrj Origin # 

Methods

icode :: Origin -> S Int32 #

icod_ :: Origin -> S Int32 #

value :: Int32 -> R Origin #

EmbPrj Relevance # 
EmbPrj Hiding # 

Methods

icode :: Hiding -> S Int32 #

icod_ :: Hiding -> S Int32 #

value :: Int32 -> R Hiding #

EmbPrj Induction # 
EmbPrj Delayed # 
EmbPrj TopLevelModuleName # 
EmbPrj QName # 

Methods

icode :: QName -> S Int32 #

icod_ :: QName -> S Int32 #

value :: Int32 -> R QName #

EmbPrj NamePart # 
EmbPrj Name # 

Methods

icode :: Name -> S Int32 #

icod_ :: Name -> S Int32 #

value :: Int32 -> R Name #

EmbPrj GenPart # 
EmbPrj AmbiguousQName # 
EmbPrj ModuleName # 
EmbPrj QName # 

Methods

icode :: QName -> S Int32 #

icod_ :: QName -> S Int32 #

value :: Int32 -> R QName #

EmbPrj Name # 

Methods

icode :: Name -> S Int32 #

icod_ :: Name -> S Int32 #

value :: Int32 -> R Name #

EmbPrj Fixity # 

Methods

icode :: Fixity -> S Int32 #

icod_ :: Fixity -> S Int32 #

value :: Int32 -> R Fixity #

EmbPrj Associativity # 
EmbPrj PrecedenceLevel # 
EmbPrj Literal # 
EmbPrj a => EmbPrj [a] # 

Methods

icode :: [a] -> S Int32 #

icod_ :: [a] -> S Int32 #

value :: Int32 -> R [a] #

EmbPrj a => EmbPrj (Maybe a) # 

Methods

icode :: Maybe a -> S Int32 #

icod_ :: Maybe a -> S Int32 #

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

EmbPrj a => EmbPrj (Seq a) # 

Methods

icode :: Seq a -> S Int32 #

icod_ :: Seq a -> S Int32 #

value :: Int32 -> R (Seq a) #

(Ord a, EmbPrj a) => EmbPrj (Set a) # 

Methods

icode :: Set a -> S Int32 #

icod_ :: Set a -> S Int32 #

value :: Int32 -> R (Set a) #

EmbPrj a => EmbPrj (Maybe a) # 

Methods

icode :: Maybe a -> S Int32 #

icod_ :: Maybe a -> S Int32 #

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

EmbPrj a => EmbPrj (Interval' a) # 

Methods

icode :: Interval' a -> S Int32 #

icod_ :: Interval' a -> S Int32 #

value :: Int32 -> R (Interval' a) #

EmbPrj a => EmbPrj (Position' a) # 

Methods

icode :: Position' a -> S Int32 #

icod_ :: Position' a -> S Int32 #

value :: Int32 -> R (Position' a) #

EmbPrj a => EmbPrj (Ranged a) # 

Methods

icode :: Ranged a -> S Int32 #

icod_ :: Ranged a -> S Int32 #

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

EmbPrj a => EmbPrj (Dom a) # 

Methods

icode :: Dom a -> S Int32 #

icod_ :: Dom a -> S Int32 #

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

EmbPrj a => EmbPrj (Arg a) # 

Methods

icode :: Arg a -> S Int32 #

icod_ :: Arg a -> S Int32 #

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

EmbPrj a => EmbPrj (WithHiding a) # 

Methods

icode :: WithHiding a -> S Int32 #

icod_ :: WithHiding a -> S Int32 #

value :: Int32 -> R (WithHiding a) #

EmbPrj a => EmbPrj (FieldAssignment' a) # 
(EmbPrj a, EmbPrj b) => EmbPrj (Either a b) # 

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

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

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

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

Methods

icode :: BiMap a b -> S Int32 #

icod_ :: BiMap a b -> S Int32 #

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

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

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

Methods

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

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

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