[MetaPRL Users] Term extraction problem

[Wojtek Moczydlowski]

On Tue, 5 Sep 2006, Aleksey Nogin wrote:

> On 05.09.2006 11:26, Wojtek Moczydlowski wrote:
>
>> Right, now it works. So back to my original problem, what's the correct way
>> of extracting lambda x.x out of this proof, if term_of_extract is a hack?
>
> Well, term_of_extract is not a hack, it's just a low-level function that 
> requires some knowledge in order to use properly for derived rules with 
> assumptions. In examples like yours, where the rule does not have any 
> assumptions, simple "term_of_extract []" should be good enough (as long as 
> you do not mind some variables being named "" - an empty string ;-) ).

Well, I still get the same message, so seems it's not good enough even in
this example:

# ls ""

* <*>
....main....
. arrow{t1; t1}

BY lamAbs

1. [*]
    ....main....
       t1 . t1
       () : unit
       # term_of_extract []
       Incomplete proof: /wojtek/i
       #

By the way, speaking of variables named "", is there a way to specify these
rules so that lamAbs also takes as an argument the name of the variable to
introduce to the context?

Thanks,

Wojtek