token algebras are era independent

Author: williamdemeo

src/Ledger/Conway/Foreign/HSLedger/Core.agda

@@ -103,5 +103,5 @@ module Implementation where
   AuxiliaryData   = ℕ
   DocHash         = ℕ
   tokenAlgebra    = Coin-TokenAlgebra
-    where open import Ledger.Conway.Specification.TokenAlgebra.Coin ScriptHash
+    where open import Ledger.Core.Specification.TokenAlgebra.Coin ScriptHash
             using (Coin-TokenAlgebra)

src/Ledger/Conway/Specification.lagda.md

@@ -134,10 +134,10 @@ import Ledger.Conway.Specification.Test.StructuredContracts
 ## Token Algebras
 
 ```agda
-import Ledger.Conway.Specification.TokenAlgebra.Base
-import Ledger.Conway.Specification.TokenAlgebra.Coin
-import Ledger.Conway.Specification.TokenAlgebra.ValueSet
-import Ledger.Conway.Specification.TokenAlgebra.ValueVector
+import Ledger.Core.Specification.TokenAlgebra.Base
+import Ledger.Core.Specification.TokenAlgebra.Coin
+import Ledger.Core.Specification.TokenAlgebra.ValueSet
+import Ledger.Core.Specification.TokenAlgebra.ValueVector
 ```
 
 ## Transactions

src/Ledger/Conway/Specification/Test/LedgerImplementation.lagda.md

@@ -83,7 +83,7 @@ module Implementation where
   AuxiliaryData   = ℕ
   DocHash         = ℕ
   tokenAlgebra    = Coin-TokenAlgebra
-    where open import Ledger.Conway.Specification.TokenAlgebra.Coin ScriptHash
+    where open import Ledger.Core.Specification.TokenAlgebra.Coin ScriptHash
             using (Coin-TokenAlgebra)
 
 

src/Ledger/Conway/Specification/Test/StructuredContracts.lagda.md

@@ -15,8 +15,8 @@ open import Data.Nat.Properties using (+-0-monoid)
 open import Ledger.Prelude; open Equivalence
 open import Ledger.Conway.Specification.Transaction
 open import Ledger.Conway.Specification.Abstract
-open import Ledger.Conway.Specification.TokenAlgebra.Base
-open import Ledger.Conway.Specification.TokenAlgebra.ValueSet
+open import Ledger.Core.Specification.TokenAlgebra.Base
+open import Ledger.Core.Specification.TokenAlgebra.ValueSet
 
 module Ledger.Conway.Specification.Test.StructuredContracts
   (txs : _) (open TransactionStructure txs)

src/Ledger/Conway/Specification/Transaction.lagda.md

@@ -27,7 +27,7 @@ import Ledger.Conway.Specification.PParams
 import Ledger.Conway.Specification.Script.Base
 import Ledger.Conway.Specification.Gov.Actions
 import Ledger.Conway.Specification.Certs
-import Ledger.Conway.Specification.TokenAlgebra.Base
+import Ledger.Core.Specification.TokenAlgebra.Base
 import Ledger.Core.Specification.Address
 
 open import Relation.Nullary.Decidable using (⌊_⌋)
@@ -88,7 +88,7 @@ record TransactionStructure : Type₁ where
 
   field cryptoStructure : _
   open CryptoStructure cryptoStructure public
-  open Ledger.Conway.Specification.TokenAlgebra.Base ScriptHash public
+  open Ledger.Core.Specification.TokenAlgebra.Base ScriptHash public
   open Ledger.Core.Specification.Address Network KeyHash ScriptHash ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ public
 
   field epochStructure : _

src/Ledger/Conway/Specification/Utxo.lagda.md

@@ -137,7 +137,7 @@ instance
 ```
 -->
 
- *UTxO transitions*
+*UTxO transitions*
 
 ```agda
 data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type

src/Ledger/Core/Specification/TokenAlgebra/Base.lagda.md

@@ -1,6 +1,6 @@
 ---
 source_branch: master
-source_path: src/Ledger/Conway/Specification/TokenAlgebra/Base.lagda
+source_path: src/Ledger/Core/Specification/TokenAlgebra/Base.lagda
 ---
 
 # Token Algebras {#sec:token-algebra}
@@ -11,7 +11,7 @@ Token algebras are used for multiple assets.
 ```agda
 {-# OPTIONS --safe #-}
 open import Prelude using (Type)
-module Ledger.Conway.Specification.TokenAlgebra.Base (
+module Ledger.Core.Specification.TokenAlgebra.Base (
 ```
 -->
  *Abstract types*

src/Ledger/Core/Specification/TokenAlgebra/Coin.lagda.md

@@ -1,18 +1,18 @@
 ---
 source_branch: master
-source_path: src/Ledger/Conway/Specification/TokenAlgebra/Coin.lagda.md
+source_path: src/Ledger/Core/Specification/TokenAlgebra/Coin.lagda.md
 ---
 
 ```agda
 {-# OPTIONS --safe #-}
 open import Ledger.Prelude
 
-module Ledger.Conway.Specification.TokenAlgebra.Coin (X : Type) where
+module Ledger.Core.Specification.TokenAlgebra.Coin (X : Type) where
 
 open import Algebra.Morphism.Construct.Identity
   using (isMonoidHomomorphism)
 
-open import Ledger.Conway.Specification.TokenAlgebra.Base X
+open import Ledger.Core.Specification.TokenAlgebra.Base X
 
 open TokenAlgebra
 

src/Ledger/Core/Specification/TokenAlgebra/ValueSet.lagda.md

@@ -1,6 +1,6 @@
 ---
 source_branch: master
-source_path: src/Ledger/Conway/Specification/TokenAlgebra/ValueSet.lagda.md
+source_path: src/Ledger/Core/Specification/TokenAlgebra/ValueSet.lagda.md
 ---
 
 ## Value Set {#sec:value-set}
@@ -12,11 +12,11 @@ source_path: src/Ledger/Conway/Specification/TokenAlgebra/ValueSet.lagda.md
 
 open import Prelude using (Type)
 
-module Ledger.Conway.Specification.TokenAlgebra.ValueSet (PolicyId AssetName : Type) where
+module Ledger.Core.Specification.TokenAlgebra.ValueSet (PolicyId AssetName : Type) where
 
 open import Ledger.Prelude                         hiding (lookup ; update ; isMagma ; isEquivalence) renaming (TotalMap to _⇒_)
 open _⇒_
-open import Ledger.Conway.Specification.TokenAlgebra.Base PolicyId using (TokenAlgebra)
+open import Ledger.Core.Specification.TokenAlgebra.Base PolicyId using (TokenAlgebra)
 
 open import Algebra                                using (Op₂ ; IsSemigroup ; IsMonoid ; IsMagma ; IsCommutativeMonoid)
 open import Algebra.Morphism                       using (IsMonoidHomomorphism ; IsMagmaHomomorphism)

src/Ledger/Core/Specification/TokenAlgebra/ValueVector.lagda.md

@@ -1,13 +1,13 @@
 ---
 source_branch: master
-source_path: src/Ledger/Conway/Specification/TokenAlgebra/ValueVector.lagda.md
+source_path: src/Ledger/Core/Specification/TokenAlgebra/ValueVector.lagda.md
 ---
 
 ```agda
 {-# OPTIONS --safe #-}
 open import Ledger.Prelude hiding (_∙_; ε)
 
-module Ledger.Conway.Specification.TokenAlgebra.ValueVector (PolicyId : Type) (n : ℕ) where
+module Ledger.Core.Specification.TokenAlgebra.ValueVector (PolicyId : Type) (n : ℕ) where
 
 import Algebra as Alg
 open import Algebra.Construct.DirectProduct
@@ -19,7 +19,7 @@ open import Data.Vec as Vec
 import stdlib.Data.Vec.Instances as Vec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Vec
 
-open import Ledger.Conway.Specification.TokenAlgebra.Base PolicyId
+open import Ledger.Core.Specification.TokenAlgebra.Base PolicyId
 
 Quantity = ℕ