From 52ebee195880f80aac7ed787c1a8c44e624e9dfc Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 2 Dec 2024 13:45:31 -0700 Subject: [PATCH 1/4] Document changes to BaseAddr This closes issue #617. --- src/Ledger/Address.lagda | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Ledger/Address.lagda b/src/Ledger/Address.lagda index db5b5e549..a9d458d2f 100644 --- a/src/Ledger/Address.lagda +++ b/src/Ledger/Address.lagda @@ -14,6 +14,14 @@ We define credentials and various types of addresses here. A credential contains a hash, either of a verifying (public) key (\isVKey) or of a (\isScript). +Note that, in the Shelley era, the type of the \AgdaField{stake} +field of the \AgdaRecord{BaseAddr} record was \AgdaType{Credential}; +to specify an address with no stake, we would use an "enterprise" address. +In contrast, in the Conway era, the type of \AgdaField{stake} is +\AgdaType{Maybe Credential}, so that we can specify an address with no +stake using the \AgdaRecord{BaseAddr} record with +\AgdaInductiveConstructor{nothing} in the stake field. + \begin{figure*}[h!] \begin{AgdaMultiCode} \emph{Abstract types} From 11374f23df8fd2b3f58730fce255f65cfbe2872d Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 2 Dec 2024 13:49:21 -0700 Subject: [PATCH 2/4] improvements --- src/Ledger/Address.lagda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Ledger/Address.lagda b/src/Ledger/Address.lagda index a9d458d2f..743b696c1 100644 --- a/src/Ledger/Address.lagda +++ b/src/Ledger/Address.lagda @@ -14,11 +14,11 @@ We define credentials and various types of addresses here. A credential contains a hash, either of a verifying (public) key (\isVKey) or of a (\isScript). -Note that, in the Shelley era, the type of the \AgdaField{stake} -field of the \AgdaRecord{BaseAddr} record was \AgdaType{Credential}; -to specify an address with no stake, we would use an "enterprise" address. -In contrast, in the Conway era, the type of \AgdaField{stake} is -\AgdaType{Maybe Credential}, so that we can specify an address with no +N.B. in the Shelley era the type of the \AgdaField{stake} field +of the \AgdaRecord{BaseAddr} record was \AgdaType{Credential}; +to specify an address with no stake, we would use an ``enterprise'' address. +In contrast, in the Conway era the type of \AgdaField{stake} is +\AgdaType{Maybe Credential}, so we can specify an address with no stake using the \AgdaRecord{BaseAddr} record with \AgdaInductiveConstructor{nothing} in the stake field. From 5c2236e9a8364845d8c2714372418c07920772dd Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Tue, 3 Dec 2024 07:49:27 -0700 Subject: [PATCH 3/4] fix typesetting of Agda tokens --- src/Ledger/Address.lagda | 13 ++++++------- src/latex/agda-latex-macros.sty | 4 ++++ 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/src/Ledger/Address.lagda b/src/Ledger/Address.lagda index 743b696c1..f5c46c8b9 100644 --- a/src/Ledger/Address.lagda +++ b/src/Ledger/Address.lagda @@ -14,13 +14,12 @@ We define credentials and various types of addresses here. A credential contains a hash, either of a verifying (public) key (\isVKey) or of a (\isScript). -N.B. in the Shelley era the type of the \AgdaField{stake} field -of the \AgdaRecord{BaseAddr} record was \AgdaType{Credential}; -to specify an address with no stake, we would use an ``enterprise'' address. -In contrast, in the Conway era the type of \AgdaField{stake} is -\AgdaType{Maybe Credential}, so we can specify an address with no -stake using the \AgdaRecord{BaseAddr} record with -\AgdaInductiveConstructor{nothing} in the stake field. +N.B.~in the Shelley era the type of the \stake field of the +\BaseAddr record was \CredentialType; to specify an address with +no stake, we would use an ``enterprise'' address. In contrast, +the type of \stake in the Conway era is \Maybe~\CredentialType, +so we can now use \BaseAddr to specify an address with no stake +by setting \stake to \nothing. \begin{figure*}[h!] \begin{AgdaMultiCode} diff --git a/src/latex/agda-latex-macros.sty b/src/latex/agda-latex-macros.sty index cbe4c524e..aacc49f07 100644 --- a/src/latex/agda-latex-macros.sty +++ b/src/latex/agda-latex-macros.sty @@ -160,6 +160,8 @@ \newcommand{\Anchor}{\AgdaRecord{Anchor}\xspace} \newcommand{\as}{\AgdaSymbol{as}\xspace} + +\newcommand{\BaseAddr}{\AgdaRecord{BaseAddr}\xspace} \newcommand{\beginstrict}{\AgdaFunction{begin-strict}\xspace} \newcommand{\Bool}{\AgdaDatatype{Bool}\xspace} @@ -169,6 +171,7 @@ \newcommand{\Coin}{\AgdaFunction{Coin}\xspace} \newcommand{\Computational}{\AgdaRecord{Computational}\xspace} \newcommand{\Credential}{\AgdaFunction{Credential}\xspace} +\newcommand{\CredentialType}{\AgdaDataType{Credential}\xspace} \newcommand{\Crypto}{\AgdaRecord{Crypto}\xspace} \newcommand{\canVote}{\AgdaFunction{canVote}\xspace} \newcommand{\case}{\AgdaFunction{case}\xspace} @@ -463,6 +466,7 @@ \newcommand{\specProperty}{\AgdaFunction{specProperty}\xspace} \newcommand{\sprime}{\AgdaGeneralizable{s'}\xspace} \newcommand{\spring}{\AgdaFunction{sp-∘}\xspace} +\newcommand{\stake}{\AgdaField{stake}\xspace} \newcommand{\stakeDistrs}{\AgdaField{stakeDistrs}\xspace} \newcommand{\stakeDistr}{\AgdaField{stakeDistr}\xspace} \newcommand{\subst}{\AgdaFunction{subst}\xspace} From 88c5df0a24f85fdd6692bdca6646ff9170ae79ec Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Tue, 3 Dec 2024 12:35:04 -0700 Subject: [PATCH 4/4] bugfix --- src/latex/agda-latex-macros.sty | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/latex/agda-latex-macros.sty b/src/latex/agda-latex-macros.sty index aacc49f07..067aa940a 100644 --- a/src/latex/agda-latex-macros.sty +++ b/src/latex/agda-latex-macros.sty @@ -171,7 +171,7 @@ \newcommand{\Coin}{\AgdaFunction{Coin}\xspace} \newcommand{\Computational}{\AgdaRecord{Computational}\xspace} \newcommand{\Credential}{\AgdaFunction{Credential}\xspace} -\newcommand{\CredentialType}{\AgdaDataType{Credential}\xspace} +\newcommand{\CredentialType}{\AgdaDatatype{Credential}\xspace} \newcommand{\Crypto}{\AgdaRecord{Crypto}\xspace} \newcommand{\canVote}{\AgdaFunction{canVote}\xspace} \newcommand{\case}{\AgdaFunction{case}\xspace}