From 12c3635880f246869d41df77d0f70ecb32bfe6a3 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Sun, 18 Feb 2024 20:19:26 -0700 Subject: [PATCH] revert to original `CHAIN` transition rule in `Ledger.Chain` --- src/Ledger/Chain.lagda | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Ledger/Chain.lagda b/src/Ledger/Chain.lagda index 82cedb217..377a9b52d 100644 --- a/src/Ledger/Chain.lagda +++ b/src/Ledger/Chain.lagda @@ -84,12 +84,10 @@ calculateStakeDistrs ls = { stakeDistr = govActionDeposits ls } +data \end{code} \begin{figure*}[h] \begin{AgdaMulticode} -\begin{code}[hide] -data -\end{code} \begin{code} _⊢_⇀⦇_,CHAIN⦈_ : ⊤ → ChainState → Block → ChainState → Set \end{code} @@ -100,7 +98,7 @@ data \end{code} \begin{figure*}[h] \begin{code} - CHAIN : + CHAIN : let open ChainState s; open Block b; open NewEpochState newEpochState open EpochState epochState; open EnactState es in