About the explanation of the ⊸ ⊢ rule #3
Description
About the explanation of the ⊸ ⊢ rule
The ⊸ ⊢ rule can be simplified to say that if one transaction produces an A for free and another transaction produces nothing for B, then we can combine both transactions together with a third transaction that can produce a B from an A.
If "for free" and "nothing for" is used in the explanation,
isn't it is about the rule without context?
| Assumptions | Conclusion | Rule |
|---|---|---|
| ⊢ A | ⊸ ⊢ | |
| B ⊢ Λ | A ⊸ B ⊢ |
Which is only a special case of the rule with context:
| Assumptions | Conclusion | Rule |
|---|---|---|
| Γ ⊢ A, Δ | ⊸ ⊢ | |
| Θ, B ⊢ Λ | Γ, Θ, A ⊸ B ⊢ Δ, Λ |