{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Test.Cardano.Ledger.Constrained.Conway.PParams where
import Cardano.Ledger.Core (PParams (..))
import Constrained
import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams (
EraSpecPParams (..),
simplePParamsSpec,
)
pparamsSpec ::
forall fn era. (EraSpecPParams era, BaseUniverse fn) => Specification fn (PParams era)
pparamsSpec :: forall (fn :: [*] -> * -> *) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec = forall a (fn :: [*] -> * -> *) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
HasSpec fn (SimpleRep a), HasSimpleRep a,
All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term fn (SimplePParams era)
simplepp -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (SimplePParams era)
simplepp (forall (fn :: [*] -> * -> *) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (SimplePParams era)
simplePParamsSpec @fn @era)