{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledgers () where import Cardano.Ledger.Conway (ConwayEra) import Cardano.Ledger.Conway.Governance (EnactState) import qualified MAlonzo.Code.Ledger.Foreign.API as Agda import Test.Cardano.Ledger.Conformance ( ExecSpecRule (..), runFromAgdaFunction, ) import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway () import Test.Cardano.Ledger.Conway.ImpTest () instance ExecSpecRule "LEDGERS" ConwayEra where type ExecContext "LEDGERS" ConwayEra = EnactState ConwayEra runAgdaRule :: HasCallStack => SpecTRC "LEDGERS" ConwayEra -> Either Text (SpecState "LEDGERS" ConwayEra) runAgdaRule = (SpecEnvironment "LEDGERS" ConwayEra -> SpecState "LEDGERS" ConwayEra -> SpecSignal "LEDGERS" ConwayEra -> ComputationResult Text (SpecState "LEDGERS" ConwayEra)) -> SpecTRC "LEDGERS" ConwayEra -> Either Text (SpecState "LEDGERS" ConwayEra) forall (rule :: Symbol) era. (SpecEnvironment rule era -> SpecState rule era -> SpecSignal rule era -> ComputationResult Text (SpecState rule era)) -> SpecTRC rule era -> Either Text (SpecState rule era) runFromAgdaFunction LEnv -> LState -> [Tx] -> T_ComputationResult_44 Text LState SpecEnvironment "LEDGERS" ConwayEra -> SpecState "LEDGERS" ConwayEra -> SpecSignal "LEDGERS" ConwayEra -> ComputationResult Text (SpecState "LEDGERS" ConwayEra) Agda.ledgersStep