The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

On Tuesday 22 August 2006 14:30, Andrew McCreight wrote:
> Hi,
>
> I've written a functorized implementation of finite sets implemented using
> lists.  The modules have worked pretty well there.  I didn't have the
> problem that you did with export.  For me, it works just fine, although I
> exported at the top level of the file instead of within a module.  Maybe
> that's the difference.
>
> I also encountered the second problem, where the names are not quite what
> you'd like.  This is a problem when the arguments are actual nat and you
> try to use Omega, because Omega says that it cannot operate on that type,
> so you have to do some unfolding.  A brute force way around this would be
> to write an unfolding tactic, but I haven't bothered.


I'd just like to mention I've also had some issues with folding/unfolding 
when 
using modules.  Sometimes I have to use explicit 'change ... with' tactics to 
apply rewrites.  I've also had cases where the Coq interface won't recognize 
terms I type (in 'apply with ...' clauses or as arguments to 'set :=' 
or 'pattern' for example) that I think are due to the same unfolding issues.

I don't recall having to do stuff like this when I'm not using modules. It's 
really quite irritating.

-- 
Rob Dockins

Talk softly and drive a Sherman tank.
Laugh hard, it's a long way to the bank.
       -- TMBG