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

Safe Haskell | None
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 Word32 Source # icod_ :: SerialisedRange -> S Word32 Source # value :: Word32 -> R SerialisedRange Source #

# Orphan instances

EmbPrj OptionsPragma Source # |
Instance details Methods icode :: OptionsPragma -> S Word32 Source # icod_ :: OptionsPragma -> S Word32 Source # value :: Word32 -> R OptionsPragma Source #
EmbPrj AmbiguousQName Source # |
Instance details Methods icode :: AmbiguousQName -> S Word32 Source # icod_ :: AmbiguousQName -> S Word32 Source # value :: Word32 -> R AmbiguousQName Source #
EmbPrj ModuleName Source # |
Instance details Methods icode :: ModuleName -> S Word32 Source # icod_ :: ModuleName -> S Word32 Source # value :: Word32 -> R ModuleName Source #
EmbPrj Name Source # |
Instance details Methods icode :: Name -> S Word32 Source # icod_ :: Name -> S Word32 Source # value :: Word32 -> R Name Source #
EmbPrj QName Source # |
Instance details Methods icode :: QName -> S Word32 Source # icod_ :: QName -> S Word32 Source # value :: Word32 -> R QName Source #
EmbPrj BuiltinId Source # |
Instance details Methods icode :: BuiltinId -> S Word32 Source # icod_ :: BuiltinId -> S Word32 Source # value :: Word32 -> R BuiltinId Source #
EmbPrj PrimitiveId Source # |
Instance details Methods icode :: PrimitiveId -> S Word32 Source # icod_ :: PrimitiveId -> S Word32 Source # value :: Word32 -> R PrimitiveId Source #
EmbPrj SomeBuiltin Source # |
Instance details Methods icode :: SomeBuiltin -> S Word32 Source # icod_ :: SomeBuiltin -> S Word32 Source # value :: Word32 -> R SomeBuiltin Source #
EmbPrj Annotation Source # |
Instance details Methods icode :: Annotation -> S Word32 Source # icod_ :: Annotation -> S Word32 Source # value :: Word32 -> R Annotation Source #
EmbPrj ArgInfo Source # |
Instance details Methods icode :: ArgInfo -> S Word32 Source # icod_ :: ArgInfo -> S Word32 Source # value :: Word32 -> R ArgInfo Source #
EmbPrj Associativity Source # |
Instance details Methods icode :: Associativity -> S Word32 Source # icod_ :: Associativity -> S Word32 Source # value :: Word32 -> R Associativity Source #
EmbPrj BoundVariablePosition Source # |
Instance details Methods icode :: BoundVariablePosition -> S Word32 Source # icod_ :: BoundVariablePosition -> S Word32 Source # value :: Word32 -> R BoundVariablePosition Source #
EmbPrj Catchall Source # |
Instance details Methods icode :: Catchall -> S Word32 Source # icod_ :: Catchall -> S Word32 Source # value :: Word32 -> R Catchall Source #
EmbPrj Cohesion Source # |
Instance details Methods icode :: Cohesion -> S Word32 Source # icod_ :: Cohesion -> S Word32 Source # value :: Word32 -> R Cohesion Source #
EmbPrj ConOrigin Source # |
Instance details Methods icode :: ConOrigin -> S Word32 Source # icod_ :: ConOrigin -> S Word32 Source # value :: Word32 -> R ConOrigin Source #
EmbPrj ConstructorOrPatternSynonym Source # |
Instance details Methods icode :: ConstructorOrPatternSynonym -> S Word32 Source # icod_ :: ConstructorOrPatternSynonym -> S Word32 Source # value :: Word32 -> R ConstructorOrPatternSynonym Source #
EmbPrj Cubical Source # |
Instance details Methods icode :: Cubical -> S Word32 Source # icod_ :: Cubical -> S Word32 Source # value :: Word32 -> R Cubical Source #
EmbPrj ExpandedEllipsis Source # |
Instance details Methods icode :: ExpandedEllipsis -> S Word32 Source # icod_ :: ExpandedEllipsis -> S Word32 Source # value :: Word32 -> R ExpandedEllipsis Source #
EmbPrj FileType Source # |
Instance details Methods icode :: FileType -> S Word32 Source # icod_ :: FileType -> S Word32 Source # value :: Word32 -> R FileType Source #
EmbPrj Fixity Source # |
Instance details Methods icode :: Fixity -> S Word32 Source # icod_ :: Fixity -> S Word32 Source # value :: Word32 -> R Fixity Source #
EmbPrj Fixity' Source # |
Instance details Methods icode :: Fixity' -> S Word32 Source # icod_ :: Fixity' -> S Word32 Source # value :: Word32 -> R Fixity' Source #
EmbPrj FixityLevel Source # |
Instance details Methods icode :: FixityLevel -> S Word32 Source # icod_ :: FixityLevel -> S Word32 Source # value :: Word32 -> R FixityLevel Source #
EmbPrj FreeVariables Source # |
Instance details Methods icode :: FreeVariables -> S Word32 Source # icod_ :: FreeVariables -> S Word32 Source # value :: Word32 -> R FreeVariables Source #
EmbPrj Hiding Source # |
Instance details Methods icode :: Hiding -> S Word32 Source # icod_ :: Hiding -> S Word32 Source # value :: Word32 -> R Hiding Source #
EmbPrj IsAbstract Source # |
Instance details Methods icode :: IsAbstract -> S Word32 Source # icod_ :: IsAbstract -> S Word32 Source # value :: Word32 -> R IsAbstract Source #
EmbPrj IsInstance Source # |
Instance details Methods icode :: IsInstance -> S Word32 Source # icod_ :: IsInstance -> S Word32 Source # value :: Word32 -> R IsInstance Source #
EmbPrj IsOpaque Source # |
Instance details Methods icode :: IsOpaque -> S Word32 Source # icod_ :: IsOpaque -> S Word32 Source # value :: Word32 -> R IsOpaque Source #
EmbPrj Language Source # |
Instance details Methods icode :: Language -> S Word32 Source # icod_ :: Language -> S Word32 Source # value :: Word32 -> R Language Source #
EmbPrj Lock Source # |
Instance details Methods icode :: Lock -> S Word32 Source # icod_ :: Lock -> S Word32 Source # value :: Word32 -> R Lock Source #
EmbPrj MetaId Source # |
Instance details Methods icode :: MetaId -> S Word32 Source # icod_ :: MetaId -> S Word32 Source # value :: Word32 -> R MetaId Source #
EmbPrj ModalPolarity Source # |
Instance details Methods icode :: ModalPolarity -> S Word32 Source # icod_ :: ModalPolarity -> S Word32 Source # value :: Word32 -> R ModalPolarity Source #
EmbPrj Modality Source # |
Instance details Methods icode :: Modality -> S Word32 Source # icod_ :: Modality -> S Word32 Source # value :: Word32 -> R Modality Source #
EmbPrj NameId Source # |
Instance details Methods icode :: NameId -> S Word32 Source # icod_ :: NameId -> S Word32 Source # value :: Word32 -> R NameId Source #
EmbPrj NotationPart Source # |
Instance details Methods icode :: NotationPart -> S Word32 Source # icod_ :: NotationPart -> S Word32 Source # value :: Word32 -> R NotationPart Source #
EmbPrj OpaqueId Source # |
Instance details Methods icode :: OpaqueId -> S Word32 Source # icod_ :: OpaqueId -> S Word32 Source # value :: Word32 -> R OpaqueId Source #
EmbPrj Origin Source # |
Instance details Methods icode :: Origin -> S Word32 Source # icod_ :: Origin -> S Word32 Source # value :: Word32 -> R Origin Source #
EmbPrj OriginIrrelevant Source # |
Instance details Methods icode :: OriginIrrelevant -> S Word32 Source # icod_ :: OriginIrrelevant -> S Word32 Source # value :: Word32 -> R OriginIrrelevant Source #
EmbPrj OriginRelevant Source # |
Instance details Methods icode :: OriginRelevant -> S Word32 Source # icod_ :: OriginRelevant -> S Word32 Source # value :: Word32 -> R OriginRelevant Source #
EmbPrj OriginShapeIrrelevant Source # |
Instance details Methods icode :: OriginShapeIrrelevant -> S Word32 Source # icod_ :: OriginShapeIrrelevant -> S Word32 Source # value :: Word32 -> R OriginShapeIrrelevant Source #
EmbPrj OverlapMode Source # |
Instance details Methods icode :: OverlapMode -> S Word32 Source # icod_ :: OverlapMode -> S Word32 Source # value :: Word32 -> R OverlapMode Source #
EmbPrj PatternOrCopattern Source # |
Instance details Methods icode :: PatternOrCopattern -> S Word32 Source # icod_ :: PatternOrCopattern -> S Word32 Source # value :: Word32 -> R PatternOrCopattern Source #
EmbPrj PolarityModality Source # |
Instance details Methods icode :: PolarityModality -> S Word32 Source # icod_ :: PolarityModality -> S Word32 Source # value :: Word32 -> R PolarityModality Source #
EmbPrj ProblemId Source # |
Instance details Methods icode :: ProblemId -> S Word32 Source # icod_ :: ProblemId -> S Word32 Source # value :: Word32 -> R ProblemId Source #
EmbPrj ProjOrigin Source # |
Instance details Methods icode :: ProjOrigin -> S Word32 Source # icod_ :: ProjOrigin -> S Word32 Source # value :: Word32 -> R ProjOrigin Source #
EmbPrj Q0Origin Source # |
Instance details Methods icode :: Q0Origin -> S Word32 Source # icod_ :: Q0Origin -> S Word32 Source # value :: Word32 -> R Q0Origin Source #
EmbPrj Q1Origin Source # |
Instance details Methods icode :: Q1Origin -> S Word32 Source # icod_ :: Q1Origin -> S Word32 Source # value :: Word32 -> R Q1Origin Source #
EmbPrj Quantity Source # |
Instance details Methods icode :: Quantity -> S Word32 Source # icod_ :: Quantity -> S Word32 Source # value :: Word32 -> R Quantity Source #
EmbPrj QωOrigin Source # |
Instance details Methods icode :: QωOrigin -> S Word32 Source # icod_ :: QωOrigin -> S Word32 Source # value :: Word32 -> R QωOrigin Source #
EmbPrj Relevance Source # |
Instance details Methods icode :: Relevance -> S Word32 Source # icod_ :: Relevance -> S Word32 Source # value :: Word32 -> R Relevance Source #
EmbPrj Induction Source # |
Instance details Methods icode :: Induction -> S Word32 Source # icod_ :: Induction -> S Word32 Source # value :: Word32 -> R Induction Source #
EmbPrj KwRange Source # |
Instance details Methods icode :: KwRange -> S Word32 Source # icod_ :: KwRange -> S Word32 Source # value :: Word32 -> R KwRange Source #
EmbPrj RecordDirective Source # |
Instance details Methods icode :: RecordDirective -> S Word32 Source # icod_ :: RecordDirective -> S Word32 Source # value :: Word32 -> R RecordDirective Source #
EmbPrj Name Source # |
Instance details Methods icode :: Name -> S Word32 Source # icod_ :: Name -> S Word32 Source # value :: Word32 -> R Name Source #
EmbPrj NameInScope Source # |
Instance details Methods icode :: NameInScope -> S Word32 Source # icod_ :: NameInScope -> S Word32 Source # value :: Word32 -> R NameInScope Source #
EmbPrj NamePart Source # |
Instance details Methods icode :: NamePart -> S Word32 Source # icod_ :: NamePart -> S Word32 Source # value :: Word32 -> R NamePart Source #
EmbPrj QName Source # |
Instance details Methods icode :: QName -> S Word32 Source # icod_ :: QName -> S Word32 Source # value :: Word32 -> R QName Source #
EmbPrj Literal Source # |
Instance details Methods icode :: Literal -> S Word32 Source # icod_ :: Literal -> S Word32 Source # value :: Word32 -> R Literal Source #
EmbPrj Range Source # | Ranges are always deserialised as `noRange`.
Instance details Methods icode :: Range -> S Word32 Source # icod_ :: Range -> S Word32 Source # value :: Word32 -> R Range Source #
EmbPrj RangeFile Source # |
Instance details Methods icode :: RangeFile -> S Word32 Source # icod_ :: RangeFile -> S Word32 Source # value :: Word32 -> R RangeFile Source #
EmbPrj TopLevelModuleName Source # |
Instance details Methods icode :: TopLevelModuleName -> S Word32 Source # icod_ :: TopLevelModuleName -> S Word32 Source # value :: Word32 -> R TopLevelModuleName Source #
EmbPrj ModuleNameHash Source # |
Instance details Methods icode :: ModuleNameHash -> S Word32 Source # icod_ :: ModuleNameHash -> S Word32 Source # value :: Word32 -> R ModuleNameHash Source #
EmbPrj Impossible Source # |
Instance details Methods icode :: Impossible -> S Word32 Source # icod_ :: Impossible -> S Word32 Source # value :: Word32 -> R Impossible Source #
EmbPrj IntSet Source # |
Instance details Methods icode :: IntSet -> S Word32 Source # icod_ :: IntSet -> S Word32 Source # value :: Word32 -> R IntSet Source #
EmbPrj Void Source # |
Instance details Methods icode :: Void -> S Word32 Source # icod_ :: Void -> S Word32 Source # value :: Word32 -> R Void Source #
EmbPrj Int32 Source # |
Instance details Methods icode :: Int32 -> S Word32 Source # icod_ :: Int32 -> S Word32 Source # value :: Word32 -> R Int32 Source #
EmbPrj CallStack Source # |
Instance details Methods icode :: CallStack -> S Word32 Source # icod_ :: CallStack -> S Word32 Source # value :: Word32 -> R CallStack Source #
EmbPrj SrcLoc Source # |
Instance details Methods icode :: SrcLoc -> S Word32 Source # icod_ :: SrcLoc -> S Word32 Source # value :: Word32 -> R SrcLoc Source #
EmbPrj Word32 Source # |
Instance details Methods icode :: Word32 -> S Word32 Source # icod_ :: Word32 -> S Word32 Source # value :: Word32 -> R Word32 Source #
EmbPrj Word64 Source # |
Instance details Methods icode :: Word64 -> S Word32 Source # icod_ :: Word64 -> S Word32 Source # value :: Word32 -> R Word64 Source #
EmbPrj Text Source # |
Instance details Methods icode :: Text -> S Word32 Source # icod_ :: Text -> S Word32 Source # value :: Word32 -> R Text Source #
EmbPrj Text Source # |
Instance details Methods icode :: Text -> S Word32 Source # icod_ :: Text -> S Word32 Source # value :: Word32 -> R Text Source #
EmbPrj Integer Source # |
Instance details Methods icode :: Integer -> S Word32 Source # icod_ :: Integer -> S Word32 Source # value :: Word32 -> R Integer Source #
EmbPrj String Source # |
Instance details Methods icode :: String -> S Word32 Source # icod_ :: String -> S Word32 Source # value :: Word32 -> R String Source #
EmbPrj () Source # |
Instance details Methods icode :: () -> S Word32 Source # icod_ :: () -> S Word32 Source # value :: Word32 -> R () Source #
EmbPrj Bool Source # |
Instance details Methods icode :: Bool -> S Word32 Source # icod_ :: Bool -> S Word32 Source # value :: Word32 -> R Bool Source #
EmbPrj Char Source # |
Instance details Methods icode :: Char -> S Word32 Source # icod_ :: Char -> S Word32 Source # value :: Word32 -> R Char Source #
EmbPrj Double Source # |
Instance details Methods icode :: Double -> S Word32 Source # icod_ :: Double -> S Word32 Source # value :: Word32 -> R Double Source #
EmbPrj Int Source # |
Instance details Methods icode :: Int -> S Word32 Source # icod_ :: Int -> S Word32 Source # value :: Word32 -> R Int Source #
EmbPrj a => EmbPrj (Arg a) Source # |
Instance details Methods icode :: Arg a -> S Word32 Source # icod_ :: Arg a -> S Word32 Source # value :: Word32 -> R (Arg a) Source #
EmbPrj a => EmbPrj (HasEta' a) Source # |
Instance details Methods icode :: HasEta' a -> S Word32 Source # icod_ :: HasEta' a -> S Word32 Source # value :: Word32 -> R (HasEta' a) Source #
EmbPrj a => EmbPrj (Ranged a) Source # |
Instance details Methods icode :: Ranged a -> S Word32 Source # icod_ :: Ranged a -> S Word32 Source # value :: Word32 -> R (Ranged a) Source #
EmbPrj a => EmbPrj (RecordDirectives' a) Source # |
Instance details Methods icode :: RecordDirectives' a -> S Word32 Source # icod_ :: RecordDirectives' a -> S Word32 Source # value :: Word32 -> R (RecordDirectives' a) Source #
EmbPrj a => EmbPrj (WithHiding a) Source # |
Instance details Methods icode :: WithHiding a -> S Word32 Source # icod_ :: WithHiding a -> S Word32 Source # value :: Word32 -> R (WithHiding a) Source #
EmbPrj a => EmbPrj (WithOrigin a) Source # |
Instance details Methods icode :: WithOrigin a -> S Word32 Source # icod_ :: WithOrigin a -> S Word32 Source # value :: Word32 -> R (WithOrigin a) Source #
EmbPrj a => EmbPrj (FieldAssignment' a) Source # |
Instance details Methods icode :: FieldAssignment' a -> S Word32 Source # icod_ :: FieldAssignment' a -> S Word32 Source # value :: Word32 -> R (FieldAssignment' a) Source #
EmbPrj a => EmbPrj (Interval' a) Source # |
Instance details Methods icode :: Interval' a -> S Word32 Source # icod_ :: Interval' a -> S Word32 Source # value :: Word32 -> R (Interval' a) Source #
EmbPrj a => EmbPrj (Position' a) Source # |
Instance details Methods icode :: Position' a -> S Word32 Source # icod_ :: Position' a -> S Word32 Source # value :: Word32 -> R (Position' a) Source #
EmbPrj a => EmbPrj (List1 a) Source # |
Instance details Methods icode :: List1 a -> S Word32 Source # icod_ :: List1 a -> S Word32 Source # value :: Word32 -> R (List1 a) Source #
EmbPrj a => EmbPrj (List2 a) Source # |
Instance details Methods icode :: List2 a -> S Word32 Source # icod_ :: List2 a -> S Word32 Source # value :: Word32 -> R (List2 a) Source #
(Ord a, EmbPrj a) => EmbPrj (Set1 a) Source # |
Instance details Methods icode :: Set1 a -> S Word32 Source # icod_ :: Set1 a -> S Word32 Source # value :: Word32 -> R (Set1 a) Source #
Typeable a => EmbPrj (SmallSet a) Source # |
Instance details Methods icode :: SmallSet a -> S Word32 Source # icod_ :: SmallSet a -> S Word32 Source # value :: Word32 -> R (SmallSet a) Source #
EmbPrj a => EmbPrj (Seq a) Source # |
Instance details Methods icode :: Seq a -> S Word32 Source # icod_ :: Seq a -> S Word32 Source # value :: Word32 -> R (Seq a) Source #
(Ord a, EmbPrj a) => EmbPrj (Set a) Source # |
Instance details Methods icode :: Set a -> S Word32 Source # icod_ :: Set a -> S Word32 Source # value :: Word32 -> R (Set a) Source #
EmbPrj a => EmbPrj (Maybe a) Source # |
Instance details Methods icode :: Maybe a -> S Word32 Source # icod_ :: Maybe a -> S Word32 Source # value :: Word32 -> R (Maybe a) Source #
EmbPrj a => EmbPrj (Maybe a) Source # |
Instance details Methods icode :: Maybe a -> S Word32 Source # icod_ :: Maybe a -> S Word32 Source # value :: Word32 -> R (Maybe a) Source #
EmbPrj a => EmbPrj [a] Source # |
Instance details Methods icode :: [a] -> S Word32 Source # icod_ :: [a] -> S Word32 Source # value :: Word32 -> R [a] Source #
(EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) Source # |
Instance details Methods icode :: ImportedName' a b -> S Word32 Source # icod_ :: ImportedName' a b -> S Word32 Source # value :: Word32 -> R (ImportedName' a b) Source #
(EmbPrj s, EmbPrj t) => EmbPrj (Named s t) Source # |
Instance details Methods icode :: Named s t -> S Word32 Source # icod_ :: Named s t -> S Word32 Source # value :: Word32 -> 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 Word32 Source # icod_ :: BiMap k v -> S Word32 Source # value :: Word32 -> R (BiMap k v) Source #
(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Trie a b) Source # |
Instance details Methods icode :: Trie a b -> S Word32 Source # icod_ :: Trie a b -> S Word32 Source # value :: Word32 -> R (Trie a b) Source #
(EmbPrj a, Typeable b) => EmbPrj (WithDefault' a b) Source # |
Instance details Methods icode :: WithDefault' a b -> S Word32 Source # icod_ :: WithDefault' a b -> S Word32 Source # value :: Word32 -> R (WithDefault' a b) Source #
(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b) Source # |
Instance details Methods icode :: Map a b -> S Word32 Source # icod_ :: Map a b -> S Word32 Source # value :: Word32 -> R (Map a b) Source #
(EmbPrj a, EmbPrj b) => EmbPrj (Either a b) Source # |
Instance details Methods icode :: Either a b -> S Word32 Source # icod_ :: Either a b -> S Word32 Source # value :: Word32 -> R (Either a b) Source #
(EmbPrj a, EmbPrj b) => EmbPrj (Pair a b) Source # |
Instance details Methods icode :: Pair a b -> S Word32 Source # icod_ :: Pair a b -> S Word32 Source # value :: Word32 -> 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 Word32 Source # icod_ :: HashMap k v -> S Word32 Source # value :: Word32 -> R (HashMap k v) Source #
(EmbPrj a, EmbPrj b) => EmbPrj (a, b) Source # |
Instance details Methods icode :: (a, b) -> S Word32 Source # icod_ :: (a, b) -> S Word32 Source # value :: Word32 -> R (a, b) Source #
(EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj (a, b, c) Source # |
Instance details Methods icode :: (a, b, c) -> S Word32 Source # icod_ :: (a, b, c) -> S Word32 Source # value :: Word32 -> R (a, b, c) Source #