Improve mkdocs toc

build-tools/static/md/mkdocs/docs/css/custom.css

@@ -198,5 +198,9 @@ body.reveal-agda-source pre.Agda.hidden-source {
 }
 /* Tighten sidebars slightly. */
 .md-sidebar--secondary {
-  width: 14rem; /* default ~15rem */
+  width: 15rem; /* default ~15rem */
+}
+.md-sidebar--primary .md-nav__list {
+  width: 9rem;
+  left: -9rem;
 }

build-tools/static/md/mkdocs/includes/links.md

@@ -38,6 +38,7 @@
 [GOVCERT]: Ledger.Conway.Specification.Certs.md#auxiliary-govcert-transition-system
 [Governance Functions]: Ledger.Conway.Specification.Gov.md#governance-functions
 [issues]: https://github.com/IntersectMBO/formal-ledger-specifications/issues
+[Introduction]: Ledger.Introduction.md
 [LEDGER]: Ledger.Conway.Specification.Ledger.md#ledger-transition-system
 [Ledger.Properties]: Ledger.Conway.Specification.Ledger.Properties.md
 [Ledger.Properties.GovDepsMatch]: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md
@@ -60,16 +61,19 @@
 [scriptsCost]: Ledger.Conway.Specification.Fees.md#scriptsCost
 [Shelley Ledger Spec (pdf)]: https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf
 [SNAP]: Ledger.Conway.Specification.Rewards.md#sec:snap-transition-system
+[STS Diagram]: Ledger.Introduction.md#fig:latest-sts-diagram
+[The GOV Transition System]: Ledger.Conway.Specification.Gov.md#the-gov-transition-system
 [The UTXOW Transition System]: Ledger.Conway.Specification.Utxow.md#sec:the-utxow-transition-system
 [thm:ChainGovDepsMatch]: Ledger.Conway.Specification.Chain.Properties.GovDepsMatch.md#thm:ChainGovDepsMatch
 [Time handling on Cardano]: https://docs.cardano.org/about-cardano/explore-more/time
 [Timing of Rewards Payout]: Ledger.Conway.Specification.Rewards.md#sec:timing-of-rewards-payout
-[The GOV Transition System]: Ledger.Conway.Specification.Gov.md#the-gov-transition-system
+[Transaction Levels]: Ledger.Dijkstra.Specification.Transaction.md#sec:transaction-levels
+[Transaction Structure]: Ledger.Dijkstra.Specification.Transaction.md#sec:transaction-structure
+[Transactions]: Ledger.Dijkstra.Specification.Transaction.md#sec:transactions
 [UTXO]: Ledger.Conway.Specification.Utxo.md#sec:the-utxo-transition-system
 [Utxo.Properties.MinSpend]: Ledger.Conway.Specification.Utxo.Properties.MinSpend.md
 [Utxo.Properties.PoV]: Ledger.Conway.Specification.Utxo.Properties.PoV.md
 [UTXOS]: Ledger.Conway.Specification.Utxo.md#sec:the-utxos-transition-rule
 [UTXOW]: Ledger.Conway.Specification.Utxow.md#sec:the-utxow-transition-system
 [Utxow module]: Ledger.Conway.Specification.Utxow.md
 [Validity and wellformedness predicates]: Ledger.Conway.Specification.Gov.md#validity-and-wellformedness-predicates
-

src/Interface/TypeClasses.lagda.md

@@ -0,0 +1,17 @@
+---
+source_branch: master
+source_path: src/Interface/TypeClasses.lagda.md
+---
+
+# Type Classes
+
+<!--
+```agda
+{-# OPTIONS --safe #-}
+
+module Interface.TypeClasses where
+
+import Interface.TypeClasses.HasSubtract
+import Interface.TypeClasses.HasSubset
+import Interface.TypeClasses.Hashable
+```

src/Interface/HasSubset.lagda.md → src/Interface/TypeClasses/HasSubset.lagda.md

@@ -1,18 +1,26 @@
 ---
 source_branch: master
-source_path: src/Interface/HasSubset.lagda.md
+source_path: src/Interface/TypeClasses/HasSubset.lagda.md
 ---
 
+<!--
 ```agda
 {-# OPTIONS --safe #-}
 
-module Interface.HasSubset where
+module Interface.TypeClasses.HasSubset where
 
 open import Level using (Level; suc)
+```
+-->
 
+```agda
 record HasSubset {a} (A : Set a) : Set (suc a) where
   field _⊆_ : A → A → Set a
   infix 4 _⊆_
+```
 
+<!--
+```agda
 open HasSubset ⦃...⦄ public
 ```
+-->

src/Interface/HasSubtract.lagda.md → src/Interface/TypeClasses/HasSubtract.lagda.md

@@ -1,17 +1,24 @@
 ---
 source_branch: master
-source_path: src/Interface/HasSubtract.lagda.md
+source_path: src/Interface/TypeClasses/HasSubtract.lagda.md
 ---
 
+<!--
 ```agda
 {-# OPTIONS --safe --cubical-compatible #-}
-module Interface.HasSubtract where
+module Interface.TypeClasses.HasSubtract where
 
 open import Agda.Primitive using () renaming (Set to Type)
+```
+-->
 
+```agda
 record HasSubtract (A B : Type) : Type where
   infixl 6 _-_
   field _-_ : A → A → B
+```
 
+<!--
+```agda
 open HasSubtract ⦃ ... ⦄ public
 ```

src/Interface/HasSubtract/Instances.lagda.md → src/Interface/TypeClasses/HasSubtract/Instances.lagda.md

@@ -1,18 +1,22 @@
 ---
 source_branch: master
-source_path: src/Interface/HasSubtract/Instances.lagda.md
+source_path: src/Interface/TypeClasses/HasSubtract/Instances.lagda.md
 ---
 
+<!--
 ```agda
 {-# OPTIONS --safe #-}
 
-module Interface.HasSubtract.Instances where
+module Interface.TypeClasses.HasSubtract.Instances where
 
-open import Interface.HasSubtract
+open import Interface.TypeClasses.HasSubtract
 
 open import Data.Integer as ℤ using (ℤ)
 open import Data.Nat     as ℕ using (ℕ)
+```
+-->
 
+```agda
 instance
   HasSubtract-ℕ : HasSubtract ℕ ℕ
   HasSubtract-ℕ ._-_ = ℕ._∸_

src/Interface/Hashable.lagda.md → src/Interface/TypeClasses/Hashable.lagda.md

@@ -1,20 +1,30 @@
 ---
 source_branch: master
-source_path: src/Interface/Hashable.lagda.md
+source_path: src/Interface/TypeClasses/Hashable.lagda.md
 ---
 
+<!--
 ```agda
 {-# OPTIONS --safe #-}
-module Interface.Hashable where
+module Interface.TypeClasses.Hashable where
 
 open import Agda.Builtin.Equality
 open import Agda.Primitive using () renaming (Set to Type)
+```
+-->
 
+```agda
 record Hashable (T THash : Type) : Type where
   field hash    : T → THash
+```
 
+<!--
+```agda
 open Hashable ⦃...⦄ public
+```
+-->
 
+```agda
 Hashable₁ : (Type → Type) → Type → Type₁
 Hashable₁ F THash = {A : Type} → ⦃ Hashable A THash ⦄ → Hashable (F A) THash
 

src/Ledger.lagda.md

@@ -8,6 +8,7 @@ module Ledger where
 
 import Ledger.Introduction
 import Ledger.PreConway
+import Ledger.Core
 import Ledger.Conway
 import Ledger.Dijkstra
 

src/Ledger/Conway/Specification.lagda.md

@@ -3,46 +3,159 @@ source_branch: master
 source_path: src/Ledger/Conway/Specification.lagda.md
 ---
 
+This is the formal specification of the Cardano ledger for the Conway era.
+
+The Agda source code which formalizes the ledger specification in the Conway era
+consists of the modules listed below.  How these modules fit together to form a
+collection of interdependent state transition systems is illustrated by the
+[STS Diagram][] in the [Introduction][] section.
+
+<!--
 ```agda
 {-# OPTIONS --safe #-}
 module Ledger.Conway.Specification where
+```
+-->
 
+## <span class="AgdaModule">BlockBody</span>
+
+The Block Body Transition updates the block body state which comprises the
+ledger state and the map describing the produced blocks.
+
+```agda
 import Ledger.Conway.Specification.BlockBody
 import Ledger.Conway.Specification.BlockBody.Properties
+```
+
+
+## Certificates
+
+```agda
 import Ledger.Conway.Specification.Certs
 import Ledger.Conway.Specification.Certs.Properties
+```
+
+
+## <span class="AgdaModule">Chain</span>
+
+```agda
 import Ledger.Conway.Specification.Chain
 import Ledger.Conway.Specification.Chain.Properties
+```
+
+## Enactment
+
+These modules concern the enactment of governance proposals and actions.
+
+```agda
 import Ledger.Conway.Specification.Enact
 import Ledger.Conway.Specification.Enact.Properties
+```
+
+## <span class="AgdaModule">Epoch</span>
+
+```agda
 import Ledger.Conway.Specification.Epoch
 import Ledger.Conway.Specification.Epoch.Properties
+```
+
+## <span class="AgdaModule">Fees</span>
+
+This module defines a function that calculates the fee for reference scripts in a
+transaction.
+
+```agda
 import Ledger.Conway.Specification.Fees
+```
+
+## Governance
+
+```agda
 import Ledger.Conway.Specification.Gov
 import Ledger.Conway.Specification.Gov.Actions
 import Ledger.Conway.Specification.Gov.Properties
 import Ledger.Conway.Specification.Gov.Properties.ChangePPGroup
+import Ledger.Conway.Specification.Types.GovStructure
+```
+
+## <span class="AgdaModule">Ledger</span>
+
+The `Ledger`{.AgdaModule} module defines the ledger transition system where valid
+transactions transform the ledger state.
+
+```agda
 import Ledger.Conway.Specification.Ledger
 import Ledger.Conway.Specification.Ledger.Properties
+```
+
+## Protocol Parameters
+
+The defines the adjustable protocol parameters of the Cardano ledger.
+
+```agda
 import Ledger.Conway.Specification.PParams
+```
+
+## Properties of the Ledger Specification
+
+```agda
 import Ledger.Conway.Specification.Properties
+```
+
+## Ratification
+
+```agda
 import Ledger.Conway.Specification.Ratify
 import Ledger.Conway.Specification.Ratify.Properties
+```
+
+## <span class="AgdaModule">Rewards</span>
+
+```agda
 import Ledger.Conway.Specification.Rewards
 import Ledger.Conway.Specification.RewardUpdate
 import Ledger.Conway.Specification.RewardUpdate.Properties
+```
+
+## Scripts
+
+```agda
 import Ledger.Conway.Specification.Script
 import Ledger.Conway.Specification.Script.Validation
+```
+
+## Tests and Examples
+
+```agda
 import Ledger.Conway.Specification.Test.Examples
 import Ledger.Conway.Specification.Test.StructuredContracts
+```
+
+## Token Algebras
+
+```agda
 import Ledger.Conway.Specification.TokenAlgebra.Base
 import Ledger.Conway.Specification.TokenAlgebra.Coin
 import Ledger.Conway.Specification.TokenAlgebra.ValueSet
 import Ledger.Conway.Specification.TokenAlgebra.ValueVector
+```
+
+## Transactions
+
+```agda
 import Ledger.Conway.Specification.Transaction
-import Ledger.Conway.Specification.Types.GovStructure
+```
+
+## <span class="AgdaModule">Utxo</span>
+
+```agda
 import Ledger.Conway.Specification.Utxo
 import Ledger.Conway.Specification.Utxo.Properties
+```
+
+## <span class="AgdaModule">Utxow</span>
+
+```agda
 import Ledger.Conway.Specification.Utxow
 import Ledger.Conway.Specification.Utxow.Properties
 ```

src/Ledger/Conway/Specification/Utxo.lagda.md

@@ -1,7 +1,5 @@
 # UTxO {#sec:utxo}
 
-This section defines types and functions needed for the UTxO transition system.
-
 The UTxO transition system is built up from a number of smaller parts defined in this
 section, culminating in the `UTXO`{.AgdaDatatype} rule given in the final
 subsection below ([UTXO Inference Rule][UTXO]).
@@ -50,6 +48,8 @@ instance
 
 ## Functions supporting UTxO rules {#sec:functions-supporting-utxo-rules}
 
+This section defines types and functions needed for the UTxO transition system.
+
 ```agda
 totExUnits : Tx → ExUnits
 totExUnits tx = ∑[ (_ , eu) ← tx .wits .txrdmrs ] eu

src/Ledger/Core.lagda.md

@@ -0,0 +1,10 @@
+---
+source_branch: master
+source_path: src/Ledger/Core.lagda.md
+---
+
+```agda
+module Ledger.Core where
+
+import Ledger.Core.Specification
+```