Skip to content

Commit 6b12753

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

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,7 @@ module _ {eps : EpochState} {e : Epoch} where
9595
Γ≡Γ' = cong₂ (λ sd acnt ⟦ sd , e , DRepsOf ls , CCHotKeysOf ls , TreasuryOf acnt , PoolsOf ls , VoteDelegsOf ls ⟧)
9696
stakeDistrs₁≡stakeDistrs₂ (cong Post-POOLREAP-Update.acnt'' pPRUpd₁≡pPRUpd₂)
9797

98-
fut'≡fut'' : EpochState.fut eps' ≡ EpochState.fut eps''
98+
fut'≡fut'' : RatifyStateOf eps' ≡ RatifyStateOf eps''
9999
fut'≡fut'' = RATIFIES-deterministic-≡ Γ≡Γ' refl refl p₃ p₃'
100100

101101
eps'≡eps'' : eps' ≡ eps''

0 commit comments

Comments
 (0)