Lifting terms

[ghost]

Should this code not work?

val foo
context
  let 'x'
  foo = 'x'

context
  val '‹f›:‹ty›' = foo

All I get is cannot lift term into context: 'x ↦ x'

[phlegmaticprogrammer]

The error message is somewhat misleading, I improved that. What it should say is "cannot AUTOMATICALLY lift term into context". This is what I tried to explain (somewhat cryptically) in my last post about cterms: when lifting cterms automatically, that is without explicitly calling lift, then the term itself may not change; if it does, automatic lifting fails. That is what is happening in above code. If you actually want the term to be lifted anyway, then you have to call lift explicitly.

The reason for this is because equality on cterms is defined as beta/eta/alpha-equality of the underlying terms after (automatically) lifting the terms into the current evaluation context. In the above the assertion

 assert lift(foo) <> foo 

will hold in the second context, and therefore automatic lifting fails.

[phlegmaticprogrammer]

Correction: lift(foo) <> foo should actually throw an error, because foo cannot automatically be lifted into the current context. The inequality would hold between the cterms, but you don't have access to that from ProofScript. Or rather, implicitly you do have access: try using lift(foo) and foo as keys in a map, then you will see that they are treated differently.