[POPLmark] [Provers] Re: Adequacy for LF

[Karl Crary]

>OK, I think I see how this would work, but how can one ensure that
>"enough" assumptions of the form 
>
>f:fvs (var v) (vcons v vnil)
>
>are in the context (without looking at the term yourself and adding
>them)?  Doesn't that require figuring out what the free variables of the
>term are (so we're back where we started)?  Would we have to make sure
>that we add f:fvs (var v) (vcons v vnil) to the context whenever we
>proceed inside a binder elsewhere in the program that might call fvs?
>Or is this what your last comment about distinguishing variables and
>terms by an assumption would address?
>  
>

That's right, whenever you enter a binder, you add a collection of 
assumptions.  This would be one of them.

    -- Karl