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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Serialise.Instances.Internal

Contents

- Orphan instances

# Documentation

blockedToMaybe :: Blocked_ -> Maybe NotBlocked Source #

blockedFromMaybe :: Maybe NotBlocked -> Blocked_ Source #

# Orphan instances

EmbPrj Blocked_ Source # |
Instance details Methods icode :: Blocked_ -> S Word32 Source # icod_ :: Blocked_ -> S Word32 Source # value :: Word32 -> R Blocked_ Source #
EmbPrj Clause Source # |
Instance details Methods icode :: Clause -> S Word32 Source # icod_ :: Clause -> S Word32 Source # value :: Word32 -> R Clause Source #
EmbPrj ConHead Source # |
Instance details Methods icode :: ConHead -> S Word32 Source # icod_ :: ConHead -> S Word32 Source # value :: Word32 -> R ConHead Source #
EmbPrj ConPatternInfo Source # |
Instance details Methods icode :: ConPatternInfo -> S Word32 Source # icod_ :: ConPatternInfo -> S Word32 Source # value :: Word32 -> R ConPatternInfo Source #
EmbPrj DBPatVar Source # |
Instance details Methods icode :: DBPatVar -> S Word32 Source # icod_ :: DBPatVar -> S Word32 Source # value :: Word32 -> R DBPatVar Source #
EmbPrj DataOrRecord Source # |
Instance details Methods icode :: DataOrRecord -> S Word32 Source # icod_ :: DataOrRecord -> S Word32 Source # value :: Word32 -> R DataOrRecord Source #
EmbPrj Level Source # |
Instance details Methods icode :: Level -> S Word32 Source # icod_ :: Level -> S Word32 Source # value :: Word32 -> R Level Source #
EmbPrj NotBlocked Source # |
Instance details Methods icode :: NotBlocked -> S Word32 Source # icod_ :: NotBlocked -> S Word32 Source # value :: Word32 -> R NotBlocked Source #
EmbPrj PatOrigin Source # |
Instance details Methods icode :: PatOrigin -> S Word32 Source # icod_ :: PatOrigin -> S Word32 Source # value :: Word32 -> R PatOrigin Source #
EmbPrj PatternInfo Source # |
Instance details Methods icode :: PatternInfo -> S Word32 Source # icod_ :: PatternInfo -> S Word32 Source # value :: Word32 -> R PatternInfo Source #
EmbPrj PlusLevel Source # |
Instance details Methods icode :: PlusLevel -> S Word32 Source # icod_ :: PlusLevel -> S Word32 Source # value :: Word32 -> R PlusLevel Source #
EmbPrj Sort Source # |
Instance details Methods icode :: Sort -> S Word32 Source # icod_ :: Sort -> S Word32 Source # value :: Word32 -> R Sort Source #
EmbPrj Term Source # |
Instance details Methods icode :: Term -> S Word32 Source # icod_ :: Term -> S Word32 Source # value :: Word32 -> R Term Source #
EmbPrj IsFibrant Source # |
Instance details Methods icode :: IsFibrant -> S Word32 Source # icod_ :: IsFibrant -> S Word32 Source # value :: Word32 -> R IsFibrant Source #
EmbPrj Univ Source # |
Instance details Methods icode :: Univ -> S Word32 Source # icod_ :: Univ -> S Word32 Source # value :: Word32 -> R Univ Source #
EmbPrj CompiledClauses Source # |
Instance details Methods icode :: CompiledClauses -> S Word32 Source # icod_ :: CompiledClauses -> S Word32 Source # value :: Word32 -> R CompiledClauses Source #
EmbPrj LazySplit Source # |
Instance details Methods icode :: LazySplit -> S Word32 Source # icod_ :: LazySplit -> S Word32 Source # value :: Word32 -> R LazySplit Source #
EmbPrj SplitTag Source # |
Instance details Methods icode :: SplitTag -> S Word32 Source # icod_ :: SplitTag -> S Word32 Source # value :: Word32 -> R SplitTag Source #
EmbPrj Key Source # |
Instance details Methods icode :: Key -> S Word32 Source # icod_ :: Key -> S Word32 Source # value :: Word32 -> R Key Source #
EmbPrj BuiltinSort Source # |
Instance details Methods icode :: BuiltinSort -> S Word32 Source # icod_ :: BuiltinSort -> S Word32 Source # value :: Word32 -> R BuiltinSort Source #
EmbPrj CheckpointId Source # |
Instance details Methods icode :: CheckpointId -> S Word32 Source # icod_ :: CheckpointId -> S Word32 Source # value :: Word32 -> R CheckpointId Source #
EmbPrj CompKit Source # |
Instance details Methods icode :: CompKit -> S Word32 Source # icod_ :: CompKit -> S Word32 Source # value :: Word32 -> R CompKit Source #
EmbPrj Definition Source # |
Instance details Methods icode :: Definition -> S Word32 Source # icod_ :: Definition -> S Word32 Source # value :: Word32 -> R Definition Source #
EmbPrj Defn Source # |
Instance details Methods icode :: Defn -> S Word32 Source # icod_ :: Defn -> S Word32 Source # value :: Word32 -> R Defn Source #
EmbPrj DisplayForm Source # |
Instance details Methods icode :: DisplayForm -> S Word32 Source # icod_ :: DisplayForm -> S Word32 Source # value :: Word32 -> R DisplayForm Source #
EmbPrj DisplayTerm Source # |
Instance details Methods icode :: DisplayTerm -> S Word32 Source # icod_ :: DisplayTerm -> S Word32 Source # value :: Word32 -> R DisplayTerm Source #
EmbPrj DoGeneralize Source # |
Instance details Methods icode :: DoGeneralize -> S Word32 Source # icod_ :: DoGeneralize -> S Word32 Source # value :: Word32 -> R DoGeneralize Source #
EmbPrj EtaEquality Source # |
Instance details Methods icode :: EtaEquality -> S Word32 Source # icod_ :: EtaEquality -> S Word32 Source # value :: Word32 -> R EtaEquality Source #
EmbPrj ExtLamInfo Source # |
Instance details Methods icode :: ExtLamInfo -> S Word32 Source # icod_ :: ExtLamInfo -> S Word32 Source # value :: Word32 -> R ExtLamInfo Source #
EmbPrj FunctionFlag Source # |
Instance details Methods icode :: FunctionFlag -> S Word32 Source # icod_ :: FunctionFlag -> S Word32 Source # value :: Word32 -> R FunctionFlag Source #
EmbPrj InstanceInfo Source # |
Instance details Methods icode :: InstanceInfo -> S Word32 Source # icod_ :: InstanceInfo -> S Word32 Source # value :: Word32 -> R InstanceInfo Source #
EmbPrj InstanceTable Source # |
Instance details Methods icode :: InstanceTable -> S Word32 Source # icod_ :: InstanceTable -> S Word32 Source # value :: Word32 -> R InstanceTable Source #
EmbPrj Instantiation Source # |
Instance details Methods icode :: Instantiation -> S Word32 Source # icod_ :: Instantiation -> S Word32 Source # value :: Word32 -> R Instantiation Source #
EmbPrj IsForced Source # |
Instance details Methods icode :: IsForced -> S Word32 Source # icod_ :: IsForced -> S Word32 Source # value :: Word32 -> R IsForced Source #
EmbPrj MutualId Source # |
Instance details Methods icode :: MutualId -> S Word32 Source # icod_ :: MutualId -> S Word32 Source # value :: Word32 -> R MutualId Source #
EmbPrj NLPSort Source # |
Instance details Methods icode :: NLPSort -> S Word32 Source # icod_ :: NLPSort -> S Word32 Source # value :: Word32 -> R NLPSort Source #
EmbPrj NLPType Source # |
Instance details Methods icode :: NLPType -> S Word32 Source # icod_ :: NLPType -> S Word32 Source # value :: Word32 -> R NLPType Source #
EmbPrj NLPat Source # |
Instance details Methods icode :: NLPat -> S Word32 Source # icod_ :: NLPat -> S Word32 Source # value :: Word32 -> R NLPat Source #
EmbPrj NumGeneralizableArgs Source # |
Instance details Methods icode :: NumGeneralizableArgs -> S Word32 Source # icod_ :: NumGeneralizableArgs -> S Word32 Source # value :: Word32 -> R NumGeneralizableArgs Source #
EmbPrj OpaqueBlock Source # |
Instance details Methods icode :: OpaqueBlock -> S Word32 Source # icod_ :: OpaqueBlock -> S Word32 Source # value :: Word32 -> R OpaqueBlock Source #
EmbPrj ProjLams Source # |
Instance details Methods icode :: ProjLams -> S Word32 Source # icod_ :: ProjLams -> S Word32 Source # value :: Word32 -> R ProjLams Source #
EmbPrj Projection Source # |
Instance details Methods icode :: Projection -> S Word32 Source # icod_ :: Projection -> S Word32 Source # value :: Word32 -> R Projection Source #
EmbPrj ProjectionLikenessMissing Source # |
Instance details Methods icode :: ProjectionLikenessMissing -> S Word32 Source # icod_ :: ProjectionLikenessMissing -> S Word32 Source # value :: Word32 -> R ProjectionLikenessMissing Source #
EmbPrj RemoteMetaVariable Source # |
Instance details Methods icode :: RemoteMetaVariable -> S Word32 Source # icod_ :: RemoteMetaVariable -> S Word32 Source # value :: Word32 -> R RemoteMetaVariable Source #
EmbPrj RewriteRule Source # |
Instance details Methods icode :: RewriteRule -> S Word32 Source # icod_ :: RewriteRule -> S Word32 Source # value :: Word32 -> R RewriteRule Source #
EmbPrj Section Source # |
Instance details Methods icode :: Section -> S Word32 Source # icod_ :: Section -> S Word32 Source # value :: Word32 -> R Section Source #
EmbPrj Signature Source # |
Instance details Methods icode :: Signature -> S Word32 Source # icod_ :: Signature -> S Word32 Source # value :: Word32 -> R Signature Source #
EmbPrj System Source # |
Instance details Methods icode :: System -> S Word32 Source # icod_ :: System -> S Word32 Source # value :: Word32 -> R System Source #
EmbPrj TermHead Source # |
Instance details Methods icode :: TermHead -> S Word32 Source # icod_ :: TermHead -> S Word32 Source # value :: Word32 -> R TermHead Source #
EmbPrj Comparison Source # |
Instance details Methods icode :: Comparison -> S Word32 Source # icod_ :: Comparison -> S Word32 Source # value :: Word32 -> R Comparison Source #
EmbPrj Polarity Source # |
Instance details Methods icode :: Polarity -> S Word32 Source # icod_ :: Polarity -> S Word32 Source # value :: Word32 -> R Polarity Source #
EmbPrj Occurrence Source # |
Instance details Methods icode :: Occurrence -> S Word32 Source # icod_ :: Occurrence -> S Word32 Source # value :: Word32 -> R Occurrence Source #
EmbPrj Permutation Source # |
Instance details Methods icode :: Permutation -> S Word32 Source # icod_ :: Permutation -> S Word32 Source # value :: Word32 -> R Permutation Source #
EmbPrj a => EmbPrj (Abs a) Source # |
Instance details Methods icode :: Abs a -> S Word32 Source # icod_ :: Abs a -> S Word32 Source # value :: Word32 -> R (Abs a) Source #
EmbPrj a => EmbPrj (Dom a) Source # |
Instance details Methods icode :: Dom a -> S Word32 Source # icod_ :: Dom a -> S Word32 Source # value :: Word32 -> R (Dom a) Source #
EmbPrj a => EmbPrj (Pattern' a) Source # |
Instance details Methods icode :: Pattern' a -> S Word32 Source # icod_ :: Pattern' a -> S Word32 Source # value :: Word32 -> R (Pattern' a) Source #
EmbPrj a => EmbPrj (Substitution' a) Source # |
Instance details Methods icode :: Substitution' a -> S Word32 Source # icod_ :: Substitution' a -> S Word32 Source # value :: Word32 -> R (Substitution' a) Source #
EmbPrj a => EmbPrj (Tele a) Source # |
Instance details Methods icode :: Tele a -> S Word32 Source # icod_ :: Tele a -> S Word32 Source # value :: Word32 -> R (Tele a) Source #
EmbPrj a => EmbPrj (Type' a) Source # |
Instance details Methods icode :: Type' a -> S Word32 Source # icod_ :: Type' a -> S Word32 Source # value :: Word32 -> R (Type' a) Source #
EmbPrj a => EmbPrj (Elim' a) Source # |
Instance details Methods icode :: Elim' a -> S Word32 Source # icod_ :: Elim' a -> S Word32 Source # value :: Word32 -> R (Elim' a) Source #
EmbPrj a => EmbPrj (Case a) Source # |
Instance details Methods icode :: Case a -> S Word32 Source # icod_ :: Case a -> S Word32 Source # value :: Word32 -> R (Case a) Source #
EmbPrj a => EmbPrj (WithArity a) Source # |
Instance details Methods icode :: WithArity a -> S Word32 Source # icod_ :: WithArity a -> S Word32 Source # value :: Word32 -> R (WithArity a) Source #
EmbPrj a => EmbPrj (SplitTree' a) Source # |
Instance details Methods icode :: SplitTree' a -> S Word32 Source # icod_ :: SplitTree' a -> S Word32 Source # value :: Word32 -> R (SplitTree' a) Source #
(EmbPrj a, Ord a) => EmbPrj (DiscrimTree a) Source # |
Instance details Methods icode :: DiscrimTree a -> S Word32 Source # icod_ :: DiscrimTree a -> S Word32 Source # value :: Word32 -> R (DiscrimTree a) Source #
EmbPrj a => EmbPrj (Builtin a) Source # |
Instance details Methods icode :: Builtin a -> S Word32 Source # icod_ :: Builtin a -> S Word32 Source # value :: Word32 -> R (Builtin a) Source #
EmbPrj a => EmbPrj (FunctionInverse' a) Source # |
Instance details Methods icode :: FunctionInverse' a -> S Word32 Source # icod_ :: FunctionInverse' a -> S Word32 Source # value :: Word32 -> R (FunctionInverse' a) Source #
EmbPrj a => EmbPrj (Judgement a) Source # |
Instance details Methods icode :: Judgement a -> S Word32 Source # icod_ :: Judgement a -> S Word32 Source # value :: Word32 -> R (Judgement a) Source #
EmbPrj a => EmbPrj (Open a) Source # |
Instance details Methods icode :: Open a -> S Word32 Source # icod_ :: Open a -> S Word32 Source # value :: Word32 -> R (Open a) Source #
EmbPrj a => EmbPrj (Drop a) Source # |
Instance details Methods icode :: Drop a -> S Word32 Source # icod_ :: Drop a -> S Word32 Source # value :: Word32 -> R (Drop a) Source #