consumed does not use rewards param

IntersectMBO · Dec 9, 2019 · 66e60de · 66e60de
1 parent 3b010d5
commit 66e60de
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/shelley/chain-and-ledger/formal-spec/utxo.tex b/shelley/chain-and-ledger/formal-spec/utxo.tex
@@ -102,9 +102,9 @@ \subsection{UTxO Transitions}
     & \text{withdrawal balance} \\
     & \fun{wbalance} ~ ws = \sum_{(\wcard\mapsto c)\in\var{ws}} c
     \nextdef
-    & \fun{consumed} \in \PParams \to \UTxO \to \StakeCreds \to \Wdrl \to \Tx \to \Coin
+    & \fun{consumed} \in \PParams \to \UTxO \to \StakeCreds \to \Tx \to \Coin
     & \text{value consumed} \\
-    & \consumed{pp}{utxo}{stkCreds}{rewards}~{tx} = \\
+    & \consumed{pp}{utxo}{stkCreds}{tx} = \\
     & ~~\ubalance{(\txins{tx} \restrictdom \var{utxo})} +
         \fun{wbalance}~(\fun{txwdrls}~{tx}) \\
     & ~~ + \keyRefunds{pp}{stkCreds}{tx} \\