IntersectMBO / formal-ledger-specifications

Formal specifications of the cardano ledger
Apache License 2.0
36 stars 13 forks source link

Postprocessing duplicates code #472

Closed WhatisRT closed 3 months ago

WhatisRT commented 3 months ago

The following code produces the wrong output:

mkStakeDistrs : Snapshot → GovState → Deposits → (Credential ⇀ VDeleg) → StakeDistrs
mkStakeDistrs ⟦ stake , _ ⟧ˢ govSt ds delegations .StakeDistrs.stakeDistr =
  aggregateBy (proj₁ delegations) (stake ∪⁺ gaDepositStake govSt ds)
Screenshot 2024-06-18 at 15 07 27

There are at least two issues here:

Also, I don't know if this is caused by the same problem, but the spacing of that pattern is super weird.