[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