[Logiweb] Meta-variables in side conditions

[Klaus Ebbe Grue]

Hi Frederik,

> Suppose you have a lemma in which a meta-variable 'X' appears in a 
> side-condition, but not anywhere else in the lemma. When using the lemma, is 
> it necessary to tell the proof checker explicitly how to instantiate X? (I 
> know it was necessary last year, but things might have changed in the 
> meantime).

Last year, uninstantated meta-variables were reported as errors.

Now, uninstantiated meta-variables are left uninstantiated.

The change from the old to the new style allows to formulate the deduction
rule. That rule was impossible to formulate in the old style.

But the change from old to new style creates a new problem: Formerly, the 
implementation of side conditions could assume that they would never 
encounter a meta-variable. Now they must be prepared for that. And maybe 
some errors lurk in the code of some of the old side conditions, ready to 
strike if they see a meta-variable :-(

I cannot guarantee that I have managed to correct all places from the old 
to the new style, but try your proof without instantiating meta-variables. 
If you get a unification error or an error saying that the meta-variable 
is not instantiated, please e-mail me a reference to the page. Also e-mail 
me if a side-condition acts silly when applied to terms that contain 
meta-variables.

Cheers,
Klaus