Skip to content

Commit d480c57

Browse files
committed
remove duplicates
1 parent b655c74 commit d480c57

File tree

1 file changed

+0
-20
lines changed

1 file changed

+0
-20
lines changed

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

Lines changed: 0 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -291,14 +291,6 @@ could be either of them.
291291
field TxIdOf : A → TxId
292292
open HasTxId ⦃...⦄ public
293293
294-
record HasSpendInputs {a} (A : Type a) : Type a where
295-
field SpendInputsOf : A → ℙ TxIn
296-
open HasSpendInputs ⦃...⦄ public
297-
298-
record HasReferenceInputs {a} (A : Type a) : Type a where
299-
field ReferenceInputsOf : A → ℙ TxIn
300-
open HasReferenceInputs ⦃...⦄ public
301-
302294
record HasFees? {a} (A : Type a) : Type a where
303295
field FeesOf? : A → Maybe Fees
304296
open HasFees? ⦃...⦄ public
@@ -392,18 +384,6 @@ could be either of them.
392384
HasSubTransactions-TopLevelTx : HasSubTransactions TopLevelTx
393385
HasSubTransactions-TopLevelTx .SubTransactionsOf = TxBody.txSubTransactions ∘ TxBodyOf
394386
395-
HasSpendInputs-TxBody : HasSpendInputs (TxBody txLevel)
396-
HasSpendInputs-TxBody .SpendInputsOf = TxBody.txIns
397-
398-
HasSpendInputs-Tx : HasSpendInputs (Tx txLevel)
399-
HasSpendInputs-Tx .SpendInputsOf = SpendInputsOf ∘ TxBodyOf
400-
401-
HasReferenceInputs-TxBody : HasReferenceInputs (TxBody txLevel)
402-
HasReferenceInputs-TxBody .ReferenceInputsOf = TxBody.refInputs
403-
404-
HasReferenceInputs-Tx : HasReferenceInputs (Tx txLevel)
405-
HasReferenceInputs-Tx .ReferenceInputsOf = ReferenceInputsOf ∘ TxBodyOf
406-
407387
HasTxId-Tx : HasTxId (Tx txLevel)
408388
HasTxId-Tx .TxIdOf = TxBody.txId ∘ TxBodyOf
409389

0 commit comments

Comments
 (0)