Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Serialise.Instances.Abstract

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 #