Formal Ledger Specification
Core
Initializing search
    GitHub
    • Navigation
    GitHub
      • Home
      • Guide for Contributors
        • Notation
      • Ledger
        • Introduction
        • Prelude
          • Base
          • Instances
        • Conway
          • Abstract
          • Address
          • BaseTypes
          • Certs
            • Properties
              • PoV
              • PoVLemmas
              • VoteDelegsVDeleg
          • Chain
            • Properties
              • CredDepsEqualDomRwds
              • EpochStep
              • GovDepsMatch
              • PParamsWellFormed
          • Crypto
          • Enact
            • Properties
          • Epoch
            • Properties
              • ConstRwds
              • GovDepsMatch
              • NoPropSameDReps
          • Fees
          • Gov
            • Base
            • Actions
            • Properties
              • ChangePPGroup
          • Ledger.Ledger
            • Properties
              • GovDepsMatch
              • PoV
          • PParams
          • Properties
          • Ratify
            • Properties
          • Rewards
          • Script
            • Base
            • Timelock
            • Validation
            • Base
            • Coin
            • ValueSet
            • ValueVector
          • Transaction
            • Epoch
            • Numeric
              • UnitInterval
              • PositiveNat
          • Utxo
            • Properties
              • MinSpend
              • PoV
          • Utxow
            • Properties
            • ExternalFunctions
            • HSLedger
              • Address
              • BaseTypes
              • Cert
              • Certs
              • Chain
              • Core
              • Enact
              • Epoch
              • ExternalStructures
              • Gov
                • Core
                • Actions
              • Ledger
              • NewEpoch
              • PParams
              • Ratify
              • Transaction
              • Utxo
            • HSTypes
            • Util
            • Certs
              • Properties
            • Chain
              • Properties
            • Epoch
              • Properties
            • Equivalence
              • Bisimilarity
              • Certs
              • Convert
              • Deposits
              • Map
              • Utxo
            • Gov
            • Ledger
              • Properties
            • Properties
            • Script
            • Utxo
              • Properties
            • Utxow
              • Properties
            • Examples
              • HelloWorld
              • SucceedIfNumber
            • LedgerImplementation
            • Lib
            • Prelude
            • StructuredContracts
        • ConwaySafe
          • HasCoin
        • PreConway
            • NewPP
              • Properties
            • PPUp
              • Properties
          • NewPP
            • Properties
          • PPUp
            • Properties
        • Convertible
          • Deriving
          • DerivingTest
        • HaskellTypes
          • Deriving
        • EssentialAgda
        • Agda Prelude
            • ComputationalRelation
            • HasSubset
            • HasSubtract
              • Instance
            • Hashable
            • STS
          • MyDebugOptions

    Core

    module Ledger.Conway.Foreign.HSLedger.Gov.Core where
    
    open import Ledger.Conway.Foreign.HSLedger.Address
    open import Ledger.Conway.Foreign.HSLedger.BaseTypes
    open import Ledger.Conway.Gov.Actions govStructure using (Vote)
    
    instance
      HsTy-GovRole = autoHsType GovRole
      Conv-GovRole = autoConvert GovRole
    
      HsTy-Anchor = autoHsType Anchor
      Conv-Anchor = autoConvert Anchor
    
      HsTy-VDeleg = autoHsType VDeleg
      Conv-VDeleg = autoConvert VDeleg
    
      HsTy-Vote = autoHsType Vote
      Conv-Vote = autoConvert Vote
    
      HsTy-GovVote = autoHsType GovVote
      Conv-GovVote = autoConvert GovVote
    
    
    Previous
    Gov
    Next
    Actions
    Made with Material for MkDocs