From 751187e210edb6a2b7fc49643f84e6ed00ed094e Mon Sep 17 00:00:00 2001
From: William DeMeo <williamdemeo@gmail.com>
Date: Sun, 18 Feb 2024 20:19:26 -0700
Subject: [PATCH] revert to original `CHAIN` transition rule in `Ledger.Chain`

---
 src/Ledger/Chain.lagda | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/src/Ledger/Chain.lagda b/src/Ledger/Chain.lagda
index 82cedb217..264d88819 100644
--- a/src/Ledger/Chain.lagda
+++ b/src/Ledger/Chain.lagda
@@ -84,12 +84,10 @@ calculateStakeDistrs ls =
     { stakeDistr = govActionDeposits ls
     }
 
-\end{code}
-\begin{figure*}[h]
-\begin{AgdaMulticode}
-\begin{code}[hide]
+
 data
 \end{code}
+\begin{figure*}[h]
 \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
@@ -112,6 +110,5 @@ data
     _ ⊢ s ⇀⦇ b ,CHAIN⦈
         record s { newEpochState = record nes { epochState = record epochState { ls = ls'} } }
 \end{code}
-\end{AgdaMulticode}
 \caption{CHAIN transition system}
 \end{figure*}