IntersectMBO / IntersectMBO/formal-ledger-specifications
What to do with the module reference
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
The question is what to do with the `\modulenote` macro. At the moment it produces a sentence that starts the section. This has the downside that it's a bit odd to start every section with an identical sentence.
I feel like it would be better to instead have it more looking like a subtitle to the section or something. It doesn't need to be a sentence, it could be as simple as
# Transactions ([Source](https://github.com/IntersectMBO/formal-ledger-specifications/blob/master/src/Ledger/Transaction.lagda))
or
# Transactions
- [Source](https://github.com/IntersectMBO/formal-ledger-specifications/blob/master/src/Ledger/Transaction.lagda)
One issue if we go with the first option is that we probably want to exclude that source link from the TOC. Is that reasonably doable?
Do we have other options or opinions?
_Originally posted by @WhatisRT in https://github.com/IntersectMBO/formal-ledger-specifications/pull/765#discussion_r2063441950_
Contributor guide
Assessment
This issue has not been assessed yet.