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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Serialise.Instances.Common

Contents

- Orphan instances

Synopsis

- newtype SerialisedRange = SerialisedRange {
  - underlyingRange :: Range
  }

# Documentation

newtype SerialisedRange Source #

Ranges that should be serialised properly.

Constructors

SerialisedRange |

Fields

- underlyingRange :: Range

#### Instances

Instances details

EmbPrj SerialisedRange Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: SerialisedRange -> S Int32 Source # icod_ :: SerialisedRange -> S Int32 Source # value :: Int32 -> R SerialisedRange Source #

# Orphan instances

EmbPrj AmbiguousQName Source # |
Instance details Methods icode :: AmbiguousQName -> S Int32 Source # icod_ :: AmbiguousQName -> S Int32 Source # value :: Int32 -> R AmbiguousQName Source #
EmbPrj ModuleName Source # |
Instance details Methods icode :: ModuleName -> S Int32 Source # icod_ :: ModuleName -> S Int32 Source # value :: Int32 -> R ModuleName Source #
EmbPrj Name Source # |
Instance details Methods icode :: Name -> S Int32 Source # icod_ :: Name -> S Int32 Source # value :: Int32 -> R Name Source #
EmbPrj QName Source # |
Instance details Methods icode :: QName -> S Int32 Source # icod_ :: QName -> S Int32 Source # value :: Int32 -> R QName Source #
EmbPrj Annotation Source # |
Instance details Methods icode :: Annotation -> S Int32 Source # icod_ :: Annotation -> S Int32 Source # value :: Int32 -> R Annotation Source #
EmbPrj ArgInfo Source # |
Instance details Methods icode :: ArgInfo -> S Int32 Source # icod_ :: ArgInfo -> S Int32 Source # value :: Int32 -> R ArgInfo Source #
EmbPrj Associativity Source # |
Instance details Methods icode :: Associativity -> S Int32 Source # icod_ :: Associativity -> S Int32 Source # value :: Int32 -> R Associativity Source #
EmbPrj Cohesion Source # |
Instance details Methods icode :: Cohesion -> S Int32 Source # icod_ :: Cohesion -> S Int32 Source # value :: Int32 -> R Cohesion Source #
EmbPrj ConOrigin Source # |
Instance details Methods icode :: ConOrigin -> S Int32 Source # icod_ :: ConOrigin -> S Int32 Source # value :: Int32 -> R ConOrigin Source #
EmbPrj Cubical Source # |
Instance details Methods icode :: Cubical -> S Int32 Source # icod_ :: Cubical -> S Int32 Source # value :: Int32 -> R Cubical Source #
EmbPrj Delayed Source # |
Instance details Methods icode :: Delayed -> S Int32 Source # icod_ :: Delayed -> S Int32 Source # value :: Int32 -> R Delayed Source #
EmbPrj ExpandedEllipsis Source # |
Instance details Methods icode :: ExpandedEllipsis -> S Int32 Source # icod_ :: ExpandedEllipsis -> S Int32 Source # value :: Int32 -> R ExpandedEllipsis Source #
EmbPrj FileType Source # |
Instance details Methods icode :: FileType -> S Int32 Source # icod_ :: FileType -> S Int32 Source # value :: Int32 -> R FileType Source #
EmbPrj Fixity Source # |
Instance details Methods icode :: Fixity -> S Int32 Source # icod_ :: Fixity -> S Int32 Source # value :: Int32 -> R Fixity Source #
EmbPrj Fixity' Source # |
Instance details Methods icode :: Fixity' -> S Int32 Source # icod_ :: Fixity' -> S Int32 Source # value :: Int32 -> R Fixity' Source #
EmbPrj FixityLevel Source # |
Instance details Methods icode :: FixityLevel -> S Int32 Source # icod_ :: FixityLevel -> S Int32 Source # value :: Int32 -> R FixityLevel Source #
EmbPrj FreeVariables Source # |
Instance details Methods icode :: FreeVariables -> S Int32 Source # icod_ :: FreeVariables -> S Int32 Source # value :: Int32 -> R FreeVariables Source #
EmbPrj GenPart Source # |
Instance details Methods icode :: GenPart -> S Int32 Source # icod_ :: GenPart -> S Int32 Source # value :: Int32 -> R GenPart Source #
EmbPrj Hiding Source # |
Instance details Methods icode :: Hiding -> S Int32 Source # icod_ :: Hiding -> S Int32 Source # value :: Int32 -> R Hiding Source #
EmbPrj Induction Source # |
Instance details Methods icode :: Induction -> S Int32 Source # icod_ :: Induction -> S Int32 Source # value :: Int32 -> R Induction Source #
EmbPrj IsAbstract Source # |
Instance details Methods icode :: IsAbstract -> S Int32 Source # icod_ :: IsAbstract -> S Int32 Source # value :: Int32 -> R IsAbstract Source #
EmbPrj Language Source # |
Instance details Methods icode :: Language -> S Int32 Source # icod_ :: Language -> S Int32 Source # value :: Int32 -> R Language Source #
EmbPrj Lock Source # |
Instance details Methods icode :: Lock -> S Int32 Source # icod_ :: Lock -> S Int32 Source # value :: Int32 -> R Lock Source #
EmbPrj MetaId Source # |
Instance details Methods icode :: MetaId -> S Int32 Source # icod_ :: MetaId -> S Int32 Source # value :: Int32 -> R MetaId Source #
EmbPrj Modality Source # |
Instance details Methods icode :: Modality -> S Int32 Source # icod_ :: Modality -> S Int32 Source # value :: Int32 -> R Modality Source #
EmbPrj ModuleNameHash Source # |
Instance details Methods icode :: ModuleNameHash -> S Int32 Source # icod_ :: ModuleNameHash -> S Int32 Source # value :: Int32 -> R ModuleNameHash Source #
EmbPrj NameId Source # |
Instance details Methods icode :: NameId -> S Int32 Source # icod_ :: NameId -> S Int32 Source # value :: Int32 -> R NameId Source #
EmbPrj Origin Source # |
Instance details Methods icode :: Origin -> S Int32 Source # icod_ :: Origin -> S Int32 Source # value :: Int32 -> R Origin Source #
EmbPrj PatternOrCopattern Source # |
Instance details Methods icode :: PatternOrCopattern -> S Int32 Source # icod_ :: PatternOrCopattern -> S Int32 Source # value :: Int32 -> R PatternOrCopattern Source #
EmbPrj ProjOrigin Source # |
Instance details Methods icode :: ProjOrigin -> S Int32 Source # icod_ :: ProjOrigin -> S Int32 Source # value :: Int32 -> R ProjOrigin Source #
EmbPrj Q0Origin Source # |
Instance details Methods icode :: Q0Origin -> S Int32 Source # icod_ :: Q0Origin -> S Int32 Source # value :: Int32 -> R Q0Origin Source #
EmbPrj Q1Origin Source # |
Instance details Methods icode :: Q1Origin -> S Int32 Source # icod_ :: Q1Origin -> S Int32 Source # value :: Int32 -> R Q1Origin Source #
EmbPrj Quantity Source # |
Instance details Methods icode :: Quantity -> S Int32 Source # icod_ :: Quantity -> S Int32 Source # value :: Int32 -> R Quantity Source #
EmbPrj QωOrigin Source # |
Instance details Methods icode :: QωOrigin -> S Int32 Source # icod_ :: QωOrigin -> S Int32 Source # value :: Int32 -> R QωOrigin Source #
EmbPrj Relevance Source # |
Instance details Methods icode :: Relevance -> S Int32 Source # icod_ :: Relevance -> S Int32 Source # value :: Int32 -> R Relevance Source #
EmbPrj Name Source # |
Instance details Methods icode :: Name -> S Int32 Source # icod_ :: Name -> S Int32 Source # value :: Int32 -> R Name Source #
EmbPrj NameInScope Source # |
Instance details Methods icode :: NameInScope -> S Int32 Source # icod_ :: NameInScope -> S Int32 Source # value :: Int32 -> R NameInScope Source #
EmbPrj NamePart Source # |
Instance details Methods icode :: NamePart -> S Int32 Source # icod_ :: NamePart -> S Int32 Source # value :: Int32 -> R NamePart Source #
EmbPrj QName Source # |
Instance details Methods icode :: QName -> S Int32 Source # icod_ :: QName -> S Int32 Source # value :: Int32 -> R QName Source #
EmbPrj TopLevelModuleName Source # |
Instance details Methods icode :: TopLevelModuleName -> S Int32 Source # icod_ :: TopLevelModuleName -> S Int32 Source # value :: Int32 -> R TopLevelModuleName Source #
EmbPrj Literal Source # |
Instance details Methods icode :: Literal -> S Int32 Source # icod_ :: Literal -> S Int32 Source # value :: Int32 -> R Literal Source #
EmbPrj Range Source # | Ranges are always deserialised as `noRange`.
Instance details Methods icode :: Range -> S Int32 Source # icod_ :: Range -> S Int32 Source # value :: Int32 -> R Range Source #
EmbPrj AbsolutePath Source # |
Instance details Methods icode :: AbsolutePath -> S Int32 Source # icod_ :: AbsolutePath -> S Int32 Source # value :: Int32 -> R AbsolutePath Source #
EmbPrj Impossible Source # |
Instance details Methods icode :: Impossible -> S Int32 Source # icod_ :: Impossible -> S Int32 Source # value :: Int32 -> R Impossible Source #
EmbPrj Void Source # |
Instance details Methods icode :: Void -> S Int32 Source # icod_ :: Void -> S Int32 Source # value :: Int32 -> R Void Source #
EmbPrj Int32 Source # |
Instance details Methods icode :: Int32 -> S Int32 Source # icod_ :: Int32 -> S Int32 Source # value :: Int32 -> R Int32 Source #
EmbPrj CallStack Source # |
Instance details Methods icode :: CallStack -> S Int32 Source # icod_ :: CallStack -> S Int32 Source # value :: Int32 -> R CallStack Source #
EmbPrj SrcLoc Source # |
Instance details Methods icode :: SrcLoc -> S Int32 Source # icod_ :: SrcLoc -> S Int32 Source # value :: Int32 -> R SrcLoc Source #
EmbPrj Word64 Source # |
Instance details Methods icode :: Word64 -> S Int32 Source # icod_ :: Word64 -> S Int32 Source # value :: Int32 -> R Word64 Source #
EmbPrj IntSet Source # |
Instance details Methods icode :: IntSet -> S Int32 Source # icod_ :: IntSet -> S Int32 Source # value :: Int32 -> R IntSet Source #
EmbPrj Text Source # |
Instance details Methods icode :: Text -> S Int32 Source # icod_ :: Text -> S Int32 Source # value :: Int32 -> R Text Source #
EmbPrj Text Source # |
Instance details Methods icode :: Text -> S Int32 Source # icod_ :: Text -> S Int32 Source # value :: Int32 -> R Text Source #
EmbPrj String Source # |
Instance details Methods icode :: String -> S Int32 Source # icod_ :: String -> S Int32 Source # value :: Int32 -> R String Source #
EmbPrj Integer Source # |
Instance details Methods icode :: Integer -> S Int32 Source # icod_ :: Integer -> S Int32 Source # value :: Int32 -> R Integer Source #
EmbPrj () Source # |
Instance details Methods icode :: () -> S Int32 Source # icod_ :: () -> S Int32 Source # value :: Int32 -> R () Source #
EmbPrj Bool Source # |
Instance details Methods icode :: Bool -> S Int32 Source # icod_ :: Bool -> S Int32 Source # value :: Int32 -> R Bool Source #
EmbPrj Char Source # |
Instance details Methods icode :: Char -> S Int32 Source # icod_ :: Char -> S Int32 Source # value :: Int32 -> R Char Source #
EmbPrj Double Source # |
Instance details Methods icode :: Double -> S Int32 Source # icod_ :: Double -> S Int32 Source # value :: Int32 -> R Double Source #
EmbPrj Int Source # |
Instance details Methods icode :: Int -> S Int32 Source # icod_ :: Int -> S Int32 Source # value :: Int32 -> R Int Source #
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 Methods icode :: HasEta' a -> S Int32 Source # icod_ :: HasEta' a -> S Int32 Source # value :: Int32 -> R (HasEta' a) Source #
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 (WithHiding a) Source # |
Instance details Methods icode :: WithHiding a -> S Int32 Source # icod_ :: WithHiding a -> S Int32 Source # value :: Int32 -> R (WithHiding a) Source #
EmbPrj a => EmbPrj (WithOrigin a) Source # |
Instance details Methods icode :: WithOrigin a -> S Int32 Source # icod_ :: WithOrigin a -> S Int32 Source # value :: Int32 -> R (WithOrigin a) Source #
EmbPrj a => EmbPrj (FieldAssignment' a) Source # |
Instance details Methods icode :: FieldAssignment' a -> S Int32 Source # icod_ :: FieldAssignment' a -> S Int32 Source # value :: Int32 -> R (FieldAssignment' a) Source #
EmbPrj a => EmbPrj (Interval' a) Source # |
Instance details Methods icode :: Interval' a -> S Int32 Source # icod_ :: Interval' a -> S Int32 Source # value :: Int32 -> R (Interval' a) Source #
EmbPrj a => EmbPrj (Position' a) Source # |
Instance details Methods icode :: Position' a -> S Int32 Source # icod_ :: Position' a -> S Int32 Source # value :: Int32 -> R (Position' 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 b => EmbPrj (WithDefault b) Source # |
Instance details Methods icode :: WithDefault b -> S Int32 Source # icod_ :: WithDefault b -> S Int32 Source # value :: Int32 -> R (WithDefault b) Source #
EmbPrj a => EmbPrj (NonEmpty a) Source # |
Instance details Methods icode :: NonEmpty a -> S Int32 Source # icod_ :: NonEmpty a -> S Int32 Source # value :: Int32 -> R (NonEmpty a) Source #
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 Methods icode :: ImportedName' a b -> S Int32 Source # icod_ :: ImportedName' a b -> S Int32 Source # value :: Int32 -> R (ImportedName' a b) Source #
(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, 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 #