[MetaPRL Users] Term extraction problem

[Aleksey Nogin]

On 05.09.2006 11:43, Wojtek Moczydlowski wrote:

> 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
>       #

Hm, works for me:

----------------

# cd "/test_th/i"
Module: /test_th
/test/test_th/i : string
# refine lamAbs thenT axiomVar 1

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

BY lamAbs thenT axiomVar 1

() : unit
# term_of_extract []
⊢ lambda{t1; v1. v1} : term
# refine lamAbs

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

BY lamAbs

1. [#]
    ....main....
    t1 ⊢ t1
() : unit
# down 1

# # <#>
....main....
t1 ⊢ t1

BY <goal>

() : unit
# refine axiomVar 1

* * <*>
....main....
t1 ⊢ t1

BY axiomVar 1

() : unit
# term_of_extract []
⊢ lambda{t1; v1. v1} : term

-------------

The test_th files used here are attached to this message.

> 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?

MetaPRL intentionally "hides" hypothesis bindings that are not being 
used (or experience shows that this simplifies life much more often than 
it complicates it). You can use nameHypT to temporarily give it a name, 
but it has to be in the form "nameHypT ... thenT foo ..." where foo 
actually uses a name that nameHypT introduced.

-- 
Aleksey Nogin

Home Page: http://nogin.org/
E-Mail: nogin at cs.caltech.edu (office), aleksey at nogin.org (personal)
Office: Moore 04, tel: (626) 395-2200
-------------- next part --------------
THEORYNAME = test
THEORYDESCR = Test Theory

# Library files
MPFILES[] =
   test_th
-------------- next part --------------
extends Base_theory

open Basic_tactics

declare arrow{'t1; 't2}
declare lambda{'t; v.'m['v]}

prim axiomVar {| elim |} 'H :
    sequent { <H>; v : 't; <J['v]> >- 't } = 'v

prim lamAbs {| intro |} :
   ('m['v] : sequent { <H>; v : 't >- 't1}) -->
   sequent { <H> >- arrow{'t;'t1}} = lambda{'t; v.'m['v]}

interactive i 't1 :
   sequent { >- arrow {'t1;'t1}} 
-------------- next part --------------
extends Base_theory

open Basic_tactics

declare arrow{'t1; 't2}
declare lambda{'t; v.'m['v]}