[Logiweb] More about "sub ... end sub"

[Klaus Ebbe Grue]

Hi Frederik,

> Putting quotes around the parameters didn't work...
>
> What did work was adding the words "apply check" to the test, like this:
>
> "[ math test sub object g equal object g
> is                     object d equal object d
> where object d is
>         object g  end sub apply check
> end test
> end math  ]"

Sorry. I didn't realise you used 'sub ... end sub' outside a proof.

All side conditions in proofs are applied to the value of the page symbol 
of the page. Most side conditions discard the value.

Some side conditions do use the value of the page symbol. As an example, a 
rule that says that all definitions are axioms needs the value of the page 
symbol to see what definitions are available. As an example, such a rule 
would allow to define e.g. f(x)=2*x+1 and then use f(x)=2*x+1 as an axiom.

When using side conditions in tests you are right that you need to apply 
them to the page symbol (or to e.g. T if you know that the side condition 
does not use the page symbol).

Cheers,
Klaus