Skip to content

Commit eed4250

Browse files
docs: add ToCs + clear obsolete SPDX-normalization follow-up note (#151)
## Summary Three small docs follow-ups bundled into one PR: - **`README.md`** — adds a manual markdown Contents section after the badges block, mirroring the Axiom.jl-style top-of-file ToC pattern - **`readme.adoc`** — adds `:toc:` + `:toclevels: 2` macros - **`EXPLAINME.adoc`** — adds `:toc:` + `:toclevels: 2` macros (was missing — the other audience-facing `.adoc` files already had `:toc:`) - **`README.md`** + **`readme.adoc`** — drop the "current practical follow-up" licensing bullet (the SPDX-header normalization it referenced just landed in #150, so the line is now obsolete) and tighten the remaining bullets from "intended to be licensed" → "licensed" `QUICKSTART-DEV.adoc` / `QUICKSTART-MAINTAINER.adoc` / `QUICKSTART-USER.adoc` / `INDEX.adoc` / `TOPOLOGY.adoc` already carry `:toc:` so are unchanged. ## Test plan - [ ] CI passes - [ ] `README.md` Contents links resolve correctly on GitHub - [ ] `readme.adoc` + `EXPLAINME.adoc` ToCs render in any AsciiDoc viewer 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 7eb621e commit eed4250

3 files changed

Lines changed: 29 additions & 6 deletions

File tree

EXPLAINME.adoc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
// SPDX-License-Identifier: CC-BY-4.0
22
= echo-types: explain me
33
:icons: font
4+
:toc:
5+
:toclevels: 2
46

57
== One paragraph
68

README.md

Lines changed: 23 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,27 @@ Constructive Agda development for echo types as a first-class notion of structur
1515

1616
loss that is not total erasure.
1717

18+
## Contents
19+
20+
- [Where things are](#️-where-things-are)
21+
- [Structural overview](#-structural-overview)
22+
- [Recommended reading order](#-recommended-reading-order)
23+
- [Core Idea](#core-idea)
24+
- [Definition (Foundation)](#definition-foundation)
25+
- [Canonical identity layer (2026-05-27)](#canonical-identity-layer-2026-05-27)
26+
- [Current Status Snapshot](#current-status-snapshot)
27+
- [Echo Core (load-bearing for the identity claim)](#echo-core-load-bearing-for-the-identity-claim)
28+
- [Ordinal / Buchholz (parallel-independent, experimental)](#ordinal--buchholz-parallel-independent-experimental)
29+
- [External Bridge Targets (local workspace)](#external-bridge-targets-local-workspace)
30+
- [What Echo Types Are For](#what-echo-types-are-for)
31+
- [Identity Claim and Falsifiability](#identity-claim-and-falsifiability)
32+
- [Build](#build)
33+
- [Installing as a library](#installing-as-a-library)
34+
- [Citation](#citation)
35+
- [Tooling Stance](#tooling-stance)
36+
- [Roadmap](#roadmap)
37+
- [Licensing](#licensing)
38+
1839
## 🗺️ Where things are
1940

2041
**New here, or can't find something? Start with the
@@ -446,6 +467,5 @@ into `roadmap.adoc` and removed.
446467

447468
## Licensing
448469

449-
- code, proofs, and tooling in this repository are intended to be licensed under `MPL-2.0`; see [LICENSE](LICENSE)
450-
- prose documentation in `docs/`, `README.md`, `readme.adoc`, and roadmap files is intended to be licensed under `CC-BY-4.0`; see [LICENSE-docs](LICENSE-docs)
451-
- current practical follow-up: normalize per-file SPDX headers across source files so file-level notices match the top-level licensing intent
470+
- code, proofs, and tooling in this repository are licensed under `MPL-2.0`; see [LICENSE](LICENSE)
471+
- prose documentation in `docs/`, `README.md`, `readme.adoc`, and roadmap files is licensed under `CC-BY-4.0`; see [LICENSE-docs](LICENSE-docs)

readme.adoc

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
// SPDX-License-Identifier: CC-BY-4.0
22
// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
33
= echo-types
4+
:toc:
5+
:toclevels: 2
46

57
image::docs/assets/banner.png[Echo Types — Proof-Relevant Information Residues,align="center"]
68

@@ -284,6 +286,5 @@ Open/gated work and cross-repo follow-ups are tracked in:
284286

285287
== Licensing
286288

287-
* code, proofs, and tooling in this repository are intended to be licensed under `MPL-2.0`; see `LICENSE`
288-
* prose documentation in `docs/`, `README.md`, `readme.adoc`, and roadmap files is intended to be licensed under `CC-BY-4.0`; see `LICENSE-docs`
289-
* practical follow-up: normalize per-file SPDX headers across source files so file-level notices match the top-level licensing intent
289+
* code, proofs, and tooling in this repository are licensed under `MPL-2.0`; see `LICENSE`
290+
* prose documentation in `docs/`, `README.md`, `readme.adoc`, and roadmap files is licensed under `CC-BY-4.0`; see `LICENSE-docs`

0 commit comments

Comments
 (0)