[Logiweb] Metavariables in side conditions ?

Allan Hvam Petersen ahvam at diku.dk
Mon Jun 6 01:06:09 CEST 2005


Hi logiweb at diku.dk

I am trying to do something like this in a proof with the "peano 
axioms"-page:

line ell a because axiom prime a four at meta q indeed
   peano all peano w indeed peano w
     peano imply
   meta q
end line

But I get this error-message in the diagnose:
   "The verify operation requires the side condition to contain no 
metavariables."

Any ideas, or am I using A4' in a wrong way?

Allan Hvam Petersen


More information about the Logiweb mailing list