{ error printing } : Theorem when abusing (?) context objects?

[ghost]

In the following code, Proofscript seems to think that x is some sort of theorem.

theory Bugs
extends root

val [ctx,x,bod]  = destabs 'x ↦ x'
val [ctx2,y,bod] = destabs 'y ↦ y'
context <ctx>
  context <ctx2>
    show x
    show y

[ghost]

Is the output expected?

** show (\Bugs:8): {error printing} : Theorem
** show (\Bugs:9): 'y'

[phlegmaticprogrammer]

Let me check that, it is fine that there is an error when printing x, because x is not defined in context ctx2. But what is strange is that it reports x to be a theorem.

[phlegmaticprogrammer]

By the way, in case it is not clear. Your example above is equivalent to:

val [ctx,x,bod]  = destabs 'x ↦ x'
val [ctx2,y,bod] = destabs 'y ↦ y'
context <ctx2>
  show x
  show y

[ghost]

I shall meditate on this further. :)

On 18/09/14 20:17, Steven Obua wrote:

By the way, in case it is not clear. Your example above is equivalent to:

val [ctx,x,bod] = destabs 'x ↦ x' val [ctx2,y,bod] = destabs 'y ↦ y' context show x show y

— Reply to this email directly or view it on GitHub https://github.com/proofpeer/proofpeer-proofscript/issues/34#issuecomment-56088174.

[phlegmaticprogrammer]

Or ... let's discuss it over a beer :-)

I've fixed the wrong error message: 8b9bbe376cb05dfaca7b7b31e1550982bd7cdb15