Skip to content

Commit aba7685

Browse files
committed
Fix GovDepsMatch
1 parent 0538bbe commit aba7685

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -180,7 +180,7 @@ For the formal statement of the lemma,
180180
a ∈ˡ map' (GovActionDeposit ∘ proj₁) (filter P? govSt) ∼⟨ ∈-fromList ⟩
181181
a ∈ fromList (map' (GovActionDeposit ∘ proj₁) (filter P? govSt)) ∎
182182
183-
u0 = EPOCH-updates0 (RatifyStateOf eps) (LStateOf eps)
183+
u0 = EPOCHUpdates0.updates (RatifyStateOf eps) (LStateOf eps)
184184
185185
ls₁ = record (LStateOf eps') { utxoSt = EPOCH-Updates0.utxoSt' u0 }
186186

0 commit comments

Comments
 (0)