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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Serialise.Instances.Abstract

Contents

- Orphan instances

# Documentation

data AbsNameWithFixity Source #

Constructors

AbsNameWithFixity Fixity QName KindOfName WhyInScope NameMetadata |

#### Instances

Instances details

EmbPrj AbsNameWithFixity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbsNameWithFixity -> S Int32 Source # icod_ :: AbsNameWithFixity -> S Int32 Source # value :: Int32 -> R AbsNameWithFixity Source #

toAbsName :: AbsNameWithFixity -> AbstractName Source #

fromAbsName :: AbstractName -> AbsNameWithFixity Source #

# Orphan instances

EmbPrj BindName Source # |
Instance details Methods icode :: BindName -> S Int32 Source # icod_ :: BindName -> S Int32 Source # value :: Int32 -> R BindName Source #
EmbPrj Suffix Source # |
Instance details Methods icode :: Suffix -> S Int32 Source # icod_ :: Suffix -> S Int32 Source # value :: Int32 -> R Suffix Source #
EmbPrj Access Source # |
Instance details Methods icode :: Access -> S Int32 Source # icod_ :: Access -> S Int32 Source # value :: Int32 -> R Access Source #
EmbPrj ParenPreference Source # |
Instance details Methods icode :: ParenPreference -> S Int32 Source # icod_ :: ParenPreference -> S Int32 Source # value :: Int32 -> R ParenPreference Source #
EmbPrj Precedence Source # |
Instance details Methods icode :: Precedence -> S Int32 Source # icod_ :: Precedence -> S Int32 Source # value :: Int32 -> R Precedence Source #
EmbPrj ConPatInfo Source # |
Instance details Methods icode :: ConPatInfo -> S Int32 Source # icod_ :: ConPatInfo -> S Int32 Source # value :: Int32 -> R ConPatInfo Source #
EmbPrj ConPatLazy Source # |
Instance details Methods icode :: ConPatLazy -> S Int32 Source # icod_ :: ConPatLazy -> S Int32 Source # value :: Int32 -> R ConPatLazy Source #
EmbPrj AbstractModule Source # |
Instance details Methods icode :: AbstractModule -> S Int32 Source # icod_ :: AbstractModule -> S Int32 Source # value :: Int32 -> R AbstractModule Source #
EmbPrj AbstractName Source # |
Instance details Methods icode :: AbstractName -> S Int32 Source # icod_ :: AbstractName -> S Int32 Source # value :: Int32 -> R AbstractName Source #
EmbPrj BindingSource Source # |
Instance details Methods icode :: BindingSource -> S Int32 Source # icod_ :: BindingSource -> S Int32 Source # value :: Int32 -> R BindingSource Source #
EmbPrj DataOrRecordModule Source # |
Instance details Methods icode :: DataOrRecordModule -> S Int32 Source # icod_ :: DataOrRecordModule -> S Int32 Source # value :: Int32 -> R DataOrRecordModule Source #
EmbPrj KindOfName Source # |
Instance details Methods icode :: KindOfName -> S Int32 Source # icod_ :: KindOfName -> S Int32 Source # value :: Int32 -> R KindOfName Source #
EmbPrj LocalVar Source # |
Instance details Methods icode :: LocalVar -> S Int32 Source # icod_ :: LocalVar -> S Int32 Source # value :: Int32 -> R LocalVar Source #
EmbPrj NameMetadata Source # |
Instance details Methods icode :: NameMetadata -> S Int32 Source # icod_ :: NameMetadata -> S Int32 Source # value :: Int32 -> R NameMetadata Source #
EmbPrj NameOrModule Source # |
Instance details Methods icode :: NameOrModule -> S Int32 Source # icod_ :: NameOrModule -> S Int32 Source # value :: Int32 -> R NameOrModule Source #
EmbPrj NameSpace Source # |
Instance details Methods icode :: NameSpace -> S Int32 Source # icod_ :: NameSpace -> S Int32 Source # value :: Int32 -> R NameSpace Source #
EmbPrj NameSpaceId Source # |
Instance details Methods icode :: NameSpaceId -> S Int32 Source # icod_ :: NameSpaceId -> S Int32 Source # value :: Int32 -> R NameSpaceId Source #
EmbPrj Scope Source # |
Instance details Methods icode :: Scope -> S Int32 Source # icod_ :: Scope -> S Int32 Source # value :: Int32 -> R Scope Source #
EmbPrj ScopeInfo Source # |
Instance details Methods icode :: ScopeInfo -> S Int32 Source # icod_ :: ScopeInfo -> S Int32 Source # value :: Int32 -> R ScopeInfo Source #
EmbPrj WhyInScope Source # |
Instance details Methods icode :: WhyInScope -> S Int32 Source # icod_ :: WhyInScope -> S Int32 Source # value :: Int32 -> R WhyInScope 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 #