Consider the following theorem and definition which do not correspond to each other:
val testThm = makeTHM("'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))") {
val i1 = have(P(x) ==> P(f(x)) |- P(x) ==> P(f(x))) by Restate;
}
show
val testdef = DEF (x) --> The(y, (y === x))(testThm)
We expect an error saying the provided theorem does not justify the definition. However, instead you get a complaint about free variables:
[info] running Exercise
Theorem testThm := 'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))
Definition of testdef at.(Exercise.scala:18) is invalid:
val testdef = DEF (x) --> The(y, (y === x))(testThm)
The definition is not allowed to contain schematic symbols or free variables.The symbols {VariableLabel(y)} are free in the expression 'y = 'x.
Consider the following theorem and definition which do not correspond to each other:
We expect an error saying the provided theorem does not justify the definition. However, instead you get a complaint about free variables: