[Logiweb] Re: sub * is * where * is * end sub

[Frederik Eriksen]

Klaus Ebbe Grue wrote:

> The "sub ... end sub" is value defined (not macro defined). So 
> evaluation of "sub ... end sub" leads to evaluation of the parameters.
>
> "object g" has no value definition, so it evaluates to T by default.
> "object g equal object g" also evaluates to T. T is not a parse tree, 
> so "sub ... end sub" complains (i.e. returns F).
>
> Solution: put "quote ... end quote" around the parameters: "[ math 
> test sub quote object g equal object g end quote is quote ... ]".
>
> Cheers,
> Klaus
>
Hello once more,

OK, I understand the need for quoting the parameters. But why don't you 
need quotes when using 'sub * is * where * is * end sub' in side 
conditions? I'm thinking about the following definition of the principle 
of mathematical induction (from the "check" page):

"[ math in theory system s rule axiom s nine says for all terms meta x 
comma meta a comma meta b comma meta c indeed
sub meta b is meta a where meta x is zero end sub endorse
sub meta c is meta a where meta x is meta x suc end sub endorse
 meta b infer
 meta a imply meta c infer
 meta a end rule end math ]"

Best Regards
Frederik.