[POPLmark] Re: [Provers] Re: adequacy

[Geoffrey A. Washburn]

On Thu, 5 May 2005, 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.

	Ugh.  I'm not reviewing what I've written closely enough.  This
  should parse better:

> > Uniqueness checking is not currently part of Twelf,
>
> 	The web page seems to say 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 is an example of just one of the meta-logical features
>   of Twelf that one might use in a proof.

-- 
-- Geoff Washburn | geoffw at cis.upenn.edu | http://www.cis.upenn.edu/~geoffw/ --