Skip to content

Commit

Permalink
revert to original CHAIN transition rule in Ledger.Chain
Browse files Browse the repository at this point in the history
  • Loading branch information
williamdemeo committed Feb 19, 2024
1 parent 7cab3e4 commit 751187e
Showing 1 changed file with 3 additions and 6 deletions.
9 changes: 3 additions & 6 deletions src/Ledger/Chain.lagda
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand All @@ -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
Expand All @@ -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*}

0 comments on commit 751187e

Please sign in to comment.