[MetaPRL Users] Term extraction problem

[Aleksey Nogin]

On 05.09.2006 11:08, Wojtek Moczydlowski wrote:

>   Thanks for the answer to the previous email. Here's even simpler 
> question.
> The relevant fragment of my theory file are:
> 
> 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}}
> 
> So I'm trying to prove t1 -> t1. Obviously I start by applying lamAbs, and
> then I want to apply axiomVar. However, no matter what number I try to use
> it with, it doesn't work:
> 
> # ls ""
> 
> # <*>
> ....main....
> . arrow{t1; t1}
> 
> BY lamAbs
> 
> 1. [#]
>    ....main....
>       t1 . t1
>       () : unit
> # refine axiomVar 0

Remember that by default "refine" updates whatever level ("rulebox") you 
are currently on. You need to either:
- use "refine lamAbs thenT axiomVar 1" to update the current rulebox to 
contain the combined step, or
- use "down 1" (or click on the subgoal number "1") to navigate to the 
subgoal before applying the axiomVar there.

P.S. Alternatively, just use "refine autoT" to have things happen 
automatically.

P.P.S. The "{| elim |} annotation on the axiomVar rule is suboptimal as 
the rule is not really an elimination one. A better annotation would be 
"{| nth_hyp |}" - this annotation says "this rule is used to match the 
conclusion against one of the hypotheses.