Skip to content

Commit f07f35c

Browse files
williamdemeowilliamdemeo
committed
improvements:
+ move Core up + improve layout of toc via css + move type class defs + add intro for `Ledger.Core.Specification`
1 parent ca269d9 commit f07f35c

File tree

10 files changed

+113
-34
lines changed

10 files changed

+113
-34
lines changed

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -198,5 +198,9 @@ body.reveal-agda-source pre.Agda.hidden-source {
198198
}
199199
/* Tighten sidebars slightly. */
200200
.md-sidebar--secondary {
201-
width: 14rem; /* default ~15rem */
201+
width: 15rem; /* default ~15rem */
202+
}
203+
.md-sidebar--primary .md-nav__list {
204+
width: 9rem;
205+
left: -9rem;
202206
}

‎build-tools/static/md/nav.yml‎

Lines changed: 19 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,12 @@
44
- Introduction: Ledger.Introduction.md
55
- Properties: Properties.md
66
- Notation: Notation.md
7+
- Core:
8+
- Introduction: Ledger.Core.Specification.md
9+
- Modules/:
10+
- Address: Ledger.Core.Specification.Address.md
11+
- Crypto: Ledger.Core.Specification.Crypto.md
12+
- Epoch: Ledger.Core.Specification.Epoch.md
713
- Conway:
814
- Introduction: Ledger.Conway.Specification.md
915
- Modules/:
@@ -133,17 +139,10 @@
133139
- Bootstrapping:
134140
- Bootstrapping Governance: ConwayBootstrap.md
135141
- Bootstrapping EnactState: ConwayBootstrapEnact.md
136-
- Era Independent Modules:
137-
- Core: Ledger.Core.md
138-
- Core/:
139-
- Specification: Ledger.Core.Specification.md
140-
- Specification/:
141-
- Address: Ledger.Core.Specification.Address.md
142-
- Crypto: Ledger.Core.Specification.Crypto.md
143-
- Epoch: Ledger.Core.Specification.Epoch.md
144-
- Misc Modules:
142+
- Era-independent Modules:
145143
- Prelude: Prelude.md
146144
- Ledger: Ledger.md
145+
- Ledger.Core: Ledger.Core.md
147146
- Ledger.Prelude: Ledger.Prelude.md
148147
- Ledger.Prelude/:
149148
- Base: Ledger.Prelude.Base.md
@@ -156,6 +155,16 @@
156155
- Numeric/:
157156
- PositiveNat: Ledger.Prelude.Numeric.PositiveNat.md
158157
- UnitInterval: Ledger.Prelude.Numeric.UnitInterval.md
158+
- Interface:
159+
- STS: Interface.STS.md
160+
- ComputationalRelation: Interface.ComputationalRelation.md
161+
- TypeClasses: Interface.TypeClasses.Hashable.md
162+
- TypeClasses/:
163+
- Hashable: Interface.TypeClasses.Hashable.md
164+
- HasSubset: Interface.TypeClasses.HasSubset.md
165+
- HasSubtract: Interface.TypeClasses.HasSubtract.md
166+
- HasSubtract/:
167+
- Instance: Interface.TypeClasses.HasSubtract.Instances.md
159168
- Foreign:
160169
- Convertible: Foreign.Convertible.md
161170
- Convertible/:
@@ -165,6 +174,7 @@
165174
- HaskellTypes/:
166175
- Deriving: Foreign.HaskellTypes.Deriving.md
167176
- MyDebugOptions: MyDebugOptions.md
177+
- Era-dependent Modules:
168178
- Dijkstra:
169179
- Ledger.Dijkstra: Ledger.Dijkstra.md
170180
- PreConway:
@@ -241,12 +251,3 @@
241251
- Utxow: Ledger.Conway.Conformance.Utxow.md
242252
- Utxow/:
243253
- Properties: Ledger.Conway.Conformance.Utxow.Properties.md
244-
- Type Classes/:
245-
- Interface:
246-
- ComputationalRelation: Interface.ComputationalRelation.md
247-
- HasSubset: Interface.HasSubset.md
248-
- HasSubtract: Interface.HasSubtract.md
249-
- HasSubtract/:
250-
- Instance: Interface.HasSubtract.Instances.md
251-
- Hashable: Interface.Hashable.md
252-
- STS: Interface.STS.md

‎src/Interface/TypeClasses.lagda.md‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
---
2+
source_branch: master
3+
source_path: src/Interface/TypeClasses.lagda.md
4+
---
5+
6+
# Type Classes
7+
8+
<!--
9+
```agda
10+
{-# OPTIONS --safe #-}
11+
12+
module Interface.TypeClasses where
13+
14+
import Interface.TypeClasses.HasSubtract
15+
import Interface.TypeClasses.HasSubset
16+
import Interface.TypeClasses.Hashable
17+
```

‎src/Interface/HasSubset.lagda.md‎ renamed to ‎src/Interface/TypeClasses/HasSubset.lagda.md‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,26 @@
11
---
22
source_branch: master
3-
source_path: src/Interface/HasSubset.lagda.md
3+
source_path: src/Interface/TypeClasses/HasSubset.lagda.md
44
---
55

6+
<!--
67
```agda
78
{-# OPTIONS --safe #-}
89
9-
module Interface.HasSubset where
10+
module Interface.TypeClasses.HasSubset where
1011
1112
open import Level using (Level; suc)
13+
```
14+
-->
1215

16+
```agda
1317
record HasSubset {a} (A : Set a) : Set (suc a) where
1418
field _⊆_ : A → A → Set a
1519
infix 4 _⊆_
20+
```
1621

22+
<!--
23+
```agda
1724
open HasSubset ⦃...⦄ public
1825
```
26+
-->

‎src/Interface/HasSubtract.lagda.md‎ renamed to ‎src/Interface/TypeClasses/HasSubtract.lagda.md‎

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,24 @@
11
---
22
source_branch: master
3-
source_path: src/Interface/HasSubtract.lagda.md
3+
source_path: src/Interface/TypeClasses/HasSubtract.lagda.md
44
---
55

6+
<!--
67
```agda
78
{-# OPTIONS --safe --cubical-compatible #-}
8-
module Interface.HasSubtract where
9+
module Interface.TypeClasses.HasSubtract where
910
1011
open import Agda.Primitive using () renaming (Set to Type)
12+
```
13+
-->
1114

15+
```agda
1216
record HasSubtract (A B : Type) : Type where
1317
infixl 6 _-_
1418
field _-_ : A → A → B
19+
```
1520

21+
<!--
22+
```agda
1623
open HasSubtract ⦃ ... ⦄ public
1724
```

‎src/Interface/HasSubtract/Instances.lagda.md‎ renamed to ‎src/Interface/TypeClasses/HasSubtract/Instances.lagda.md‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,22 @@
11
---
22
source_branch: master
3-
source_path: src/Interface/HasSubtract/Instances.lagda.md
3+
source_path: src/Interface/TypeClasses/HasSubtract/Instances.lagda.md
44
---
55

6+
<!--
67
```agda
78
{-# OPTIONS --safe #-}
89
9-
module Interface.HasSubtract.Instances where
10+
module Interface.TypeClasses.HasSubtract.Instances where
1011
11-
open import Interface.HasSubtract
12+
open import Interface.TypeClasses.HasSubtract
1213
1314
open import Data.Integer as ℤ using (ℤ)
1415
open import Data.Nat as ℕ using (ℕ)
16+
```
17+
-->
1518

19+
```agda
1620
instance
1721
HasSubtract-ℕ : HasSubtract ℕ ℕ
1822
HasSubtract-ℕ ._-_ = ℕ._∸_

‎src/Interface/Hashable.lagda.md‎ renamed to ‎src/Interface/TypeClasses/Hashable.lagda.md‎

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,30 @@
11
---
22
source_branch: master
3-
source_path: src/Interface/Hashable.lagda.md
3+
source_path: src/Interface/TypeClasses/Hashable.lagda.md
44
---
55

6+
<!--
67
```agda
78
{-# OPTIONS --safe #-}
8-
module Interface.Hashable where
9+
module Interface.TypeClasses.Hashable where
910
1011
open import Agda.Builtin.Equality
1112
open import Agda.Primitive using () renaming (Set to Type)
13+
```
14+
-->
1215

16+
```agda
1317
record Hashable (T THash : Type) : Type where
1418
field hash : T → THash
19+
```
1520

21+
<!--
22+
```agda
1623
open Hashable ⦃...⦄ public
24+
```
25+
-->
1726

27+
```agda
1828
Hashable₁ : (Type → Type) → Type → Type₁
1929
Hashable₁ F THash = {A : Type} → ⦃ Hashable A THash ⦄ → Hashable (F A) THash
2030

‎src/Ledger/Core/Specification.lagda.md‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,38 @@ source_branch: master
33
source_path: src/Ledger/Core.Specification.lagda.md
44
---
55

6+
7+
The submodules collected here, under the `Ledger.Core.Specification`{.AgdaModule}
8+
module, define some of the core types of the ledger that remain unchanged across
9+
ledger eras.
10+
11+
<!--
612
```agda
713
module Ledger.Core.Specification where
14+
```
15+
-->
16+
17+
## Addresses
18+
19+
The `Address`{.AgdaModule} module defines credentials and various address types.
820

21+
```agda
922
import Ledger.Core.Specification.Address
23+
```
24+
25+
## Cryptography
26+
27+
The `Crypto`{.AgdaModule} module defines cryptographic primitives and structures.
28+
29+
```agda
1030
import Ledger.Core.Specification.Crypto
31+
```
32+
33+
34+
## Epoch
35+
36+
The `Epoch`{.AgdaModule} module defines epoch-related concepts and structures.
37+
38+
```agda
1139
import Ledger.Core.Specification.Epoch
1240
```

‎src/Ledger/Prelude.lagda.md‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -30,10 +30,10 @@ open import stdlib-classes.Class.HasCast public
3030
open import Class.HasOrder public
3131
open import Class.ToBool public
3232
open import Interface.ComputationalRelation public
33-
open import Interface.Hashable public
34-
open import Interface.HasSubset public
35-
open import Interface.HasSubtract public
36-
open import Interface.HasSubtract.Instances public
33+
open import Interface.TypeClasses.Hashable public
34+
open import Interface.TypeClasses.HasSubset public
35+
open import Interface.TypeClasses.HasSubtract public
36+
open import Interface.TypeClasses.HasSubtract.Instances public
3737
open import Ledger.Prelude.Instances public
3838
open import Ledger.Prelude.HasCoin public
3939
open import Tactic.Defaults public

‎src/Ledger/Prelude/Instances.lagda.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,8 @@ module Ledger.Prelude.Instances where
1111
open import Prelude
1212
open import Ledger.Prelude.Base
1313
open import Ledger.Prelude.HasCoin
14-
open import Interface.HasSubtract
15-
open import Interface.HasSubset
14+
open import Interface.TypeClasses.HasSubtract
15+
open import Interface.TypeClasses.HasSubset
1616
1717
open import abstract-set-theory.FiniteSetTheory
1818
renaming (_⊆_ to _⊆ˢ_)

0 commit comments

Comments
 (0)