ChangePPGroup

{-# OPTIONS --safe #-}

open import Ledger.Conway.Abstract
open import Ledger.Conway.Transaction

module Ledger.Conway.Gov.Properties.ChangePPGroup
  (txs : _) (open TransactionStructure txs)
  where

open import Ledger.Prelude

instance
  _ : IsSet TxBody GovProposal
  _ = record { toSet = fromList ∘ TxBody.txprop }

- *Informally*. Let : `GovProposal`{.AgdaRecord} be a governance proposal and suppose the `GovActionType`{.AgdaDatatype} of `.action`{.AgdaField} is `ChangePParams`{.AgdaInductiveConstructor}. If the data field of —that is = `.action`{.AgdaField} `.gaData`{.AgdaField}—is denoted by (“parameter update”), then the set `updateGroups`{.AgdaField} is nonempty. - *Formally*.

ChangePPHasGroup : {tx : Tx} {p : GovProposal} (pu : PParamsUpdate)
  → p ∈ Tx.body tx → p .GovProposal.action ≡ $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1560}{\htmlId{898}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Gov.Properties.ChangePPGroup.html#831}{\htmlId{914}{\htmlClass{Bound}{\text{pu}}}}\, \end{pmatrix}$
  → Type
ChangePPHasGroup pu _ _ = updateGroups pu ≢ ∅

- *Proof*. *To appear* (in the module of the [formal ledger repository](\repourl)).