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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Serialise.Instances.Internal

Contents

- Orphan instances

# Orphan instances

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