revert to original CHAIN transition rule in Ledger.Chain

IntersectMBO · Feb 19, 2024 · 12c3635 · 12c3635
1 parent 7cab3e4
commit 12c3635
Showing 1 changed file with 2 additions and 4 deletions.
diff --git 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