final improvements

+ move EssentialAgda module outside Ledger module
+ add new macro for referencing official Agda docs
+ uncomment paragraph that may have been deleted accidentally;
  (remove it later if it was deleted on purpose)

CONTRIBUTING.md

@@ -114,7 +114,8 @@ niv update nixpkgs -v 21.11.337905.902d91def1e
 
 ## Setup without nix-shell
 
-- Install Agda version `2.7.0` (e.g. follow the instructions in <https://agda.readthedocs.io/en/latest/getting-started/installation.html#step-1-install-agda>).
+- Install Agda version `2.7.0` (e.g. follow the instructions in <https://agda.readthedocs.io/en/v2.7.0/getting-started/installation.html#step-1-install-agda>
+).
 - In a folder `LIB`, clone the dependencies
     + [agda-stdlib](https://github.com/agda/agda-stdlib)
     + [agda-stdlib-classes](https://github.com/agda/agda-stdlib-classes)

src/Ledger/EssentialAgda.lagda → src/EssentialAgda.lagda

@@ -3,12 +3,12 @@
 Here we describe some of the essential concepts and syntax of the Agda programming language and proof assistant.
 The goal is to provide some background for readers who are not already familiar with Agda, to help them
 understand the other sections of the specification.  For more details, the reader is
-encouraged to consult the official Agda documentation~(\cite{agda2024}).
+encouraged to consult the official \hrefAgdaDocs{}~(\cite{agda2024}).
 
 \begin{code}[hide]
 {-# OPTIONS --safe #-}
 
-module Ledger.EssentialAgda where
+module EssentialAgda where
 
 open import Prelude using (Type)
 open import Data.Nat
@@ -53,4 +53,4 @@ p24 = record p23 { snd = 4 }
 This results a new record, \AgdaFunction{p24}, which denotes the pair
 \AgdaInductiveConstructor{⦅}~\AgdaNumber{2}~\AgdaInductiveConstructor{,}~\AgdaNumber{4}~\AgdaInductiveConstructor{⦆}.
 \\[6pt]
-See also \url{https://agda.readthedocs.io/en/\AgdaVersion/language/record-types.html}.
+See also \hrefAgdaDocs[language/record-types.html][agda.readthedocs.io/record-types].

src/Ledger/Certs.lagda

@@ -189,10 +189,10 @@ private variable
 
 \subsection{Changes Introduced in Conway Era}
 
-% In the Conway era, support for pointer addresses, genesis delegations and MIR
-% certificates is removed (see~\cite{cip1694}).  In \DState, this means that the four
-% fields relating to those features are no longer present, and \DelegEnv contains none
-% of the fields it used to in the Shelley era~(\cite[Sec.~9.2]{shelley-ledger-spec}).
+In the Conway era, support for pointer addresses, genesis delegations and MIR
+certificates is removed (see~\cite{cip1694}).  In \DState, this means that the four
+fields relating to those features are no longer present, and \DelegEnv contains none
+of the fields it used to in the Shelley era~(\cite[Sec.~9.2]{shelley-ledger-spec}).
 
 \subsubsection{Delegation}
 

src/Ledger/PDF.lagda

@@ -56,7 +56,7 @@ open import Ledger.Chain
 
 open import Ledger.Properties
 
-open import Ledger.EssentialAgda
+open import EssentialAgda
 open import Ledger.PDF.ConwayBootstrapEnact
 open import Ledger.PDF.ConwayBootstrap
 \end{code}
@@ -95,7 +95,7 @@ open import Ledger.PDF.ConwayBootstrap
 
 \appendix
 
-\input{Ledger/EssentialAgda}
+\input{EssentialAgda}
 \input{Ledger/PDF/ConwayBootstrapEnact}
 \input{Ledger/PDF/ConwayBootstrap}
 

src/latex/preamble.tex

@@ -79,3 +79,13 @@
 \msg_new:nnn {agda-latex-macros} {invalid-cip}
   {CIP-#1 is not a known CIP. The hyperlink will not be created.}
 \ExplSyntaxOff
+
+\NewDocumentCommand{\hrefAgdaDocs}{O{} O{Agda documentation}}{%
+  \href{https://agda.readthedocs.io/en/\AgdaVersion/#1}{#2}%
+}
+% For a link to the main Agda documentation website, just use \hrefAgdaDocs{}.
+% For a link to a specific section of the Agda docs, use
+% \hrefAgdaDocs[URLsuffix]{Link text}.
+% For example, \hrefAgdaDocs[language/record-types.html][agda.readthedocs.io/record-types],
+% produces a link to url https://agda.readthedocs.io/en/\AgdaVersion/language/record-types.html
+% with link text "agda.readthedocs.io/record-types".