There are a few rules that you should be aware of, but you needn’t worry too much about them because you will naturally tend to follow them anyway, as long as you are writing a Meson script that makes sense. If you do break any of these rules, you will be notified about it when you try to build your module.
If any of the terms in this section are unclear, you may wish to review the Proofscape Module Tutorial.
A deduction arrow may not have a subdeduction or a modal node at its head.
There can be at most one flow arrow leaving any single node, and at most one entering it.
Any given pair of nodes may be connected by at most one arrow, of any kind.
Every node that is a target of a deduction must lie at the head of at least one arrow in that deduction. In other words, a deduction must eventually deduce all the conclusions it claims to prove.
Tis a target of deduction
Tmay not lie at the tail of any arrow whose head lies in
D. This is in order to avoid breaking unidirectional flow. The problem and solution are discussed in Downward Flow.