Agda-2.5.3: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.Serialise.Instances.Internal
Contents
Methods
icode :: Permutation -> S Int32 Source #
icod_ :: Permutation -> S Int32 Source #
value :: Int32 -> R Permutation Source #
icode :: Occurrence -> S Int32 Source #
icod_ :: Occurrence -> S Int32 Source #
value :: Int32 -> R Occurrence Source #
icode :: ConPatternInfo -> S Int32 Source #
icod_ :: ConPatternInfo -> S Int32 Source #
value :: Int32 -> R ConPatternInfo Source #
icode :: DBPatVar -> S Int32 Source #
icod_ :: DBPatVar -> S Int32 Source #
value :: Int32 -> R DBPatVar Source #
icode :: Clause -> S Int32 Source #
icod_ :: Clause -> S Int32 Source #
value :: Int32 -> R Clause Source #
icode :: LevelAtom -> S Int32 Source #
icod_ :: LevelAtom -> S Int32 Source #
value :: Int32 -> R LevelAtom Source #
icode :: PlusLevel -> S Int32 Source #
icod_ :: PlusLevel -> S Int32 Source #
value :: Int32 -> R PlusLevel Source #
icode :: Level -> S Int32 Source #
icod_ :: Level -> S Int32 Source #
value :: Int32 -> R Level Source #
icode :: Sort -> S Int32 Source #
icod_ :: Sort -> S Int32 Source #
value :: Int32 -> R Sort Source #
icode :: Term -> S Int32 Source #
icod_ :: Term -> S Int32 Source #
value :: Int32 -> R Term Source #
icode :: ConHead -> S Int32 Source #
icod_ :: ConHead -> S Int32 Source #
value :: Int32 -> R ConHead Source #
icode :: CompiledClauses -> S Int32 Source #
icod_ :: CompiledClauses -> S Int32 Source #
value :: Int32 -> R CompiledClauses Source #
icode :: CtxId -> S Int32 Source #
icod_ :: CtxId -> S Int32 Source #
value :: Int32 -> R CtxId Source #
icode :: MutualId -> S Int32 Source #
icod_ :: MutualId -> S Int32 Source #
value :: Int32 -> R MutualId Source #
icode :: TermHead -> S Int32 Source #
icod_ :: TermHead -> S Int32 Source #
value :: Int32 -> R TermHead Source #
icode :: Defn -> S Int32 Source #
icod_ :: Defn -> S Int32 Source #
value :: Int32 -> R Defn Source #
icode :: FunctionFlag -> S Int32 Source #
icod_ :: FunctionFlag -> S Int32 Source #
value :: Int32 -> R FunctionFlag Source #
icode :: EtaEquality -> S Int32 Source #
icod_ :: EtaEquality -> S Int32 Source #
value :: Int32 -> R EtaEquality Source #
icode :: ProjLams -> S Int32 Source #
icod_ :: ProjLams -> S Int32 Source #
value :: Int32 -> R ProjLams Source #
icode :: Projection -> S Int32 Source #
icod_ :: Projection -> S Int32 Source #
value :: Int32 -> R Projection Source #
icode :: ExtLamInfo -> S Int32 Source #
icod_ :: ExtLamInfo -> S Int32 Source #
value :: Int32 -> R ExtLamInfo Source #
icode :: Polarity -> S Int32 Source #
icod_ :: Polarity -> S Int32 Source #
value :: Int32 -> R Polarity Source #
icode :: Definition -> S Int32 Source #
icod_ :: Definition -> S Int32 Source #
value :: Int32 -> R Definition Source #
icode :: RewriteRule -> S Int32 Source #
icod_ :: RewriteRule -> S Int32 Source #
value :: Int32 -> R RewriteRule Source #
icode :: NLPType -> S Int32 Source #
icod_ :: NLPType -> S Int32 Source #
value :: Int32 -> R NLPType Source #
icode :: NLPat -> S Int32 Source #
icod_ :: NLPat -> S Int32 Source #
value :: Int32 -> R NLPat Source #
icode :: DisplayTerm -> S Int32 Source #
icod_ :: DisplayTerm -> S Int32 Source #
value :: Int32 -> R DisplayTerm Source #
icode :: DisplayForm -> S Int32 Source #
icod_ :: DisplayForm -> S Int32 Source #
value :: Int32 -> R DisplayForm Source #
icode :: Section -> S Int32 Source #
icod_ :: Section -> S Int32 Source #
value :: Int32 -> R Section Source #
icode :: Signature -> S Int32 Source #
icod_ :: Signature -> S Int32 Source #
value :: Int32 -> R Signature Source #
icode :: Drop a -> S Int32 Source #
icod_ :: Drop a -> S Int32 Source #
value :: Int32 -> R (Drop a) Source #
icode :: Substitution' a -> S Int32 Source #
icod_ :: Substitution' a -> S Int32 Source #
value :: Int32 -> R (Substitution' a) Source #
icode :: Pattern' a -> S Int32 Source #
icod_ :: Pattern' a -> S Int32 Source #
value :: Int32 -> R (Pattern' a) Source #
icode :: Tele a -> S Int32 Source #
icod_ :: Tele a -> S Int32 Source #
value :: Int32 -> R (Tele a) Source #
icode :: Type' a -> S Int32 Source #
icod_ :: Type' a -> S Int32 Source #
value :: Int32 -> R (Type' a) Source #
icode :: Abs a -> S Int32 Source #
icod_ :: Abs a -> S Int32 Source #
value :: Int32 -> R (Abs a) Source #
icode :: Elim' a -> S Int32 Source #
icod_ :: Elim' a -> S Int32 Source #
value :: Int32 -> R (Elim' a) Source #
icode :: Case a -> S Int32 Source #
icod_ :: Case a -> S Int32 Source #
value :: Int32 -> R (Case a) Source #
icode :: WithArity a -> S Int32 Source #
icod_ :: WithArity a -> S Int32 Source #
value :: Int32 -> R (WithArity a) Source #
icode :: Builtin a -> S Int32 Source #
icod_ :: Builtin a -> S Int32 Source #
value :: Int32 -> R (Builtin a) Source #
icode :: FunctionInverse' a -> S Int32 Source #
icod_ :: FunctionInverse' a -> S Int32 Source #
value :: Int32 -> R (FunctionInverse' a) Source #
icode :: Local a -> S Int32 Source #
icod_ :: Local a -> S Int32 Source #
value :: Int32 -> R (Local a) Source #
icode :: Open a -> S Int32 Source #
icod_ :: Open a -> S Int32 Source #
value :: Int32 -> R (Open a) Source #