{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.NewEpoch () where

import Cardano.Ledger.Conway (ConwayEra)
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (ExecSpecRule (..), SpecTRC (..), unComputationResult_)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()
import Test.Cardano.Ledger.Conway.ImpTest ()

instance ExecSpecRule "NEWEPOCH" ConwayEra where
  runAgdaRuleWithDebug :: HasCallStack =>
SpecTRC "NEWEPOCH" ConwayEra
-> Either Text (SpecState "NEWEPOCH" ConwayEra, Text)
runAgdaRuleWithDebug (SpecTRC SpecEnvironment "NEWEPOCH" ConwayEra
env SpecState "NEWEPOCH" ConwayEra
st SpecSignal "NEWEPOCH" ConwayEra
sig) = ComputationResult Void (T_Pair_22 () () NewEpochState Text)
-> Either Text (T_Pair_22 () () NewEpochState Text)
forall a e. ComputationResult Void a -> Either e a
unComputationResult_ (ComputationResult Void (T_Pair_22 () () NewEpochState Text)
 -> Either Text (T_Pair_22 () () NewEpochState Text))
-> ComputationResult Void (T_Pair_22 () () NewEpochState Text)
-> Either Text (T_Pair_22 () () NewEpochState Text)
forall a b. (a -> b) -> a -> b
$ ()
-> NewEpochState
-> Integer
-> ComputationResult Void (T_Pair_22 () () NewEpochState Text)
Agda.newEpochStep ()
SpecEnvironment "NEWEPOCH" ConwayEra
env NewEpochState
SpecState "NEWEPOCH" ConwayEra
st Integer
SpecSignal "NEWEPOCH" ConwayEra
sig