Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
This module provides the necessary instances of HasSpec
and HasSimpleRep
to write specs for the environments,
states, and signals in the conway STS rules. Note some simple
types used in the PParams (Coin, EpochInterval, etc.) have their
instances defined in Test.Cardano.Ledger.Constrained.Conway.InstancesBasic
and they are reexported here.
Documentation
data StringFn (fn ∷ [Type] → Type → Type) as b Source #
Instances
FunctionLike (StringFn fn) Source # | |
IsConwayUniv fn ⇒ Functions (StringFn fn) fn Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Instances propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ StringFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ StringFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ StringFn fn '[a] b → TypeSpec fn a → Specification fn b Source # | |
IsConwayUniv fn ⇒ Show (StringFn fn as b) Source # | |
IsConwayUniv fn ⇒ Eq (StringFn fn as b) Source # | |
type ProposalTree = (StrictMaybe (GovActionId StandardCrypto), [Tree GAS]) Source #
onJust' ∷ (HasSpec fn a, IsNormalType a, IsPred p fn) ⇒ Term fn (StrictMaybe a) → (Term fn a → p) → Pred fn Source #
onSized ∷ (IsConwayUniv fn, HasSpec fn a, IsPred p fn) ⇒ Term fn (Sized a) → (Term fn a → p) → Pred fn Source #
cKeyHashObj ∷ (IsConwayUniv fn, Typeable r, Crypto c) ⇒ Term fn (KeyHash r c) → Term fn (Credential r c) Source #
cScriptHashObj ∷ (IsConwayUniv fn, Typeable r, Crypto c) ⇒ Term fn (ScriptHash c) → Term fn (Credential r c) Source #
maryValueCoin_ ∷ (IsConwayUniv fn, Crypto c) ⇒ Term fn (MaryValue c) → Term fn Coin Source #
strLen_ ∷ ∀ fn s. (Member (StringFn fn) fn, StringLike s, HasSpec fn s) ⇒ Term fn s → Term fn Int Source #
txOutVal_ ∷ (HasSpec fn (Value era), Era era, HasSpec fn (Data era), Val (Value era), HasSpec fn (Script era), IsConwayUniv fn, HasSpec fn (BabbageTxOut era), IsNormalType (Script era)) ⇒ Term fn (BabbageTxOut era) → Term fn (Value era) Source #
pProcDeposit_ ∷ (EraPP Conway, IsConwayUniv fn) ⇒ Term fn (ProposalProcedure Conway) → Term fn Coin Source #
pProcGovAction_ ∷ (EraPP Conway, IsConwayUniv fn) ⇒ Term fn (ProposalProcedure Conway) → Term fn (GovAction Conway) Source #
type IsConwayUniv fn = (BaseUniverse fn, Member (CoinFn fn) fn, Member (CoerceFn fn) fn, Member (StringFn fn) fn, Member (MapFn fn) fn, Member (FunFn fn) fn, Member (TreeFn fn) fn) Source #
gasId_ ∷ (EraPP Conway, IsConwayUniv fn) ⇒ Term fn (GovActionState Conway) → Term fn (GovActionId StandardCrypto) Source #
gasCommitteeVotes_ ∷ (EraPP Conway, IsConwayUniv fn) ⇒ Term fn (GovActionState Conway) → Term fn (Map (Credential 'HotCommitteeRole StandardCrypto) Vote) Source #
gasDRepVotes_ ∷ (EraPP Conway, IsConwayUniv fn) ⇒ Term fn (GovActionState Conway) → Term fn (Map (Credential 'DRepRole StandardCrypto) Vote) Source #
gasProposalProcedure_ ∷ (EraPP Conway, IsConwayUniv fn) ⇒ Term fn (GovActionState Conway) → Term fn (ProposalProcedure Conway) Source #
data ProposalsSplit Source #
Instances
coerce_ ∷ ∀ a b fn. (Member (CoerceFn fn) fn, HasSpec fn a, HasSpec fn b, CoercibleLike a b) ⇒ Term fn a → Term fn b Source #
toDelta_ ∷ (HasSpec fn Coin, HasSpec fn DeltaCoin, Member (CoinFn fn) fn) ⇒ Term fn Coin → Term fn DeltaCoin Source #