Skip to content

Commit fdc562b

Browse files
Update src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda
Co-authored-by: William DeMeo <williamdemeo@gmail.com>
1 parent 02c5969 commit fdc562b

File tree

1 file changed

+6
-4
lines changed

1 file changed

+6
-4
lines changed

src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -59,12 +59,14 @@ module _ {eps : EpochState} {e : Epoch} where
5959
(p₁' , p₂' , p₃')
6060
) = eps'≡eps''
6161
where
62-
ls = EpochState.ls eps
63-
fut = EpochState.fut eps
62+
ls : LState
63+
ls = LStateOf eps
6464

65-
es = EnactStateOf fut
65+
es : EnactState
66+
es = EnactStateOf (RatifyStateOf eps)
6667

67-
govUpd = GovernanceUpdate.updates ls fut
68+
govUpd : Governance-Update
69+
govUpd = GovernanceUpdate.updates ls (RatifyStateOf eps)
6870

6971
govSt' = Governance-Update.govSt' govUpd
7072

0 commit comments

Comments
 (0)