[POPLmark] Re: [Provers] Re: adequacy

[Karl Crary]

Well, a look at the Twelf web page suggests that you are right; it lists 
uniqueness checking as a new undocumented feature.  Of course, as an 
undocumented feature, you shouldn't really be expecting to find it in 
the canonical documentation.

In any case, we didn't use it in our Poplmark solution.  It looks cool, 
but I haven't learned to use it yet.

    -- Karl


Geoffrey A. Washburn wrote:

>On Thu, 5 May 2005, Karl Crary wrote:
>
>  
>
>>Uniqueness checking is not currently part of Twelf,
>>    
>>
>
>	The web page seems to says it is.  I seem recall reading something
>  recently about it now being integrated with coverage checking.  I've
>  personally experimented with it myself.
>
>  
>
>>and has nothing that I know of to do with the current discussion.
>>    
>>
>
>	Uniqueness an example of just one of the meta-logical features of
>  Twelf that one might use.
>
>  
>