Agda-2.6.4.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Serialise.Instances.Internal

Documentation

blockedToMaybe :: Blocked_ -> Maybe NotBlocked Source #

blockedFromMaybe :: Maybe NotBlocked -> Blocked_ Source #

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 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 IsFibrant Source # 
Instance details

Methods

icode :: IsFibrant -> S Int32 Source #

icod_ :: IsFibrant -> S Int32 Source #

value :: Int32 -> R IsFibrant Source #

EmbPrj Univ Source # 
Instance details

Methods

icode :: Univ -> S Int32 Source #

icod_ :: Univ -> S Int32 Source #

value :: Int32 -> R Univ 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 BuiltinSort Source # 
Instance details

Methods

icode :: BuiltinSort -> S Int32 Source #

icod_ :: BuiltinSort -> S Int32 Source #

value :: Int32 -> R BuiltinSort 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 Comparison Source # 
Instance details

Methods

icode :: Comparison -> S Int32 Source #

icod_ :: Comparison -> S Int32 Source #

value :: Int32 -> R Comparison 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 Instantiation Source # 
Instance details

Methods

icode :: Instantiation -> S Int32 Source #

icod_ :: Instantiation -> S Int32 Source #

value :: Int32 -> R Instantiation 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 OpaqueBlock Source # 
Instance details

Methods

icode :: OpaqueBlock -> S Int32 Source #

icod_ :: OpaqueBlock -> S Int32 Source #

value :: Int32 -> R OpaqueBlock 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 ProjectionLikenessMissing Source # 
Instance details

Methods

icode :: ProjectionLikenessMissing -> S Int32 Source #

icod_ :: ProjectionLikenessMissing -> S Int32 Source #

value :: Int32 -> R ProjectionLikenessMissing Source #

EmbPrj RemoteMetaVariable Source # 
Instance details

Methods

icode :: RemoteMetaVariable -> S Int32 Source #

icod_ :: RemoteMetaVariable -> S Int32 Source #

value :: Int32 -> R RemoteMetaVariable 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 (Judgement a) Source # 
Instance details

Methods

icode :: Judgement a -> S Int32 Source #

icod_ :: Judgement a -> S Int32 Source #

value :: Int32 -> R (Judgement 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 #