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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Serialise.Instances.Common

Contents

Synopsis

Documentation

newtype SerialisedRange #

Ranges that should be serialised properly.

Constructors

SerialisedRange 

Orphan instances

EmbPrj Bool # 
Instance details

Methods

icode :: Bool -> S Int32 #

icod_ :: Bool -> S Int32 #

value :: Int32 -> R Bool #

EmbPrj Char # 
Instance details

Methods

icode :: Char -> S Int32 #

icod_ :: Char -> S Int32 #

value :: Int32 -> R Char #

EmbPrj Double # 
Instance details

Methods

icode :: Double -> S Int32 #

icod_ :: Double -> S Int32 #

value :: Int32 -> R Double #

EmbPrj Int # 
Instance details

Methods

icode :: Int -> S Int32 #

icod_ :: Int -> S Int32 #

value :: Int32 -> R Int #

EmbPrj Int32 # 
Instance details

Methods

icode :: Int32 -> S Int32 #

icod_ :: Int32 -> S Int32 #

value :: Int32 -> R Int32 #

EmbPrj Integer # 
Instance details

EmbPrj Word64 # 
Instance details

Methods

icode :: Word64 -> S Int32 #

icod_ :: Word64 -> S Int32 #

value :: Int32 -> R Word64 #

EmbPrj () # 
Instance details

Methods

icode :: () -> S Int32 #

icod_ :: () -> S Int32 #

value :: Int32 -> R () #

EmbPrj Void # 
Instance details

Methods

icode :: Void -> S Int32 #

icod_ :: Void -> S Int32 #

value :: Int32 -> R Void #

EmbPrj String # 
Instance details

Methods

icode :: String -> S Int32 #

icod_ :: String -> S Int32 #

value :: Int32 -> R String #

EmbPrj ByteString # 
Instance details

EmbPrj IntSet # 
Instance details

Methods

icode :: IntSet -> S Int32 #

icod_ :: IntSet -> S Int32 #

value :: Int32 -> R IntSet #

EmbPrj Impossible # 
Instance details

EmbPrj Empty # 
Instance details

Methods

icode :: Empty -> S Int32 #

icod_ :: Empty -> S Int32 #

value :: Int32 -> R Empty #

EmbPrj AbsolutePath # 
Instance details

EmbPrj Range #

Ranges are always deserialised as noRange.

Instance details

Methods

icode :: Range -> S Int32 #

icod_ :: Range -> S Int32 #

value :: Int32 -> R Range #

EmbPrj Fixity' # 
Instance details

EmbPrj MetaId # 
Instance details

Methods

icode :: MetaId -> S Int32 #

icod_ :: MetaId -> S Int32 #

value :: Int32 -> R MetaId #

EmbPrj NameId # 
Instance details

Methods

icode :: NameId -> S Int32 #

icod_ :: NameId -> S Int32 #

value :: Int32 -> R NameId #

EmbPrj IsAbstract # 
Instance details

EmbPrj DataOrRecord # 
Instance details

EmbPrj ProjOrigin # 
Instance details

EmbPrj ConOrigin # 
Instance details

EmbPrj ArgInfo # 
Instance details

EmbPrj FreeVariables # 
Instance details

EmbPrj Origin # 
Instance details

Methods

icode :: Origin -> S Int32 #

icod_ :: Origin -> S Int32 #

value :: Int32 -> R Origin #

EmbPrj Relevance # 
Instance details

EmbPrj Quantity # 
Instance details

EmbPrj Modality # 
Instance details

EmbPrj Hiding # 
Instance details

Methods

icode :: Hiding -> S Int32 #

icod_ :: Hiding -> S Int32 #

value :: Int32 -> R Hiding #

EmbPrj Induction # 
Instance details

EmbPrj HasEta # 
Instance details

Methods

icode :: HasEta -> S Int32 #

icod_ :: HasEta -> S Int32 #

value :: Int32 -> R HasEta #

EmbPrj Delayed # 
Instance details

EmbPrj TopLevelModuleName # 
Instance details

EmbPrj QName # 
Instance details

Methods

icode :: QName -> S Int32 #

icod_ :: QName -> S Int32 #

value :: Int32 -> R QName #

EmbPrj NamePart # 
Instance details

EmbPrj Name # 
Instance details

Methods

icode :: Name -> S Int32 #

icod_ :: Name -> S Int32 #

value :: Int32 -> R Name #

EmbPrj GenPart # 
Instance details

EmbPrj AmbiguousQName # 
Instance details

EmbPrj ModuleName # 
Instance details

EmbPrj QName # 
Instance details

Methods

icode :: QName -> S Int32 #

icod_ :: QName -> S Int32 #

value :: Int32 -> R QName #

EmbPrj Name # 
Instance details

Methods

icode :: Name -> S Int32 #

icod_ :: Name -> S Int32 #

value :: Int32 -> R Name #

EmbPrj Literal # 
Instance details

EmbPrj Fixity # 
Instance details

Methods

icode :: Fixity -> S Int32 #

icod_ :: Fixity -> S Int32 #

value :: Int32 -> R Fixity #

EmbPrj Associativity # 
Instance details

EmbPrj PrecedenceLevel # 
Instance details

EmbPrj a => EmbPrj [a] # 
Instance details

Methods

icode :: [a] -> S Int32 #

icod_ :: [a] -> S Int32 #

value :: Int32 -> R [a] #

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

Methods

icode :: Maybe a -> S Int32 #

icod_ :: Maybe a -> S Int32 #

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

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

Methods

icode :: Seq a -> S Int32 #

icod_ :: Seq a -> S Int32 #

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

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

Methods

icode :: Set a -> S Int32 #

icod_ :: Set a -> S Int32 #

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

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

Methods

icode :: Maybe a -> S Int32 #

icod_ :: Maybe a -> S Int32 #

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

EmbPrj a => EmbPrj (NonemptyList a) # 
Instance details

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

Methods

icode :: Interval' a -> S Int32 #

icod_ :: Interval' a -> S Int32 #

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

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

Methods

icode :: Position' a -> S Int32 #

icod_ :: Position' a -> S Int32 #

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

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

Methods

icode :: Ranged a -> S Int32 #

icod_ :: Ranged a -> S Int32 #

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

EmbPrj a => EmbPrj (Dom a) # 
Instance details

Methods

icode :: Dom a -> S Int32 #

icod_ :: Dom a -> S Int32 #

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

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

Methods

icode :: Arg a -> S Int32 #

icod_ :: Arg a -> S Int32 #

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

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

Methods

icode :: WithHiding a -> S Int32 #

icod_ :: WithHiding a -> S Int32 #

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

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

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

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

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

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

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

Methods

icode :: BiMap a b -> S Int32 #

icod_ :: BiMap a b -> S Int32 #

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

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

Methods

icode :: Trie a b -> S Int32 #

icod_ :: Trie a b -> S Int32 #

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

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

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

Methods

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

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

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