[POPLmark] Twelf question

[Karl Crary]

You need to add another variable to rblock with the type "assm_var d v", 
as we did in our solution.

Keep in mind that the %total directive is checking the totality of a 
relation; it is not (directly) checking the existence of an output.  
When proof search encounters a goal of the form "assm_var d X", it gets 
stuck because it doesn't have any rules would allow it to derive that 
goal.  It's not good enough that the desired output is around; you need 
also to have a rule that will return that output.  You arrange that by 
adding the rule at the same time as you add the assm assumption.

    -- Karl


Randy Pollack wrote:

>Consider the following Twelf script:
>
>   tp : type.  %name tp T.
>   top	: tp.
>
>   assm : tp -> tp -> type.
>   var  : tp -> type.
>
>   %block rblock : some {t:tp}
>		   block {x:tp} {d: assm x t} {v:var x}.
>
>   assm_var : assm T _ -> var T -> type.
>   %mode assm_var +X1 -X2.
>   %worlds (rblock) (assm_var _ _).
>   %total {} (assm_var _ _).
>
>Twelf gives an error message:
>
>   Coverage error --- missing cases:
>   {T1:tp} {#rblock:{x:tp} {d:assm x T1} {v:var x}} {X1:var #rblock_x}
>      |- assm_var #rblock_d X1.
>
>I guess it means `since you allow a block containing "assm x T1" you
>are required to produce a proof of "var x"'.  How can I express that I
>want Twelf to use the proof "var x" from the same block?
>
>  
>