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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Serialise.Instances.Internal

Contents

Orphan instances

EmbPrj Permutation # 
Instance details

Methods

icode :: Permutation -> S Int32 #

icod_ :: Permutation -> S Int32 #

value :: Int32 -> R Permutation #

EmbPrj Occurrence # 
Instance details

Methods

icode :: Occurrence -> S Int32 #

icod_ :: Occurrence -> S Int32 #

value :: Int32 -> R Occurrence #

EmbPrj ConPatternInfo # 
Instance details

Methods

icode :: ConPatternInfo -> S Int32 #

icod_ :: ConPatternInfo -> S Int32 #

value :: Int32 -> R ConPatternInfo #

EmbPrj DBPatVar # 
Instance details

Methods

icode :: DBPatVar -> S Int32 #

icod_ :: DBPatVar -> S Int32 #

value :: Int32 -> R DBPatVar #

EmbPrj PatOrigin # 
Instance details

Methods

icode :: PatOrigin -> S Int32 #

icod_ :: PatOrigin -> S Int32 #

value :: Int32 -> R PatOrigin #

EmbPrj Clause # 
Instance details

Methods

icode :: Clause -> S Int32 #

icod_ :: Clause -> S Int32 #

value :: Int32 -> R Clause #

EmbPrj LevelAtom # 
Instance details

Methods

icode :: LevelAtom -> S Int32 #

icod_ :: LevelAtom -> S Int32 #

value :: Int32 -> R LevelAtom #

EmbPrj PlusLevel # 
Instance details

Methods

icode :: PlusLevel -> S Int32 #

icod_ :: PlusLevel -> S Int32 #

value :: Int32 -> R PlusLevel #

EmbPrj Level # 
Instance details

Methods

icode :: Level -> S Int32 #

icod_ :: Level -> S Int32 #

value :: Int32 -> R Level #

EmbPrj Sort # 
Instance details

Methods

icode :: Sort -> S Int32 #

icod_ :: Sort -> S Int32 #

value :: Int32 -> R Sort #

EmbPrj Term # 
Instance details

Methods

icode :: Term -> S Int32 #

icod_ :: Term -> S Int32 #

value :: Int32 -> R Term #

EmbPrj ConHead # 
Instance details

Methods

icode :: ConHead -> S Int32 #

icod_ :: ConHead -> S Int32 #

value :: Int32 -> R ConHead #

EmbPrj CompiledClauses # 
Instance details

Methods

icode :: CompiledClauses -> S Int32 #

icod_ :: CompiledClauses -> S Int32 #

value :: Int32 -> R CompiledClauses #

EmbPrj MutualId # 
Instance details

Methods

icode :: MutualId -> S Int32 #

icod_ :: MutualId -> S Int32 #

value :: Int32 -> R MutualId #

EmbPrj TermHead # 
Instance details

Methods

icode :: TermHead -> S Int32 #

icod_ :: TermHead -> S Int32 #

value :: Int32 -> R TermHead #

EmbPrj Defn # 
Instance details

Methods

icode :: Defn -> S Int32 #

icod_ :: Defn -> S Int32 #

value :: Int32 -> R Defn #

EmbPrj FunctionFlag # 
Instance details

Methods

icode :: FunctionFlag -> S Int32 #

icod_ :: FunctionFlag -> S Int32 #

value :: Int32 -> R FunctionFlag #

EmbPrj EtaEquality # 
Instance details

Methods

icode :: EtaEquality -> S Int32 #

icod_ :: EtaEquality -> S Int32 #

value :: Int32 -> R EtaEquality #

EmbPrj ProjLams # 
Instance details

Methods

icode :: ProjLams -> S Int32 #

icod_ :: ProjLams -> S Int32 #

value :: Int32 -> R ProjLams #

EmbPrj Projection # 
Instance details

Methods

icode :: Projection -> S Int32 #

icod_ :: Projection -> S Int32 #

value :: Int32 -> R Projection #

EmbPrj ExtLamInfo # 
Instance details

Methods

icode :: ExtLamInfo -> S Int32 #

icod_ :: ExtLamInfo -> S Int32 #

value :: Int32 -> R ExtLamInfo #

EmbPrj IsForced # 
Instance details

Methods

icode :: IsForced -> S Int32 #

icod_ :: IsForced -> S Int32 #

value :: Int32 -> R IsForced #

EmbPrj Polarity # 
Instance details

Methods

icode :: Polarity -> S Int32 #

icod_ :: Polarity -> S Int32 #

value :: Int32 -> R Polarity #

EmbPrj Definition # 
Instance details

Methods

icode :: Definition -> S Int32 #

icod_ :: Definition -> S Int32 #

value :: Int32 -> R Definition #

EmbPrj RewriteRule # 
Instance details

Methods

icode :: RewriteRule -> S Int32 #

icod_ :: RewriteRule -> S Int32 #

value :: Int32 -> R RewriteRule #

EmbPrj NLPType # 
Instance details

Methods

icode :: NLPType -> S Int32 #

icod_ :: NLPType -> S Int32 #

value :: Int32 -> R NLPType #

EmbPrj NLPat # 
Instance details

Methods

icode :: NLPat -> S Int32 #

icod_ :: NLPat -> S Int32 #

value :: Int32 -> R NLPat #

EmbPrj DisplayTerm # 
Instance details

Methods

icode :: DisplayTerm -> S Int32 #

icod_ :: DisplayTerm -> S Int32 #

value :: Int32 -> R DisplayTerm #

EmbPrj DisplayForm # 
Instance details

Methods

icode :: DisplayForm -> S Int32 #

icod_ :: DisplayForm -> S Int32 #

value :: Int32 -> R DisplayForm #

EmbPrj Section # 
Instance details

Methods

icode :: Section -> S Int32 #

icod_ :: Section -> S Int32 #

value :: Int32 -> R Section #

EmbPrj Signature # 
Instance details

Methods

icode :: Signature -> S Int32 #

icod_ :: Signature -> S Int32 #

value :: Int32 -> R Signature #

EmbPrj CheckpointId # 
Instance details

Methods

icode :: CheckpointId -> S Int32 #

icod_ :: CheckpointId -> S Int32 #

value :: Int32 -> R CheckpointId #

EmbPrj a => EmbPrj (Drop a) # 
Instance details

Methods

icode :: Drop a -> S Int32 #

icod_ :: Drop a -> S Int32 #

value :: Int32 -> R (Drop a) #

EmbPrj a => EmbPrj (Substitution' a) # 
Instance details

Methods

icode :: Substitution' a -> S Int32 #

icod_ :: Substitution' a -> S Int32 #

value :: Int32 -> R (Substitution' a) #

EmbPrj a => EmbPrj (Pattern' a) # 
Instance details

Methods

icode :: Pattern' a -> S Int32 #

icod_ :: Pattern' a -> S Int32 #

value :: Int32 -> R (Pattern' a) #

EmbPrj a => EmbPrj (Tele a) # 
Instance details

Methods

icode :: Tele a -> S Int32 #

icod_ :: Tele a -> S Int32 #

value :: Int32 -> R (Tele a) #

EmbPrj a => EmbPrj (Type' a) # 
Instance details

Methods

icode :: Type' a -> S Int32 #

icod_ :: Type' a -> S Int32 #

value :: Int32 -> R (Type' a) #

EmbPrj a => EmbPrj (Abs a) # 
Instance details

Methods

icode :: Abs a -> S Int32 #

icod_ :: Abs a -> S Int32 #

value :: Int32 -> R (Abs a) #

EmbPrj a => EmbPrj (Elim' a) # 
Instance details

Methods

icode :: Elim' a -> S Int32 #

icod_ :: Elim' a -> S Int32 #

value :: Int32 -> R (Elim' a) #

EmbPrj a => EmbPrj (Case a) # 
Instance details

Methods

icode :: Case a -> S Int32 #

icod_ :: Case a -> S Int32 #

value :: Int32 -> R (Case a) #

EmbPrj a => EmbPrj (WithArity a) # 
Instance details

Methods

icode :: WithArity a -> S Int32 #

icod_ :: WithArity a -> S Int32 #

value :: Int32 -> R (WithArity a) #

EmbPrj a => EmbPrj (Builtin a) # 
Instance details

Methods

icode :: Builtin a -> S Int32 #

icod_ :: Builtin a -> S Int32 #

value :: Int32 -> R (Builtin a) #

EmbPrj a => EmbPrj (FunctionInverse' a) # 
Instance details

Methods

icode :: FunctionInverse' a -> S Int32 #

icod_ :: FunctionInverse' a -> S Int32 #

value :: Int32 -> R (FunctionInverse' a) #

EmbPrj a => EmbPrj (Open a) # 
Instance details

Methods

icode :: Open a -> S Int32 #

icod_ :: Open a -> S Int32 #

value :: Int32 -> R (Open a) #