search

IntersectMBO / formal-ledger-specifications

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

Remove field and constructor keywords from pdf #462

Closed williamdemeo closed 3 months ago

williamdemeo commented 3 months ago

Description

This closes issue #441.

Checklist

williamdemeo commented 3 months ago

There are still some showing:

  • constructor for UTxOState and GovEnv
  • field for everything in Figure 3 and UTxOState

I don't see field in Figure 3. 🤔

I removed the remaining ones you found in UTxOState and GovEnv. (Good catch! Sorry... I'm not sure how I missed those.)

I did one final global search and I believe every field and constructor that previously appeared in non-hidden code blocks in .lagda files is now hidden, with the exception of one constructor in the "Essential Agda" section. If I'm still missing anything, please let me know.

WhatisRT commented 3 months ago

Are you looking at conway-ledger.pdf? Figure 3 is things relating to protocol parameters, and that's still not fixed in your most recent commit.

williamdemeo commented 3 months ago

I was looking at cardano-ledger.pdf 🤦🏼‍♂️ ...will fix it now.