Typo and informal notation in Babbage spec pdf

[williamdemeo]

In the babbage-ledger.pdf formal spec document, txscripts is defined as follows:

txscripts : Tx → UTxO → ScriptHash →∗ Script
txscripts tx utxo = txwitscripts tx ∪ refScripts tx utxo

Thus txscripts tx utxo has type ScriptHash →∗ Script, which is essentially a collection of (hash, script) pairs, so the expression

s ∈ range(txscripts tx utxo )

is well typed, but the expression

 s ∈ txscripts tx utxo

in Fig 2 is ill-typed, so must be a typo.

Also, in Fig 6, in the expression,

∀s ∈ (txscripts txw utxo neededHashes ) ∩ Scriptᵖʰ¹

an informal shorthand is used to apply a function txscripts txw utxo to a collection neededHashes of elements in its domain. One way to express this more formally would be as as follows:

∀s ∈ map proj₂ ((txscripts txw utxo) ∩ (neededHashes × Scriptᵖʰ¹))

[facundominguez]

∀s ∈ map proj₂ ((txscripts txw utxo) ∩ (neededHashes × Scriptᵖʰ¹))

Another attempt. After a few corrections it doesn't look particularly better anymore to me :)

∀s ∈ range ((neededHashes ◃ txscripts txw utxo) ▹ Scriptᵖʰ¹)