Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Contents

Orphan instances

Documentation

data ConwayCertExecContext era Source #

Constructors

ConwayCertExecContext

The UMap of the DState has a field with type: Map (Credential 'Staking) DRep The VState field vsDReps has type: Map (Credential DRepRole) DRepState The DRepState field drepDelegs has type: Set (Credential Staking) Every (Credential 'DRepRole c) corresponds to a unique (DRep) the ccecDelegatees field helps maintain that correspondance, It is used in vstateSpec and bootstrapDStateSpec. Also see getDelegatees :: DState era -> Map (Credential 'DRepRole) (Set (Credential 'Staking)) in Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs, which defines the exact correspondance. }

Fields

ccecWithdrawals ∷ !(Map RewardAccount Coin)
ccecDeposits ∷ !(Map DepositPurpose Coin)
ccecVotes ∷ !(VotingProcedures era)
ccecDelegatees ∷ !(Set (Credential 'DRepRole))

Instances

Instances details

(IsConwayUniv fn, Era era) ⇒ HasSpec fn (ConwayCertExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Associated Types type TypeSpec fn (ConwayCertExecContext era) Source # type Prerequisites fn (ConwayCertExecContext era) Source # Methods emptySpec ∷ TypeSpec fn (ConwayCertExecContext era) Source # combineSpec ∷ TypeSpec fn (ConwayCertExecContext era) → TypeSpec fn (ConwayCertExecContext era) → Specification fn (ConwayCertExecContext era) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (ConwayCertExecContext era) → GenT m (ConwayCertExecContext era) Source # conformsTo ∷ ConwayCertExecContext era → TypeSpec fn (ConwayCertExecContext era) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (ConwayCertExecContext era) → ConwayCertExecContext era → [ConwayCertExecContext era] Source # toPreds ∷ Term fn (ConwayCertExecContext era) → TypeSpec fn (ConwayCertExecContext era) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (ConwayCertExecContext era) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (ConwayCertExecContext era) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (ConwayCertExecContext era) → BinaryShow Source # monadConformsTo ∷ ConwayCertExecContext era → TypeSpec fn (ConwayCertExecContext era) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (ConwayCertExecContext era) → [ConwayCertExecContext era] → Specification fn (ConwayCertExecContext era) Source # guardTypeSpec ∷ [String] → TypeSpec fn (ConwayCertExecContext era) → Specification fn (ConwayCertExecContext era) Source # prerequisites ∷ Evidence (Prerequisites fn (ConwayCertExecContext era)) Source #
Reflect era ⇒ Arbitrary (ConwayCertExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods arbitrary ∷ Gen (ConwayCertExecContext era) Source # shrink ∷ ConwayCertExecContext era → [ConwayCertExecContext era] Source #
Generic (ConwayCertExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Associated Types type Rep (ConwayCertExecContext era) ∷ Type → Type # Methods from ∷ ConwayCertExecContext era → Rep (ConwayCertExecContext era) x # to ∷ Rep (ConwayCertExecContext era) x → ConwayCertExecContext era #
Show (ConwayCertExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods showsPrec ∷ Int → ConwayCertExecContext era → ShowS # show ∷ ConwayCertExecContext era → String # showList ∷ [ConwayCertExecContext era] → ShowS #
Reflect era ⇒ DecCBOR (ConwayCertExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods decCBOR ∷ Decoder s (ConwayCertExecContext era) Source # dropCBOR ∷ Proxy (ConwayCertExecContext era) → Decoder s () Source # label ∷ Proxy (ConwayCertExecContext era) → Text Source #
Era era ⇒ EncCBOR (ConwayCertExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods encCBOR ∷ ConwayCertExecContext era → Encoding Source # encodedSizeExpr ∷ (∀ t. EncCBOR t ⇒ Proxy t → Size) → Proxy (ConwayCertExecContext era) → Size Source # encodedListSizeExpr ∷ (∀ t. EncCBOR t ⇒ Proxy t → Size) → Proxy [ConwayCertExecContext era] → Size Source #
HasSimpleRep (ConwayCertExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Associated Types type SimpleRep (ConwayCertExecContext era) Source # type TheSop (ConwayCertExecContext era) ∷ [Type] Source # Methods toSimpleRep ∷ ConwayCertExecContext era → SimpleRep (ConwayCertExecContext era) Source # fromSimpleRep ∷ SimpleRep (ConwayCertExecContext era) → ConwayCertExecContext era Source #
Era era ⇒ NFData (ConwayCertExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods rnf ∷ ConwayCertExecContext era → () #
Eq (ConwayCertExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods (==) ∷ ConwayCertExecContext era → ConwayCertExecContext era → Bool # (/=) ∷ ConwayCertExecContext era → ConwayCertExecContext era → Bool #
Era era ⇒ ToExpr (ConwayCertExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods toExpr ∷ ConwayCertExecContext era → Expr Source # listToExpr ∷ [ConwayCertExecContext era] → Expr Source #
Inject (ConwayCertExecContext era) (VotingProcedures era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods inject ∷ ConwayCertExecContext era → VotingProcedures era Source #
Inject (ConwayCertExecContext era) (Map RewardAccount Coin) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods inject ∷ ConwayCertExecContext era → Map RewardAccount Coin Source #
Inject (ConwayCertExecContext era) (Map DepositPurpose Coin) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods inject ∷ ConwayCertExecContext era → Map DepositPurpose Coin Source #
Inject (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) (VotingProcedures ConwayEra) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert Methods inject ∷ (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) → VotingProcedures ConwayEra Source #
Inject (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) (Set (Credential 'DRepRole)) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg Methods inject ∷ (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) → Set (Credential 'DRepRole) Source #
Inject (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) (Map RewardAccount Coin) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert Methods inject ∷ (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) → Map RewardAccount Coin Source #
type Prerequisites fn (ConwayCertExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base type Prerequisites fn (ConwayCertExecContext era) = ()
type TypeSpec fn (ConwayCertExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base type TypeSpec fn (ConwayCertExecContext era) = TypeSpec fn (SimpleRep (ConwayCertExecContext era))
type Rep (ConwayCertExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base type Rep (ConwayCertExecContext era) = D1 ('MetaData "ConwayCertExecContext" "Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base" "cardano-ledger-conformance-9.9.9.9-inplace" 'False) (C1 ('MetaCons "ConwayCertExecContext" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ccecWithdrawals") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map RewardAccount Coin)) :: S1 ('MetaSel ('Just "ccecDeposits") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map DepositPurpose Coin))) :: (S1 ('MetaSel ('Just "ccecVotes") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (VotingProcedures era)) :*: S1 ('MetaSel ('Just "ccecDelegatees") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Set (Credential 'DRepRole))))))
type SimpleRep (ConwayCertExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base type SimpleRep (ConwayCertExecContext era) = SOP (TheSop (ConwayCertExecContext era))
type TheSop (ConwayCertExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base type TheSop (ConwayCertExecContext era) = SOPOf (Rep (ConwayCertExecContext era))

conwayCertExecContextSpec ∷ ∀ fn era. (Reflect era, IsConwayUniv fn) ⇒ WitUniv era → Integer → Specification fn (ConwayCertExecContext era) Source #

data ConwayRatifyExecContext era Source #

Constructors

ConwayRatifyExecContext
Fields crecTreasury ∷ Coin crecGovActionMap ∷ [GovActionState era]

Instances

Instances details

(IsConwayUniv fn, EraPParams era, HasSpec fn (GovActionState era)) ⇒ HasSpec fn (ConwayRatifyExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Associated Types type TypeSpec fn (ConwayRatifyExecContext era) Source # type Prerequisites fn (ConwayRatifyExecContext era) Source # Methods emptySpec ∷ TypeSpec fn (ConwayRatifyExecContext era) Source # combineSpec ∷ TypeSpec fn (ConwayRatifyExecContext era) → TypeSpec fn (ConwayRatifyExecContext era) → Specification fn (ConwayRatifyExecContext era) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (ConwayRatifyExecContext era) → GenT m (ConwayRatifyExecContext era) Source # conformsTo ∷ ConwayRatifyExecContext era → TypeSpec fn (ConwayRatifyExecContext era) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (ConwayRatifyExecContext era) → ConwayRatifyExecContext era → [ConwayRatifyExecContext era] Source # toPreds ∷ Term fn (ConwayRatifyExecContext era) → TypeSpec fn (ConwayRatifyExecContext era) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (ConwayRatifyExecContext era) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (ConwayRatifyExecContext era) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (ConwayRatifyExecContext era) → BinaryShow Source # monadConformsTo ∷ ConwayRatifyExecContext era → TypeSpec fn (ConwayRatifyExecContext era) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (ConwayRatifyExecContext era) → [ConwayRatifyExecContext era] → Specification fn (ConwayRatifyExecContext era) Source # guardTypeSpec ∷ [String] → TypeSpec fn (ConwayRatifyExecContext era) → Specification fn (ConwayRatifyExecContext era) Source # prerequisites ∷ Evidence (Prerequisites fn (ConwayRatifyExecContext era)) Source #
(Era era, Arbitrary (PParamsHKD StrictMaybe era)) ⇒ Arbitrary (ConwayRatifyExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods arbitrary ∷ Gen (ConwayRatifyExecContext era) Source # shrink ∷ ConwayRatifyExecContext era → [ConwayRatifyExecContext era] Source #
Generic (ConwayRatifyExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Associated Types type Rep (ConwayRatifyExecContext era) ∷ Type → Type # Methods from ∷ ConwayRatifyExecContext era → Rep (ConwayRatifyExecContext era) x # to ∷ Rep (ConwayRatifyExecContext era) x → ConwayRatifyExecContext era #
EraPParams era ⇒ Show (ConwayRatifyExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods showsPrec ∷ Int → ConwayRatifyExecContext era → ShowS # show ∷ ConwayRatifyExecContext era → String # showList ∷ [ConwayRatifyExecContext era] → ShowS #
EraPParams era ⇒ DecCBOR (ConwayRatifyExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods decCBOR ∷ Decoder s (ConwayRatifyExecContext era) Source # dropCBOR ∷ Proxy (ConwayRatifyExecContext era) → Decoder s () Source # label ∷ Proxy (ConwayRatifyExecContext era) → Text Source #
EraPParams era ⇒ EncCBOR (ConwayRatifyExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods encCBOR ∷ ConwayRatifyExecContext era → Encoding Source # encodedSizeExpr ∷ (∀ t. EncCBOR t ⇒ Proxy t → Size) → Proxy (ConwayRatifyExecContext era) → Size Source # encodedListSizeExpr ∷ (∀ t. EncCBOR t ⇒ Proxy t → Size) → Proxy [ConwayRatifyExecContext era] → Size Source #
HasSimpleRep (ConwayRatifyExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Associated Types type SimpleRep (ConwayRatifyExecContext era) Source # type TheSop (ConwayRatifyExecContext era) ∷ [Type] Source # Methods toSimpleRep ∷ ConwayRatifyExecContext era → SimpleRep (ConwayRatifyExecContext era) Source # fromSimpleRep ∷ SimpleRep (ConwayRatifyExecContext era) → ConwayRatifyExecContext era Source #
EraPParams era ⇒ NFData (ConwayRatifyExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods rnf ∷ ConwayRatifyExecContext era → () #
EraPParams era ⇒ Eq (ConwayRatifyExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods (==) ∷ ConwayRatifyExecContext era → ConwayRatifyExecContext era → Bool # (/=) ∷ ConwayRatifyExecContext era → ConwayRatifyExecContext era → Bool #
ToExpr (PParamsHKD StrictMaybe era) ⇒ ToExpr (ConwayRatifyExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods toExpr ∷ ConwayRatifyExecContext era → Expr Source # listToExpr ∷ [ConwayRatifyExecContext era] → Expr Source #
Inject (ConwayRatifyExecContext era) Coin Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods inject ∷ ConwayRatifyExecContext era → Coin Source #
Inject (ConwayRatifyExecContext era) [GovActionState era] Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base Methods inject ∷ ConwayRatifyExecContext era → [GovActionState era] Source #
type Prerequisites fn (ConwayRatifyExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base type Prerequisites fn (ConwayRatifyExecContext era) = ()
type TypeSpec fn (ConwayRatifyExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base type TypeSpec fn (ConwayRatifyExecContext era) = TypeSpec fn (SimpleRep (ConwayRatifyExecContext era))
type Rep (ConwayRatifyExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base type Rep (ConwayRatifyExecContext era) = D1 ('MetaData "ConwayRatifyExecContext" "Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base" "cardano-ledger-conformance-9.9.9.9-inplace" 'False) (C1 ('MetaCons "ConwayRatifyExecContext" 'PrefixI 'True) (S1 ('MetaSel ('Just "crecTreasury") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Coin) :*: S1 ('MetaSel ('Just "crecGovActionMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [GovActionState era])))
type SimpleRep (ConwayRatifyExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base type SimpleRep (ConwayRatifyExecContext era) = SOP (TheSop (ConwayRatifyExecContext era))
type TheSop (ConwayRatifyExecContext era) Source #
Instance details Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base type TheSop (ConwayRatifyExecContext era) = SOPOf (Rep (ConwayRatifyExecContext era))

nameEpoch ∷ EpochNo → String Source #

nameEnact ∷ EnactSignal era → String Source #

nameGovAction ∷ GovAction era → String Source #

crecTreasuryL ∷ Lens' (ConwayRatifyExecContext era) Coin Source #

crecGovActionMapL ∷ Lens' (ConwayRatifyExecContext era) [GovActionState era] Source #

enactStateSpec ∷ IsConwayUniv fn ⇒ ConwayEnactExecContext ConwayEra → ConwayExecEnactEnv ConwayEra → Specification fn (EnactState ConwayEra) Source #

externalFunctions ∷ ExternalFunctions Source #

Orphan instances

IsConwayUniv fn ⇒ ExecSpecRule fn "ENACT" ConwayEra Source #
Instance details Associated Types type ExecContext fn "ENACT" ConwayEra Source # type ExecEnvironment fn "ENACT" ConwayEra Source # type ExecState fn "ENACT" ConwayEra Source # type ExecSignal fn "ENACT" ConwayEra Source # Methods environmentSpec ∷ ExecContext fn "ENACT" ConwayEra → Specification fn (ExecEnvironment fn "ENACT" ConwayEra) Source # stateSpec ∷ ExecContext fn "ENACT" ConwayEra → ExecEnvironment fn "ENACT" ConwayEra → Specification fn (ExecState fn "ENACT" ConwayEra) Source # signalSpec ∷ ExecContext fn "ENACT" ConwayEra → ExecEnvironment fn "ENACT" ConwayEra → ExecState fn "ENACT" ConwayEra → Specification fn (ExecSignal fn "ENACT" ConwayEra) Source # classOf ∷ ExecSignal fn "ENACT" ConwayEra → Maybe String Source # genExecContext ∷ Gen (ExecContext fn "ENACT" ConwayEra) Source # runAgdaRule ∷ SpecRep (ExecEnvironment fn "ENACT" ConwayEra) → SpecRep (ExecState fn "ENACT" ConwayEra) → SpecRep (ExecSignal fn "ENACT" ConwayEra) → Either OpaqueErrorString (SpecRep (ExecState fn "ENACT" ConwayEra)) Source # translateInputs ∷ ExecEnvironment fn "ENACT" ConwayEra → ExecState fn "ENACT" ConwayEra → ExecSignal fn "ENACT" ConwayEra → ExecContext fn "ENACT" ConwayEra → ImpTestM ConwayEra (SpecRep (ExecEnvironment fn "ENACT" ConwayEra), SpecRep (ExecState fn "ENACT" ConwayEra), SpecRep (ExecSignal fn "ENACT" ConwayEra)) Source # testConformance ∷ ExecContext fn "ENACT" ConwayEra → ExecEnvironment fn "ENACT" ConwayEra → ExecState fn "ENACT" ConwayEra → ExecSignal fn "ENACT" ConwayEra → Property Source # extraInfo ∷ Globals → ExecContext fn "ENACT" ConwayEra → Environment (EraRule "ENACT" ConwayEra) → State (EraRule "ENACT" ConwayEra) → Signal (EraRule "ENACT" ConwayEra) → Either OpaqueErrorString (State (EraRule "ENACT" ConwayEra), [Event (EraRule "ENACT" ConwayEra)]) → Doc AnsiStyle Source #
fn ~ ConwayFn ⇒ ExecSpecRule fn "EPOCH" ConwayEra Source #
Instance details Associated Types type ExecContext fn "EPOCH" ConwayEra Source # type ExecEnvironment fn "EPOCH" ConwayEra Source # type ExecState fn "EPOCH" ConwayEra Source # type ExecSignal fn "EPOCH" ConwayEra Source # Methods environmentSpec ∷ ExecContext fn "EPOCH" ConwayEra → Specification fn (ExecEnvironment fn "EPOCH" ConwayEra) Source # stateSpec ∷ ExecContext fn "EPOCH" ConwayEra → ExecEnvironment fn "EPOCH" ConwayEra → Specification fn (ExecState fn "EPOCH" ConwayEra) Source # signalSpec ∷ ExecContext fn "EPOCH" ConwayEra → ExecEnvironment fn "EPOCH" ConwayEra → ExecState fn "EPOCH" ConwayEra → Specification fn (ExecSignal fn "EPOCH" ConwayEra) Source # classOf ∷ ExecSignal fn "EPOCH" ConwayEra → Maybe String Source # genExecContext ∷ Gen (ExecContext fn "EPOCH" ConwayEra) Source # runAgdaRule ∷ SpecRep (ExecEnvironment fn "EPOCH" ConwayEra) → SpecRep (ExecState fn "EPOCH" ConwayEra) → SpecRep (ExecSignal fn "EPOCH" ConwayEra) → Either OpaqueErrorString (SpecRep (ExecState fn "EPOCH" ConwayEra)) Source # translateInputs ∷ ExecEnvironment fn "EPOCH" ConwayEra → ExecState fn "EPOCH" ConwayEra → ExecSignal fn "EPOCH" ConwayEra → ExecContext fn "EPOCH" ConwayEra → ImpTestM ConwayEra (SpecRep (ExecEnvironment fn "EPOCH" ConwayEra), SpecRep (ExecState fn "EPOCH" ConwayEra), SpecRep (ExecSignal fn "EPOCH" ConwayEra)) Source # testConformance ∷ ExecContext fn "EPOCH" ConwayEra → ExecEnvironment fn "EPOCH" ConwayEra → ExecState fn "EPOCH" ConwayEra → ExecSignal fn "EPOCH" ConwayEra → Property Source # extraInfo ∷ Globals → ExecContext fn "EPOCH" ConwayEra → Environment (EraRule "EPOCH" ConwayEra) → State (EraRule "EPOCH" ConwayEra) → Signal (EraRule "EPOCH" ConwayEra) → Either OpaqueErrorString (State (EraRule "EPOCH" ConwayEra), [Event (EraRule "EPOCH" ConwayEra)]) → Doc AnsiStyle Source #
fn ~ ConwayFn ⇒ ExecSpecRule fn "NEWEPOCH" ConwayEra Source #
Instance details Associated Types type ExecContext fn "NEWEPOCH" ConwayEra Source # type ExecEnvironment fn "NEWEPOCH" ConwayEra Source # type ExecState fn "NEWEPOCH" ConwayEra Source # type ExecSignal fn "NEWEPOCH" ConwayEra Source # Methods environmentSpec ∷ ExecContext fn "NEWEPOCH" ConwayEra → Specification fn (ExecEnvironment fn "NEWEPOCH" ConwayEra) Source # stateSpec ∷ ExecContext fn "NEWEPOCH" ConwayEra → ExecEnvironment fn "NEWEPOCH" ConwayEra → Specification fn (ExecState fn "NEWEPOCH" ConwayEra) Source # signalSpec ∷ ExecContext fn "NEWEPOCH" ConwayEra → ExecEnvironment fn "NEWEPOCH" ConwayEra → ExecState fn "NEWEPOCH" ConwayEra → Specification fn (ExecSignal fn "NEWEPOCH" ConwayEra) Source # classOf ∷ ExecSignal fn "NEWEPOCH" ConwayEra → Maybe String Source # genExecContext ∷ Gen (ExecContext fn "NEWEPOCH" ConwayEra) Source # runAgdaRule ∷ SpecRep (ExecEnvironment fn "NEWEPOCH" ConwayEra) → SpecRep (ExecState fn "NEWEPOCH" ConwayEra) → SpecRep (ExecSignal fn "NEWEPOCH" ConwayEra) → Either OpaqueErrorString (SpecRep (ExecState fn "NEWEPOCH" ConwayEra)) Source # translateInputs ∷ ExecEnvironment fn "NEWEPOCH" ConwayEra → ExecState fn "NEWEPOCH" ConwayEra → ExecSignal fn "NEWEPOCH" ConwayEra → ExecContext fn "NEWEPOCH" ConwayEra → ImpTestM ConwayEra (SpecRep (ExecEnvironment fn "NEWEPOCH" ConwayEra), SpecRep (ExecState fn "NEWEPOCH" ConwayEra), SpecRep (ExecSignal fn "NEWEPOCH" ConwayEra)) Source # testConformance ∷ ExecContext fn "NEWEPOCH" ConwayEra → ExecEnvironment fn "NEWEPOCH" ConwayEra → ExecState fn "NEWEPOCH" ConwayEra → ExecSignal fn "NEWEPOCH" ConwayEra → Property Source # extraInfo ∷ Globals → ExecContext fn "NEWEPOCH" ConwayEra → Environment (EraRule "NEWEPOCH" ConwayEra) → State (EraRule "NEWEPOCH" ConwayEra) → Signal (EraRule "NEWEPOCH" ConwayEra) → Either OpaqueErrorString (State (EraRule "NEWEPOCH" ConwayEra), [Event (EraRule "NEWEPOCH" ConwayEra)]) → Doc AnsiStyle Source #
IsConwayUniv fn ⇒ ExecSpecRule fn "RATIFY" ConwayEra Source #
Instance details Associated Types type ExecContext fn "RATIFY" ConwayEra Source # type ExecEnvironment fn "RATIFY" ConwayEra Source # type ExecState fn "RATIFY" ConwayEra Source # type ExecSignal fn "RATIFY" ConwayEra Source # Methods environmentSpec ∷ ExecContext fn "RATIFY" ConwayEra → Specification fn (ExecEnvironment fn "RATIFY" ConwayEra) Source # stateSpec ∷ ExecContext fn "RATIFY" ConwayEra → ExecEnvironment fn "RATIFY" ConwayEra → Specification fn (ExecState fn "RATIFY" ConwayEra) Source # signalSpec ∷ ExecContext fn "RATIFY" ConwayEra → ExecEnvironment fn "RATIFY" ConwayEra → ExecState fn "RATIFY" ConwayEra → Specification fn (ExecSignal fn "RATIFY" ConwayEra) Source # classOf ∷ ExecSignal fn "RATIFY" ConwayEra → Maybe String Source # genExecContext ∷ Gen (ExecContext fn "RATIFY" ConwayEra) Source # runAgdaRule ∷ SpecRep (ExecEnvironment fn "RATIFY" ConwayEra) → SpecRep (ExecState fn "RATIFY" ConwayEra) → SpecRep (ExecSignal fn "RATIFY" ConwayEra) → Either OpaqueErrorString (SpecRep (ExecState fn "RATIFY" ConwayEra)) Source # translateInputs ∷ ExecEnvironment fn "RATIFY" ConwayEra → ExecState fn "RATIFY" ConwayEra → ExecSignal fn "RATIFY" ConwayEra → ExecContext fn "RATIFY" ConwayEra → ImpTestM ConwayEra (SpecRep (ExecEnvironment fn "RATIFY" ConwayEra), SpecRep (ExecState fn "RATIFY" ConwayEra), SpecRep (ExecSignal fn "RATIFY" ConwayEra)) Source # testConformance ∷ ExecContext fn "RATIFY" ConwayEra → ExecEnvironment fn "RATIFY" ConwayEra → ExecState fn "RATIFY" ConwayEra → ExecSignal fn "RATIFY" ConwayEra → Property Source # extraInfo ∷ Globals → ExecContext fn "RATIFY" ConwayEra → Environment (EraRule "RATIFY" ConwayEra) → State (EraRule "RATIFY" ConwayEra) → Signal (EraRule "RATIFY" ConwayEra) → Either OpaqueErrorString (State (EraRule "RATIFY" ConwayEra), [Event (EraRule "RATIFY" ConwayEra)]) → Doc AnsiStyle Source #
Inject (EpochExecEnv era) () Source #
Instance details Methods inject ∷ EpochExecEnv era → () Source #