Skip to content

Commit

Permalink
PDF cleanup: Fig 13 PParams (#242)
Browse files Browse the repository at this point in the history
* Replace `pparamsWellFormed` with a predicate instead of a boolean.

Addresses an item concerning Fig 13 in issue
[146](#146)

* reflect formatting suggestions of @omelkonian

* remove overzelous alignment, as requested
  • Loading branch information
williamdemeo authored Oct 17, 2023
1 parent 889771c commit 26e228d
Showing 1 changed file with 6 additions and 6 deletions.
12 changes: 6 additions & 6 deletions src/Ledger/PParams.lagda
Original file line number Diff line number Diff line change
Expand Up @@ -90,12 +90,12 @@ record PParams : Set where
-- collateralPercent : ℕ
maxCollateralInputs : ℕ

paramsWellFormed : PParams → Bool
paramsWellFormed pp = ¿ 0 ∉ fromList
paramsWellFormed : PParams → Set
paramsWellFormed pp = 0 ∉ fromList
( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize ∷ minUTxOValue ∷ poolDeposit
∷ collateralPercent ∷ ccMaxTermLength ∷ govActionLifetime ∷ govActionDeposit
∷ drepDeposit ∷ [])
× ℕtoEpoch govActionLifetime ≤ drepActivity ¿ᵇ
∷ drepDeposit ∷ [] )
× ℕtoEpoch govActionLifetime ≤ drepActivity
where open PParams pp
\end{code}
\end{AgdaAlign}
Expand Down Expand Up @@ -147,8 +147,8 @@ record PParamsDiff : Set₁ where
applyUpdate : PParams → UpdateT → PParams
ppdWellFormed : UpdateT → Bool
ppdWellFormed⇒WF : ∀ {u} → ppdWellFormed u ≡ true → ∀ pp
→ paramsWellFormed pp ≡ true
→ paramsWellFormed (applyUpdate pp u) ≡ true
→ paramsWellFormed pp
→ paramsWellFormed (applyUpdate pp u)

record GovParams : Set₁ where
field ppUpd : PParamsDiff
Expand Down

0 comments on commit 26e228d

Please sign in to comment.