IntersectMBO / IntersectMBO/formal-ledger-specifications

What to do with the module reference

Open
#775 0 comments 0 reactions 0 assignees View on GitHub
discussion documentation
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

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.